Streett automaton

A Streett automaton is one of the many types of finite automata on infinite strings. It is of the form $mathcal\{A\}\; =\; (Q,~Sigma,~q\_0,~delta,~Omega)$ where $Q,~q\_0$ and $Sigma$ are defined as for Büchi automata. $delta:\; Q\; imes\; Sigma\; ightarrow\; Q$ is the transition function, and $Omega$ is a set of pairs $(E\_j,~F\_j)$ with $E\_j,\; F\_j\; subset\; Q$. $mathcal\{A\}$ accepts the input word $alpha$ if for the run $ho\; in\; Q^omega$ of $mathcal\{A\}$ on $alpha$, for every index $i$, $inf(\; ho)cap\; E\_j\; eempty\; o\; inf(\; ho)cap\; F\_j\; eempty$ (where $inf(\; ho)$ is the group of states in $Q$ that the run $ho$ visits infinitely often).

Less formally, a Streett acceptance condition defines a set of ordered pairs $(E,~F)$ of finite sets of states taken from the automaton's graph. A pair is satisfied by any run $~\; ho$ that either does not contain infinitely many $E$ states, or contains infinitely many $E$ states and infinitely many $F$ states. The Streett acceptance condition is met if all pairs are satisfied. The automaton may be nondeterministic, so an input word (which is infinite) may produce innumerable runs; the word is accepted if at least one run is accepted.

The acceptance condition is dual to the Rabin acceptance condition: The Streett condition is the logical negation of the Rabin condition, and therefore, if a language $L$ can be recognized by a deterministic Streett automaton, then its complement can be recognized by some deterministic Rabin automaton, and vice versa.

ee also

Rabin automaton - A closely related automaton with the same components but a different acceptance condition.