LTL to Smaller Self-Loop Alternating Automata and Back
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F19%3A00107795" target="_blank" >RIV/00216224:14330/19:00107795 - isvavai.cz</a>
Výsledek na webu
<a href="https://link.springer.com/chapter/10.1007/978-3-030-32505-3_10" target="_blank" >https://link.springer.com/chapter/10.1007/978-3-030-32505-3_10</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-030-32505-3_10" target="_blank" >10.1007/978-3-030-32505-3_10</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
LTL to Smaller Self-Loop Alternating Automata and Back
Popis výsledku v původním jazyce
Self-loop alternating automata (SLAA) with Büchi or co-Büchi acceptance are popular intermediate formalisms in translations of LTL to deterministic or nondeterministic automata. This paper considers SLAA with generic transition-based Emerson-Lei acceptance and presents translations of LTL to these automata and back. Importantly, the translation of LTL to SLAA with generic acceptance produces considerably smaller automata than previous translations of LTL to Büchi or co-Büchi SLAA. Our translation is already implemented in the tool LTL3TELA, where it helps to produce small deterministic or nondeterministic automata for given LTL formulae.
Název v anglickém jazyce
LTL to Smaller Self-Loop Alternating Automata and Back
Popis výsledku anglicky
Self-loop alternating automata (SLAA) with Büchi or co-Büchi acceptance are popular intermediate formalisms in translations of LTL to deterministic or nondeterministic automata. This paper considers SLAA with generic transition-based Emerson-Lei acceptance and presents translations of LTL to these automata and back. Importantly, the translation of LTL to SLAA with generic acceptance produces considerably smaller automata than previous translations of LTL to Büchi or co-Büchi SLAA. Our translation is already implemented in the tool LTL3TELA, where it helps to produce small deterministic or nondeterministic automata for given LTL formulae.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
—
OECD FORD obor
10200 - Computer and information sciences
Návaznosti výsledku
Projekt
<a href="/cs/project/GA19-24397S" target="_blank" >GA19-24397S: Automaty v rozhodovacích procedurách a verifikaci</a><br>
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Ostatní
Rok uplatnění
2019
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
Theoretical Aspects of Computing - ICTAC 2019 - 16th International Colloquium, Hammamet, Tunisia, October 31 - November 4, 2019, Proceedings
ISBN
9783030325046
ISSN
0302-9743
e-ISSN
1611-3349
Počet stran výsledku
20
Strana od-do
152-171
Název nakladatele
Springer
Místo vydání
Cham (Switzerland)
Místo konání akce
Hammamet, Tunisia
Datum konání akce
1. 1. 2019
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
000582443200010