An SMT-based approach to satisfiability checking of MITL

作者：Bersani Marcello M^*; Rossi Matteo; San Pietro Pierluigi

来源：Information and Computation, 2015, 245: 72-97.

DOI：10.1016/j.ic.2015.06.007

We present a satisfiability-preserving reduction from MITL interpreted over finitely-variable continuous behaviors to Constraint LTL over clocks, a variant of CLTL that is decidable, and for which an SMT-based bounded satisfiability checker is available. The result is a new complete and effective decision procedure for MITL. Although decision procedures for MITL already exist, the automata-based techniques they employ appear to be very difficult to realize in practice, and, to the best of our knowledge, no implementation currently exists for them. Aprototype tool for MITL based on the encoding presented here has, instead, been implemented and is publicly available.

• 出版日期2015-12