Other formats:
BibTeX
LaTeX
RIS
@inproceedings{489814,
author = {Barnat, Jiří and Brim, Luboš and Chaloupka, Jakub},
address = {Montreal},
booktitle = {18th IEEE International Conference on Automated Software Engineering (ASE'03)},
keywords = {model checking; parallel algorithm; breadth first search},
language = {eng},
location = {Montreal},
isbn = {0-7695-2035-9},
pages = {106-115},
publisher = {IEEE Computer Society},
title = {Parallel Breadth-First Search LTL Model-Checking},
year = {2003}
}
TY - JOUR
ID - 489814
AU - Barnat, Jiří - Brim, Luboš - Chaloupka, Jakub
PY - 2003
TI - Parallel Breadth-First Search LTL Model-Checking
PB - IEEE Computer Society
CY - Montreal
SN - 0769520359
KW - model checking
KW - parallel algorithm
KW - breadth first search
N2 - We propose a practical parallel on-the-fly algorithm for enumerative LTL model-checking. The algorithm is designed for a cluster of workstations communicating via MPI. The detection of cycles (faulty runs) effectively employs the so called back-level edges. In particular, a parallel level-synchronized breadth-first search of the graph is performed to discover back-level edges. For each level the back-level edges are checked in parallel by a nested depth-first search to confirm or refute the presence of a cycle. Several optimizations of the basic algorithm are presented and advantages and drawbacks of their application to distributed LTL model checking are discussed. Experimental implementation of the algorithm shows promising results.
ER -
BARNAT, Jiří, Luboš BRIM and Jakub CHALOUPKA. Parallel Breadth-First Search LTL Model-Checking. In \textit{18th IEEE International Conference on Automated Software Engineering (ASE'03)}. Montreal: IEEE Computer Society, 2003, p.~106-115. ISBN~0-7695-2035-9.
|
