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).

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.