Streett-Automat
# 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.

