Minimising Deterministic Büchi Automata Precisely using SAT Solving
Rüdiger Ehlers
We show how deterministic Büchi automata can be fully minimised by reduction to the satisfiability (SAT) problem, yielding the first automated method for this task. Size reduction of such omega-automata is an important step in probabilistic model checking as well as synthesis of finite-state systems. Our experiments demonstrate that state-of-the-art SAT solvers are capable of solving the resulting satisfiability problem instances quickly, making the approach presented valuable in practice.
Thirteenth International Conference on Theory and Applications of Satisfiability Testing (SAT 2010).
Copyright by Springer Verlag. The original publication is available at www.springerlink.com.