Distributed Memory LTL Model Checking Based on Breadth First Search

BARNAT, Jiří, Luboš BRIM and Jakub CHALOUPKA. Distributed Memory LTL Model Checking Based on Breadth First Search. Brno: Faculty of Informatics, Masaryk University Brno, 2004, 57 pp. FIMU-RS-2004-07.

Basic information

Original name

Distributed Memory LTL Model Checking Based on Breadth First Search

Name in Czech

Distrubuované ovřování modelu pro LTL založené na prohledávání do šířky

Authors

BARNAT, Jiří (203 Czech Republic, guarantor), Luboš BRIM (203 Czech Republic) and Jakub CHALOUPKA (203 Czech Republic)

Edition

Brno, 57 pp. FIMU-RS-2004-07, 2004

Publisher

Faculty of Informatics, Masaryk University Brno

---

Other information

Language

English

Type of outcome

Odborná kniha

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í

References:

URL

RIV identification code

RIV/00216224:14330/04:00010726

Organization unit

Faculty of Informatics

Keywords in English

Distributed memory LTL model checking; breadth first search; cycle detection

Tags

breadth first search, cycle detection

Tags

International impact

---

Abstract

V originále

We propose a parallel distributed memory on-the-fly algorithm for enumerative LTL model checking. The algorithm is designed for network of workstations communicating via MPI. The detection of cycles (faulty runs) effectively employs the so called back-level edges. In particular, a parallel level synchronized breadth first search of the graph is performed to discover all back-level edges and for each level the back-level edges are checked in parallel by a nested search procedure to confirm or refute the presence of a cycle. Several optimizations of the basic algorithm are presented and advantages and drawbacks of their application to distributed LTL model checking are discussed. Experimental evaluation of the algorithm is presented.

In Czech

Je navržen distribuovaný algoritmus pro ověřování modelu pro logiku LTL. Tento algoritmus je založen na prohledávání stavového prostoru do šířky a k detekci cyklů využívá zpětných hran.

---

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