2018 | OriginalPaper | Buchkapitel
Revisiting MITL to Fix Decision Procedures
verfasst von : Nima Roohi, Mahesh Viswanathan
Erschienen in: Verification, Model Checking, and Abstract Interpretation
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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 $$\mathcal {R}$$ operator. We present the right semantics of $$\mathcal {R}$$ and give new, correct decision procedures for MITL. We show that both satisfiability and model checking for MITLare , as was previously claimed. We also identify a fragment of MITLthat we call MITLWIthat is richer than $$\texttt {MITL}_{0,\!\infty }$$, for which we show that both satisfiability and model checking are . Many of our results have been formally proved in PVS