Abstract
In the paper we propose a translation of the existential model checking problem for timed automata and properties expressible in MITL to the existential model checking problem for HLTL. Such a translation, for example, allows to adopt LTL bounded model checking method for verification of the MITL properties.
Get full access to this article
View all access options for this article.