MightyL is a tool to convert formulas written in the MITL logic into a set of timed automata, whose syncrhonous product accepts the language of the formula. Those automata can then be analysed using clasical tools such as UppAal or LTSMin, to check for emptiness of the formula or perform model-checking, for instance.

This webpage gives access to an online demo of the tool. Users can enter MITL formulas, and obtain, as output, the models that can be analysed with UppAal or LTSMin.

Online Demo

Welcome to the MightyL online demo!

Please enter a formula in the box below and press the button.

Enter an MITL formula:
Select the semantics for analysis:  Pointwise  Continuous (experimental!)


In the pointwise semantics, intervals can be of the following forms: [a,b], (a,b], [a,b) or (a,b), with 0 ≤ a < b ≤ ∞ (use infty for ∞), or [0,0].

In the continuous semantics only intervals of the form (0,a] or (0,a) with 0 ≤ a are supported. When no interval is specified in the operators, the interval (0, ∞) is assumed by default.

The following operators are supported, where I is an interval (see above):


Examples of formula:


MightyL requires a working version of OCaml:


MightyL has been written and is maintained by Hsi-Ming Ho. The MightyL team is composed of:

The project has received support from the Belgian National Fund of Scientific Research (F.R.S./FNRS), through grant PDR SyVeRLo.

The main publication documenting MightyL is: