BARNAT, Jiří, Luboš BRIM a Jakub CHALOUPKA. From Distributed Memory Cycle Detection to Parallel LTL Model Checking. In Proceedings of the Ninth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2004). Linz, Austria: Institute for Systems Engineering & Automation, Kepler university Linz, 2004. s. 17-34, 18 s. ISBN 3-902457-03-1.
Další formáty:   BibTeX LaTeX RIS
Zá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í Linz, Austria, Proceedings of the Ninth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2004), od s. 17-34, 18 s. 2004.
Nakladatel Institute for Systems Engineering & Automation, Kepler university Linz
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Česká republika
Utajení není předmětem státního či obchodního tajemství
Kód RIV RIV/00216224:14330/04:00010725
Organizační jednotka Fakulta informatiky
ISBN 3-902457-03-1
Klíčová slova anglicky LTL model checking; breadth first search; distributed memory
Štítky breadth first search, distributed memory, LTL model checking
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: prof. RNDr. Luboš Brim, CSc., učo 197. Změněno: 22. 11. 2006 08:32.
Anotace
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.
Anotace č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 VaVNázev: Automatizovaná verifikace paralelních a distribuovaných systémů
Investor: Grantová agentura ČR, Standardní projekty
MSM 143300001, záměrNázev: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumné záměry
VytisknoutZobrazeno: 22. 1. 2020 16:15