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

Language

English

Type of outcome

Článek v odborném periodiku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

United States of America

Confidentiality degree

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

References:

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

V originále

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