| 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.
|
