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
• Σ ist eine endliche Menge von Symbolen, das Eingabealphabet
• δ ist die Übergangsfunktion:
  • im deterministischen Fall mit $\delta: Q \times \Sigma \rightarrow Q$
  • im nicht-deterministischen Fall mit $\delta: 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_1a_2 \ldots$ wird vom deterministischen Streett-Automaten $\mathcal{A}$ akzeptiert genau dann, wenn für den zugehörigen unendlichen Pfad $\pi = q_0 \; \begin{matrix} {}_{a_1} \\ \rightarrow \\ \,\end{matrix} \; q_1 \; \begin{matrix} {}_{a_2} \\ \rightarrow \\ \,\end{matrix} \; q_2 \; \ldots$ gilt:

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

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

Diese Akzeptanzbedingung ist dual zur Akzeptanzbedingung des Rabin-Automaten.

Literatur

• Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of LNCS, E Gradel, W Thomas, T Wilke - Notes in Comp. Sci. Springer, 2002