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í	2004
Druh	Článek ve sborníku
Konference	Proceedings of the Ninth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2004)
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ů Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů