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 …