LTL to Büchi Automata Translation: Fast and More Deterministic (2012)výskyt výsledku
| Identifikační kód | RIV/00216224:14330/12:00057222 |
|---|---|
| Název v anglickém jazyce | LTL to Büchi Automata Translation: Fast and More Deterministic |
| Druh | D - Článek ve sborníku |
| Jazyk | eng - angličtina |
| Obor - skupina | I - Informatika |
| Obor | IN - Informatika |
| Rok uplatnění | 2012 |
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
| Počet výskytů výsledku | 2 |
| Počet tvůrců celkem | 4 |
| Počet domácích tvůrců | 4 |
| Výčet všech uvedených jednotlivých tvůrců | Tomáš Babiak (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 9653023) Mojmír Křetínský (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 5598095) Vojtěch Řehák (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 8986371) Jan Strejček (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 3978915) |
| Popis výsledku v anglické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 formulawhere 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 competitivewith the current version of SPOT, sometimes outperforming it substantially. |
| Klíčová slova oddělená středníkem | Linear Temporal Logic; Büchi Automata |
| Stránka www, na které se nachází výsledek | - |
| DOI výsledku | 10.1007/978-3-642-28756-5_8 |
Údaje o výsledku v závislosti na druhu výsledku
| Název sborníku | TACAS 2012: 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems |
|---|---|
| ISBN | 9783642287558 |
| ISSN | 0302-9743 |
| Počet stran výsledku | 15 |
| Strana od-do | 95-109 |
| Název nakladatele | Springer-Verlag |
| Místo vydání | Berlin, Heidelberg |
| Místo konání akce | Tallinn, Estonia |
| Datum konání akce | 2012 |
| Typ akce podle státní příslušnosti účastníků | WRD - Celosvětová |
| Kód UT WoS článku podle Web of Science | - |
Ostatní informace o výsledku
| Předkladatel | Masarykova univerzita / Fakulta informatiky |
|---|---|
| Dodavatel | GA0 - Grantová agentura České republiky (GA ČR) |
| Rok sběru | 2013 |
| Specifikace | RIV/00216224:14330/12:00057222!RIV13-GA0-14330___ |
| Datum poslední aktualizace výsledku | 04.09.2013 |
| Kontrolní číslo | 43534974 |
Informace o dalších výskytech výsledku dodaného stejným předkladatelem
| Dodáno MŠMT v roce 2013 | 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 podporovaný GA ČR v programu GA | GA201/09/1389 - Verifikace a analýza velmi velkých počítačových systémů (2009 - 2011) |
|---|---|
| Projekt podporovaný GA ČR v programu GA | GAP202/10/1469 - Formální metody pro analýzu a verifikaci komplexních systémů (2010 - 2014) |
| Projekt podporovaný GA ČR v programu GB | GBP202/12/G061 - Centrum excelence - Institut teoretické informatiky (CE-ITI) (2012 - 2018) |
| Projekt podporovaný GA ČR v programu GD | 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) |
| Projekt podporovaný GA ČR v programu GP | GPP202/12/P612 - Formální verifikace stochastických systémů s reálným časem (2012 - 2014) |
| Výzkumný záměr podporovaný MŠMT | MSM0021622419 - Vysoce paralelní a distribuované výpočetní systémy (2005 - 2011) |
| Podpora / návaznosti | Specifický výzkum na vysokých školách, poskytovatel MŠMT |