Distributed breadth-first search LTL model checking
| Authors | |
|---|---|
| Year of publication | 2006 |
| Type | Article in Periodical |
| Magazine / Source | Formal Methods in System Design |
| MU Faculty or unit | |
| Citation | |
| Web | http://www.springerlink.com/content/94376q360325p688/?p=1a1a7d483531453686a95f499872d47e&pi=1 |
| Field | Informatics |
| Keywords | LTL model checking; Distributed memory; Breadth-first Search |
| Description | 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: |
|