BLAHOUDEK, František, Juraj MAJOR and Jan STREJČEK. LTL to Smaller Self-Loop Alternating Automata and Back. 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. p. 152-171. ISBN 978-3-030-32504-6. doi:10.1007/978-3-030-32505-3_10. 2019.
Other formats:   BibTeX LaTeX RIS
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
Original language English
Type of outcome Proceedings paper
Field of Study 10200 1.2 Computer and information sciences
Country of publisher Switzerland
Confidentiality degree is not subject to a state or trade secret
Publication form electronic version available online
WWW 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 0302-9743
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
Tags alternating automata, automata, firank_B, formela-conference, linear temporal logic, LTL, omega-automata, 𝜔-automata
Tags International impact, Reviewed
Changed by Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 28/4/2020 00:00.
Abstract
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 projectName: Automaty v rozhodovacích procedurách a verifikaci (Acronym: AUTODEV)
Investor: Czech Science Foundation
MUNI/A/1018/2018, interní kód MUName: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII.
Investor: Masaryk University, Category A
MUNI/A/1040/2018, interní kód MUName: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 19 (Acronym: SKOMU)
Investor: Masaryk University, Category A
PrintDisplayed: 19/4/2024 11:27