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:

References in zbMATH (referenced in 99 articles )

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

1 2 3 4 5 next

  1. Blahoudek, František; Major, Juraj; Strejček, Jan: LTL to self-loop alternating automata with generic acceptance and back (2020)
  2. Gutierrez, Julian; Najib, Muhammad; Perelli, Giuseppe; Wooldridge, Michael: Automated temporal equilibrium analysis: verification and synthesis of multi-player games (2020)
  3. Kloetzer, Marius; Mahulea, Cristian: Path planning for robotic teams based on LTL specifications and Petri net models (2020)
  4. Clemente, Lorenzo; Mayr, Richard: Efficient reduction of nondeterministic automata with application to language inclusion testing (2019)
  5. Dimitrova, Rayna; Finkbeiner, Bernd; Torfah, Hazem: Approximate automata for omega-regular languages (2019)
  6. Löding, Christof; Pirogov, Anton: New optimizations and heuristics for determinization of Büchi automata (2019)
  7. Zhao, Liang; Wang, Xiaobing; Duan, Zhenhua: Model checking of pushdown systems for projection temporal logic (2019)
  8. Bezděk, Peter; Beneš, Nikola; Černá, Ivana; Barnat, Jiří: On clock-aware LTL parameter synthesis of timed automata (2018)
  9. Bloem, Roderick; Chatterjee, Krishnendu; Jobstmann, Barbara: Graph games and reactive synthesis (2018)
  10. Bradfield, Julian; Walukiewicz, Igor: The mu-calculus and model checking (2018)
  11. Kupferman, Orna: Automata theory and model checking (2018)
  12. Faymonville, Peter; Zimmermann, Martin: Parametric linear dynamic logic (2017)
  13. Hutschenreiter, Lisa; Peñaloza, Rafael: An automata view to goal-directed methods (2017)
  14. Tomita, Takashi; Ueno, Atsushi; Shimakawa, Masaya; Hagihara, Shigeki; Yonezaki, Naoki: Safraless LTL synthesis considering maximal realizability (2017)
  15. Unel, Gulay; Toman, David: Logic programming approach to automata-based decision procedures (2017)
  16. Duan, Zhenhua; Tian, Cong; Zhang, Nan: A canonical form based decision procedure and model checking approach for propositional projection temporal logic (2016)
  17. Esparza, Javier; Křetínský, Jan; Sickert, Salomon: From LTL to deterministic automata. A safraless compositional approach (2016)
  18. Molnár, Vince; Vörös, András; Darvas, Dániel; Bartha, Tamás; Majzik, István: Component-wise incremental LTL model checking (2016)
  19. Unel, Gulay: Incremental reasoning on monadic second-order logics with logic programming (2016)
  20. Yang, Fan; Yang, Guowu; Hao, Yujie: The modeling library of eavesdropping methods in quantum cryptography protocols by model checking (2016)

1 2 3 4 5 next