Other formats:
BibTeX
LaTeX
RIS
@inproceedings{1577339,
author = {Major, Juraj and Blahoudek, František and Strejček, Jan and Jánošová, Miriama and Zbončáková, Tatiana},
address = {Cham (Switzerland)},
booktitle = {Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings},
doi = {http://dx.doi.org/10.1007/978-3-030-31784-3_21},
editor = {Yu-Fang Chen, Chih-Hong Cheng, Javier Esparza},
keywords = {ltl3tela; LTL; linear temporal logic; automata; automata over infinite words; LTL to automata},
howpublished = {elektronická verze "online"},
language = {eng},
location = {Cham (Switzerland)},
isbn = {978-3-030-31783-6},
pages = {357-365},
publisher = {Springer},
title = {ltl3tela: LTL to Small Deterministic or Nondeterministic Emerson-Lei Automata},
url = {https://link.springer.com/chapter/10.1007/978-3-030-31784-3_21},
year = {2019}
}
TY - JOUR
ID - 1577339
AU - Major, Juraj - Blahoudek, František - Strejček, Jan - Jánošová, Miriama - Zbončáková, Tatiana
PY - 2019
TI - ltl3tela: LTL to Small Deterministic or Nondeterministic Emerson-Lei Automata
PB - Springer
CY - Cham (Switzerland)
SN - 9783030317836
KW - ltl3tela
KW - LTL
KW - linear temporal logic
KW - automata
KW - automata over infinite words
KW - LTL to automata
UR - https://link.springer.com/chapter/10.1007/978-3-030-31784-3_21
L2 - https://link.springer.com/chapter/10.1007/978-3-030-31784-3_21
N2 - The paper presents a new tool ltl3tela translating LTL to deterministic or nondeterministic transition-based Emerson-Lei automata (TELA). Emerson-Lei automata use generic acceptance formulae with basic terms corresponding to Büchi and co-Büchi acceptance. The tool combines algorithms of Spot library, a new translation of LTL to TELA via alternating automata, a pattern-based automata reduction method, and few other heuristics. Experimental evaluation shows that ltl3tela can produce deterministic automata that are, on average, noticeably smaller than deterministic TELA produced by state-of-the-art translators Delag, Rabinizer 4, and Spot. For nondeterministic automata, the improvement over Spot is smaller, but still measurable.
ER -
MAJOR, Juraj, František BLAHOUDEK, Jan STREJČEK, Miriama JÁNOŠOVÁ and Tatiana ZBONČÁKOVÁ. ltl3tela: LTL to Small Deterministic or Nondeterministic Emerson-Lei Automata. Online. In Yu-Fang Chen, Chih-Hong Cheng, Javier Esparza. \textit{Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings}. Cham (Switzerland): Springer, 2019, p.~357-365. ISBN~978-3-030-31783-6. Available from: https://dx.doi.org/10.1007/978-3-030-31784-3\_{}21.
|
