Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / WS 2011/12 / Oberseminar / Stephan Barth, SAT-based minimization for nondeterministic Büchi automata


Inhaltsbereich

Stephan Barth, SAT-based minimization for nondeterministic Büchi automata

TCS Oberseminar, 9.12.2011 14:15 Stephan Barth
Wann 14:15 15:15 09.12.2011
von bis
Wo L109
Termin übernehmen vCal
iCal

Stephan Barth
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.

Artikelaktionen

abgelegt unter:

Funktionsleiste