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.

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

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

Für deterministische Automaten ist die Transitionsrelation eine Funktion ${\displaystyle \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 ${\displaystyle 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.

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

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

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

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

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

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

• 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.