RIV/00216224:14330/13:00066141 - Compositional Approach to Suspension and Other Improvements to LTL Translation (2013)

Údaje o výsledku
Identifikační kódRIV/00216224:14330/13:00066141
Název v původním jazyceCompositional Approach to Suspension and Other Improvements to LTL Translation
DruhD - Článek ve sborníku
Jazykeng - angličtina
OborIN - Informatika
Rok uplatnění2013
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íD - Článek ve sborníku
Skupina oboru v hodnocení04 - Technické a informatické vědy
Konkrétní způsob(y) hodnocení výsledkuČlánek ve sborníku evidovaném v databázi Scopus bodovaný podle SJR zdroje typu Book Series nebo Conference Proceedings
Bodové ohodnocení46,181
Faktor korekce50,1 %
Body (upravené podle přílohy č. 8 Metodiky)23,141
Rozdělení výsledku mezi předkladatele
OrganizaceVýzkumná organizace?PodílBodyBody (upravené podle přílohy č. 8 Metodiky)
Masarykova univerzita / Fakulta informatikyano75,0 %34,63617,356
Tvůrci výsledku
Počet tvůrců celkem5
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ůrceBadie Thomas (státní příslušnost: FR - Francouzská republika)
TvůrceDuret-Lutz Alexandre (státní příslušnost: FR - Francouzská republika)
TvůrceKřetínský Mojmír (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; vedidk: 5598095)
TvůrceStrejček Jan (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; vedidk: 3978915)
Údaje blíže specifikující výsledek
Popis v původním jazyceRecently, there was defined a fragment of LTL (containing fairness properties among other interesting formulae) whose validity over a given infinite word depends only on an arbitrary suffix of the word. Building upon an existing translation from LTL to Büchi automata, we introduce a compositional approach where subformulae of this fragment are translated separately from the rest of an input formula and the produced automata are composed in a way that the subformulae are checked only in relevant accepting strongly connected components of the final automaton. Further, we suggest improvements over some procedures commonly applied to generalized Büchi automata, namely over generalized acceptance simplification and over degeneralization. Finally we show how existing simulation-based reductions can be implemented in a signature-based framework in a way that improves the determinism of the automaton.
Klíčová slovalinear time logic; model-checking; translation LTL to Buchi automata
Název sborníkuModel Checking Software - 20th International Symposium, SPIN 2013
Rozsah stran81-98
Forma vydáníP - Tištěná verze „print“
ISSN0302-9743
ISBN9783642391750
Počet stran výsledku18
Název nakladateleSpringer-Verlag
Místo vydáníBerlin Heidelberg
Místo konání akceStony Brook, NY, USA
Rok konání akce2013
Typ akce podle státní příslušnoti účastníkůWRD - Světová
DOI výsledku10.1007/978-3-642-39176-7_6
Údaje o tomto záznamu o výsledku
PředkladatelMasarykova univerzita / Fakulta informatiky
DodavatelGA0 - Grantová agentura České republiky (GA ČR)
Rok sběru2014
Systémové označení dodávky datRIV14-GA0-14330___/01:1
SpecifikaceRIV/00216224:14330/13:00066141!RIV14-GA0-14330___
Kontrolní kód[6BEE7B523476]
Další výskyty tohoto výsledku od stejného předkladatele
Dodáno MŠMT v roce 2014Záznam s identifikačním kódem RIV/00216224:14330/13:00066141 v dodávce dat RIV14-MSM-14330___/01:1
Odkazy na výzkumné aktivity, při jejichž řešení výsledek vznikl
ProjektGBP202/12/G061 - Centrum excelence - Institut teoretické informatiky (CE-ITI) (2012-2018, GA0/GB)
S - Specifický výzkum na vysokých školách