Large-Scale Directed Model Checking LTL

Abstract

To analyze larger models for explicit-state model checking, directed model checking applies error-guided search, external model checking uses secondary storage media, and distributed model checking exploits parallel exploration on multiple processors.

In this paper we propose an external, distributed and directed on-the-fly model checking algorithm to check general LTL properties in the model checker SPIN. Previous attempts are restricted to checking safety properties. The worst-case I/O complexity is bounded by $O(\mbox{\em sort}(|{\cal F}||{\cal R}|)/p+ l \cdot \mbox{\em scan}(|{\cal F}||{\cal S}|))$, where ${\cal S}$ and ${\cal R}$ are the sets of visited states and transitions in the synchronized product of the Büchi automata for the model and the property specification, ${\cal F}$ is the number of accepting states, l is the length of the shortest counterexample, and p is the number of processors. The algorithm we propose returns minimal lasso-shaped counterexamples and includes refinements for property-driven exploration.