Distributed breadth-first search LTL model checking

Investor logo
Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BARNAT Jiří ČERNÁ Ivana

Year of publication 2006
Type Article in Periodical
Magazine / Source Formal Methods in System Design
MU Faculty or unit

Faculty of Informatics

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:

You are running an old browser version. We recommend updating your browser to its latest version.