Cluster-based LTL model checking of large systems

Abstract

In recent years a bundle of parallel and distributed algorithms for verification of finite state systems has appeared. We survey distributed-memory enumerative LTL model checking algorithms designed for networks of workstations communicating via MPI. In the automata-based approach to LTL model checking the problem is reduced to the accepting cycle detection problem in a graph. Distributed algorithms, in opposite to sequential ones, cannot rely on depth-first search postorder which is essential for efficient detection of accepting cycles. Therefore, diverse conditions that characterise the existence of cycles in a graph have to be employed in order to come up with efficient and practical distributed algorithms. We compare these algorithms both theoretically and experimentally and determine cases where particular algorithms can be successful. © Springer-Verlag Berlin Heidelberg 2006.