Ω-Automat

Ein ω-Automat ist ein mathematisches Modell, der 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 (z.B. Betriebssysteme), die per Definition eigentlich nicht terminieren sollen, sondern unendlich lange betrieben werden.

Beschreibung

Ausgehend von einem besonderen Zustand (Startzustand) liest der ω-Automat eine unendlich abzählbare 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 $\delta$ in Abhängigkeit des aktuell gelesenen Zeichens 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.

Darstellung

Ein ω-Automat läßt 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 dar. Auf 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.

Typen

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.

Formale Definition

Ein ω-Automat ist ein 5-Tupel:

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

Dabei sind die Elemente wie folgt definiert.

$\Sigma$ - Ist eine endliche Menge.

$Z$ - Ist eine zu $\Sigma$ disjunkte endliche Menge.

$Z_{0}$ - Ist eine Element von $Z\qquad \qquad Z_{0}\in Z$

$\delta$ - Eine Funktion $\Sigma \times Z\rightarrow Z$ (total)

$Z_{E}$ - Ist eine vom Automatentyp abhängige Komponente

Die Semantik der einzelnen Elemente ist die folgende:

$\Sigma$ - Ist das Eingabealphabet

$Z$ - Ist die Zustandsmenge

$Z_{0}$ - Ist der Startzustand

$\delta$ - Ist die Überführungsfunktion, sie ist gewöhnlich total, d.h. jedes Element der Ausgangsmenge $\Sigma$ hat ein Bild. Bei nichtdeterministischen Automaten wird an Stelle von $Z$ die Potenzmenge P(Z) benutzt, da der Automat dann sich in verschiedenen Zuständen gleichzeitig aufhalten kann und sich auch bei der Eingabe eines neuen Zeichens eben nichtdeterministisch in verschiedene Zustände bewegen kann.

$Z_{E}$ - Diese Komponente regelt, wann ein Wort akzeptiert wird, bei Büchi-Automaten z.B. ist dies eine Teilmenge von $Z$.

Siehe auch

• Endlicher Automat
• Model Checking
• Automatenanalyse
• Abdeckungsanalyse