Selected publications by Paul Gastin

Abstract:
We present an algorithm to generate Büchi automata from LTL formulae. This algorithm generates a very weak alternating automaton and then transforms it into a Büchi automaton, using a generalized Büchi 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/ltl2ba

@inproceedings{GaOd01,
   address = {Paris, France},
   author = {Gastin, Paul and Oddoux, Denis},
   booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on {C}omputer {A}ided {V}erification ({CAV}'01)},
   editor = {Berry, G{\'e}rard and Comon, Hubert and Finkel, Alain},
   month = jul,
   pages = {53-65},
   publisher = {Springer},
   series = {Lecture Notes in Computer Science},
   title = {Fast {LTL} to {B}{\"u}chi Automata Translation},
   url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Cav01go.ps},
   volume = {2102},
   year = {2001},
}

About LSV