Sciweavers

Share
FSTTCS
2001
Springer

Distributed LTL Model Checking Based on Negative Cycle Detection

10 years 7 months ago
Distributed LTL Model Checking Based on Negative Cycle Detection
Abstract. 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.
Lubos Brim, Ivana Cerná, Pavel Krcál
Added 28 Jul 2010
Updated 28 Jul 2010
Type Conference
Year 2001
Where FSTTCS
Authors Lubos Brim, Ivana Cerná, Pavel Krcál, Radek Pelánek
Comments (0)
books