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. |
Další formáty:
BibTeX
LaTeX
RIS
|
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 | |
---|---|
Originální 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 | 0302-9743 |
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 |
Změnil | Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 30. 4. 2014 05:52. |
Anotace |
---|
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. |
Anotace č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ů |
VytisknoutZobrazeno: 9. 9. 2024 20:02