Large-Scale Directed Model Checking LTL
| Autor: | Shahid Jabbar, Stefan Edelkamp |
|---|---|
| Rok vydání: | 2006 |
| Předmět: | |
| Zdroj: | Model Checking Software ISBN: 9783540331025 SPIN |
| DOI: | 10.1007/11691617_1 |
| Popis: | 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 Buchi 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|