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. |
Další formáty:
BibTeX
LaTeX
RIS
@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 a Jan STREJČEK. LTL to self-loop alternating automata with generic acceptance and back. \textit{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.
|