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 <math>A=(Q, \Sigma, q_0, \Delta, \mathcal F)</math>. Hierbei gilt:

• <math>Q</math> ist die Menge der Zustände, <math>q_0 \in Q</math> ist der Startzustand
• <math>\Delta \subseteq Q \times \Sigma \times Q</math> ist die Transitionsrelation
• <math>\mathcal F \subseteq 2^Q</math> ist die Tafel, d. h. <math>\mathcal F = \lbrace F_1, \dots , F_k \rbrace </math> für bestimmte Mengen <math>F_1, \dots , F_k \subseteq Q</math>

Für deterministische Automaten ist die Transitionsrelation eine Funktion <math>\delta\colon Q \times \Sigma \to Q</math>, 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 <math>F_i \in \mathcal F</math> die richtige Menge ist, die unendlich oft durchlaufen werden muss, und von wann an die Durchläufe beginnen müssen.

Akzeptanzverhalten

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

<math>A</math> akzeptiert ein Wort <math>\alpha</math>, wenn ein Lauf von <math>A</math> auf <math>\alpha</math> erfolgreich ist.

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

Es muss zur Akzeptierung also eine bestimmte Menge <math>F_i</math> aus der Tafel <math>\mathcal F</math> unendlich oft komplett durchlaufen werden.

Muller-Automat zur Baumerkennung

Ein Muller-Baumautomat hat das Format <math>A = (Q, \Sigma, q_0, \Delta, \mathcal F)</math>, wobei <math>\Delta \subseteq Q \times \Sigma \times Q \times Q</math> und <math>\mathcal F</math> eine Menge von Teilmengen von <math>Q</math> ist.

Ein Muller-Baumautomat akzeptiert einen Baum <math>t</math>, wenn es einen Lauf <math>\rho</math> von <math>A</math> auf <math>t</math> gibt, so dass auf jedem Pfad von <math>\rho</math> die Menge <math>M</math> der unendlich oft vorkommenden Zustände ein Element von <math>F</math> 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.