Metric Interval Temporal Logic Revisited

Hsi-Ming Ho
Friday, 24 February, 2017 - 10:15
NO, salle Solvay (5th floor)

Metric Interval Temporal Logic (MITL) was first proposed in the early 1990s as a specification language for real-time systems. Apart from its appealing intuitive syntax, there are also theoretical evidences suggesting that MITL is the ‘right’ real-time counterpart of Linear Temporal Logic (LTL). Unfortunately, the tool support for MITL-based verification is still lacking to this day. In this paper, we propose a new construction from MITL to timed automata via one-clock alternating timed automata (OCATA). Our construction (1) subsumes the well-known construction for LTL by Gastin and Oddoux (2) is compositional and (3) the number of clocks used for each subformula is optimal up to an additive constant. We implement the construction in the tool MightyL and report some experiments using Uppaal and LTSmin as back-ends.