Ω-Automat

Ein ω-Automat (Omega-Automat) ist ein mathematisches Modell, das eine Erweiterung des endlichen Automaten auf die Eingabe unendlicher Wörter darstellt. Endlich heißt der Automat deshalb, weil die Anzahl seiner inneren Zustände endlich ist. Ebenso ist das Alphabet, über dem dieser Automat arbeitet, endlich.

Der griechische Buchstabe ω (omega) steht hier für die kleinste unendliche Ordinalzahl.

Motiviert wird die Betrachtung solcher Automaten durch viele Systeme (zum Beispiel Betriebssysteme), die per definitionem eigentlich nicht terminieren sollen, sondern unendlich lange betrieben werden.

Ausgehend von einem besonderen Zustand (Startzustand) liest der ω-Automat eine abzählbar unendliche Folge von Symbolen (Eingabewort), die Elemente einer endlichen Menge von Symbolen (Eingabealphabet) sind.

Dabei geht der ω-Automat schrittweise vor, wobei in jedem Schritt das jeweils nächste Symbol des Eingabewortes gelesen wird. Den Folgezustand bestimmt die Zustandsübergangsfunktion ${\displaystyle \delta }$ in Abhängigkeit vom aktuell gelesenen Zeichen und dem momentanen Zustand.

Die Frage, ob das Eingabewort akzeptiert wird, ist von der Art des ω-Automaten abhängig. In jedem Fall wird die Menge der Zustände zu Rate gezogen, die unendlich oft durchlaufen werden.

Ein ω-Automat lässt sich sowohl als Zustandsdiagramm als auch als Zustandstabelle darstellen:

		a b s0 s0 s1 s1 s0 s2 s2 s1 s2
Zustandsdiagramm		Zustandstabelle

Das Diagramm liest sich wie folgt:

• Einfache Kreise stellen Zustände dar.
• Im Kreis steht der Name des Zustands bzw. der Zustand.
• Pfeile stellen Transitionen (Zustandsübergänge) dar. An den Pfeilen steht, welches Zeichen (oder gar welche Wörter) der Automat bei der Transition liest.
• Der Anfangszustand ist dadurch gekennzeichnet, dass er Endpunkt eines Pfeils ist, der keinen Zustand als Ausgangspunkt hat.
• Endzustände sind durch doppelte Kreise gekennzeichnet (aber nicht bei allen Typen des ω-Automaten gibt es Endzustände; die Akzeptanzmechanismen sind unterschiedlich).

Wie bei den endlichen Automaten unterscheidet man auch bei den ω-Automaten zwischen deterministischen und nichtdeterministischen Automaten.

Weiterhin unterscheidet man die Automaten nach der Art, wie entschieden wird, ob ein eingegebenes Wort akzeptiert wird oder nicht. Diese Akzeptanz eines Wortes entscheidet sich in den meisten Fällen nach den unendlich oft angenommenen Zuständen. Beispiele für ω-Automaten sind der Büchi-Automat, der Muller-Automat, der Rabin-Automat, der Streett-Automat und der Parity-Automat.

Außer dem deterministischen Büchi-Automaten erkennen alle genannten Automaten die Klasse der ω-regulären Ausdrücke (die Erweiterung der regulären Ausdrücke auf unendliche Zeichenfolgen). Der deterministische Büchi-Automat erkennt nur eine Teilmenge dieser Ausdrücke und stellt eine echt schwächere Automatenklasse dar.

Ein ω-Automat ist ein 5-Tupel:

${\displaystyle M=(\Sigma ,Z,Z_{0},\delta ,Z_{E})}$

Dabei sind die Elemente wie folgt definiert:

• ${\displaystyle \Sigma }$ ist eine endliche Menge, das Eingabealphabet, aus dessen Elementen die eingegebenen Wörter zusammengesetzt sind.
• ${\displaystyle Z}$ ist die zu ${\displaystyle \Sigma }$ disjunkte endliche Menge der Zustände des Automaten.
• ${\displaystyle Z_{0}\in Z}$ ist der Startzustand.
• ${\displaystyle \delta :\Sigma \times Z\rightarrow Z}$ ist die Überführungsfunktion, sie ist gewöhnlich total, d. h. jedes Element der Urbildmenge ${\displaystyle \Sigma \times Z}$ hat ein Bild.
• ${\displaystyle Z_{E}}$ ist eine vom Automatentyp abhängige Komponente, die regelt, wann ein Wort akzeptiert wird, bei Büchi-Automaten zum Beispiel ist dies eine Teilmenge von ${\displaystyle Z}$.

Bei nichtdeterministischen Automaten wird die (nicht zwingend totale) Überführungsrelation als ${\displaystyle \Delta :\Sigma \times Z\rightarrow P(Z)}$ definiert, wobei ${\displaystyle P(Z)}$ die Potenzmenge von ${\displaystyle Z}$ ist. Der Automat kann dann bei der Eingabe eines neuen Zeichens nichtdeterministisch in einen von mehreren Zuständen gehen, die durch das Bild (Menge von Zuständen) der Funktion gegeben werden.

• Modellprüfung