Publication details
Distributed Memory LTL Model Checking Based on Breadth First Search
| Basic information | |
|---|---|
| Original title: | Distributed Memory LTL Model Checking Based on Breadth First Search |
| Authors: | Jiří Barnat, Luboš Brim, Jakub Chaloupka |
| Further information | |
|---|---|
| Citation: | BARNAT, Jiří  - BRIM, Luboš - CHALOUPKA, Jakub. Distributed Memory LTL Model Checking Based on Breadth First Search. Brno : Faculty of Informatics, Masaryk University Brno, 2004. 57 pp. FIMU-RS-2004-07. |
| Original language: | English |
| Field: | Informatika |
| WWW: |  http://www.fi.muni.cz/veda/reports/files/2004/FIMU-RS-2004-07.ps.iso-8859-1 |
| Type: | Monograph |
| Keywords: | Distributed memory LTL model checking; breadth first search; cycle detection |
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 the presence 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.
Related projects:
- Automated Verification of Parallel and Distributed Systems
- Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing
