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. 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. A prototype tool for MITL based on the encoding presented here has, instead, been implemented and is publicly available.
Deciding the Satisfiability of MITL Specifications
BERSANI, MARCELLO MARIA;ROSSI, MATTEO GIOVANNI;SAN PIETRO, PIERLUIGI
2013-01-01
Abstract
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. 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. A prototype tool for MITL based on the encoding presented here has, instead, been implemented and is publicly available.File | Dimensione | Formato | |
---|---|---|---|
1307.4469v1.pdf
Accesso riservato
:
Post-Print (DRAFT o Author’s Accepted Manuscript-AAM)
Dimensione
263.16 kB
Formato
Adobe PDF
|
263.16 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.