Distributed Memory LTL Model Checking Based on Breadth First Search

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F04%3A00010726" target="_blank" >RIV/00216224:14330/04:00010726 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—

Result language
angličtina
Original language name
Distributed Memory LTL Model Checking Based on Breadth First Search
Original language description
We propose a parallel distributed memory on-the-fly algorithm for enumerative LTL model checking. The algorithm is designed for network of workstations communicating via MPI. The detection of cycles (faulty runs) effectively employs the so called back-level edges. In particular, a parallel level synchronized breadth first search of the graph is performed to discover all back-level edges and for each level the back-level edges are checked in parallel by a nested search procedure to confirm or refute thepresence of a cycle. Several optimizations of the basic algorithm are presented and advantages and drawbacks of their application to distributed LTL model checking are discussed. Experimental evaluation of the algorithm is presented.
Czech name
Distrubuované ovřování modelu pro LTL založené na prohledávání do šířky
Czech description
Je navržen distribuovaný algoritmus pro ověřování modelu pro logiku LTL. Tento algoritmus je založen na prohledávání stavového prostoru do šířky a k detekci cyklů využívá zpětných hran.

Project
<a href="/en/project/GA201%2F03%2F0509" target="_blank" >GA201/03/0509: Automated Verification of Parallel and Distributed Systems</a><br>
Continuities
Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year
2004
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)