LTL to Smaller Self-Loop Alternating Automata and Back

D 2019

LTL to Smaller Self-Loop Alternating Automata and Back

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

Basic information

Original name

LTL to Smaller Self-Loop Alternating Automata 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

Cham (Switzerland), Theoretical Aspects of Computing - ICTAC 2019 - 16th International Colloquium, Hammamet, Tunisia, October 31 - November 4, 2019, Proceedings, p. 152-171, 20 pp. 2019

Publisher

Springer

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10200 1.2 Computer and information sciences

Country of publisher

Switzerland

Confidentiality degree

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

Publication form

electronic version available online

References:

URL

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/19:00107795

Organization unit

Faculty of Informatics

ISBN

978-3-030-32504-6

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-32505-3_10

UT WoS

000582443200010

Keywords in English

LTL; linear temporal logic; automata; automata over infinite words; alternating automata; LTL to automata; ltl3tela

Abstract

V originále

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.

Links

GA19-24397S, research and development project

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

Investor: Czech Science Foundation

MUNI/A/1018/2018, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII.

Investor: Masaryk University, Category A

MUNI/A/1040/2018, interní kód MU

Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 19 (Acronym: SKOMU)

Investor: Masaryk University, Category A

Citovat

BLAHOUDEK, František, Juraj MAJOR and Jan STREJČEK. LTL to Smaller Self-Loop Alternating Automata and Back. Online. In Robert Mark Hierons, Mohamed Mosbah. Theoretical Aspects of Computing - ICTAC 2019 - 16th International Colloquium, Hammamet, Tunisia, October 31 - November 4, 2019, Proceedings. Cham (Switzerland): Springer, 2019, p. 152-171. ISBN 978-3-030-32504-6. Available from: https://dx.doi.org/10.1007/978-3-030-32505-3_10.

@inproceedings{1580376,
   author = {Blahoudek, František and Major, Juraj and Strejček, Jan},
   address = {Cham (Switzerland)},
   booktitle = {Theoretical Aspects of Computing - ICTAC 2019 - 16th International Colloquium, Hammamet, Tunisia, October 31 - November 4, 2019, Proceedings},
   doi = {http://dx.doi.org/10.1007/978-3-030-32505-3_10},
   editor = {Robert Mark Hierons, Mohamed Mosbah},
   keywords = {LTL; linear temporal logic; automata; automata over infinite words; alternating automata; LTL to automata; ltl3tela},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Cham (Switzerland)},
   isbn = {978-3-030-32504-6},
   pages = {152-171},
   publisher = {Springer},
   title = {LTL to Smaller Self-Loop Alternating Automata and Back},
   url = {https://link.springer.com/chapter/10.1007/978-3-030-32505-3_10},
   year = {2019}
}

TY  - JOUR
ID  - 1580376
AU  - Blahoudek, František - Major, Juraj - Strejček, Jan
PY  - 2019
TI  - LTL to Smaller Self-Loop Alternating Automata and Back
PB  - Springer
CY  - Cham (Switzerland)
SN  - 9783030325046
KW  - LTL
KW  - linear temporal logic
KW  - automata
KW  - automata over infinite words
KW  - alternating automata
KW  - LTL to automata
KW  - ltl3tela
UR  - https://link.springer.com/chapter/10.1007/978-3-030-32505-3_10
L2  - https://link.springer.com/chapter/10.1007/978-3-030-32505-3_10
N2  - 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.
ER  -

BLAHOUDEK, František, Juraj MAJOR and Jan STREJČEK. LTL to Smaller Self-Loop Alternating Automata and Back. Online. In Robert Mark Hierons, Mohamed Mosbah. \textit{Theoretical Aspects of Computing - ICTAC 2019 - 16th International Colloquium, Hammamet, Tunisia, October 31 - November 4, 2019, Proceedings}. Cham (Switzerland): Springer, 2019, p.~152-171. ISBN~978-3-030-32504-6. Available from: https://dx.doi.org/10.1007/978-3-030-32505-3\_{}10.

Detailed Information on Publication Record