1. A Genealogy of Emptiness-Check Algorithms

This graph represents a chronology of published algorithms for checking Büchi automata for emptiness. Three kinds of automata are distinguished:

Legend

Büchi automata accepting states

Generalized Büchi automata with accepting states

Generalized Büchi automata with accepting transitions (see TGBA)

Depth-first search and\nlinear graph algorthms\nTarjan, 1971 Tarjan's Algorithm\nMakes On-the-Fly LTL\nVerification More Efficient\nGeldenhuys & Valmari, 2004 Truly On-The-Fly\nLTL Model Checking\nHammer et al., 2005 Finding the maximum\nstrong components in\na directed graph\nDijkstra, 1973 On-the-fly Verification of\nLinear Temporal Logic\nCouvreur, 1999 Checking That Finite State\nConcurrent Programs Satisfy\nTheir Linear Specification\nLichtenstein and Pnueli, 1985 Memory-Efficient Algorithms for the\nVerification of Temporal Properties\nCourcoubetis et al., 1990 On the Verification of\nTemporal Properties\nGodefroid & Holzmann, 1993 An Improvement in Formal Verification\nHolzmann & Peled, 1994 On Nested Depth First Search\nHolzmann et al., 1996 Nested Emptiness Search\nfor GBA\nTauriainen, 2003 Minimization of \ncounterexamples in SPIN\nGastin et al., 2004 More Efficient On-the-fly\nLTL Verification with\nTarjan's Algorithm\nGeldenhuys & Valmari, 2005 On-the-fly emptiness checks\nfor generalized Büchi automata\nCouvreur et al., 2005 On Translating LTL\ninto Alternating and\nNondeterministic Automata\nTauriainen, 2003 A note on the worst-case memory\nrequirements of generalized NDFS\nTauriainen, 2005 A Note on On-The-Fly\nVerification Algorithms\nSchwoon & Esparza, 2004

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

[courcoubetis.90.cav]
Costas Courcoubetis, Moshe Y. Vardi, Pierre Wolper, and Mihalis Yannakakis. Memory-efficient algorithm for the verification of temporal properties. In Edmund M. Clarke and Robert P. Kurshan, editors, Proceedings of the 2nd international workshop on Computer Aided Verification (CAV'90), volume 531 of Lecture Notes in Computer Science, pages 233-242. ©Springer-Verlag, 1991.

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

[couvreur.05.spin]
Jean-Michel Couvreur, Alexandre Duret-Lutz, and Denis Poitrenaud. On-the-fly emptiness checks for generalized Büchi automata. In Patrice Godefroid, editor, Proceedings of the 12th International SPIN Workshop on Model Checking of Software, volume 3639 of Lecture Notes in Computer Science, pages 143-158. ©Springer-Verlag, August 2005.
[ .pdf ]

[dijkstra.73.ewd376]
Edsger Wybe Dijkstra. EWD 376: Finding the maximum strong components in a directed graph. http://www.cs.utexas.edu/users/EWD/ewd03xx/EWD376.PDF, May 1973. Republished in [dijkstra.76.dop].

[dijkstra.76.dop]
Edsger Wybe Dijkstra. Finding the maximal strong components in a directed graph. In A Discipline of Programming, chapter 25, pages 192-200. Prentice-Hall, 1976.

[gastin.04.spin]
Paul Gastin, Pierre Moro, and Marc Zeitoun. Minimization of counterexamples in SPIN. In S. Graf and L. Mounier, editors, Proceedings of the 11th International SPIN Workshop on Model Checking of Software (SPIN'04), volume 2989 of Lecture Notes in Computer Science, pages 92­-108, April 2004.

[geldenhuys.04.tacas]
Jaco Geldenhuys and Antti Valmari. Tarjan's algorithm makes on-the-fly LTL verification more efficient. In Kurt Jensen and Andreas Podelski, editors, Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'04), volume 2988 of Lecture Notes in Computer Science, pages 205-219. ©Springer-Verlag, 2004.

[geldenhuys.05.tcs]
Jaco Geldenhuys and Antti Valmari. More efficient on-the-fly LTL verification with Tarjan's algorithm. Theoretical Computer Science, 345(1):60-82, November 2005. Conference paper selected for journal publication.

[godefroid.93.pstv]
Patrice Godefroid and Gerard J. Holzmann. On the verification of temporal properties. In André A. S. Danthine, Guy Leduc, and Pierre Wolper, editors, Proceedings of the 13th IFIP TC6/WG6.1 International Symposium on Protocol Specification, Testing, and Verification (PSTV'93), volume C-16 of IFIP Transactions, pages 109-124, Liege, Belgium, May 1993. North-Holland.

[hammer.05.tacas]
Moritz Hammer, Alexander Knapp, and Stephan Merz. Truly on-the-fly LTL model checking. In Nicolas Halbwachs and Lenore Zuck, editors, Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05), Lecture Notes in Computer Science, Edinburgh, Scotland, April 2005. ©Springer-Verlag.

[holzmann.94.forte]
Gerard J. Holzmann and Doron A. Peled. An improvement in formal verification. In Proceeding of the 7th IFIP WG 6.1 International Conference on Formal Description Techniques (FORTE'94), volume 6 of IFIP Conference Proceedings, pages 109-124, Berne, Switzerland, 1994. Chapman & Hall.

[holzmann.96.spin]
Gerard J. Holzmann, Doron A. Peled, and Mihalis Yannakakis. On nested depth first search. In Jean-Charles Grégoire, Gerard J. Holzmann, and Doron A. Peled, editors, Proceedings of the 2nd Spin Workshop, volume 32 of DIMACS: Series in Discrete Mathematics and Theoretical Computer Science. American Mathematical Society, May 1996.

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

[schwoon.04.tr]
Stefan Schwoon and Javier Esparza. A note on on-the-fly verification algorithms. Technical report, Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik, November 2004. Republished as [schwoon.05.tacas].

[schwoon.05.tacas]
Stefan Schwoon and Javier Esparza. A note on on-the-fly verification algorithms. In Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05), Lecture Notes in Computer Science. ©Springer-Verlag, April 2005. To appear.

[tarjan.71.ssat]
Robert Tarjan. Depth-first search and linear graph algorithms. In Conference records of the 12th Annual IEEE Symposium on Switching and Automata Theory, pages 114-121. IEEE, October 1971. Later republished as [tarjan.72.siam].

[tarjan.72.siam]
Robert Tarjan. Depth-first search and linear graph algorithms. SIAM Journal on Computing, 1(2):146-160, 1972.

See also This Week's Citation Classic (July 25, 1983).

[tauriainen.03.a79]
Heikki Tauriainen. Nested emptiness search for generalized Büchi automata. Research Report A79, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, July 2003. Republished as [tauriainen.04.acsd].

[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. Reprint of Licentiate's thesis.

[tauriainen.04.acsd]
Heikki Tauriainen. Nested emptiness search for generalized Büchi automata. In Proceedings of the 4th International Conference on Application of Concurrency to System Design (ACSD'04), pages 165-174. IEEE Computer Society, June 2004.

[tauriainen.05.a96]
Heikki Tauriainen. A note on the worst-case memory requirements of generalized nested depth-first search. Research Report A96, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, September 2005.

3. See also

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

EmptinessCheckAlgorithms (last edited 2007-10-04 21:21:49 by AlexandreDuretLutz)

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