Další formáty:
BibTeX
LaTeX
RIS
@article{702477,
author = {Barnat, Jiří and Černá, Ivana},
article_number = {2},
keywords = {LTL model checking; Distributed memory; Breadth-first Search},
language = {eng},
issn = {0925-9856},
journal = {Formal Methods in System Design},
title = {Distributed breadth-first search LTL model checking},
url = {http://www.springerlink.com/content/94376q360325p688/?p=1a1a7d483531453686a95f499872d47e&pi=1},
volume = {29},
year = {2006}
}
TY - JOUR
ID - 702477
AU - Barnat, Jiří - Černá, Ivana
PY - 2006
TI - Distributed breadth-first search LTL model checking
JF - Formal Methods in System Design
VL - 29
IS - 2
SP - 117-134
EP - 117-134
PB - Springer Netherlands
SN - 09259856
KW - LTL model checking
KW - Distributed memory
KW - Breadth-first Search
UR - http://www.springerlink.com/content/94376q360325p688/?p=1a1a7d483531453686a95f499872d47e&pi=1
N2 - We propose a parallel distributed memory on-the-fly algorithm for enumerative LTL model checking. The algorithm is designed for networks 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 all back-level edges, and for each level the back-level edges are checked in parallel by a nested search procedure to confirm or refute the presence of a cycle. Several improvements of the basic algorithm are presented and advantages and drawbacks of their application to distributed LTL model checking are discussed.
ER -
BARNAT, Jiří a Ivana ČERNÁ. Distributed breadth-first search LTL model checking. \textit{Formal Methods in System Design}. Springer Netherlands, 2006, roč.~29, č.~2, s.~117-134. ISSN~0925-9856.
|
