Distributed Memory LTL Model Checking Based on Breadth First Search
| Authors | |
|---|---|
| Year of publication | 2004 |
| Type | Monograph |
| MU Faculty or unit | |
| Citation | |
| 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 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: |