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

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.

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

• Originální 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í
• WWW: 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

Anotace

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