RIV/00216224:14330/12:00057076 - On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties (2012)

Údaje o výsledku
Identifikační kódRIV/00216224:14330/12:00057076
Název v původním jazyceOn-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties
DruhJ - Článek v odborném periodiku
Jazykeng - angličtina
OborIN - Informatika
Rok uplatnění2012
Kód důvěrnosti údajůS - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
Počet výskytů výsledku3
Údaje z Hodnocení výsledků výzkumných organizací 2014
Výsledek byl hodnocen v Pilíři I
Rozsah vyřazení výsledkuTento výskyt výsledku není vyřazen
Zařazení výsledku v hodnoceníJimp - Článek v impaktovaném časopise evidovaném ve Web of Science
Skupina oboru v hodnocení04 - Technické a informatické vědy
Konkrétní způsob(y) hodnocení výsledkuVýsledek hodnocený již v předchozím hodnocení, body se přebírají
Bodové ohodnocení15,475
Faktor korekce90,8 %
Body (upravené podle přílohy č. 8 Metodiky)14,054
Rozdělení výsledku mezi předkladatele
OrganizaceVýzkumná organizace?PodílBodyBody (upravené podle přílohy č. 8 Metodiky)
Masarykova univerzita / Fakulta informatikyano100,0 %15,47514,054
Tvůrci výsledku
Počet tvůrců celkem3
Počet domácích tvůrců3
TvůrceBarnat Jiří (státní příslušnost: SK - Slovenská republika; A - domácí tvůrce; G - garant výsledku; vedidk: 5692792)
TvůrceBrim Luboš (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; vedidk: 6500773)
TvůrceRočkai Petr (státní příslušnost: SK - Slovenská republika; A - domácí tvůrce; vedidk: 1292358)
Údaje blíže specifikující výsledek
Popis v původním jazyceOne 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á slovaExplicit Model Checking; Parallel; On-the-fly; Partial Order Reduction
Kód UT ISI000308732800004
Název periodkaScience of Computer Programming
Rozsah stran1272-1288
ISSN0167-6423
Svazek periodika77
Číslo periodika v rámci uvedeného svazku12
Stát vydavatele periodikaUS - Spojené státy americké
Počet stran výsledku17
DOI výsledku10.1016/j.scico.2011.03.001
Údaje o tomto záznamu o výsledku
PředkladatelMasarykova univerzita / Fakulta informatiky
DodavatelMSM - Ministerstvo školství, mládeže a tělovýchovy (MŠMT)
Rok sběru2013
Systémové označení dodávky datRIV13-MSM-14330___/02:2
SpecifikaceRIV/00216224:14330/12:00057076!RIV13-MSM-14330___
Kontrolní kód[FF07E969C451]
Další výskyty tohoto výsledku od stejného předkladatele
Dodáno AV ČR v roce 2013Záznam s identifikačním kódem RIV/00216224:14330/12:00057076 v dodávce dat RIV13-AV0-14330___/02:2
Dodáno GA ČR v roce 2013Záznam s identifikačním kódem 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
ProjektGA201/09/1389 - Verifikace a analýza velmi velkých počítačových systémů (2009-2011, GA0/GA)
ProjektGP201/09/P497 - Automatizovaná formální verifikace s využitím soudobého hardware (2009-2011, GA0/GP)
Projekt1ET400300504 - Realistická aplikace formálních metod v komponentových systémech (2005-2009, AV0/1E)
Projekt1ET408050503 - Techniky automatické verifikace a validace softwarových a hardwarových systémů (2005-2009, AV0/1E)
Výzkumný záměrMSM0021622419 - Vysoce paralelní a distribuované výpočetní systémy (2005-2011, MSM)
S - Specifický výzkum na vysokých školách