PV2 ⊧ MightyLcompiles a temporal logic formula to a timed automaton

Translates MITL (Metric Interval Temporal Logic) into timed automata

Application domain/field

• Metric Interval Temporal Logic (MITL)
• Real-time systems
• Automata
• Timed automata

Type of tool

Logic-to-automata translator

Expected input

MITL formula

Expected output

Automata equivalent to the MITL formula in UPPAAL XML format.

Internals

Metric Interval Temporal Logic (MITL) is an extension of LTL that can be used to characterise real-time properties of computer systems. After using MightyL, you can then use model checkers such as UPPAAL or LTSMin on the output produced by MightyL.