Other formats:
BibTeX
LaTeX
RIS
@book{563034,
author = {Barnat, Jiří and Brim, Luboš and Chaloupka, Jakub},
address = {Brno},
keywords = {Distributed memory LTL model checking; breadth first search; cycle detection},
language = {eng},
location = {Brno},
publisher = {Faculty of Informatics, Masaryk University Brno},
title = {Distributed Memory LTL Model Checking Based on Breadth First Search},
url = {http://www.fi.muni.cz/veda/reports/files/2004/FIMU-RS-2004-07.ps.iso-8859-1},
year = {2004}
}
TY - BOOK
ID - 563034
AU - Barnat, Jiří - Brim, Luboš - Chaloupka, Jakub
PY - 2004
TI - Distributed Memory LTL Model Checking Based on Breadth First Search
VL - FIMU-RS-2004-07
PB - Faculty of Informatics, Masaryk University Brno
CY - Brno
KW - Distributed memory LTL model checking
KW - breadth first search
KW - cycle detection
UR - http://www.fi.muni.cz/veda/reports/files/2004/FIMU-RS-2004-07.ps.iso-8859-1
N2 - We propose a parallel distributed memory on-the-fly algorithm for enumerative LTL model checking. The algorithm is designed for network 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 optimizations of the basic algorithm are presented and advantages and drawbacks of their application to distributed LTL model checking are discussed. Experimental evaluation of the algorithm is presented.
ER -
BARNAT, Jiří, Luboš BRIM and Jakub CHALOUPKA. \textit{Distributed Memory LTL Model Checking Based on Breadth First Search}. Brno: Faculty of Informatics, Masaryk University Brno, 2004, 57 pp. FIMU-RS-2004-07.
|
