Rabin machine

The Rabin automaton is a special form of the ω automaton . They are named after their inventor Michael O. Rabin , who used them in 1969 to generalize finite automata to infinite words for the first time.

Rabin machines for word recognition

Nondeterministic Rabin machine for word recognition

A nondeterministic Rabin automaton (NRA) is a 5-tuple where: ${\ displaystyle {\ mathcal {A}} = \ left (Q, \ Sigma, \ Delta, I, {\ mathcal {R}} \ right)}$

${\ displaystyle Q}$ is a finite set of states, the state set
${\ displaystyle \ Sigma}$ is a finite set of symbols, the input alphabet
${\ displaystyle \ Delta}$ is the transition relation with ${\ displaystyle \ Delta \ subseteq Q \ times \ Sigma \ times Q}$
${\ displaystyle I}$ is a finite set of states with , the starting state set ${\ displaystyle I \ subseteq Q}$
${\ displaystyle {\ mathcal {R}} \ subseteq 2 ^ {Q} \ times 2 ^ {Q}}$ is a family of pairs of state sets

Deterministic Rabin machine for word recognition

A deterministic Rabin automaton (DRA) is a 5-tuple where: ${\ displaystyle {\ mathcal {A}} = \ left (Q, \ Sigma, \ delta, q_ {0}, {\ mathcal {R}} \ right)}$

${\ displaystyle Q}$ is a finite set of states, the state set
${\ displaystyle \ Sigma}$ is a finite set of symbols, the input alphabet
${\ displaystyle \ delta}$ is the transition function with ${\ displaystyle \ delta \ colon Q \ times \ Sigma \ rightarrow Q}$
${\ displaystyle q_ {0}}$ is the start state with ${\ displaystyle q_ {0} \ in Q}$
${\ displaystyle {\ mathcal {R}} \ subseteq 2 ^ {Q} \ times 2 ^ {Q}}$ is a family of pairs of state sets

The power of is called the index of the automaton. ${\ displaystyle {\ mathcal {R}}}$

Acceptance behavior

An infinite word is accepted by the deterministic Rabin automaton if and only if there is a pair with for the corresponding infinite path ${\ displaystyle w = a_ {1} a_ {2} \ ldots}$ ${\ displaystyle {\ mathcal {A}}}$ ${\ displaystyle \ pi = q_ {0} \; {\ xrightarrow {a_ {1}}} \; q_ {1} \; {\ xrightarrow {a_ {2}}} \; q_ {2} \; \ ldots }$ ${\ displaystyle (L, U) \ in {\ mathcal {R}}}$

${\ displaystyle \ operatorname {Inf} (\ pi) \ cap L = \ emptyset}$ , d. H. all states from are only visited finitely often ${\ displaystyle L}$
${\ displaystyle \ operatorname {Inf} (\ pi) \ cap U \ neq \ emptyset}$ , d. H. at least one state from is visited infinitely often ${\ displaystyle U}$

Relationship to Büchi, Streett and Muller machines

The acceptance behavior of a nondeterministic Rabin machine (NRA) is more general than a nondeterministic Büchi machine (NBA), therefore:

For every NBA of size n there is an equivalent NRA with index 1 and the same size n.

By generalized Potzen automaton construction it can be shown that:

For every NBA there is a DRA with an identical language .

A Rabin condition can also be converted into a Büchi condition, the following applies:

For every NRA of size n and index k there is an equivalent NBA with at most states. ${\ displaystyle n \ cdot (k + 1)}$

The acceptance condition of the Rabin machine is dual to the acceptance condition of the Streett machine . Therefore, deterministic Rabin and Streett automata can easily be complemented with one another and the following applies:

For every DRA of size n and of index k there is a deterministic Streett machine of size n and of index k whose language is complementary to the language of : ${\ displaystyle {\ mathcal {A}}}$ ${\ displaystyle {\ overline {\ mathcal {A}}}}$ ${\ displaystyle {\ mathcal {A}}}$ ${\ displaystyle L ({\ overline {\ mathcal {A}}}) = \ Sigma ^ {\ omega} \ setminus L ({\ mathcal {A}})}$

The following also applies:

Each DRA is equivalent to a deterministic Muller machine (DMA) and vice versa.

Sources & web links

Martin Hofmann, Martin Lange: Automata Theory and Logic . In: eXamen.press . Springer-Verlag, 2011, ISBN 978-3-642-18089-7 .
Lecture notes on "Automata, Formal Languages and Computability", given by Prof. Dr. Markus Holzer, winter semester 2004/05 - chapter 2.5.3 (PDF file; 461 kB)

Individual evidence

↑ ^a ^b ^c ^d ^e ^f Martin Hofmann, Martin Lange: Automata theory and logic . In: eXamen.press . Springer-Verlag, 2011, ISBN 978-3-642-18089-7 .
↑ Michael O. Rabin: Decidability of second-order theories and automata on infinite trees . tape 141 , no. 5 . Trans. Amer. Math. Soc., 1969, p. 1-35 .
↑ Markus Holzer; Created by Benjamin Gufler: Automata, formal languages and predictability. Retrieved February 3, 2017 .

[:0-1] ↑ ^a ^b ^c ^d ^e ^f Martin Hofmann, Martin Lange: Automata theory and logic . In: eXamen.press . Springer-Verlag, 2011, ISBN 978-3-642-18089-7 .

[2] Michael O. Rabin: Decidability of second-order theories and automata on infinite trees . tape 141 , no. 5 . Trans. Amer. Math. Soc., 1969, p. 1-35 .

[3] Markus Holzer; Created by Benjamin Gufler: Automata, formal languages and predictability. Retrieved February 3, 2017 .