Streett automaton

From Wikipedia, the free encyclopedia

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 $Σ$ are defined as for Büchi automata. $\delta: Q \times \Sigma \rightarrow Q$ is the transition function, and $Ω$ is a set of pairs $(E_j,~F_j)$ with $E_j, F_j \subset Q$ . $\mathcal{A}$ accepts the input word $α$ if for the run $\rho \in Q^\omega$ of $\mathcal{A}$ on $α$ , for every index $i$ , $inf(\rho)\cap E_j\ne\empty\to inf(\rho)\cap F_j\ne\empty$ (where $i n f (ρ)$ is the group of states in $Q$ that the run $ρ$ 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 $~\rho$ 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 $\bar{L}$ can be recognized by some deterministic Rabin automaton, and vice versa.