| Údaje o výsledku |
| Identifikační kód | RIV/00216224:14330/12:00057483 |
| Název v původním jazyce | Deterministic Automata for the (F,G)-fragment of LTL |
| Druh | D - Článek ve sborníku |
| Jazyk | eng - angličtina |
| Obor | IN - 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ý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 | Výsledek hodnocený již v předchozím hodnocení, body se přebírají |
| Bodové ohodnocení | 44,376 |
| Faktor korekce | 77,6 % |
| Body (upravené podle přílohy č. 8 Metodiky) | 34,420 |
| 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 | 66,7 % | 29,584 | 22,947 |
|
| Tvůrci výsledku |
| Počet tvůrců celkem | 2 |
| Počet domácích tvůrců | 1 |
| Tvůrce | Křetínský Jan (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; G - garant výsledku; vedidk: 3503054) |
| Tvůrce | Esparza Javier (státní příslušnost: ES - Španělské království) |
| Údaje blíže specifikující výsledek |
| Popis v původním jazyce | When dealing with linear temporal logic properties in the setting of e.g. games or probabilistic systems, one often needs to express them as deterministic omega-automata. In order to translate LTL to deterministic omega-automata, the traditional approach first translates the formula to a non-deterministic Buchi automaton. Then a determinization procedure such as of Safra is performed yielding a deterministic omega-automaton. We present a direct translation of the (F,G)-fragment of LTL into deterministic omega-automata with no determinization procedure involved. Since our approach is tailored to LTL, we often avoid the typically unnecessarily large blowup caused by general determinization algorithms. We investigate the complexity of this translation and provide experimental results and compare them to the traditional method. |
| Klíčová slova | linear temporal logic; automata; determinism |
| Rozsah stran | 7-22 |
| Název sborníku | Computer Aided Verification - 24th International Conference |
| Forma vydání | P - Tištěná verze „print“ |
| ISSN | 0302-9743 |
| Počet stran výsledku | 16 |
| ISBN | 9783642314230 |
| Název nakladatele | Springer-Verlag |
| Místo vydání | Heidelberg Dordrecht London New York |
| Místo konání akce | Berkeley, CA, USA |
| Rok konání akce | 2012 |
| Typ akce podle státní příslušnoti účastníků | WRD - Světová |
| DOI výsledku | 10.1007/978-3-642-31424-7_7 |
| Ú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 | 2013 |
| Systémové označení dodávky dat | RIV13-GA0-14330___/02:2 |
| Specifikace | RIV/00216224:14330/12:00057483!RIV13-GA0-14330___ |
| Kontrolní kód | [A04A95D79EB7] |
| Další výskyty tohoto výsledku od stejného předkladatele |
| Dodáno MŠMT v roce 2013 | Záznam s identifikačním kódem RIV/00216224:14330/12:00057483 v dodávce dat RIV13-MSM-14330___/02:2 |
| 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 |