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


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

EmptinessCheckAlgorithms/Genealogy (last edited 2006-01-25 09:45:23 by AlexandreDuretLutz)

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