. "RIV/00216224:14330/04:00010726!RIV09-GA0-14330___" . "Distributed Memory LTL Model Checking Based on Breadth First Search" . . "14330" . "Chaloupka, Jakub" . "Barnat, Ji\u0159\u00ED" . "57"^^ . . . "Distrubuovan\u00E9 ov\u0159ov\u00E1n\u00ED modelu pro LTL zalo\u017Een\u00E9 na prohled\u00E1v\u00E1n\u00ED do \u0161\u00ED\u0159ky"@cs . . "Distributed Memory LTL Model Checking Based on Breadth First Search" . "Masarykova univerzita. Fakulta informatiky" . "3"^^ . "Brno" . "3"^^ . . . . "Distributed Memory LTL Model Checking Based on Breadth First Search"@en . . "RIV/00216224:14330/04:00010726" . . "FIMU-RS-2004-07" . . . "Distributed Memory LTL Model Checking Based on Breadth First Search"@en . "[5F826F08A71D]" . "560844" . "Distributed memory LTL model checking; breadth first search; cycle detection"@en . . "Distributed Memory LTL Model Checking Based on Breadth First Search" . "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."@en . . "Distrubuovan\u00E9 ov\u0159ov\u00E1n\u00ED modelu pro LTL zalo\u017Een\u00E9 na prohled\u00E1v\u00E1n\u00ED do \u0161\u00ED\u0159ky"@cs . "Brim, Lubo\u0161" . . "Je navr\u017Een distribuovan\u00FD algoritmus pro ov\u011B\u0159ov\u00E1n\u00ED modelu pro logiku LTL. Tento algoritmus je zalo\u017Een na prohled\u00E1v\u00E1n\u00ED stavov\u00E9ho prostoru do \u0161\u00ED\u0159ky a k detekci cykl\u016F vyu\u017E\u00EDv\u00E1 zp\u011Btn\u00FDch hran."@cs . "57"^^ . "P(GA201/03/0509), Z(MSM 143300001)" . "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." . . . . .