Informace o publikaci
From Distributed Memory Cycle Detection to Parallel LTL Model Checking
| Název česky | Od distribuovane detekce cyklu k paralelnimu LTL overovani modelu |
|---|---|
| Autoři | |
| 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 | |
| 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: |