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 61 to 80 of 100.
Sorted by year (citations)
  1. Vardi, Moshe Y.: From philosophical to industrial logics (2009)
  2. De Wulf, M.; Doyen, L.; Maquet, N.; Raskin, J.-F.: Antichains: Alternative algorithms for LTL satisfiability and model-checking (2008)
  3. Esparza, Javier; Heljanko, Keijo: Unfoldings: A partial-order approach to model checking. (2008)
  4. Farzan, Azadeh; Chen, Yu-Fang; Clarke, Edmund M.; Tsay, Yih-Kuen; Wang, Bow-Yaw: Extending automated compositional verification to the full class of omega-regular languages (2008)
  5. Harel, David; Maoz, Shahar: Assert and negate revisited: Modal semantics for UML sequence diagrams (2008) ioport
  6. Jin, Naiyong; Shen, Chengjie; Chen, Jun; Ni, Taoyong: Engineering of an assertion-based (PSL^\textSimple)-Verilog dynamic verifier by alternating automata (2008) ioport
  7. Morgenstern, Andreas; Schneider, Klaus: From LTL to symbolically represented deterministic automata (2008)
  8. Tsay, Yih-Kuen; Chen, Yu-Fang; Tsai, Ming-Hsien; Chan, Wen-Chin; Luo, Chi-Jian: GOAL extended: Towards a research tool for omega automata and temporal logic (2008)
  9. Basin, David; Kuruma, Hironobu; Miyazaki, Kunihiko; Takaragi, Kazuo; Wolff, Burkhart: Verifying a signature architecture: a comparative case study (2007)
  10. Bianculli, Domenico; Spoletini, Paola; Morzenti, Angelo; Pradella, Matteo; San Pietro, Pierluigi: Model checking temporal metric specifications with Trio2Promela (2007)
  11. Doyen, Laurent; Raskin, Jean-François: Improved algorithms for the automata-based approach to model-checking (2007)
  12. Biere, Armin; Heljanko, Keijo; Junttila, Tommi; Latvala, Timo; Schuppan, Viktor: Linear encodings of bounded LTL model checking (2006)
  13. Geldenhuys, Jaco; Hansen, Henri: Larger automata and less work for LTL model checking (2006)
  14. Kerjean, Sylvain; Kabanza, Froduald; St-Denis, Richard; Thiébaux, Sylvie: Analyzing LTL model checking techniques for plan synthesis and controller synthesis (work in progress) (2006)
  15. Klein, Joachim; Baier, Christel: Experiments with deterministic (\omega)-automata for formulas of linear temporal logic (2006)
  16. Kloetzer, Marius; Belta, Calin: A fully automated framework for control of linear systems from LTL specifications (2006)
  17. Kupferman, Orna; Sheinvald-Faragy, Sarai: Finding shortest witnesses to the nonemptiness of automata on infinite words (2006)
  18. Pelánek, Radek; Strejček, Jan: Deeper connections between LTL and alternating automata (2006)
  19. d’Amorim, Marcelo; Roşu, Grigore: Efficient monitoring of (\omega)-languages (2005)
  20. Fritz, Carsten: Concepts of automata construction from LTL (2005)