From Distributed Memory Cycle Detection to Parallel LTL Model Checking

Investor logo

Warning

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

BARNAT Jiří BRIM Luboš CHALOUPKA Jakub

Year of publication 2005
Type Article in Periodical
Magazine / Source Electronical Notes in Theoretical Computer Science
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords LTL model checking; breadth first search; distributed memory
Description 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:

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