Parallel Breadth-First Search LTL Model-Checking

BARNAT, Jiří, Luboš BRIM and Jakub CHALOUPKA. Parallel Breadth-First Search LTL Model-Checking. In 18th IEEE International Conference on Automated Software Engineering (ASE'03). Montreal: IEEE Computer Society, 2003, p. 106-115. ISBN 0-7695-2035-9.

Basic information

Original name

Parallel Breadth-First Search LTL Model-Checking

Authors

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

Edition

Montreal, 18th IEEE International Conference on Automated Software Engineering (ASE'03), p. 106-115, 10 pp. 2003

Publisher

IEEE Computer Society

---

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Canada

Confidentiality degree

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

RIV identification code

RIV/00216224:14330/03:00008593

Organization unit

Faculty of Informatics

ISBN

0-7695-2035-9

UT WoS

000186519300011

Keywords in English

model checking; parallel algorithm; breadth first search

Tags

breadth first search, Model checking, parallel algorithm

Tags

International impact, Reviewed

---

Abstract

V originále

We propose a practical parallel on-the-fly algorithm for enumerative LTL model-checking. The algorithm is designed for a cluster 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 back-level edges. For each level the back-level edges are checked in parallel by a nested depth-first search 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 implementation of the algorithm shows promising results.

---

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