Publication details
Distributed breadth
-first search LTL model checking
| Basic information | |
|---|---|
| Original title: | Distributed breadth-first search LTL model checking |
| Authors: | Jiří Barnat, Ivana Černá |
| Further information | |
|---|---|
| Citation: | BARNAT, Jiří - ČERNÁ, Ivana. Distributed breadth-first search LTL model checking. Formal Methods in System Design, Springer Netherlands, The Nederlands. ISSN 0925-9856, 2006, vol. 29, no. 2, pp. 117-134. |
| Original language: | English |
| Field: | Informatika |
| WWW: |  http://www.springerlink.com/content/94376q360325p688/?p=1a1a7d483531453686a95f499872d47e&pi=1 |
| Type: | Article in Periodical |
| Keywords: | LTL model checking; Distributed memory; Breadth-first Search |
We propose a parallel distributed memory on-the-fly algorithm for enumerative LTL model checking. The algorithm is designed for networks 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 improvements of the basic algorithm are presented and advantages and drawbacks of their application to distributed LTL model checking are discussed.
Related projects:
- Integrated approach to education of PhD students in the area of parallel and distributed systems
- Techniques for automatic verification and validation of software nad hardware systems
- Institute for Theoretical Computer Science
- Highly Parallel and Distributed Computing Systems
- Automated software verification
