Streett-Automat

In der Automatentheorie, einem Teilgebiet der Informatik, ist ein Streett-Automat eine spezielle Form des ω-Automaten.

Streett-Automaten zur Worterkennung

Ein (nicht-)deterministischer Streett-Automat ist ein 5-Tupel ${\mathcal {A}}=\left(Q,\Sigma ,\delta ,q_{0},{\mathcal {R}}\right)$ wobei gilt:

• $Q$ ist eine endliche Menge von Zuständen, die Zustandsmenge
• $\Sigma$ ist eine endliche Menge von Symbolen, das Eingabealphabet
• $\delta$ ist die Übergangsfunktion:
  • im deterministischen Fall mit $\delta \colon Q\times \Sigma \rightarrow Q$
  • im nicht-deterministischen Fall mit $\delta \colon Q\times \Sigma \rightarrow 2^{Q}$
• $q_{0}\in Q$ ist der Startzustand
• ${\mathcal {R}}\subseteq 2^{Q}\times 2^{Q}$ ist eine Familie von Paaren von Zustandsmengen

Dabei bezeichnet $2^{Q}$ die Potenzmenge von $Q$.

Akzeptanzverhalten

Ein unendliches Wort $w=a_{1}a_{2}\ldots$ wird vom Streett-Automaten ${\mathcal {A}}$ akzeptiert genau dann, wenn für einen (deterministisch: den) zugehörigen unendlichen Pfad $\pi =q_{0}\;{\xrightarrow {a_{1}}}\;q_{1}\;{\xrightarrow {a_{2}}}\;q_{2}\;\ldots$ gilt:

$\forall (E,F)\in {\mathcal {R}}:\operatorname {Inf} (\pi )\cap F\neq \emptyset \Rightarrow \operatorname {Inf} (\pi )\cap E\neq \emptyset$, d. h. falls ein Zustand aus $F$ unendlich oft besucht wird, dann wird auch mindestens ein Zustand aus dem zugehörigen $E$ unendlich oft besucht.

Alternativ findet sich die äquivalente Akzeptanzbedingung $\forall (E,F)\in {\mathcal {R}}:\operatorname {Inf} (\pi )\cap E\neq \emptyset \lor \operatorname {Inf} (\pi )\cap F=\emptyset$.

Diese Akzeptanzbedingung ist dual zur Akzeptanzbedingung des Rabin-Automaten.

Literatur

• Erich Grädel, Wolfgang Thomas, Thomas Wilke (Hrsg.): Automata, Logics, and Infinite Games. A Guide to Current Research (= Lecture Notes in Computer Science. Bd. 2500). Springer, Berlin u. a. 2002, ISBN 3-540-00388-6.