kirancodes.me
To Proof Maintenance & Beyond!
ASE 2003

Parallel Breadth-First Search LTL Model-Checking

Jiri Barnat, Lubos Brim, Jakub Chaloupka

DOI 10.1109/ase.2003.1240299dblp

Abstract

We propose a practical parallel on-the-fly algorithm for enumerative LTL (linear temporal logic) model checking. The algorithm is designed for a cluster of workstations communicating via MPI (message passing interface). 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.

BibTeX
@inproceedings{Barnat-al:ASE03,
  author    = {Jiri Barnat and
               Lubos Brim and
               Jakub Chaloupka},
  title     = {Parallel {Breadth-First} Search {LTL} {Model-Checking}},
  booktitle = {ASE},
  pages     = {106--115},
  publisher = {{IEEE} Computer Society},
  year      = {2003},
}

Related papers