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) or (a,b), with 0 ≤ a < b ≤
∞ (use infty for ∞), or
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
The following operators are supported, where I is an
interval (see above):
- The Globaly operator G I phi, meaning
that phi must hold at all positions that occur
after a duration in I from now.
- The Finally operator F I phi,
meaning that phi must hold at some position
that occurs after a duration in I from now.
- The Until operator phi1 U I
phi2, meaning that formula phi1 must hold in all
positions until phi2 holds, and that this position
where phi2 holds must occur after a duration in
I from now.
- The Next operator X I phi,
meaning that formula phi must hold in the next
position, which occurs after a duration in I from
now. Not supported in the continuous semantics.
- The Boolean operators: || (or),
&& (and), ! (not) and ->
Examples of formula:
- Formulae that are satisfiable in the continuous semantics
but not in the pointwise semantics:
- p && ( p U ( !p ) ) && G ( ( !p ) -> G ( !p ) ) && G ( p -> F(0, 1) p )
- p && F (!p) && G ( (!p) -> G (!p) ) && !( p U (!p) )
- Parametric formulae with Untils:
- p1 U[0,5] ( p2 U[0,5] p3 )
- p1 U[0,5] ( p2 U[0,5] ( p3 U[0,5] p4 ) )
- p1 U[0,5] ( p2 U[0,5] ( p3 U[0,5] ( p4 U[0,5] p5 ) ) )
- p1 U[0,5] ( p2 U[0,5] ( p3 U[0,5] ( p4 U[0,5] ( p5 U[0,5] p6 ) ) ) )
- Parametric motion planning formulae (to be checked with
UppAal). The vehicle must visit several goals within
given time frames, while avoid bad states (variable b).
- F[0,3] goal1 && G (!b)
- F[0,3] goal1 && F[3,6] goal2 && G (!b)
- F[0,3] goal1 && F[3,6] goal2 && F[6,9] goal3 && G (!b)
Parametric request-response formulae under fairness constraints:
- ((G F p1) -> G(q -> F[0,5] r))
- ((G F p1 && G F p2) -> G(q -> F[0,5] r))
MightyL requires a working version of OCaml:
- Sources for the pointwise semantics (zip file).
- The sources for the continuous semantics will be available soon.
MightyL has been written and is maintained by Hsi-Ming Ho. The
MightyL team is composed of:
Brihaye and Hsi-Ming
Ho, Mathematics Department, at UMONS, Mons, Belgium.
Geeraerts, Formal methods and Verification group at ULB,
Laboratoire d'Informatique Fondamentale at the
Université Aix-Marseille, Marseille, France
The project has received support from the Belgian National Fund of Scientific
(F.R.S./FNRS), through grant PDR SyVeRLo.
The main publication documenting MightyL is:
- Thomas Brihaye, Gilles Geeraerts, Hsi-Ming Ho and Benjamin
Monmege. MightyL: A Compositional Translation from MITL to Timed
Automata. Accepted for publication in the proceedings of CAV
2017, to appear, Springer 2017