Distributed LTL Model-Checking Based on Negative Cycle Detection

Investor logo
Investor logo

Warning

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

BRIM Luboš ČERNÁ Ivana KRČÁL Pavel PELÁNEK Radek

Year of publication 2001
Type Article in Proceedings
Conference FST-TCS 2001
MU Faculty or unit

Faculty of Informatics

Citation
Field Computer hardware and software
Description This paper addresses the state explosion problem in automata based LTL model checking. To deal with large space requirements we turn to use a distributed approach. All the known methods for automata based model checking are based on depth first traversal of the state space which is difficult to parallelise as the ordering in which vertices are visited plays an important role. We come up with entirely different approach which is dependent on locating cycles with negative length in a directed graph with real number length of edges. Our method allows reasonable distribution and the experimental results confirm its usefulness for distributed model checking.
Related projects:

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

More info