2011-05-27 18:11:32 +00:00
|
|
|
ltl2ba implements an algorithm of P. Gastin and D. Oddoux to generate
|
|
|
|
|
Buechi automata from linear temporal logic (LTL) formulae. This
|
|
|
|
|
algorithm generates a very weak alternating automaton and then
|
|
|
|
|
transforms it into a Buechi automaton, using a generalized Buechi
|
|
|
|
|
automaton as an intermediate step. Each automaton is simplified
|
|
|
|
|
on-the-fly in order to save memory and time. As usual the LTL formula
|
|
|
|
|
is simplified before any treatment. ltl2ba is more efficient than
|
2012-01-08 07:01:25 +00:00
|
|
|
Spin 3.4.1, with regard to the size of the resulting automaton,
|
2011-05-27 18:11:32 +00:00
|
|
|
the time of the computation, and the memory used.
|
|
|
|
|
|
2016-05-23 18:36:52 +00:00
|
|
|
WWW: http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/
|
