forked from mklokocka/seminator
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathblahoudek.20.cav.bib
29 lines (29 loc) · 1.34 KB
/
blahoudek.20.cav.bib
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
@inproceedings{blahoudek.20.cav,
author = {Franti\v{s}ek Blahoudek and Alexandre Duret-Lutz and Jan
Strej\v{c}ek},
title = {{S}eminator~2 Can Complement Generalized {B\"u}chi
Automata via Improved Semi-Determinization},
booktitle = {Proceedings of the 32nd International Conference on
Computer-Aided Verification (CAV'20)},
year = {2020},
publisher = {Springer},
volume = {12225},
series = {Lecture Notes in Computer Science},
pages = {15--27},
month = jul,
abstract = {We present the second generation of the tool Seminator
that transforms transition-based generalized B{\"u}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 \texttt{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.},
doi = {10.1007/978-3-030-53291-8_2}
}