JANKOLA, Marek a Jan STREJČEK. Tighter Construction of Tight Büchi Automata. Online. In Naoki Kobayashi and James Worrell. Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I. Cham: Springer, 2024, s. 234-255. ISBN 978-3-031-57227-2. Dostupné z: https://dx.doi.org/10.1007/978-3-031-57228-9_12. |
Další formáty:
BibTeX
LaTeX
RIS
@inproceedings{2396421, author = {Jankola, Marek and Strejček, Jan}, address = {Cham}, booktitle = {Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I}, doi = {http://dx.doi.org/10.1007/978-3-031-57228-9_12}, editor = {Naoki Kobayashi and James Worrell}, keywords = {tight automata; shortest counterexamples; LTL}, howpublished = {elektronická verze "online"}, language = {eng}, location = {Cham}, isbn = {978-3-031-57227-2}, pages = {234-255}, publisher = {Springer}, title = {Tighter Construction of Tight Büchi Automata}, url = {https://link.springer.com/chapter/10.1007/978-3-031-57228-9_12}, year = {2024} }
TY - JOUR ID - 2396421 AU - Jankola, Marek - Strejček, Jan PY - 2024 TI - Tighter Construction of Tight Büchi Automata PB - Springer CY - Cham SN - 9783031572272 KW - tight automata KW - shortest counterexamples KW - LTL UR - https://link.springer.com/chapter/10.1007/978-3-031-57228-9_12 N2 - Tight automata are useful in providing the shortest counterexample in LTL model checking and also in constructing a maximally satisfying strategy in LTL strategy synthesis. There exists a translation of LTL formulas to tight Büchi automata and several translations of Büchi automata to equivalent tight Büchi automata. This paper presents another translation of Büchi automata to equivalent tight Büchi automata. The translation is designed to produce smaller tight automata and it asymptotically improves the best-known upper bound on the size of a tight Büchi automaton equivalent to a given Büchi automaton. We also provide a lower bound, which is more precise than the previously known one. Further, we show that automata reduction methods based on quotienting preserve tightness. Our translation was implemented in a tool called Tightener. Experimental evaluation shows that Tightener usually produces smaller tight automata than the translation from LTL to tight automata known as CGH. ER -
JANKOLA, Marek a Jan STREJČEK. Tighter Construction of Tight Büchi Automata. Online. In Naoki Kobayashi and James Worrell. \textit{Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I}. Cham: Springer, 2024, s.~234-255. ISBN~978-3-031-57227-2. Dostupné z: https://dx.doi.org/10.1007/978-3-031-57228-9\_{}12.
|