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 $𝒜=(Q,\mathrm{\Sigma },\delta ,q_0,ℛ)$ wobei gilt:

• $Q$ ist eine endliche Menge von Zuständen, die Zustandsmenge
• $\mathrm{\Sigma }$ ist eine endliche Menge von Symbolen, das Eingabealphabet
• $\delta$ ist die Übergangsfunktion:
  • im deterministischen Fall mit $\delta :Q\times \mathrm{\Sigma }\to Q$
  • im nicht-deterministischen Fall mit $\delta :Q\times \mathrm{\Sigma }\to 2^Q$
• $q_0\in Q$ ist der Startzustand
• $ℛ\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\dots$ wird vom Streett-Automaten $𝒜$ akzeptiert genau dann, wenn für einen (deterministisch: den) zugehörigen unendlichen Pfad $\pi =q_0\stackrel{a_1}{\to }{q}_1\stackrel{a_2}{\to }{q}_2\dots$ gilt:

$\mathrm{\forall }(E,F)\in ℛ:\mathrm{Inf}(\pi )\cap F\ne \mathrm{\varnothing }\Rightarrow \mathrm{Inf}(\pi )\cap E\ne \mathrm{\varnothing }$, 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 $\mathrm{\forall }(E,F)\in ℛ:\mathrm{Inf}(\pi )\cap E\ne \mathrm{\varnothing }\vee \mathrm{Inf}(\pi )\cap F=\mathrm{\varnothing }$.

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.