Parallel Breadth-First Search LTL Model-Checking
| Autoři | |
|---|---|
| Rok publikování | 2003 |
| Druh | Článek ve sborníku |
| Konference | 18th IEEE International Conference on Automated Software Engineering (ASE'03) |
| Fakulta / Pracoviště MU | |
| Citace | |
| Obor | Informatika |
| Klíčová slova | model checking; parallel algorithm; breadth first search |
| Popis | We propose a practical parallel on-the-fly algorithm for enumerative LTL model-checking. The algorithm is designed for a cluster 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 back-level edges. For each level the back-level edges are checked in parallel by a nested depth-first search 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 implementation of the algorithm shows promising results. |
| Související projekty: |