An ω-language L is ω-regular if it has the form The elements of Aω are obtained by concatenating words from A infinitely many times.
Theorem: An ω-language is recognized by a Büchi automaton if and only if it is an ω-regular language.
Proof: Every ω-regular language is recognized by a nondeterministic Büchi automaton; the translation is constructive.
Using the closure properties of Büchi automata and structural induction over the definition of ω-regular language, it can be easily shown that a Büchi automaton can be constructed for any given ω-regular language.
Büchi showed in 1962 that ω-regular languages are precisely the ones definable in a particular monadic second-order logic called S1S.