Muller-Automat

Den Muller-Automat bezeichnet in der Automatentheorie ein 1963 von David E. Muller vorgestelltes Konzept eines ω-Automaten. Dieser Typ – deterministisch wie nichtdeterministisch – hat die gleiche Ausdrucksstärke wie nichtdeterministische Büchi-Automaten. Im Gegensatz dazu wird die Menge der unendlich oft besuchten Zustände genau festgelegt, was präzisere Aussagen zum Akzeptanzverhalten zulässt.

Muller-Automat zur Worterkennung

Ein nicht-deterministischer Muller-Automat hat die Form $A=(Q,\Sigma ,q_{0},\Delta ,{\mathcal {F}})$ . Hierbei gilt:

$Q$ ist die Menge der Zustände, $q_{0}\in Q$ ist der Startzustand
$\Delta \subseteq Q\times \Sigma \times Q$ ist die Transitionsrelation
${\mathcal {F}}\subseteq 2^{Q}$ ist die Tafel, d. h. ${\mathcal {F}}=\lbrace F_{1},\dots ,F_{k}\rbrace$ für bestimmte Mengen $F_{1},\dots ,F_{k}\subseteq Q$

Für deterministische Automaten ist die Transitionsrelation eine Funktion $\delta \colon Q\times \Sigma \to Q$ , hat also eindeutige Bilder und der Automat damit eindeutige Läufe.

Die Muller-akzeptierbaren ω-Sprachen sind die booleschen Kombinationen der deterministisch-Büchi-erkennbaren ω-Sprachen. Jeder deterministische Büchi-Automat kann als Muller-Automat ausgedrückt werden. Die Klasse der Muller-erkennbaren ω-Sprachen ist also unter booleschen Operationen abgeschlossen. Um zu einem Muller-Automaten einen (nichtdeterministischen) Büchi-Automaten zu konstruieren, lässt man den Büchi-Automaten raten, welches $F_{i}\in {\mathcal {F}}$ die richtige Menge ist, die unendlich oft durchlaufen werden muss, und von wann an die Durchläufe beginnen müssen.

Akzeptanzverhalten

Ein Lauf $\rho$ ist erfolgreich, wenn $\operatorname {Inf} (\rho )\in F$ , wobei $\operatorname {Inf} (\rho )=\lbrace q\in Q\mid q{\text{ erscheint unendlich oft in }}\rho \rbrace$ . Dies nennt man die Muller-Akzeptierung.

$A$ akzeptiert ein Wort $\alpha$ , wenn ein Lauf von $A$ auf $\alpha$ erfolgreich ist.

Die Muller-Bedingung lautet: $\operatorname {Inf} (\rho )=F_{i}$ für ein $i=1,\dots ,k$

Es muss zur Akzeptierung also eine bestimmte Menge $F_{i}$ aus der Tafel ${\mathcal {F}}$ unendlich oft komplett durchlaufen werden.

Muller-Automat zur Baumerkennung

Ein Muller-Baumautomat hat das Format $A=(Q,\Sigma ,q_{0},\Delta ,{\mathcal {F}})$ , wobei $\Delta \subseteq Q\times \Sigma \times Q\times Q$ und ${\mathcal {F}}$ eine Menge von Teilmengen von $Q$ ist.

Ein Muller-Baumautomat akzeptiert einen Baum $t$ , wenn es einen Lauf $\rho$ von $A$ auf $t$ gibt, so dass auf jedem Pfad von $\rho$ die Menge $M$ der unendlich oft vorkommenden Zustände ein Element von $F$ ist.

Literatur

Wolfgang Thomas: Automata on Infinite Objects. In: Jan van Leeuwen (Hrsg.): Handbook of Theoretical Computer Science. Band B: Formal Models and Semantics. Elsevier Science Publishers u. a., Amsterdam u. a. 1990, ISBN 0-444-88074-7, S. 133–164.