Omega-regular language

The ω-regular languages are a class of ω-languages which 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

A^ω where A is a nonempty 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 {ε}, 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 iff 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 = (Q,Σ,Δ,I,F), 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-1,a_j of w. For every q,q'∈ Q, we define a regular language L_q,q' that is accepted by the finite automaton (Q,Σ,Δ,{q},{q'}).

Lemma: We claim that Büchi automaton A recognizes language ⋃_q∈I,q'∈F L_q,q' (L_q',q' - {ε} )^ω.

Proof: Let's suppose word w ∈ L(A) and q₀,q₁,q₂,... is an accepting run of A on w. Therefore, q₀ is in I and there must be an state q' in F such that q' occurs infinitely often in the accepting run. Let's pick the increasing infinite sequence of indexes i₀,i₁,i₂... such that, for all k≥0, q_{i_k} is q'. Therefore, w(0,i₀)∈L_q₀,q' and, for all k≥0, w(i_k,i_k+1)∈L_q',q' . Therefore, w ∈ L_q₀,q' (L_q',q' )^ω.

Now, suppose w ∈ L_q,q' (L_q',q' - {ε} )^ω for some q∈I and q'∈F. Therefore, there is an infinite and strictly increasing sequence i₀,i₁,i₂... such that w(0,i₀) ∈ L_q,q' and, for all k≥0,w(i_k,i_k+1)∈L_q',q' . By definition of L_q,q', there is a finite run of A from q to q' on word w(0,i₀). For all k≥0, there is a finite run of A from q' to q' on word w(i_k,i_k+1). By this construction, there is a run of A, which starts from q and in which q' occurs infinitely often. Hence, w ∈ L(A).

Bibliography

W. Thomas, "Automata on infinite objects." In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, pages 133-192. Elsevier Science Publishers, Amsterdam, 1990.