LTL to self-loop alternating automata with generic acceptance
and back

J 2020

LTL to self-loop alternating automata with generic acceptance and back

BLAHOUDEK, František, Juraj MAJOR a Jan STREJČEK

Základní údaje

Originální název

LTL to self-loop alternating automata with generic acceptance and back

Autoři

BLAHOUDEK, František (203 Česká republika), Juraj MAJOR (703 Slovensko, domácí) a Jan STREJČEK (203 Česká republika, garant, domácí)

Vydání

Theoretical Computer Science, AMSTERDAM, North Holland, 2020, 0304-3975

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Nizozemské království

Utajení

není předmětem státního či obchodního tajemství

Odkazy

URL

Impakt faktor

Impact factor: 0.827

Kód RIV

RIV/00216224:14330/20:00114391

Organizační jednotka

Fakulta informatiky

DOI

http://dx.doi.org/10.1016/j.tcs.2020.07.015

UT WoS

000572872700006

Klíčová slova anglicky

LTL; Omega-automata; LTL to automata translation; Alternating automata; ltl3tela

Štítky

alternating automata, formela-journal, linear temporal logic, LTL, 𝜔-automata

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 29. 4. 2021 12:31, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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ávaznosti

GA19-24397S, projekt VaV

Název: Automaty v rozhodovacích procedurách a verifikaci (Akronym: AUTODEV)

Investor: Grantová agentura ČR, Automata for Decision Procedures and Verification

MUNI/A/1050/2019, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IX (Akronym: SV-FI MAV IX)

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IX, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

Citovat

BLAHOUDEK, František, Juraj MAJOR a Jan STREJČEK. LTL to self-loop alternating automata with generic acceptance and back. Theoretical Computer Science. AMSTERDAM: North Holland, 2020, roč. 840, Nov 2020, s. 122-142. ISSN 0304-3975. Dostupné z: https://dx.doi.org/10.1016/j.tcs.2020.07.015.

@article{1686867,
   author = {Blahoudek, František and Major, Juraj and Strejček, Jan},
   article_location = {AMSTERDAM},
   article_number = {Nov 2020},
   doi = {http://dx.doi.org/10.1016/j.tcs.2020.07.015},
   keywords = {LTL; Omega-automata; LTL to automata translation; Alternating automata; ltl3tela},
   language = {eng},
   issn = {0304-3975},
   journal = {Theoretical Computer Science},
   title = {LTL to self-loop alternating automata with generic acceptance and back},
   url = {https://www.sciencedirect.com/science/article/pii/S030439752030390X},
   volume = {840},
   year = {2020}
}

TY  - JOUR
ID  - 1686867
AU  - Blahoudek, František - Major, Juraj - Strejček, Jan
PY  - 2020
TI  - LTL to self-loop alternating automata with generic acceptance and back
JF  - Theoretical Computer Science
VL  - 840
IS  - Nov 2020
SP  - 122-142
EP  - 122-142
PB  - North Holland
SN  - 03043975
KW  - LTL
KW  - Omega-automata
KW  - LTL to automata translation
KW  - Alternating automata
KW  - ltl3tela
UR  - https://www.sciencedirect.com/science/article/pii/S030439752030390X
L2  - https://www.sciencedirect.com/science/article/pii/S030439752030390X
N2  - 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.
ER  -

BLAHOUDEK, František, Juraj MAJOR a Jan STREJČEK. LTL to self-loop alternating automata with generic acceptance and back. \textit{Theoretical Computer Science}. AMSTERDAM: North Holland, 2020, roč.~840, Nov 2020, s.~122-142. ISSN~0304-3975. Dostupné z: https://dx.doi.org/10.1016/j.tcs.2020.07.015.

Podrobný výpis o publikaci