Abstract
We present an algorithm to generate Büchi automata from LTL formulae. This algorithm generates a very weak alternating co-Büchi 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
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
M. Daniele, F. Giunchiglia, and M. Vardi. Improved automata generation for linear temporal logic. In Proc. 11th International Computer Aided Verification Conference, pages 249–260, 1999.
K. Etessami and G. Holzmann. Optimizing Büchi automata. In Proceedings of 11th Int. Conf. on Concurrency Theory (CONCUR), 2000.
R. Gerth, D. Peled, M. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Protocol Specification Testing and Verification, pages 3–18, Warsaw, Poland, 1995. Chapman & Hall.
G. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279–295, May 1997.
O. Kupferman and M. Vardi. Weak alternating automata are not that weak. In Proc. 5th Israeli Symposium on Theory of Computing and Systems ISTCS’97, pages 147–158. IEEE, 1997.
D. Muller and P. Schupp. Alternating automata on infinite objects: Determinacy and Rabin’s theorem. In Proceedings of the Ecole de Printemps d'Informatique Théoretique on Automata on Infinite Words, volume 192 of LNCS, pages 100–107, Le Mont Dore, France, May 1984. Springer.
D. Muller and P. Schupp. Alternating automata on infinite trees. Theoretical Computer Science, 54(2–3):267–276, October 1987.
D. Muller and P. Schupp. Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra. Theoretical Computer Science, 141(1–2):69–107, April 1995.
S. Rohde. Alternating automata and the temporal logic of ordinals. PhD Thesis in Mathematics, University of Illinois at Urbana-Champaign, 1997.
F. Somenzi and R. Bloem. Efficient Büchi automata from LTL formulae. In CAV: International Conference on Computer Aided Verification, 2000.
H. Tauriainen. A randomized testbench for algorithms translating linear temporal logic formulae into Büchi automata. In Workshop Concurrency, Specifications and Programming, pages 251–262, Warsaw, Poland, 1999.
M. Vardi. An Automata-Theoretic Approach to Linear Temporal Logic, volume 1043 of Lecture Notes in Computer Science, pages 238–266. Springer-Verlag Inc., New York, NY, USA, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gastin, P., Oddoux, D. (2001). Fast LTL to Büchi Automata Translation. In: Berry, G., Comon, H., Finkel, A. (eds) Computer Aided Verification. CAV 2001. Lecture Notes in Computer Science, vol 2102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44585-4_6
Download citation
DOI: https://doi.org/10.1007/3-540-44585-4_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42345-4
Online ISBN: 978-3-540-44585-2
eBook Packages: Springer Book Archive