Distributed breadth-first search LTL model checking |
| |
Authors: | Ji?í Barnat Ivana ?erná |
| |
Affiliation: | (1) Faculty of Informatics, MU Brno, Botanická 68a, 602 00 Brno, Czech Republic |
| |
Abstract: | 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.Research partially supported by grant No. 1ET-408050503 and the Grant Agency of Czech Republic grant No. 201/03/0509.
|
| |
Keywords: | LTL model checking Breadth-first search Distributed memory |
本文献已被 SpringerLink 等数据库收录! |
|