On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties

BARNAT, Jiří, Luboš BRIM and Petr ROČKAI. On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties. Science of Computer Programming. Elsevier, 2012, vol. 77, No 12, p. 1272-1288. ISSN 0167-6423. Available from: https://dx.doi.org/10.1016/j.scico.2011.03.001.

Basic information

• Original name: On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties
• Authors: BARNAT, Jiří (703 Slovakia, guarantor, belonging to the institution), Luboš BRIM (203 Czech Republic, belonging to the institution) and Petr ROČKAI (703 Slovakia, belonging to the institution).
• Edition: Science of Computer Programming, Elsevier, 2012, 0167-6423.

Other information

• Original language: English
• Type of outcome: Article in a journal
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: United States of America
• Confidentiality degree: is not subject to a state or trade secret
• WWW: URL
• Impact factor: Impact factor: 0.568
• RIV identification code: RIV/00216224:14330/12:00057076
• Organization unit: Faculty of Informatics
• Doi: http://dx.doi.org/10.1016/j.scico.2011.03.001
• UT WoS: 000308732800004
• Keywords in English: Explicit Model Checking; Parallel; On-the-fly; Partial Order Reduction
• Tags: International impact, Reviewed

Abstract

One of the most important open problems of parallel LTL model checking is to design an on-the-fly scalable parallel algorithm with linear time complexity. Such an algorithm would provide the same optimality we have in sequential LTL model checking. In this paper we give a partial solution to the problem: we propose an algorithm that has the required properties for a very rich subset of LTL properties, namely those expressible by weak Buchi automata. In addition to the previous version of the paper, we demonstrate how our new algorithm can be efficiently combined with a particular parallel technique for Partial Order Reduction and report on additional experiments.

Links

• GA201/09/1389, research and development project: Name: Verifikace a analýza velmi velkých počítačových systémů

Investor: Czech Science Foundation, Verification and Analysis of Large-Scale Computer Systems

• GP201/09/P497, research and development project: Name: Automatizovaná formální verifikace s využitím soudobého hardware

Investor: Czech Science Foundation, Automated formal verification using modern hardware

• 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

• MUNI/A/0057/2011, interní kód MU: Name: Posílení zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKONF)

Investor: Masaryk University, Category A

• MUNI/A/0914/2009, interní kód MU: Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Acronym: SV-FI MAV)

Investor: Masaryk University, Category A

• 1ET400300504, research and development project: Name: Realistická aplikace formálních metod v komponentových systémech

Investor: Academy of Sciences of the Czech Republic, Realistic application of formal methods in component 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