2004
Distributed Memory LTL Model Checking Based on Breadth First Search
BARNAT, Jiří, Luboš BRIM a Jakub CHALOUPKAZákladní údaje
Originální název
Distributed Memory LTL Model Checking Based on Breadth First Search
Název česky
Distrubuované ovřování modelu pro LTL založené na prohledávání do šířky
Autoři
BARNAT, Jiří (203 Česká republika, garant), Luboš BRIM (203 Česká republika) a Jakub CHALOUPKA (203 Česká republika)
Vydání
Brno, 57 s. FIMU-RS-2004-07, 2004
Nakladatel
Faculty of Informatics, Masaryk University Brno
Další údaje
Jazyk
angličtina
Typ výsledku
Odborná kniha
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Česká republika
Utajení
není předmětem státního či obchodního tajemství
Odkazy
Kód RIV
RIV/00216224:14330/04:00010726
Organizační jednotka
Fakulta informatiky
Klíčová slova anglicky
Distributed memory LTL model checking; breadth first search; cycle detection
Štítky
Příznaky
Mezinárodní význam
Změněno: 23. 6. 2009 14:31, prof. RNDr. Jiří Barnat, Ph.D.
V originále
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.
Česky
Je navržen distribuovaný algoritmus pro ověřování modelu pro logiku LTL. Tento algoritmus je založen na prohledávání stavového prostoru do šířky a k detekci cyklů využívá zpětných hran.
Návaznosti
| GA201/03/0509, projekt VaV |
| ||
| MSM 143300001, záměr |
|