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.
Recommendations
Cited in
(12)- Topology-aware planning under linear temporal logic constraints
- \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
- Formalizing MLTL formula progression in Isabelle/HOL
- 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)
