Stephan Barth, SAT-based minimization for nondeterministic Büchi automata
SAT-based minimization for nondeterministic Büchi automata
Büchi Automata are an automaton model for describing infinite languages. Despite its similarities to finite automata determinisation is not always possible in this model and no canonical minimization algorithm exists.
This work describes SAT-based minimization procedure for nondeterministic Büchi automata (NBA).
For a given NBA A the procedure finds an equivalent NBA A_min with the minimal number of states. This is done by successively computing automata A' that approximate A in the sense that they accept a given finite set of positive examples and reject a given finite set of negative examples. In the course of the procedure these example sets are successively increased. Thus, our method can be seen as an instance of a generic learning algorithm based on a "minimally adequate teacher" in the sense of Angluin.
We use a SAT solver to find NBA for given sets of positive and negative examples. We use Ramsey-based complementation to check candidates computed in this manner for equivalence with A. Failure of equivalence yields new positive or negative examples. Our method proved successful on a series of small examples that are nontrivial in the sense that they are difficult or impossible to minimize by hand. In particular, we succeed in minimizing all NBA with two states and two-letter alphabet as well as some instances of Michel's NBA which were introduced to establish an n! lower bound on complementation of NBA.