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''1''B''1ω ∪ ... ∪ ''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''1''a''2... 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 ''Lq,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''0,''q''1,''q''2,... is an accepting run of ''A'' on ''w''. Therefore, ''q''0 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''0,''i''1,''i''2... 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''0,''i''1,''i''2... such that and, for all By definition of ''Lq,q''', there is a finite run of from to on word ''w''(0,''i''0). For all ''k''≥0, there is a finite run of from to on word ''w''(''ik'',''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