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 and Jan STREJČEK

Basic information

Original name

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

Authors

BLAHOUDEK, František (203 Czech Republic), Juraj MAJOR (703 Slovakia, belonging to the institution) and Jan STREJČEK (203 Czech Republic, guarantor, belonging to the institution)

Edition

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

Other information

Language

English

Type of outcome

Článek v odborném periodiku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Netherlands

Confidentiality degree

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

References:

URL

Impact factor

Impact factor: 0.827

RIV identification code

RIV/00216224:14330/20:00114391

Organization unit

Faculty of Informatics

DOI

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

UT WoS

000572872700006

Keywords in English

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

Abstract

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.

Links

GA19-24397S, research and development project

Name: Automaty v rozhodovacích procedurách a verifikaci (Acronym: AUTODEV)

Investor: Czech Science Foundation

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

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

Investor: Masaryk University, Category A

Citovat

BLAHOUDEK, František, Juraj MAJOR and Jan STREJČEK. LTL to self-loop alternating automata with generic acceptance and back. Theoretical Computer Science. AMSTERDAM: North Holland, 2020, vol. 840, Nov 2020, p. 122-142. ISSN 0304-3975. Available from: 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 and Jan STREJČEK. LTL to self-loop alternating automata with generic acceptance and back. \textit{Theoretical Computer Science}. AMSTERDAM: North Holland, 2020, vol.~840, Nov 2020, p.~122-142. ISSN~0304-3975. Available from: https://dx.doi.org/10.1016/j.tcs.2020.07.015.

Detailed Information on Publication Record