TY - GEN
T1 - Revisiting MITL to fix decision procedures
AU - Roohi, Nima
AU - Viswanathan, Mahesh
N1 - Funding Information:
Part of this work was carried out while the first author was at the University of Illinois, Urbana-Champaign. We gratefully acknowledge the support of the following grants: Nima Roohi was partially supported by NSFCNS-1505799 and the Intel-NSF Partnership for Cyber-Physical Systems Security and Privacy and by ONRN000141712012. Mahesh Viswanathan was partially supported by NSFCCF 1422798, NSF CNS 1329991, and AFOSRFA9950-15-1-0059.
Funding Information:
We gratefully acknowledge the support of the following grants: Nima Roohi was partially supported by NSF CNS-1505799 and the Intel-NSF Partnership for Cyber-Physical Systems Security and Privacy and by ONR N000141712012. Mahesh Viswanathan was partially supported by NSF CCF 1422798, NSF CNS 1329991, and AFOSR FA9950-15-1-0059.
Publisher Copyright:
© Springer International Publishing AG 2018.
PY - 2018
Y1 - 2018
N2 - Metric Interval Temporal Logic (MITL) is a well studied real-time, temporal logic that has decidable satisfiability and model checking problems. The decision procedures for MITLrely on the automata theoretic approach, where logic formulas are translated into equivalent timed automata. Since timed automata are not closed under complementation, decision procedures for MITLfirst convert a formula into negated normal form before translating to a timed automaton. We show that, unfortunately, these 20-year-old procedures are incorrect, because they rely on an incorrect semantics of the R operator. We present the right semantics of R and give new, correct decision procedures for MITL. We show that both satisfiability and model checking for MITL are, as was previously claimed. We also identify a fragment of MITL that we call MITL WIthat is richer than MITL0,∞, for which we show that both satisfiability and model checking are. Many of our results have been formally proved in PVS.
AB - Metric Interval Temporal Logic (MITL) is a well studied real-time, temporal logic that has decidable satisfiability and model checking problems. The decision procedures for MITLrely on the automata theoretic approach, where logic formulas are translated into equivalent timed automata. Since timed automata are not closed under complementation, decision procedures for MITLfirst convert a formula into negated normal form before translating to a timed automaton. We show that, unfortunately, these 20-year-old procedures are incorrect, because they rely on an incorrect semantics of the R operator. We present the right semantics of R and give new, correct decision procedures for MITL. We show that both satisfiability and model checking for MITL are, as was previously claimed. We also identify a fragment of MITL that we call MITL WIthat is richer than MITL0,∞, for which we show that both satisfiability and model checking are. Many of our results have been formally proved in PVS.
UR - http://www.scopus.com/inward/record.url?scp=85041862127&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85041862127&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-73721-8_22
DO - 10.1007/978-3-319-73721-8_22
M3 - Conference contribution
AN - SCOPUS:85041862127
SN - 9783319737201
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 474
EP - 494
BT - Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Proceedings
A2 - Dillig, Isil
A2 - Palsberg, Jens
PB - Springer
T2 - 19th International Conference on Verification, Model Checking, and Abstract Interpretation, 2018
Y2 - 7 January 2018 through 9 January 2018
ER -