RIV/00216224:14330/12:00057181 - Almost linear Büchi automata (2012)

Údaje o výsledku
Identifikační kódRIV/00216224:14330/12:00057181
Název v původním jazyceAlmost linear Büchi automata
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ýsledku2
Ú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í20,833
Faktor korekce90,8 %
Body (upravené podle přílohy č. 8 Metodiky)18,920
Rozdělení výsledku mezi předkladatele
OrganizaceVýzkumná organizace?PodílBodyBody (upravené podle přílohy č. 8 Metodiky)
Masarykova univerzita / Fakulta informatikyano100,0 %20,83318,920
Tvůrci výsledku
Počet tvůrců celkem3
Počet domácích tvůrců3
TvůrceBabiak Tomáš (státní příslušnost: SK - Slovenská republika; A - domácí tvůrce; vedidk: 9653023)
TvůrceStrejček Jan (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; vedidk: 3978915)
TvůrceŘehák Vojtěch (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; G - garant výsledku; vedidk: 8986371)
Údaje blíže specifikující výsledek
Popis v původním jazyceWe introduce a new fragment of Linear temporal logic (LTL) called LIO and a new class of Büchi automata (BA) called Almost linear Büchi automata (ALBA). We provide effective translations between LIO and ALBA showing that the two formalisms are expressively equivalent. As we expect applications of our results in model checking, we use two standard sources of specification formulae, namely Spec Patterns and BEEM, to study practical relevance of LIO fragment, and to compare our translation of LIO to ALBA with two standard translations of LTL to BA via alternating automata. Finally, we demonstrate that the LIO to ALBA translation can be much faster than the standard translation and the produced automata can be substantially smaller.
Klíčová slovaLTL; linear time logic; model checking
Kód UT ISI000300844900004
Název periodkaMathematical Structures in Computer Science
Rozsah stran203-235
ISSN0960-1295
Svazek periodika22
Číslo periodika v rámci uvedeného svazku2
Stát vydavatele periodikaCZ - Česká republika
Počet stran výsledku33
DOI výsledku10.1017/S0960129511000399
Údaje o tomto záznamu o výsledku
PředkladatelMasarykova univerzita / Fakulta informatiky
DodavatelGA0 - Grantová agentura České republiky (GA ČR)
Rok sběru2013
Systémové označení dodávky datRIV13-GA0-14330___/02:2
SpecifikaceRIV/00216224:14330/12:00057181!RIV13-GA0-14330___
Kontrolní kód[2C083437627B]
Další výskyty tohoto výsledku od stejného předkladatele
Dodáno MŠMT v roce 2013Záznam s identifikačním kódem RIV/00216224:14330/12:00057181 v dodávce dat RIV13-MSM-14330___/02:2
Odkazy na výzkumné aktivity, při jejichž řešení výsledek vznikl
ProjektGAP202/10/1469 - Formální metody pro analýzu a verifikaci komplexních systémů (2010-2014, GA0/GA)
ProjektGA201/09/1389 - Verifikace a analýza velmi velkých počítačových systémů (2009-2011, GA0/GA)
ProjektGD102/09/H042 - Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů (2009-2012, GA0/GD)
ProjektGP201/08/P375 - Formální verifikace: algoritmy, vlastnosti modelovacích formalismů a temporálních logik (2008-2010, GA0/GP)
ProjektGP201/08/P459 - Nové možnosti automatické verifikace síťových protokolů (2008-2010, GA0/GP)
Projekt1M0545 - Institut Teoretické Informatiky (2005-2011, MSM/1M)
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