Deciding the Satisfiability of MITL Specifications
Marcello Maria Bersani
Pierluigi San Pietro
- Publisher: Open Publishing Association
Electronic Proceedings in Theoretical Computer Science
Mathematics | Electronic computers. Computer science | Computer Science - Logic in Computer Science | F.4.1 | QA1-939 | QA75.5-76.95
In this paper 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. T...