BLAHOUDEK, František, Juraj MAJOR a 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, s. 152-171. ISBN 978-3-030-32504-6. Dostupné z: https://dx.doi.org/10.1007/978-3-030-32505-3_10. |
Další formáty:
BibTeX
LaTeX
RIS
@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 a 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, s.~152-171. ISBN~978-3-030-32504-6. Dostupné z: https://dx.doi.org/10.1007/978-3-030-32505-3\_{}10.
|