ω-regular Language

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''_''n''''B''_''n''^ω for some ''n'', where the ''A''_''i''s and ''B''_''i''s are regular languages and the ''B''_''i''s 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''-1''a''_''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
:Proof: Let's suppose word and ''q''₀,''q''₁,''q''₂,... is an accepting run of ''A'' on ''w''. Therefore, ''q''₀ is in and there must be a state in ''F'' such that 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, is . Therefore, and, for all Therefore,
:Conversely, suppose for some and Therefore, there is an infinite and strictly increasing sequence ''i''₀,''i''₁,''i''₂... such that and, for all By definition of ''L_q,q''', there is a finite run of from to on word ''w''(0,''i''₀). For all ''k''≥0, there is a finite run of from to on word ''w''(''i_k'',''i''_''k''+1). By this construction, there is a run of ''A'', which starts from and in which occurs infinitely often. Hence, {{math, 1=''w'' ∈ ''L''(''A'').

Equivalence to Monadic second-order logic

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

Bibliography

* 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.

Formal languages