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
| pages = ?? to ??
+
| 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>,
pages = <nowiki>{</nowiki>??--??<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>,
note = <nowiki>{</nowiki>To appear<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

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