Streett-Automat

aus Wikipedia, der freien Enzyklopädie
Wechseln zu: Navigation, Suche

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

Streett-Automaten zur Worterkennung[Bearbeiten]

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: 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[Bearbeiten]

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}: \operatorname{Inf}(\pi) \cap F \neq \emptyset \Rightarrow \operatorname{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}: \operatorname{Inf}(\pi) \cap E \neq \emptyset \or \operatorname{Inf}(\pi) \cap F = \emptyset.

Diese Akzeptanzbedingung ist dual zur Akzeptanzbedingung des Rabin-Automaten.

Literatur[Bearbeiten]

  • 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