BLAHOUDEK, František, Juraj MAJOR a 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. s. 152-171. ISBN 978-3-030-32504-6. doi:10.1007/978-3-030-32505-3_10. 2019.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název LTL to Smaller Self-Loop Alternating Automata 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í Cham (Switzerland), Theoretical Aspects of Computing - ICTAC 2019 - 16th International Colloquium, Hammamet, Tunisia, October 31 - November 4, 2019, Proceedings, od s. 152-171, 20 s. 2019.
Nakladatel Springer
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10200 1.2 Computer and information sciences
Stát vydavatele Švýcarsko
Utajení není předmětem státního či obchodního tajemství
Forma vydání elektronická verze "online"
WWW URL
Impakt faktor Impact factor: 0.402 v roce 2005
Kód RIV RIV/00216224:14330/19:00107795
Organizační jednotka Fakulta informatiky
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
Klíčová slova anglicky LTL; linear temporal logic; automata; automata over infinite words; alternating automata; LTL to automata; ltl3tela
Štítky alternating automata, automata, firank_B, formela-conference, linear temporal logic, LTL, omega-automata, 𝜔-automata
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 28. 4. 2020 00:00.
Anotace
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.
Návaznosti
GA19-24397S, projekt VaVNázev: Automaty v rozhodovacích procedurách a verifikaci (Akronym: AUTODEV)
Investor: Grantová agentura ČR, Automata for Decision Procedures and Verification
MUNI/A/1018/2018, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII.
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/1040/2018, interní kód MUNázev: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 19 (Akronym: SKOMU)
Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 19, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
VytisknoutZobrazeno: 19. 4. 2024 12:15