\input zb-basic
\input zb-ioport
\iteman{io-port 02227822}
\itemau{Schwoon, Stefan; Esparza, Javier}
\itemti{A note on on-the-fly verification algorithms.}
\itemso{Halbwachs, Nicolas (ed.) et al., Tools and algorithms for the construction and analysis of systems. 11th international conference, TACAS 2005, held as part of the joint European conference on theory and practice of software, ETAPS 2005, Edinburgh, UK, April 4--8, 2005. Proceedings. Berlin: Springer (ISBN 3-540-25333-5/pbk). Lecture Notes in Computer Science 3440, 174-190 (2005).}
\itemab
Summary: The automata-theoretic approach to LTL verification relies on an algorithm for finding accepting cycles in a B\"uchi automaton. Explicit-state model checkers typically construct the automaton ``on the fly'' and explore its states using depth-first search. We survey algorithms proposed for this purpose and identify two good algorithms, a new algorithm based on nested DFS, and another based on strongly connected components. We compare these algorithms both theoretically and experimentally and determine cases where both algorithms can be useful.
\itemrv{~}
\itemcc{}
\itemut{}
\itemli{doi:10.1007/b107194}
\end