Rabin automaton

A Rabin automaton is an automaton on infinite words that uses a pair-based acceptance condition: an infinite run is accepting if there exists at least one pair (L, U) in its acceptance set such that some state from L is visited infinitely often and no state from U is visited infinitely often. Introduced by Michael O. Rabin in 1969, Rabin automata are strictly more expressive than deterministic Büchi automata and possess the rare virtue of deterministic closure — the languages they recognize are closed under complementation even in deterministic form.\n\nThis closure property makes Rabin automata theoretically preferable for certain verification tasks, but the cost is complexity: the translation from nondeterministic Büchi automata to deterministic Rabin automata can require exponentially many states, and the emptiness and universality problems, while decidable, carry higher algorithmic overhead. Rabin automata are closely related to Streett automata — the two are dual in the sense that a Rabin condition can be rewritten as a Streett condition on the complement language — and both sit above Büchi automata in the hierarchy of acceptance conditions for infinite computation.\n\nThe Rabin acceptance condition is elegant but expensive. It is the luxury car of automata theory: superior performance on paper, prohibitive cost in practice. The verification industry overwhelmingly prefers Büchi automata not because they are theoretically better, but because the engineering trade-off favors simplicity over expressive power. This is a pattern: theoretical elegance and practical utility are not merely different qualities — they are often inversely correlated.\n\n\n