The ω-regular languages are a class of
ω-languages that generalize the definition of
regular language
In theoretical computer science and formal language theory, a regular language (also called a rational language) is a formal language that can be defined by a regular expression, in the strict sense in theoretical computer science (as opposed to ...
s 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 formal language theory, the empty string, or empty word, is the unique string of length zero.
Formal theory
Formally, a string is a finite, ordered sequence of characters such as letters, digits or spaces. The empty string is the special cas ...
, 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
In computer science and automata theory, a deterministic Büchi automaton is a theoretical machine which either accepts or rejects infinite inputs. Such a machine has a set of states and a transition function, which determines which state the machi ...
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
In theoretical computer science and formal language theory, a regular language (also called a rational language) is a formal language that can be defined by a regular expression, in the strict sense in theoretical computer science (as opposed to ...
''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''
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 ''L
q,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''(''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 In mathematical logic, monadic second-order logic (MSO) is the fragment of second-order logic where the second-order quantification is limited to quantification over sets. It is particularly important in the logic of graphs, because of Courcelle's ...
called S1S.
Bibliography
* Wolfgang Thomas, "Automata on infinite objects." In
Jan van Leeuwen
Jan van Leeuwen (born December 17, 1946, in Waddinxveen) is a Dutch computer scientist and Emeritus professor of computer science at the Department of Information and Computing Sciences at Utrecht University. , editor, ''Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics'', pages 133-192. Elsevier Science Publishers, Amsterdam, 1990.
Formal languages