Údaje o výsledku |
Identifikační kód | RIV/00216224:14330/13:00066141 |
Název v původním jazyce | Compositional Approach to Suspension and Other Improvements to LTL Translation |
Druh | D - Článek ve sborníku |
Jazyk | eng - angličtina |
Obor | IN - 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ýsledku | 2 |
Údaje z Hodnocení výsledků výzkumných organizací 2014 |
Výsledek byl hodnocen v Pilíři I |
Rozsah vyřazení výsledku | Tento 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 korekce | 50,1 % |
Body (upravené podle přílohy č. 8 Metodiky) | 23,141 |
Rozdělení výsledku mezi předkladatele |
Organizace | Výzkumná organizace? | Podíl | Body | Body (upravené podle přílohy č. 8 Metodiky) |
Masarykova univerzita / Fakulta informatiky | ano | 75,0 % | 34,636 | 17,356 |
|
Tvůrci výsledku |
Počet tvůrců celkem | 5 |
Počet domácích tvůrců | 3 |
Tvůrce | Babiak Tomáš (státní příslušnost: SK - Slovenská republika; A - domácí tvůrce; vedidk: 9653023) |
Tvůrce | Badie Thomas (státní příslušnost: FR - Francouzská republika) |
Tvůrce | Duret-Lutz Alexandre (státní příslušnost: FR - Francouzská republika) |
Tvůrce | Křetínský Mojmír (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; vedidk: 5598095) |
Tvůrce | Strejč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 jazyce | Recently, 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á slova | linear time logic; model-checking; translation LTL to Buchi automata |
Název sborníku | Model Checking Software - 20th International Symposium, SPIN 2013 |
Rozsah stran | 81-98 |
Forma vydání | P - Tištěná verze „print“ |
ISSN | 0302-9743 |
ISBN | 9783642391750 |
Počet stran výsledku | 18 |
Název nakladatele | Springer-Verlag |
Místo vydání | Berlin Heidelberg |
Místo konání akce | Stony Brook, NY, USA |
Rok konání akce | 2013 |
Typ akce podle státní příslušnoti účastníků | WRD - Světová |
DOI výsledku | 10.1007/978-3-642-39176-7_6 |
Údaje o tomto záznamu o výsledku |
Předkladatel | Masarykova univerzita / Fakulta informatiky |
Dodavatel | GA0 - Grantová agentura České republiky (GA ČR) |
Rok sběru | 2014 |
Systémové označení dodávky dat | RIV14-GA0-14330___/01:1 |
Specifikace | RIV/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 2014 | Zá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 |
Projekt | GBP202/12/G061 - Centrum excelence - Institut teoretické informatiky (CE-ITI) (2012-2018, GA0/GB) |
S - Specifický výzkum na vysokých školách |