LTL2BA

Fast LTL to Büchi automata translation. We present an algorithm to generate Büchi automata from Linear Time Logic (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.


References in zbMATH (referenced in 100 articles )

Showing results 81 to 100 of 100.
Sorted by year (citations)

previous 1 2 3 4 5

  1. Fritz, Carsten; Wilke, Thomas: Simulation relations for alternating Büchi automata (2005)
  2. Geldenhuys, Jaco; Valmari, Antti: More efficient on-the-fly LTL verification with Tarjan’s algorithm (2005)
  3. Ridge, Tom; Margetson, James: A mechanically verified, sound and complete theorem prover for first order logic (2005)
  4. Sebastiani, Roberto; Tonetta, Stefano; Vardi, Moshe Y.: Symbolic systems, explicit properties: On hybrid approaches for LTL symbolic model checking (2005)
  5. Tuerk, Thomas; Schneider, Klaus: From PSL to LTL: a formal validation in HOL (2005)
  6. de Moura, Leonardo; Rueß, Harald: An experimental evaluation of ground decision procedures (2004)
  7. Eker, Steven; Meseguer, José; Sridharanarayanan, Ambarish: The Maude LTL model checker (2004)
  8. Geldenhuys, Jaco; Valmari, Antti: Tarjan’s algorithm makes on-the-fly LTL verification more efficient (2004)
  9. Latvala, Timo; Mäkelä, Marko: LTL model checking for modular Petri nets (2004)
  10. Nugraheni, Cecilia E.: Predicate diagrams as basis for the verification of reactive systems. (2004)
  11. Dajani-Brown, Samar; Cofer, Darren; Hartmann, Gary; Pratt, Steve: Formal modeling and analysis of an avionics triplex sensor voter (2003)
  12. D’Souza, Deepak; Mukund, Madhavan: Checking consistency of SDL+MSC specifications (2003)
  13. Eker, Steven; Meseguer, José; Sridharanarayanan, Ambarish: The Maude LTL model checker and its implementation (2003)
  14. Gastin, Paul; Oddoux, Denis: LTL with past and two-way very-weak alternating automata (2003)
  15. Håkansson, John; Jonsson, Bengt; Lundqvist, Ola: Generating online test oracles from temporal logic specifications (2003) ioport
  16. Latvala, Timo: Efficient model checking of safety properties (2003)
  17. Garavel, Hubert; Lang, Frédéric: NTIF: A general symbolic model for communicating sequential processes with data (2002)
  18. Penczek, Wojciech; Woźna, Bożena; Zbrzezny, Andrzej: Bounded model checking for the universal fragment of CTL. (2002)
  19. Gastin, Paul; Oddoux, Denis: Fast LTL to Büchi automata translation (2001)
  20. Schneider, Klaus: Improving automata generation for linear temporal logic by considering the automaton hierarchy (2001)

previous 1 2 3 4 5