Revisiting MITL to fix decision procedures

DOI10.1007/978-3-319-73721-8_22zbMATH Open1446.68099arXiv1910.04216OpenAlexW2780338284MaRDI QIDQ3296347FDOQ3296347

Authors: Nima Roohi, Mahesh Viswanathan 

Publication date: 7 July 2020

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

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 MITL rely 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 MITL first 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 EXPSPACE-complete, as was previously claimed. We also identify a fragment of MITL that we call MITL_{WI} that is richer than MITL_{0,infty}, for which we show that both satisfiability and model checking are PSPACE-complete. Many of our results have been formally proved in PVS.

Full work available at URL: https://arxiv.org/abs/1910.04216

Recommendations

• Deciding the satisfiability of MITL specifications
• An SMT-based approach to satisfiability checking of MITL
• On Expressiveness and Complexity in Real-Time Model Checking
• Some Recent Results in Metric Temporal Logic
• Parametric Metric Interval Temporal Logic

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Temporal logic (03B44)

Cited In (10)

• \textsc{MightyL}: a compositional translation from MITL to timed automata
• An SMT-based approach to satisfiability checking of MITL
• Complexity of metric temporal logics with counting and the Pnueli modalities
• The compound interest in relaxing punctuality
• Deciding the satisfiability of MITL specifications
• On MITL and alternating timed automata over infinite words
• Parametric metric interval temporal logic
• Timed-automata-based verification of MITL over signals
• A translation of the existential model checking problem from MITL to HLTL
• Rebuilding MP on a logical ground

This page was built for publication: Revisiting MITL to fix decision procedures

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3296347)