Deciding the Satisfiability of MITL Specifications

Article, Preprint English OPEN
Marcello Maria Bersani ; Matteo Rossi ; Pierluigi San Pietro (2013)
  • Publisher: Open Publishing Association
  • Journal: Electronic Proceedings in Theoretical Computer Science (issn: 2075-2180)
  • Related identifiers: doi: 10.4204/EPTCS.119.8
  • Subject: 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... View more
Share - Bookmark