We present an algorithm to generate Buchi automata from LTL formulae. This algorithm generates a very weak alternating automaton and then transforms it into a Buchi automaton, using a generalized Buchi automaton as an intermediate step. Each automaton is simplified on the fly in order to save memory and time. As usual we
simplify the LTL formula before any treatment. We implemented this
algorithm and compared it with Spin: the experiments show that our
algorithm is much more efficient than Spin. The criteria of
comparison are the size of the resulting automaton, the time of the
computation and the memory used. Our implementation is available on
the web at the following address:
http://verif.liafa.jussieu.fr/~oddoux
