Difference between revisions of "Publications/blahoudek.20.cav"
From LRDE
(Created page with "{{Publication | published = true | date = 2020-05-14 | authors = František Blahoudek, Alexandre Duret-Lutz, Jan Strejček | title = Seminator 2 Can Complement Generalize...") |
|||
Line 6: | Line 6: | ||
| booktitle = Proceedings of the 32nd International Conference on Computer-Aided Verification (CAV'20) |
| booktitle = Proceedings of the 32nd International Conference on Computer-Aided Verification (CAV'20) |
||
| publisher = Springer |
| publisher = Springer |
||
− | | |
+ | | volume = 12225 |
+ | | series = Lecture Notes in Computer Science |
||
+ | | pages = 15 to 27 |
||
| abstract = 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. FurtherSeminator 2 has been extended with an improved NCSB complementation procedure for semi-deterministic automataproviding a new way to complement automata that is competitive with state-of-the-art complementation tools. |
| abstract = 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. FurtherSeminator 2 has been extended with an improved NCSB complementation procedure for semi-deterministic automataproviding a new way to complement automata that is competitive with state-of-the-art complementation tools. |
||
| lrdeprojects = Spot |
| lrdeprojects = Spot |
||
| lrdenewsdate = 2020-05-14 |
| lrdenewsdate = 2020-05-14 |
||
| lrdepaper = http://www.lrde.epita.fr/dload/papers/blahoudek.20.cav.pdf |
| lrdepaper = http://www.lrde.epita.fr/dload/papers/blahoudek.20.cav.pdf |
||
− | | note = To appear |
||
| type = inproceedings |
| type = inproceedings |
||
| id = blahoudek.20.cav |
| id = blahoudek.20.cav |
||
+ | | identifier = doi:10.1007/978-3-030-53291-8_2 |
||
| bibtex = |
| bibtex = |
||
@InProceedings<nowiki>{</nowiki> blahoudek.20.cav, |
@InProceedings<nowiki>{</nowiki> blahoudek.20.cav, |
||
Line 24: | Line 26: | ||
year = <nowiki>{</nowiki>2020<nowiki>}</nowiki>, |
year = <nowiki>{</nowiki>2020<nowiki>}</nowiki>, |
||
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>, |
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>, |
||
− | + | volume = <nowiki>{</nowiki>12225<nowiki>}</nowiki>, |
|
+ | series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>, |
||
+ | pages = <nowiki>{</nowiki>15--27<nowiki>}</nowiki>, |
||
month = jul, |
month = jul, |
||
abstract = <nowiki>{</nowiki>We present the second generation of the tool Seminator |
abstract = <nowiki>{</nowiki>We present the second generation of the tool Seminator |
||
Line 40: | Line 44: | ||
providing a new way to complement automata that is |
providing a new way to complement automata that is |
||
competitive with state-of-the-art complementation tools.<nowiki>}</nowiki>, |
competitive with state-of-the-art complementation tools.<nowiki>}</nowiki>, |
||
− | + | doi = <nowiki>{</nowiki>10.1007/978-3-030-53291-8_2<nowiki>}</nowiki> |
|
<nowiki>}</nowiki> |
<nowiki>}</nowiki> |
||
Latest revision as of 11:15, 21 July 2020
- Authors
- František Blahoudek, Alexandre Duret-Lutz, Jan Strejček
- Where
- Proceedings of the 32nd International Conference on Computer-Aided Verification (CAV'20)
- Type
- inproceedings
- Publisher
- Springer
- Projects
- Spot
- Date
- 2020-05-14
Abstract
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. FurtherSeminator 2 has been extended with an improved NCSB complementation procedure for semi-deterministic automataproviding a new way to complement automata that is competitive with state-of-the-art complementation tools.
Documents
Bibtex (lrde.bib)
@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} }