More efficient on-the-fly LTL verification with Tarjan's algorithm

Abstract

State-of-the-art algorithms for on-the-fly automata-theoretic LTL model checking make use of nested depth-first search to look for accepting cycles in the product of the system and the Büchi automaton. Here, we present two new single depth-first search algorithms that accomplish the same task. The first is based on Tarjan's algorithm for detecting strongly connected components, while the second is a combination of the first and Couvreur's algorithm for finding acceptance cycles in the product of a system and a generalized Büchi automaton. Both new algorithms report an accepting cycle immediately after all transitions in the cycle have been investigated. We show their correctness, describe efficient implementations and discuss how they interact with some other model checking techniques, such as bitstate hashing. The algorithms are compared to the nested search algorithms in experiments on both random and actual state spaces, using random and real formulas. Our measurements indicate that our algorithms investigate at most as many states as the old ones. In the case of a violation of the correctness property, the algorithms often explore significantly fewer states. © 2005 Elsevier B.V. All rights reserved.