BARNAT, Jiří, Luboš BRIM and 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. p. 17-34, 18 pp. ISBN 3-902457-03-1.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name From Distributed Memory Cycle Detection to Parallel LTL Model Checking
Name in Czech Od distribuovane detekce cyklu k paralelnimu LTL overovani modelu
Authors BARNAT, Jiří (203 Czech Republic), Luboš BRIM (203 Czech Republic, guarantor) and Jakub CHALOUPKA (203 Czech Republic).
Edition Linz, Austria, Proceedings of the Ninth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2004), p. 17-34, 18 pp. 2004.
Publisher Institute for Systems Engineering & Automation, Kepler university Linz
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Czech Republic
Confidentiality degree is not subject to a state or trade secret
RIV identification code RIV/00216224:14330/04:00010725
Organization unit Faculty of Informatics
ISBN 3-902457-03-1
Keywords in English LTL model checking; breadth first search; distributed memory
Tags breadth first search, distributed memory, LTL model checking
Tags International impact, Reviewed
Changed by Changed by: prof. RNDr. Luboš Brim, CSc., učo 197. Changed: 22/11/2006 08:32.
Abstract
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.
Abstract (in Czech)
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.
Links
GA201/03/0509, research and development projectName: Automatizovaná verifikace paralelních a distribuovaných systémů
Investor: Czech Science Foundation, Standard Projects
MSM 143300001, plan (intention)Name: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministry of Education, Youth and Sports of the CR, Research Intents
PrintDisplayed: 23/2/2020 18:17