On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties (2012)výskyt výsledku
| Identifikační kód | RIV/00216224:14330/12:00057076 |
|---|---|
| Název v anglickém jazyce | On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties |
| Druh | J - Článek v odborném periodiku |
| Jazyk | eng - angličtina |
| Obor - skupina | I - Informatika |
| Obor | IN - Informatika |
| Rok uplatnění | 2012 |
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
| Počet výskytů výsledku | 3 |
| Počet tvůrců celkem | 3 |
| Počet domácích tvůrců | 3 |
| Výčet všech uvedených jednotlivých tvůrců | Jiří Barnat (státní příslušnost: SK - Slovenská republika, domácí tvůrce: A, vedidk: 5692792) Luboš Brim (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 6500773) Petr Ročkai (státní příslušnost: SK - Slovenská republika, domácí tvůrce: A, vedidk: 1292358) |
| Popis výsledku v anglickém jazyce | 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. |
| Klíčová slova oddělená středníkem | Explicit Model Checking; Parallel; On-the-fly; Partial Order Reduction |
| Stránka www, na které se nachází výsledek | - |
| DOI výsledku | 10.1016/j.scico.2011.03.001 |
Údaje o výsledku v závislosti na druhu výsledku
| Název periodika | Science of Computer Programming |
|---|---|
| ISSN | 0167-6423 |
| Svazek periodika | 77 |
| Číslo periodika v rámci uvedeného svazku | 12 |
| Stát vydavatele periodika | US - Spojené státy americké |
| Počet stran výsledku | 17 |
| Strana od-do | 1272-1288 |
| Kód UT WoS článku podle Web of Science | 000308732800004 |
| EID výsledku v databázi Scopus | - |
Ostatní informace o výsledku
| Předkladatel | Masarykova univerzita / Fakulta informatiky |
|---|---|
| Dodavatel | AV0 - Akademie věd České republiky (AV ČR) |
| Rok sběru | 2013 |
| Specifikace | RIV/00216224:14330/12:00057076!RIV13-AV0-14330___ |
| Datum poslední aktualizace výsledku | 05.09.2013 |
| Kontrolní číslo | 43679670 |
Informace o dalších výskytech výsledku dodaného stejným předkladatelem
| Dodáno MŠMT v roce 2013 | RIV/00216224:14330/12:00057076 v dodávce dat RIV13-MSM-14330___/02:2 |
|---|---|
| Dodáno GA ČR v roce 2013 | RIV/00216224:14330/12:00057076 v dodávce dat RIV13-GA0-14330___/02:2 |
Odkazy na výzkumné aktivity, při jejichž řešení výsledek vznikl
| Projekt podporovaný AV ČR v programu 1E | 1ET400300504 - Realistická aplikace formálních metod v komponentových systémech (2005 - 2009) |
|---|---|
| Projekt podporovaný AV ČR v programu 1E | 1ET408050503 - Techniky automatické verifikace a validace softwarových a hardwarových systémů (2005 - 2009) |
| Projekt podporovaný GA ČR v programu GA | GA201/09/1389 - Verifikace a analýza velmi velkých počítačových systémů (2009 - 2011) |
| Projekt podporovaný GA ČR v programu GP | GP201/09/P497 - Automatizovaná formální verifikace s využitím soudobého hardware (2009 - 2011) |
| Výzkumný záměr podporovaný MŠMT | MSM0021622419 - Vysoce paralelní a distribuované výpočetní systémy (2005 - 2011) |
| Podpora / návaznosti | Specifický výzkum na vysokých školách, poskytovatel MŠMT |