LTL to self-loop alternating automata with generic acceptance 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%2F20%3A00114391" target="_blank" >RIV/00216224:14330/20:00114391 - isvavai.cz</a>
Výsledek na webu
<a href="https://www.sciencedirect.com/science/article/pii/S030439752030390X" target="_blank" >https://www.sciencedirect.com/science/article/pii/S030439752030390X</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1016/j.tcs.2020.07.015" target="_blank" >10.1016/j.tcs.2020.07.015</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
LTL to self-loop alternating automata with generic acceptance and back
Popis výsledku v původním jazyce
Self-loop alternating automata (SLAA) with Buchi or co-Buchi acceptance are popular formalisms also known as very weak alternating automata (VWAA). They are often used as an intermediate results 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 Buchi or co-Buchi SLAA. Our translation is already implemented in the tool ltl3tela, where it helps to produce small deterministic or nondeterministic transition-based Emerson-Lei automata for given LTL formulae. (C) 2020 Elsevier B.V. All rights reserved.
Název v anglickém jazyce
LTL to self-loop alternating automata with generic acceptance and back
Popis výsledku anglicky
Self-loop alternating automata (SLAA) with Buchi or co-Buchi acceptance are popular formalisms also known as very weak alternating automata (VWAA). They are often used as an intermediate results 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 Buchi or co-Buchi SLAA. Our translation is already implemented in the tool ltl3tela, where it helps to produce small deterministic or nondeterministic transition-based Emerson-Lei automata for given LTL formulae. (C) 2020 Elsevier B.V. All rights reserved.
Klasifikace
Druh
J<sub>imp</sub> - Článek v periodiku v databázi Web of Science
CEP obor
—
OECD FORD obor
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
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í
2020
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 periodika
Theoretical Computer Science
ISSN
0304-3975
e-ISSN
1879-2294
Svazek periodika
840
Číslo periodika v rámci svazku
Nov 2020
Stát vydavatele periodika
NL - Nizozemsko
Počet stran výsledku
21
Strana od-do
122-142
Kód UT WoS článku
000572872700006
EID výsledku v databázi Scopus
2-s2.0-85088801451