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. Beide erkennen genau die regulären ω-Sprachen. Die Idee der Muller-Automaten ist, die unendlich oft besuchten Zustände genau festzulegen, was gegenüber Büchi-Automaten präzisere Aussagen zum Akzeptanzverhalten zulässt.

Muller-Automat zur Worterkennung

Ein deterministischer Muller-Automat hat die Form A = (Q,Σ,q₀,δ,F). Hierbei gilt:

• Q ist die Menge der Zustände
• $\delta: Q \times \Sigma \rightarrow Q$ ist die Transitionsfunktion
• $F \subseteq 2^Q$, d.h. $F = \lbrace F_1, \dots , F_k \rbrace$ für bestimmte Mengen $F_1, \dots , F_k \subseteq Q$

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. Unter booleschen Operatoren ist die Klasse der Muller-erkennbaren ω-Automaten abgeschlossen. Um zu einem Muller-Automaten einen (nichtdeterministischen) Büchi-Automaten zu konstruieren, lässt man den Büchi-Automaten raten, welche Menge F_i die richtige Menge ist, die unendlich oft durchlaufen werden muss, und von wann an die Durchläufe beginnen müssen.

Akzeptanzverhalten

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

A akzeptiert ein Wort α, wenn der Lauf von A auf α erfolgreich ist.

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

Es muss zur Akzeptanz also eine bestimmte Menge F_i aus der Akzeptanzkomponente F unendlich oft komplett durchlaufen werden.

Muller-Automat zur Baumerkennung

Ein Muller-Baumautomat hat das Format A = (Q,Σ,q₀,Δ,Acc), wobei $\Delta \subseteq Q \times \Sigma \times Q \times Q$.

Ein Muller-Baumautomat akzeptiert einen Baum t, wenn es einen Lauf ρ von A auf t gibt, so dass auf jedem Pfad von ρ unendlich oft ein Zustand aus F vorkommt.

Literatur

• Wolfgang Thomas: Automata on infinite objects. In: Van Leeuwen (Hrsg.): Handbook of Theoretical Computer Science. S. 133-164, Elsevier, 1990