Další formáty:
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 a Jakub CHALOUPKA. \textit{Distributed Memory LTL Model Checking Based on Breadth First Search}. Brno: Faculty of Informatics, Masaryk University Brno, 2004, 57 s. FIMU-RS-2004-07.
|