Mechanizing the Minimization of Deterministic Generalized Büchi Automata

Authors

Souheib Baarir, Alexandre Duret-Lutz

Where

Proceedings of the 34th IFIP International Conference on Formal Techniques for Distributed Objects, Components and Systems (FORTE'14)

Type

inproceedings

Publisher

Springer

Projects

Spot

Date

2014-03-21

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.

Documents

• Paper

Bibtex (lrde.bib)

@InProceedings{	  baarir.14.forte,
  author	= {Souheib Baarir and Alexandre Duret-Lutz},
  title		= {Mechanizing the Minimization of Deterministic Generalized
		  {B\"u}chi Automata},
  booktitle	= {Proceedings of the 34th IFIP International Conference on
		  Formal Techniques for Distributed Objects, Components and
		  Systems (FORTE'14)},
  year		= 2014,
  month		= jun,
  series	= {Lecture Notes in Computer Science},
  volume	= 8461,
  pages		= {266--283},
  publisher	= {Springer},
  doi		= {10.1007/978-3-662-43613-4_17},
  abstract	= {Deterministic B{\"u}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.}
}