2005
From Distributed Memory Cycle Detection to Parallel LTL Model Checking
BARNAT, Jiří, Luboš BRIM a Jakub CHALOUPKAZákladní údaje
Originální název
From Distributed Memory Cycle Detection to Parallel LTL Model Checking
Název česky
Od distribuovane detekce cyklu k paralelnimu LTL overovani modelu
Autoři
BARNAT, Jiří (203 Česká republika), Luboš BRIM (203 Česká republika, garant) a Jakub CHALOUPKA (203 Česká republika)
Vydání
Electronical Notes in Theoretical Computer Science, Elsevier, 2005, 1571-0661
Další údaje
Jazyk
angličtina
Typ výsledku
Článek v odborném periodiku
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Nizozemské království
Utajení
není předmětem státního či obchodního tajemství
Kód RIV
RIV/00216224:14330/05:00012493
Organizační jednotka
Fakulta informatiky
Klíčová slova anglicky
LTL model checking; breadth first search; distributed memory
Příznaky
Mezinárodní význam, Recenzováno
Změněno: 22. 11. 2006 08:32, prof. RNDr. Luboš Brim, CSc.
V originále
We propose a parallel graph algorithm for detecting cycles in very large directed graphs distributed over a network of workstations. The algorithm employs back-level edges as computed by the breadth first search. In this paper we describe how to turn the algorithm into an explicit state distributed memory LTL model checker by extending it with detection of accepting cycles, counterexample generation and partial order reduction. We discuss these extensions and show experimental results.
Česky
V článku je popsán paralelní a distribuovaný algoritmus pro detekci cyklu v rozsáhlých distribuovaných grafech. Algoritmus využívá tzv. back-level hrany, jež lze spočítat s využitím distribuovaného prohledávání grafu do šířky. Dále článek popisuje jak lze tento algoritmus upravit za účelem použití pro ověřování modelu LTL. Konkrétně je navrženo rozšíření algoritmu o detekci akceptujících cyklů, generování protipříkladů a redukci stavového prostoru s využitím redukce částečným uspořádáním. Článek také podává nezbytné experimentální vyhodnocení algoritmu.
Návaznosti
GA201/03/0509, projekt VaV |
| ||
MSM0021622419, záměr |
| ||
1M0545, projekt VaV |
|