omega-regular language

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.

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 {{math|1=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-1a_j of w.

For every {{math|1=q, {{var|q'}} ∈ Q}}, we define a regular language L_q,q' that is accepted by the finite automaton {{math|1=(Q, Σ, δ, q, {{mset|{{var|q'}}}})}}.

:Lemma: We claim that the Büchi automaton A recognizes the language {{math|1=⋃_q∈I,q'∈F L_q,q' (L_q',q' − {{mset|ε}} )^ω.}}

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

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

Büchi showed in 1962 that ω-regular languages are precisely the ones definable in a particular monadic second-order logic called S1S.

• Wolfgang 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.

Category:Formal languages