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

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.

Evert Willem Beth. The Foundations of Mathematics. North Holland, 1959. Second edition revised in 1965.

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.

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 ]

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 ]

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.

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.

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.

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.

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.

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 ]

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 ]

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.

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.

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

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 ]

Raymon M. Smullyan. First-Order Logic. ©Springer-Verlag, 1968.

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.

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.

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

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.

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

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].

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

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

LtlTranslationAlgorithms/References (last edited 2011-06-17 21:53:35 by AlexandreDuretLutz)

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