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 73 articles )

Showing results 1 to 20 of 73.
Sorted by year (citations)

1 2 3 4 next

  1. Unel, Gulay; Toman, David: Logic programming approach to automata-based decision procedures (2017)
  2. Duan, Zhenhua; Tian, Cong; Zhang, Nan: A canonical form based decision procedure and model checking approach for propositional projection temporal logic (2016)
  3. Molnár, Vince; Vörös, András; Darvas, Dániel; Bartha, Tamás; Majzik, István: Component-wise incremental LTL model checking (2016)
  4. Unel, Gulay: Incremental reasoning on monadic second-order logics with logic programming (2016)
  5. Yang, Fan; Yang, Guowu; Hao, Yujie: The modeling library of eavesdropping methods in quantum cryptography protocols by model checking (2016)
  6. Kirchner, Florent; Kosmatov, Nikolai; Prevosto, Virgile; Signoles, Julien; Yakobowski, Boris: Frama-C: a software analysis perspective (2015) ioport
  7. Shan, Laixiang; Qin, Jun; Chen, Mingshi; Qin, Zheng: Degeneralization algorithm for generation of Büchi automata based on contented situation (2015)
  8. 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)
  9. Abdulla, Parosh Aziz; Chen, Yu-Fang; Holík, Lukáš; Vojnar, Tomáš: Mediating for reduction (on minimizing alternating Büchi automata) (2014)
  10. Baader, Franz; Lippmann, Marcel: Runtime verification using the temporal description logic $\mathcalALC$-LTL revisited (2014)
  11. Beyene, Tewodros; Chaudhuri, Swarat; Popeea, Corneliu; Rybalchenko, Andrey: A constraint-based approach to solving games on infinite graphs (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 $(F,G)$-fragment (2013)
  15. Ben Salem, Ala-Eddine; Duret-Lutz, Alexandre; Kordon, Fabrice: Model checking using generalized testing automata (2012)
  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(F,G)$ (2012)
  19. Penczek, Wojciech; Woźna-Szcześniak, Bożena; Zbrzezny, Andrzej: Towards SAT-based BMC for LTLK over interleaved interpreted systems (2012)
  20. Bentakouk, Lina; Poizat, Pascal; Zaïdi, Fatiha: Checking the behavioral conformance of web services with symbolic testing and an SMT solver (2011) ioport

1 2 3 4 next