/!\ Warning: This page has not been updated from 2006. Many new LTL translation algorithms have been published since.

1. A Genealogy of LTL-to-Büchi Translators

This graph represents a chronology of algorithms for translating LTL to Büchi automata. Three kinds of automata are distinguished:

Legend

Büchi automata with labeled and accepting states

Büchi automata with labeled transitions and accepting states

Büchi automata with labeled and accepting transitions (see TGBA)

All of them are as expressive as the other. It's easy to show that pink automata (i.e. TGBA) are more compact than blue automata which in turn are more compact that yellow automata. Some of the translation algorithms colored in pink actually use TGBA only as an intermediate step; it doesn't matter (since Spot handles TGBA we are interested by algorithms that produces TGBA at any moment).

Semantic Tableau\nBeth, 1959 Analytic Tableau\nSmullyan, 1968 Temporal Logic Can Be More Expressive\nWolper, 1983 Reasoning about infinite computation paths\nWolper et al., 1983 Reasoning about infinite computations\nVardi & Wolper, 1994 Tableau Method for TL\nWolper, 1985 Simple On-The-Fly Verification of LTL\nGerth et al., 1995 Alternating Finite Automata on w-words\nMiyano & Hayashi, 1984 Constructing BA from LTL using\nSimulation Relations for Alternating BA\nFritz, 2003 Checking that Finite State Concurrent Programs\nSatify their Linear Specification\nLichtenstein & Pnueli, 1985 Fair SMG and Linear Time Model Checking\nBarringer et al., 1989 Decision Algorithm for Full PTL\nKesten et al., 1993 Point de Vue Symbolique sur LTL\nCouvreur, 2000 On-The-Fly Verification of LTL\nCouvreur, 1999 Symbolic Model Checking:\n10^20 States and Beyond\nBurch et al., 1990 Improved Automata Generation for LTL\nDaniele et al., 1999 Optimizing Büchi Automata\nEtessami & Holzmann, 2000 Simple and Efficient Translation from LTL,\nThirioux, 2002 Wring\nSomenzi & Bloem, 2000 From States to Transitions\nGiannakopoulou & Lerda, 2002 Fast LTL to Büchi Automata translation\nGastin & Oddoux, 2001 Fair Simulation Relations, Parity Games,\n and State Space Reduction for BA\nEtessami et al., 2001 On translating LTL into\nAlternating and Nondeterministic Automata\nTauriainen, 2003 Automata and LTL: translations with transition-based acceptance\nHeikki Tauriainen, 2006

2. References

(When adding new entries to this page, please complete the HlinsDatabase with the author homepages and other things that must be turned into hyperlinks.)

[barringer.89.avmfss]
Howard Barringer, Michael D. Fisher, and Graham D. Gough. Fair SMG and linear time model checking. In Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, volume 407 of Lecture Notes in Computer Science, pages 133-150. ©Springer-Verlag, 1989.

[beth.59.fom]
Evert Willem Beth. The Foundations of Mathematics. North Holland, 1959. Second edition revised in 1965.

[burch.91.slcd]
Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pages 1-33, Washington, D.C., 1990. IEEE Computer Society Press.

[couvreur.00.lacim]
Jean-Michel Couvreur. Un point de vue symbolique sur la logique temporelle linéaire. In Pierre Leroux, editor, Actes du Colloque LaCIM 2000, volume 27 of Publications du LaCIM, pages 131-140. Université du Québec à Montréal, August 2000.
[ .pdf ]

[couvreur.99.fm]
Jean-Michel Couvreur. On-the-fly verification of linear temporal logic. In Jeannette M. Wing, Jim Woodcock, and Jim Davies, editors, Proceedings of the World Congress on Formal Methods in the Development of Computing Systems (FM'99), volume 1708 of Lecture Notes in Computer Science, pages 253-271, Toulouse, France, September 1999. ©Springer-Verlag.
[ .pdf ]

[daniele.99.cav]
Marco Daniele, Fausto Giunchiglia, and Moshe Y. Vardi. Improved automata generation for Linear Temporal Logic. In N. Halbwachs and Doron A. Peled, editors, Proceedings of the 11th International Conference on Computer Aided Verification (CAV'99), volume 1633 of Lecture Notes in Computer Science, pages 249-260. ©Springer-Verlag, 1999.

[etessami.00.concur]
Kousha Etessami and Gerard J. Holzmann. Optimizing Büchi automata. In C. Palamidessi, editor, Proceedings of the 11th International Conference on Concurrency Theory (Concur'2000), volume 1877 of Lecture Notes in Computer Science, pages 153-167. ©Springer-Verlag, 2000.

[etessami.01.alp]
Kousha Etessami, Thomas Wilke, and Rebecca A. Schuller. Fair simulation relations, parity games, and state space reduction for buchi automata. In Fernando Orejas, Paul G. Spirakis, and Jan van Leeuwen, editors, Proceedings of the 28th international colloquium on Automata, Languages and Programming, volume 2076 of Lecture Notes in Computer Science, pages 694-707, Crete, Greece, July 2001. ©Springer-Verlag.

[fritz.03.ciaa]
Carsten Fritz. Constructing Büchi automata from linear temporal logic using simulation relations for alternating Büchi automata. In Oscar H. Ibarra and Zhe Dang, editors, Proceedings of the 8th International Conference on Implementation and Application of Automata (CIAA'03), volume 2759 of Lecture Notes in Computer Science, pages 35-48, Santa Barbara, California, July 2003. ©Springer-Verlag.

[gastin.01.cav]
Paul Gastin and Denis Oddoux. Fast LTL to Büchi automata translation. In G. Berry, H. Comon, and A. Finkel, editors, Proceedings of the 13th International Conference on Computer Aided Verification (CAV'01), volume 2102 of Lecture Notes in Computer Science, pages 53-65. ©Springer-Verlag, 2001.

[gerth.95.pstv]
Rob Gerth, Doron A. Peled, Moshe Y. Vardi, and Pierre Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Proceedings of the 15th Workshop on Protocol Specification Testing and Verification (PSTV'95), pages 3-18, Warsaw, Poland, 1996. Chapman & Hall.
[ .html ]

[giannakopoulou.02.forte]
Dimitra Giannakopoulou and Flavio Lerda. From states to transitions: Improving translation of LTL formulae to Büchi automata. In Doron A. Peled and Moshe Y. Vardi, editors, Proceedings of the 22nd IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'02), volume 2529 of Lecture Notes in Computer Science, pages 308-326, Houston, Texas, November 2002. ©Springer-Verlag.
[ .pdf ]

[kesten.93.cav]
Yonit Kesten, Zohar Manna, Hugh McGuire, and Amir Pnueli. A decision algorithm for full propositional temporal logic. In C. Courcoubetis, editor, Proceedings for the 5th Conference on Computer Aided Verification (CAV'93), volume 697 of Lecture Notes in Computer Science, pages 97-109. ©Springer-Verlag, 1993.

[lichtenstein.85.popl]
Orna Lichtenstein and Amir Pnueli. Checking that finite state cocurrent programs satisfy they linear specification. In Proceedings of the 12th ACM Symposium on Principles of Programming Languages (POPL'85), pages 97-107. ACM, 1985.

[miyano.84.tcs]
Satoru Miyano and Takeshi Hayashi. Alternating finite automata on ω-words. Theoretical Computer Science, 32:321-330, 1984.

[sebastiani.03.charme]
Roberto Sebastiani and Stefano Tonetta. more deterministic vs. smaller Büchi automata for efficient ltl model checking. In G. Goos, J. Hartmanis, and J. van Leeuwen, editors, Proceedings for the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME'03), volume 2860 of Lecture Notes in Computer Science, pages 126-140. ©Springer-Verlag, October 2003.
[ .ps ]

[smullyan.68.fol]
Raymon M. Smullyan. First-Order Logic. ©Springer-Verlag, 1968.

[somenzi.00.cav]
Fabio Somenzi and Roderick Bloem. Efficient Büchi automata for LTL formulae. In Proceedings of the 12th International Conference on Computer Aided Verification (CAV'00), volume 1855 of Lecture Notes in Computer Science, pages 247-263. ©Springer-Verlag, 2000.

[tauriainen.03.a83]
Heikki Tauriainen. On translating linear temporal logic into alternating and nondeterministic automata. Research Report A83, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, December 2003.

[tauriainen.06.phd]
Heikki Tauriainen. Automata and Linear Temporal Logic: Translation with Transition-based Acceptance. PhD thesis, Helsinki University of Technology, Espoo, Finland, September 2006.

[thirioux.02.fmics]
Xavier Thirioux. Simple and efficient translation from LTL formulas to Büchi automata. In Rance Cleaveland and Hubert Garavel, editors, Proceedings of the 7th International ERCIM Workshop in Formal Methods for Industrial Critical Systems (FMICS'02), volume 66(2) of Electronic Notes in Theoretical Computer Science, Málaga, Spain, July 2002. Elsevier.

[vardi.94.ic]
Moshe Y. Vardi and Pierre Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1-37, Nov 1994.

[wolper.83.focs]
Pierre Wolper, Moshe Y. Vardi, and Aravinda Prasad Sistla. Reasoning about infinite computation paths. In Proceedings of the 24th IEEE Symposium on Foundations of Computer Science (FOCS'83), pages 185-194. IEEE Computer Society Press, 1983. Later extended and published as [vardi.94.ic].

[wolper.83.ic]
Pierre Wolper. Temporal logic can be more expressive. Information and Control, 56(1-2):72-99, 1983.

[wolper.85.la]
Pierre Wolper. The tableau method for temporal logic: An overview. Logique et Analyse, (110-111):119-136, 1985.

3. See also

You might also be interested in a similar genealogy of EmptinessCheckAlgorithms.

LtlTranslationAlgorithms (last edited 2012-11-23 13:56:36 by AlexandreDuretLutz)

All text is available under the terms of the GNU Free Documentation License, see SpotWikiLicense for details.