Omega-regular language explained

The ω-regular languages are a class of ω-languages that generalize the definition of regular languages to infinite words.

Formal definition

An ω-language L is ω-regular if it has the form

• A^ω where A is a regular language not containing the empty string
• AB, the concatenation of a regular language A and an ω-regular language B (Note that BA is not well-defined)
• A ∪ B where A and B are ω-regular languages (this rule can only be applied finitely many times)

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 for example, the set containing only the empty string, in which case A^ω=A, which is not an ω-language and therefore not an ω-regular language.

It is a straightforward consequence of the definition that the ω-regular languages are precisely the ω-languages of the form A₁B₁^ω ∪ ... ∪ A_nB_n^ω for some n, where the A_is and B_is are regular languages and the B_is do not contain the empty string.

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, we construct an ω-regular language and then we will show that this language is recognized by A. For an ω-word w = a₁a₂... let w(i,j) be the finite segment a_i+1...a_j-1a_j of w.For every, we define a regular language L_q,q' that is accepted by the finite automaton .

Lemma: We claim that the Büchi automaton A recognizes the language