From Distributed Memory Cycle Detection to Parallel LTL Model Checking

Varování

Publikace nespadá pod Ekonomicko-správní 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