Efficient Algorithms and Tools for MITL Model-Checking and Synthesis

Metric Interval Temporal Logic (MITL) is an extension of the classical Linear Time Logic (LTL) that can be used to characterise real-time properties of computer systems. While the practical interest of MITL is undeniable, there is still today a remarkable lack of tool support for this logic. In this short paper, we report on our on-going work effort to complete the theoretical knowledge about MITL. We also report on our recently introduced tool MightyL, which translates MITL formulae into timed automata, enabling efficient model-checking of this logic. Finally, we sketch the future directions of our current line of research, which will be to extend MightyL to support reactive synthesis of MITL properties.