Distributed LTL Model-Checking Based on Negative Cycle Detection

Logo poskytovatele
Logo poskytovatele

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

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

Rok publikování 2001
Druh Článek ve sborníku
Konference FST-TCS 2001
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Obor Počítačový hardware a software
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.