From Distributed Memory Cycle Detection to Parallel LTL Model Checking

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. ISBN 3-902457-03-1.

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

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

---

Anotace

V originále

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.

Č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 VaV	Název: Automatizovaná verifikace paralelních a distribuovaných systémů Investor: Grantová agentura ČR, Automatizovaná verifikace paralelních a distribuovaných systémů
MSM 143300001, záměr	Ná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, Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů