Publication details
From Distributed Memory Cycle Detection to Parallel LTL Model Checking
| Basic information | |
|---|---|
| Original title: | From Distributed Memory Cycle Detection to Parallel LTL Model Checking |
| Authors: | Jiří Barnat, Luboš Brim, Jakub Chaloupka |
| Further information | |
|---|---|
| Citation: | BARNAT, Jiří  - BRIM, Luboš - CHALOUPKA, Jakub. From Distributed Memory Cycle Detection to Parallel LTL Model Checking. Electronical Notes in Theoretical Computer Science, Elsevier, The Nederlands. ISSN 1571-0661, 2005, vol. 2005, no. 133, pp. 21-39. |
| Original language: | English |
| Field: | Informatika |
| Type: | Article in Periodical |
| Keywords: | LTL model checking; breadth first search; distributed memory |
We propose a parallel graph algorithm for detecting cycles in very large directed graphs distributed over a network of workstations. The algorithm employs back-level edges as computed by the breadth first search. In this paper we describe how to turn the algorithm into an explicit state distributed memory LTL model checker by extending it with detection of accepting cycles, counterexample generation and partial order reduction. We discuss these extensions and show experimental results.
Related projects:
- Automated Verification of Parallel and Distributed Systems
- Institute for Theoretical Computer Science
- Highly Parallel and Distributed Computing Systems
