Cluster-Based LTL Model Checking of Large Systems

BARNAT, Jiří, Luboš BRIM and Ivana ČERNÁ. Cluster-Based LTL Model Checking of Large Systems. In Formal Methods for Components and Objects. Berlin: Springer, 2006, p. 259-279. ISBN 978-3-540-36749-9.

Basic information

Original name

Cluster-Based LTL Model Checking of Large Systems

Name in Czech

LTL ověřování modelu rozsáhlých systémů s využitím počítačových klastrů

Authors

BARNAT, Jiří (203 Czech Republic), Luboš BRIM (203 Czech Republic, guarantor) and Ivana ČERNÁ (203 Czech Republic)

Edition

Berlin, Formal Methods for Components and Objects, p. 259-279, 21 pp. 2006

Publisher

Springer

---

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Netherlands

Confidentiality degree

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

RIV identification code

RIV/00216224:14330/06:00015451

Organization unit

Faculty of Informatics

ISBN

978-3-540-36749-9

UT WoS

00240360000013

Keywords in English

distributed LTL model checking

Tags

distributed LTL model checking

Tags

International impact, Reviewed

---

Abstract

V originále

In recent years a bundle of parallel and distributed algorithms for verification of finite state systems has appeared. We survey distributed memory enumerative LTL model checking algorithms designed for networks of workstations communicating via MPI. The automata-based approach to LTL model checking reduces the model checking problem to the accepting cycle detection problem. Contrary to sequential algorithms, distributed algorithms cannot rely on depth-first search postorder which is essential for efficient cycle detection. Therefore, they have to employ diverse conditions that characterize the existence of cycles in a graph in order to come up with an efficient and practical solution. We compare these algorithms both theoretically and experimentally and determine cases where particular algorithms can be useful.

In Czech

Přehledová práce shrnující výzkum v oblasti paralelního a distribuovaného ověřování modelu formulemi lineární temporální logiky. Jednotlivé algoritmy jsou teoreticky ale i experimentálně porovnány.

---

Links

GA201/06/1338, research and development project	Name: Automatizovaná verifikace softwaru Investor: Czech Science Foundation, Automated software verification
GD102/05/H050, research and development project	Name: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů Investor: Czech Science Foundation, Integrated approach to education of PhD students in the area of parallel and distributed systems
MSM0021622419, plan (intention)	Name: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems
1ET408050503, research and development project	Name: Techniky automatické verifikace a validace softwarových a hardwarových systémů Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware systems
1M0545, research and development project	Name: Institut Teoretické Informatiky Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science