Rabin automaton

:"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 $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\; subseteq\; Q$. $mathcal\{A\}$ accepts the input word $alpha$ if for the run $ho\; in\; Q^omega$ of $mathcal\{A\}$ on $alpha$ 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 $~\; ho$ 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.

ee also

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

References

* [http://portal.acm.org/citation.cfm?id=114895 Automata on Infinite Objects, Handbook of Theoretical Computer Science (Vol. B), 1991.] A survey by Wolfgang Thomas.
* [http://www.tcs.tifr.res.in/~pandya/grad/aut06/lect4.pdf Automata on Infinite Words] Slides for a tutorial by Paritosh K. Pandya.