| Abstrakt: |
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. [ABSTRACT FROM AUTHOR] |
