BLAHOUDEK, František, Alexandre DURET-LUTZ and Jan STREJČEK. Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization. Online. In Shuvendu K. Lahiri and Chao Wang. Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II. Cham (Switzerland): Springer, 2020, p. 15-27. ISBN 978-3-030-53290-1. Available from: https://dx.doi.org/10.1007/978-3-030-53291-8_2. |
Other formats:
BibTeX
LaTeX
RIS
@inproceedings{1686896, author = {Blahoudek, František and DuretandLutz, Alexandre and Strejček, Jan}, address = {Cham (Switzerland)}, booktitle = {Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II}, doi = {http://dx.doi.org/10.1007/978-3-030-53291-8_2}, editor = {Shuvendu K. Lahiri and Chao Wang}, keywords = {semi-determinization; complementation; generalized Büchi automata; Seminator}, howpublished = {elektronická verze "online"}, language = {eng}, location = {Cham (Switzerland)}, isbn = {978-3-030-53290-1}, pages = {15-27}, publisher = {Springer}, title = {Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization}, url = {https://link.springer.com/chapter/10.1007%2F978-3-030-53291-8_2}, year = {2020} }
TY - JOUR ID - 1686896 AU - Blahoudek, František - Duret-Lutz, Alexandre - Strejček, Jan PY - 2020 TI - Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization PB - Springer CY - Cham (Switzerland) SN - 9783030532901 KW - semi-determinization KW - complementation KW - generalized Büchi automata KW - Seminator UR - https://link.springer.com/chapter/10.1007%2F978-3-030-53291-8_2 L2 - https://link.springer.com/chapter/10.1007%2F978-3-030-53291-8_2 N2 - We present the second generation of the tool Seminator that transforms transition-based generalized Büchi automata (TGBAs) into equivalent semi-deterministic automata. The tool has been extended with numerous optimizations and produces considerably smaller automata than its first version. In connection with the state-of-the-art LTL to TGBAs translator Spot, Seminator 2 produces smaller (on average) semi-deterministic automata than the direct LTL to semi-deterministic automata translator ltl2ldgba of the Owl library. Further, Seminator 2 has been extended with an improved NCSB complementation procedure for semi-deterministic automata, providing a new way to complement automata that is competitive with state-of-the-art complementation tools. ER -
BLAHOUDEK, František, Alexandre DURET-LUTZ and Jan STREJČEK. Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization. Online. In Shuvendu K. Lahiri and Chao Wang. \textit{Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II}. Cham (Switzerland): Springer, 2020, p.~15-27. ISBN~978-3-030-53290-1. Available from: https://dx.doi.org/10.1007/978-3-030-53291-8\_{}2.
|