Revisiting MITL to fix decision procedures

Nima Roohi, Mahesh Viswanathan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Proceedings
EditorsIsil Dillig, Jens Palsberg
PublisherSpringer-Verlag
Pages474-494
Number of pages21
ISBN (Print)9783319737201
DOIs
StatePublished - Jan 1 2018
Event19th International Conference on Verification, Model Checking, and Abstract Interpretation, 2018 - [state] CA, United States
Duration: Jan 7 2018Jan 9 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10747 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other19th International Conference on Verification, Model Checking, and Abstract Interpretation, 2018
CountryUnited States
City[state] CA
Period1/7/181/9/18

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Revisiting MITL to fix decision procedures'. Together they form a unique fingerprint.

  • Cite this

    Roohi, N., & Viswanathan, M. (2018). Revisiting MITL to fix decision procedures. In I. Dillig, & J. Palsberg (Eds.), Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Proceedings (pp. 474-494). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10747 LNCS). Springer-Verlag. https://doi.org/10.1007/978-3-319-73721-8_22