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

BARNAT, Jiří; Luboš BRIM a 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, roč. 77, č. 12, s. 1272-1288. ISSN 0167-6423. Dostupné z: https://doi.org/10.1016/j.scico.2011.03.001.

Základní údaje

Originální název

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

Autoři

BARNAT, Jiří; Luboš BRIM a Petr ROČKAI

Vydání

Science of Computer Programming, Elsevier, 2012, 0167-6423

---

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Spojené státy

Utajení

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

Odkazy

URL

Impakt faktor

Impact factor: 0.568

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/12:00057076

Organizační jednotka

Fakulta informatiky

DOI

https://doi.org/10.1016/j.scico.2011.03.001

UT WoS

000308732800004

Klíčová slova anglicky

Explicit Model Checking; Parallel; On-the-fly; Partial Order Reduction

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

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.

---

Návaznosti

GA201/09/1389, projekt VaV	Název: Verifikace a analýza velmi velkých počítačových systémů Investor: Grantová agentura ČR, Verifikace a analýza velmi velkých počítačových systémů
GP201/09/P497, projekt VaV	Název: Automatizovaná formální verifikace s využitím soudobého hardware Investor: Grantová agentura ČR, Automatizovaná formální verifikace s využitím soudobého hardware
MSM0021622419, záměr	Název: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
MUNI/A/0057/2011, interní kód MU	Název: Posílení zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKONF) Investor: Masarykova univerzita, Posílení zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/0914/2009, interní kód MU	Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Akronym: SV-FI MAV) Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
1ET400300504, projekt VaV	Název: Realistická aplikace formálních metod v komponentových systémech Investor: Akademie věd ČR, Realistická aplikace formálních metod v komponentových systémech
1ET408050503, projekt VaV	Název: Techniky automatické verifikace a validace softwarových a hardwarových systémů Investor: Akademie věd ČR, Techniky automatické verifikace a validace softwarových a hardwarových systémů