Omega-regular language
Encyclopedia
The ω-regular languages are a class of ω-languages
which generalize the definition of regular language
s 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.
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.
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=a1,a2,... , let w(i,j) be the finite segment ai+1,...,aj-1,aj of w.
For every q,q'∈ Q, we define a regular language
Lq,q' that is accepted by the finite automaton (Q,Σ,Δ,{q},{q'}).
Omega language
An ω-language is a set of infinite-length sequences of symbols.-Formal definition:Let Σ be a set of symbols . Following the standard definition from formal language theory, Σ* is the set of all finite words over Σ. Every finite word has a length, which is, obviously, a natural number...
which generalize the definition of regular language
Regular language
In theoretical computer science and formal language theory, a regular language is a formal language that can be expressed using regular expression....
s 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
Empty string
In computer science and formal language theory, the empty string is the unique string of length zero. It is denoted with λ or sometimes Λ or ε....
, 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 automatonBüchi automaton
In computer science and automata theory, a Büchi automaton is a type of ω-automaton, which extends a finite automaton to infinite inputs. It accepts an infinite input sequence iff there exists a run of the automaton that visits one of the final states infinitely often. Büchi automata recognize the...
iff it is an ω-regular language.
Proof: Every ω-regular language is recognized by a nondeterministic Büchi automaton
Büchi automaton
In computer science and automata theory, a Büchi automaton is a type of ω-automaton, which extends a finite automaton to infinite inputs. It accepts an infinite input sequence iff there exists a run of the automaton that visits one of the final states infinitely often. Büchi automata recognize the...
; 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=a1,a2,... , let w(i,j) be the finite segment ai+1,...,aj-1,aj of w.
For every q,q'∈ Q, we define a regular language
Regular language
In theoretical computer science and formal language theory, a regular language is a formal language that can be expressed using regular expression....
Lq,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 Lq,q' (Lq',q' - {ε} )ω.
- Proof: Let's suppose word w ∈ L(A) and q0,q1,q2,... is an accepting run of A on w. Therefore, q0 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 i0,i1,i2... such that, for all k≥0, qik is q'. Therefore, w(0,i0)∈Lq0,q' and, for all k≥0, w(ik,ik+1)∈Lq',q' . Therefore, w ∈ Lq0,q' (Lq',q' )ω.
- Now, suppose w ∈ Lq,q' (Lq',q' - {ε} )ω for some q∈I and q'∈F. Therefore, there is an infinite and strictly increasing sequence i0,i1,i2... such that w(0,i0) ∈ Lq,q' and, for all k≥0,w(ik,ik+1)∈Lq',q' . By definition of Lq,q', there is a finite run of A from q to q' on word w(0,i0). For all k≥0, there is a finite run of A from q' to q' on word w(ik,ik+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).