| BARNAT, Jiří, Luboš BRIM and Jakub CHALOUPKA. From Distributed Memory Cycle Detection to Parallel LTL Model Checking. Electronical Notes in Theoretical Computer Science. Elsevier, 2005, vol. 2005, No 133, p. 21-39, 10 pp. ISSN 1571-0661. |
Other formats:
BibTeX
LaTeX
RIS
@article{572153,
author = {Barnat, Jiří and Brim, Luboš and Chaloupka, Jakub},
article_number = {133},
keywords = {LTL model checking; breadth first search; distributed memory},
language = {eng},
issn = {1571-0661},
journal = {Electronical Notes in Theoretical Computer Science},
title = {From Distributed Memory Cycle Detection to Parallel LTL Model Checking},
volume = {2005},
year = {2005}
}
TY - JOUR
ID - 572153
AU - Barnat, Jiří - Brim, Luboš - Chaloupka, Jakub
PY - 2005
TI - From Distributed Memory Cycle Detection to Parallel LTL Model Checking
JF - Electronical Notes in Theoretical Computer Science
VL - 2005
IS - 133
SP - 21-39
EP - 21-39
PB - Elsevier
SN - 15710661
KW - LTL model checking
KW - breadth first search
KW - distributed memory
N2 - 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.
ER -
BARNAT, Jiří, Luboš BRIM and Jakub CHALOUPKA. From Distributed Memory Cycle Detection to Parallel LTL Model Checking. \textit{Electronical Notes in Theoretical Computer Science}. Elsevier, 2005, vol.~2005, No~133, p.~21-39, 10 pp. ISSN~1571-0661.
|
