Comparison of LTL to Deterministic Rabin Automata Translators
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F13%3A00066512" target="_blank" >RIV/00216224:14330/13:00066512 - isvavai.cz</a>
Výsledek na webu
<a href="http://dx.doi.org/10.1007/978-3-642-45221-5_12" target="_blank" >http://dx.doi.org/10.1007/978-3-642-45221-5_12</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-642-45221-5_12" target="_blank" >10.1007/978-3-642-45221-5_12</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Comparison of LTL to Deterministic Rabin Automata Translators
Popis výsledku v původním jazyce
Increasing interest in control synthesis and probabilistic model checking caused recent development of LTL to deterministic omega-automata translation. The standard approach represented by ltl2dstar tool employs Safra's construction to determinize a Büchi automaton produced by some LTL to Büchi automata translator. Since 2012, three new LTL to deterministic Rabin automata translators appeared, namely Rabinizer, LTL3DRA, and Rabinizer 2. They all avoid Safra's construction and work on LTL fragments only.We compare performance and automata produced by the mentioned tools, where ltl2dstar is combined with several LTL to Büchi automata translators: besides traditionally used LTL2BA, we also consider LTL->NBA, LTL3BA, and Spot.
Název v anglickém jazyce
Comparison of LTL to Deterministic Rabin Automata Translators
Popis výsledku anglicky
Increasing interest in control synthesis and probabilistic model checking caused recent development of LTL to deterministic omega-automata translation. The standard approach represented by ltl2dstar tool employs Safra's construction to determinize a Büchi automaton produced by some LTL to Büchi automata translator. Since 2012, three new LTL to deterministic Rabin automata translators appeared, namely Rabinizer, LTL3DRA, and Rabinizer 2. They all avoid Safra's construction and work on LTL fragments only.We compare performance and automata produced by the mentioned tools, where ltl2dstar is combined with several LTL to Büchi automata translators: besides traditionally used LTL2BA, we also consider LTL->NBA, LTL3BA, and Spot.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
IN - Informatika
OECD FORD obor
—
Návaznosti výsledku
Projekt
<a href="/cs/project/GAP202%2F10%2F1469" target="_blank" >GAP202/10/1469: Formální metody pro analýzu a verifikaci komplexních systémů</a><br>
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach
Ostatní
Rok uplatnění
2013
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název statě ve sborníku
Logic for Programming Artificial Intelligence and Reasoning, LPAR-19
ISBN
9783642452208
ISSN
0302-9743
e-ISSN
—
Počet stran výsledku
9
Strana od-do
164-172
Název nakladatele
Springer
Místo vydání
Berlin Heidelberg
Místo konání akce
Stellenbosch, South Africa
Datum konání akce
1. 1. 2013
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
—