Rabin automaton

From Wikipedia, the free encyclopedia

A Rabin 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 $α$ there exists an index $i$ such that some state from $F i$ is visited infinitely often, while all states from $E i$ are visited finitely often.