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 41 to 60 of 100.
Sorted by year (citations)
  1. Bentakouk, Lina; Poizat, Pascal; Zaïdi, Fatiha: Checking the behavioral conformance of web services with symbolic testing and an SMT solver (2011) ioport
  2. Bonnet, Rémi: Decidability of LTL for vector addition systems with one zero-test (2011)
  3. Ehlers, Rüdiger: Unbeast: symbolic bounded synthesis (2011)
  4. Morse, Jeremy; Cordeiro, Lucas; Nicole, Denis; Fischer, Bernd: Context-bounded model checking of LTL properties for ANSI-C software (2011) ioport
  5. Rozier, Kristin Y.: Linear temporal logic symbolic model checking (2011)
  6. Salamah, Salamah; Gates, Ann Q.; Roach, Steve; Engskow, Matthew: Towards support for software model checking: improving the efficiency of formal specifications (2011) ioport
  7. Tsay, Yih-Kuen; Tsai, Ming-Hsien; Chang, Jinn-Shu; Chang, Yi-Wen: Büchi Store: an open repository of Büchi automata (2011)
  8. Bae, Kyungmin; Meseguer, José: The linear temporal logic of rewriting Maude model checker (2010)
  9. Jones, Kevin D.; Konrad, Victor; Ničković, Dejan: Analog property checkers: a DDR2 case study (2010)
  10. Katz, Gal; Peled, Doron: MCGP: a software synthesis tool based on model checking and genetic programming (2010) ioport
  11. Montali, Marco: Specification and verification of declarative open interaction models. A logic-based approach (2010)
  12. Rozier, Kristin Y.; Vardi, Moshe Y.: LTL satisfiability checking (2010) ioport
  13. Abdulla, Parosh A.; Chen, Yu-Fang; Holik, Lukáš; Vojnar, Tomáš: Mediating for reduction (on minimizing alternating Büchi automata) (2009)
  14. Cristau, Julien: Automata and temporal logic over arbitrary linear time (2009)
  15. Doyen, Laurent; Raskin, Jean-François: Antichains for the automata-based approach to model-checking (2009)
  16. Duret-Lutz, Alexandre; Poitrenaud, Denis; Couvreur, Jean-Michel: On-the-fly emptiness check of transition-based Streett automata (2009)
  17. Gaiser, Andreas; Schwoon, Stefan: Comparison of algorithms for checking emptiness on Büchi automata (2009)
  18. Parisaca Vargas, Abigail; Garis, Ana G.; Tapia Tarifa, S. Lizeth; George, Chris: Model checking LTL formulae in RAISE with FDR (2009)
  19. Schimpf, Alexander; Merz, Stephan; Smaus, Jan-Georg: Construction of Büchi automata for LTL model checking verified in Isabelle/HOL (2009)
  20. Tsay, Yih-Kuen; Chen, Yu-Fang; Tsai, Ming-Hsien; Wu, Kang-Nien; Chan, Wen-Chin; Luo, Chi-Jian; Chang, Jinn-Shu: Tool support for learning Büchi automata and linear temporal logic (2009)