D 2004

From Distributed Memory Cycle Detection to Parallel LTL Model Checking

BARNAT, Jiří, Luboš BRIM and Jakub CHALOUPKA

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

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Czech Republic

Confidentiality degree

není předmětem státního či obchodního tajemství

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

Tags

International impact, Reviewed
Změněno: 22/11/2006 08:32, prof. RNDr. Luboš Brim, CSc.

Abstract

ORIG CZ

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.

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 project
Name: Automatizovaná verifikace paralelních a distribuovaných systémů
Investor: Czech Science Foundation, Automated Verification of Parallel and Distributed Systems
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, Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing