Reference:

Stefan Schwoon and Javier Esparza. A note on on-the-fly verification algorithms. 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), volume 3440 of Lecture Notes in Computer Science, pages 174–190, Edinburgh, UK, April 2005. Springer.

Abstract:

The automata-theoretic approach to LTL verification relies on an algorithm for finding accepting cycles in a Büchi 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.

Suggested BibTeX entry:

@inproceedings{SE05,
    address = {Edinburgh, UK},
    author = {Stefan Schwoon and Javier Esparza},
    booktitle = {Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
    editor = {Nicolas Halbwachs and Lenore Zuck},
    month = {April},
    pages = {174--190},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    title = {A Note on On-The-Fly Verification Algorithms},
    volume = {3440},
    year = {2005}
}