math/ltl2ba/pkg-descr

   1 ltl2ba implements an algorithm of P. Gastin and D. Oddoux to generate
   2 Buechi automata from linear temporal logic (LTL) formulae.  This
   3 algorithm generates a very weak alternating automaton and then
   4 transforms it into a Buechi automaton, using a generalized Buechi
   5 automaton as an intermediate step. Each automaton is simplified
   6 on-the-fly in order to save memory and time. As usual the LTL formula
   7 is simplified before any treatment.  ltl2ba is more efficient than
   8 Spin 3.4.1, with regard to the size of the resulting automaton,
   9 the time of the computation, and the memory used.
  10
  11 WWW: http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/