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 21 to 40 of 100.
Sorted by year (citations)
  1. Yang, Fan; Yang, Guowu; Hao, Yujie: The modeling library of eavesdropping methods in quantum cryptography protocols by model checking (2016)
  2. Kirchner, Florent; Kosmatov, Nikolai; Prevosto, Virgile; Signoles, Julien; Yakobowski, Boris: Frama-C: a software analysis perspective (2015) ioport
  3. Peleska, Jan: Translating testing theories for concurrent systems (2015)
  4. Shan, Laixiang; Du, Xiaomin; Qin, Zheng: Efficient approach of translating LTL formulae into Büchi automata (2015)
  5. Shan, Laixiang; Qin, Jun; Chen, Mingshi; Qin, Zheng: Degeneralization algorithm for generation of Büchi automata based on contented situation (2015)
  6. Taha, Safouan; Julliand, Jacques; Dadeau, Frédéric; Castillos, Kalou Cabrera; Kanso, Bilal: A compositional automata-based semantics and preserving transformation rules for testing property patterns (2015)
  7. Abdulla, Parosh Aziz; Chen, Yu-Fang; Holík, Lukáš; Vojnar, Tomáš: Mediating for reduction (on minimizing alternating Büchi automata) (2014)
  8. Baader, Franz; Lippmann, Marcel: Runtime verification using the temporal description logic (\mathcalALC)-LTL revisited (2014)
  9. Beyene, Tewodros; Chaudhuri, Swarat; Popeea, Corneliu; Rybalchenko, Andrey: A constraint-based approach to solving games on infinite graphs (2014)
  10. Ding, Xuchu; Lazar, Mircea; Belta, Calin: LTL receding horizon control for finite deterministic systems (2014)
  11. Komárková, Zuzana; Křetínský, Jan: Rabinizer 3: Safraless translation of LTL to small deterministic automata (2014)
  12. Seki, Hirohisa: Extending co-logic programs for branching-time model checking (2014)
  13. Wimmer, Ralf; Jansen, Nils; Ábrahám, Erika; Katoen, Joost-Pieter; Becker, Bernd: Minimal counterexamples for linear-time probabilistic verification (2014)
  14. Babiak, Tomáš; Blahoudek, František; Křetínský, Mojmír; Strejček, Jan: Effective translation of LTL to deterministic Rabin automata: beyond the ((\mathrmF,\mathrmG))-fragment (2013)
  15. Li, Jianwen; Pu, Geguang; Zhang, Lijun; Wang, Zheng; He, Jifeng; Guldstrand Larsen, Kim: On the relationship between LTL normal forms and Büchi automata (2013)
  16. Cook, Byron; Koskinen, Eric; Vardi, Moshe: Temporal property verification as a program analysis task (2012)
  17. Ehlers, Rüdiger: Symbolic bounded synthesis (2012)
  18. Gaiser, Andreas; Křetínský, Jan; Esparza, Javier: Rabinizer: small deterministic automata for (\mathrmLTL(\mathrmF,\mathrmG)) (2012)
  19. Penczek, Wojciech; Woźna-Szcześniak, Bożena; Zbrzezny, Andrzej: Towards SAT-based BMC for LTLK over interleaved interpreted systems (2012)
  20. Salem, Ala-Eddine Ben; Duret-Lutz, Alexandre; Kordon, Fabrice: Model checking using generalized testing automata (2012)