Distributed breadth-first search LTL model checking

• 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
• 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

• Integrated approach to education of PhD students in the area of parallel and distributed systems
• Techniques for automatic verification and validation of software nad hardware systems
• Institute for Theoretical Computer Science
• Highly Parallel and Distributed Computing Systems
• Automated software verification