Revisiting MITL to fix decision procedures

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

Mahesh Viswanathan, Nima Roohi

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 (4)

• Complexity of metric temporal logics with counting and the Pnueli modalities
• The compound interest in relaxing punctuality
• Timed-automata-based verification of MITL over signals
• 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)