View source for Publications/baarir.14.forte

{{Publication
| published = true
| date = 2014-03-21
| authors = Souheib Baarir, Alexandre Duret-Lutz
| title = Mechanizing the Minimization of Deterministic Generalized Büchi Automata
| booktitle = Proceedings of the 34th IFIP International Conference on Formal Techniques for Distributed Objects, Components and Systems (FORTE'14)
| series = Lecture Notes in Computer Science
| volume = 8461
| pages = 266 to 283
| publisher = Springer
| lrdeprojects = Spot
| lrdenewsdate = 2014-03-21
| lrdepaper = http://www.lrde.epita.fr/dload/papers/baarir.14.forte.pdf
| abstract = Deterministic Büchi automata (DBA) are useful to (probabilistic) model checking and synthesis. We survey techniques used to obtain and minimize DBAs for different classes of properties. We extend these techniques to support DBA that have generalized and transition-based acceptance (DTGBA) as they can be even smaller. Our minimization technique—a reduction to a SAT problem—synthesizes a DTGBA equivalent to the input DTGBA for any given number of states and number of acceptance sets (assuming such automaton exists). We present benchmarks using a framework that implements all these techniques.
| type = inproceedings
| id = baarir.14.forte
| bibtex = 
@InProceedings<nowiki>{</nowiki>	  baarir.14.forte,
  author	= <nowiki>{</nowiki>Souheib Baarir and Alexandre Duret-Lutz<nowiki>}</nowiki>,
  title		= <nowiki>{</nowiki>Mechanizing the Minimization of Deterministic Generalized
		  <nowiki>{</nowiki>B\"u<nowiki>}</nowiki>chi Automata<nowiki>}</nowiki>,
  booktitle	= <nowiki>{</nowiki>Proceedings of the 34th IFIP International Conference on
		  Formal Techniques for Distributed Objects, Components and
		  Systems (FORTE'14)<nowiki>}</nowiki>,
  year		= 2014,
  month		= jun,
  series	= <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>,
  volume	= 8461,
  pages		= <nowiki>{</nowiki>266--283<nowiki>}</nowiki>,
  publisher	= <nowiki>{</nowiki>Springer<nowiki>}</nowiki>,
  abstract	= <nowiki>{</nowiki>Deterministic B<nowiki>{</nowiki>\"u<nowiki>}</nowiki>chi automata (DBA) are useful to
		  (probabilistic) model checking and synthesis. We survey
		  techniques used to obtain and minimize DBAs for different
		  classes of properties. We extend these techniques to
		  support DBA that have generalized and transition-based
		  acceptance (DTGBA) as they can be even smaller. Our
		  minimization technique---a reduction to a SAT
		  problem---synthesizes a DTGBA equivalent to the input DTGBA
		  for any given number of states and number of acceptance
		  sets (assuming such automaton exists). We present
		  benchmarks using a framework that implements all these
		  techniques.<nowiki>}</nowiki>
<nowiki>}</nowiki>

}}