12 lines
634 B
Text
12 lines
634 B
Text
|
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
|
||
|
|
Spin 3.4.1, with regard to the the size of the resulting automaton,
|
||
|
|
the time of the computation, and the memory used.
|
||
|
|
|
||
|
|
WWW: http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/
|