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"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. 1 Introduction The model-checking problem for finite-state systems and linear-time temporal logic (LTL) is usually reduced to checking the emptiness of a B"uchi automaton, i.e. the product of the system and an automaton for the negated formula [24]. Various strategies exist for reducing the size of the automaton. For instance, symbolic model checking employs data structures that compactly represent large sets of states. This strategy combines well with breadth-first search, leading to solutions whose worst-case time is essentially O(n2) or O(n log n), if n is the size of the product. A survey of symbolic emptiness algorithms can be found in [8]. Explicit-state model checkers, on the other hand, construct the product automaton `on the fly', i.e. while searching the automaton. Thus, the model checker may be able to find a counterexample without ever constructing the complete state space. This technique can be combined with partial order methods [18, 15] to reduce the state-explosion effect. The best known on-the-fly algorithms use depth-first-search (DFS) strategies to explore the state space; their running times are linear in the size of the product (i.e. the number of states plus the number of transitions). These algorithms can be partitioned into two classes