| Údaje o výsledku |
| Identifikační kód | RIV/00216224:14330/12:00057222 |
| Název v původním jazyce | LTL to Büchi Automata Translation: Fast and More Deterministic |
| 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 | 100,0 % | 44,376 | 34,420 |
|
| Tvůrci výsledku |
| Počet tvůrců celkem | 4 |
| Počet domácích tvůrců | 4 |
| Tvůrce | Babiak Tomáš (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; G - garant výsledku; vedidk: 9653023) |
| Tvůrce | Křetínský Mojmír (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; vedidk: 5598095) |
| Tvůrce | Řehák Vojtěch (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; vedidk: 8986371) |
| 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 | We introduce improvements in the algorithm by Gastin and Oddoux translating LTL formulae into Büchi automata via very weak alternating co-Büchi automata and generalized Büchi automata. Several improvements are based on specific properties of any formula where each branch of its syntax tree contains at least one eventually operator and at least one always operator. These changes usually result in faster translations and smaller automata. Other improvements reduce non-determinism in the produced automata. In fact, we modified all the steps of the original algorithm and its implementation known as LTL2BA. Experimental results show that our modifications are real improvements. Their implementations within an LTL2BA translation made LTL2BA very competitive with the current version of SPOT, sometimes outperforming it substantially. |
| Klíčová slova | Linear Temporal Logic; Büchi Automata |
| Název sborníku | TACAS 2012: 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems |
| Rozsah stran | 95-109 |
| Forma vydání | C - Paměťový nosič (CD, DVD, flash disk, …) |
| ISSN | 0302-9743 |
| ISBN | 9783642287558 |
| Počet stran výsledku | 15 |
| Název nakladatele | Springer-Verlag |
| Místo vydání | Berlin, Heidelberg |
| Místo konání akce | Tallinn, Estonia |
| 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-28756-5_8 |
| Ú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:00057222!RIV13-GA0-14330___ |
| Kontrolní kód | [0DFE4B76434F] |
| 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:00057222 v dodávce dat RIV13-MSM-14330___/02:2 |
| Odkazy na výzkumné aktivity, při jejichž řešení výsledek vznikl |
| Projekt | GAP202/10/1469 - Formální metody pro analýzu a verifikaci komplexních systémů (2010-2014, GA0/GA) |
| Projekt | GA201/09/1389 - Verifikace a analýza velmi velkých počítačových systémů (2009-2011, GA0/GA) |
| Projekt | GBP202/12/G061 - Centrum excelence - Institut teoretické informatiky (CE-ITI) (2012-2018, GA0/GB) |
| Projekt | GD102/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) |
| Projekt | GPP202/12/P612 - Formální verifikace stochastických systémů s reálným časem (2012-2014, GA0/GP) |
| Výzkumný záměr | MSM0021622419 - Vysoce paralelní a distribuované výpočetní systémy (2005-2011, MSM) |
| S - Specifický výzkum na vysokých školách |