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

BARNAT, Jiří, Luboš BRIM a 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, s. 407-425. ISBN 978-3-642-10372-8. Dostupné z: https://dx.doi.org/10.1007/978-3-642-10373-5_21.

Základní údaje

Originální název

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

Název česky

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

Autoři

BARNAT, Jiří (203 Česká republika, garant, domácí), Luboš BRIM (203 Česká republika, domácí) a Petr ROČKAI (703 Slovensko, domácí)

Vydání

Germany, Formal Methods and Software Engineering, od s. 407-425, 19 s. 2009

Nakladatel

Springer Berlin / Heidelberg

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Brazílie

Utajení

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

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/09:00065777

Organizační jednotka

Fakulta informatiky

ISBN

978-3-642-10372-8

ISSN

DOI

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

UT WoS

000280073000021

Klíčová slova česky

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

Klíčová slova anglicky

on-the-fly; parallel; LTL Model Checking

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

Česky

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

---

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