From Distributed Memory Cycle Detection to Parallel LTL Model Checking

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Název česky	Od distribuovane detekce cyklu k paralelnimu LTL overovani modelu
Autoři	BARNAT Jiří BRIM Luboš CHALOUPKA Jakub
Rok publikování	2005
Druh	Článek v odborném periodiku
Časopis / Zdroj	Electronical Notes in Theoretical Computer Science
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
Obor	Informatika
Klíčová slova	LTL model checking; breadth first search; distributed memory
Popis	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.
Související projekty:	Automatizovaná verifikace paralelních a distribuovaných systémů Institut Teoretické Informatiky Vysoce paralelní a distribuované výpočetní systémy