Omega-regular language


The ω-regular languages are a class of ω-languages that generalize the definition of regular languages to infinite words. Büchi showed in 1962 that ω-regular languages are precisely the ones definable in a particular monadic second-order logic called S1S.

Formal definition

An ω-language L is ω-regular if it has the form
The elements of Aω are obtained by concatenating words from A infinitely many times.
Note that if A is regular, Aω is not necessarily ω-regular, since A could be, the set containing only the empty string, in which case Aω=A, which is not an ω-language and therefore not an ω-regular language.

Equivalence to Büchi automaton

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.
Conversely, for a given Büchi automaton A = , we construct an ω-regular language and then we will show that this language is recognized by A. For an ω-word w = a1a2... let w be the finite segment ai+1...aj-1aj of w.
For every q, q' ∈ Q, we define a regular language Lq,q' that is accepted by the finite automaton.