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.
Welcome to the MightyL online demo!
Please enter a formula in the box below and press the button.
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:
© All rights reserved. | Design by TEMPLATED.