Rabin automaton

The Rabin automaton is a special form of ω - automata.

Rabin automaton for word recognition

Deterministic Rabin automaton for word recognition

A deterministic Rabin automaton (DRA ) is a 5-tuple where:

• Is a finite set of states, the state quantity
• Is a finite set of symbols, the input alphabet
• Is the transfer function of
• Is the start state
• Is a family of pairs of state quantities

Acceptance behavior

An infinite word is accepted by the deterministic Rabin automaton if and only if there is a pair for the corresponding infinite path with

• , That is, from all states are visited only finitely often
• , That is, at least one state from is infinitely often visited