Rabin automaton

From Wikipedia, the free encyclopedia

Aside from the definition given below, a Rabin automaton may also refer to a type of probabilistic automaton.

In mathematics, 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 \subseteq 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.

Less formally, a Rabin 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 contains infinitely many $F$ states, but does not contain infinitely many $E$ states; and the Rabin acceptance condition is met if any pair is 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.