A note on on-the-fly verification algorithms

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 DPS, and another based on strongly connected components. We compare these algorithms both theoretically and experimentally and determine cases where both algorithms can be useful. © Springer-Verlag Berlin Heidelberg 2005.