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 <math>\mathcal{A} = \left(Q,\Sigma,\delta,q_0,\mathcal{R}\right)</math> wobei gilt:
- <math>Q</math> ist eine endliche Menge von Zuständen, die Zustandsmenge
- <math>\Sigma</math> ist eine endliche Menge von Symbolen, das Eingabealphabet
- <math>\delta</math> ist die Übergangsfunktion:
- im deterministischen Fall mit <math>\delta\colon Q \times \Sigma \rightarrow Q</math>
- im nicht-deterministischen Fall mit <math>\delta\colon Q \times \Sigma \rightarrow 2^Q</math>
- <math>q_0 \in Q</math> ist der Startzustand
- <math>\mathcal{R} \subseteq 2^Q \times 2^Q</math> ist eine Familie von Paaren von Zustandsmengen
Dabei bezeichnet <math>2^Q</math> die Potenzmenge von <math>Q</math>.
Akzeptanzverhalten
Ein unendliches Wort <math>w=a_1a_2 \ldots</math> wird vom Streett-Automaten <math>\mathcal{A}</math> akzeptiert genau dann, wenn für einen (deterministisch: den) zugehörigen unendlichen Pfad <math>\pi = q_0 \; \xrightarrow{a_1} \; q_1 \; \xrightarrow{a_2} \; q_2 \; \ldots</math> gilt:
<math>\forall (E, F) \in \mathcal{R}: \operatorname{Inf}(\pi) \cap F \neq \emptyset \Rightarrow \operatorname{Inf}(\pi) \cap E \neq \emptyset</math>, d. h. falls ein Zustand aus <math>F</math> unendlich oft besucht wird, dann wird auch mindestens ein Zustand aus dem zugehörigen <math>E</math> unendlich oft besucht.
Alternativ findet sich die äquivalente Akzeptanzbedingung <math>\forall (E, F) \in \mathcal{R}: \operatorname{Inf}(\pi) \cap E \neq \emptyset \lor \operatorname{Inf}(\pi) \cap F = \emptyset</math>.
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.