التفاصيل البيبلوغرافية
| العنوان: |
Large-Scale Directed Model Checking LTL. |
| المؤلفون: |
Valmari, Antti, Edelkamp, Stefan, Jabbar, Shahid |
| المصدر: |
Model Checking Software (9783540331025); 2006, p1-18, 18p |
| مستخلص: |
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] |
|
Copyright of Model Checking Software (9783540331025) is the property of Springer eBooks and its content may not be copied or emailed to multiple sites or posted to a listserv without the copyright holder's express written permission. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) |
| قاعدة البيانات: |
Supplemental Index |
