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.
|