A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties

BARNAT, Jiří; Luboš BRIM and Petr ROČKAI. A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties. In Formal Methods and Software Engineering. Germany: Springer Berlin / Heidelberg, 2009, p. 407-425. ISBN 978-3-642-10372-8. Available from: https://dx.doi.org/10.1007/978-3-642-10373-5_21.

Basic information

Original name

A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties

Name in Czech

Časově optimální on-the-fly paralelní algoritmus pro ověřování modelu slabých LTL vlastností

Authors

BARNAT, Jiří (203 Czech Republic, 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

Germany, Formal Methods and Software Engineering, p. 407-425, 19 pp. 2009

Publisher

Springer Berlin / Heidelberg

---

Other information

Language

English

Type of outcome

Proceedings paper

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Brazil

Confidentiality degree

is not subject to a state or trade secret

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/09:00065777

Organization unit

Faculty of Informatics

ISBN

978-3-642-10372-8

ISSN

DOI

http://dx.doi.org/10.1007/978-3-642-10373-5_21

UT WoS

000280073000021

Keywords (in Czech)

On-the-fly; paralelní; ověřování modelu; LTL

Keywords in English

on-the-fly; parallel; LTL Model Checking

Tags

International impact, Reviewed

---

Abstract

In the original language

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 give the 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 Czech

Jeden z nejdůležitějších otevřených problému v paralelním ověřování modelu LTL je existence on-the-fly škálovatelného paralelního algoritmu s lineární časovou složitostí. V tomto článku dáváme částečnou odpověď na tento problém, jmenovitě řešíme tento problém pro poměrně bohatou podtřídu LTL vlastností, a to konkrétně slabých LTL vlastností.

---

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