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

• Original language: English
• Type of outcome: Proceedings paper
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: Netherlands
• Confidentiality degree: is not subject to a state or trade secret
• 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

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.

Abstract (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