Omega-regular language

In computer science and formal language theory, the ω-regular languages are a class of ω-languages that generalize the definition of regular languages to infinite words. As regular languages accept finite strings (such as strings beginning in an a, or strings alternating between a and b), ω-regular languages accept infinite words (such as, infinite sequences beginning in an a, or infinite sequences alternating between a and b).

Formal definition

Let A be a language. Denote by A^ω the set whose elements are obtained by concatenating words from A infinitely many times, i.e the set of functions $\omega \to A$ .

The class of ω-regular ω-languages is defined inductively as follows

A^ω, where A is a regular language not containing the empty string, is ω-regular;
AB, the concatenation of a regular language A and an ω-regular language B (Note that BA is not well-defined), is ω-regular;
A ∪ B, where A and B are ω-regular languages (this rule can only be applied finitely many times), is ω-regular.

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.

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 $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 $q, q' \in Q$ , we define a regular language L_q,q' that is accepted by the finite automaton $(Q, Σ, δ, q, {q'})$ .

Lemma— We claim that the Büchi automaton A recognizes the language $⋃ q \in I, q' \in F L q,q' (L q',q' - {ε} ) ω .$

Proof

Let's suppose word $w \in L (A)$ and q₀,q₁,q₂,... is an accepting run of A on w. Therefore, q₀ is in $I$ and there must be a state $q'$ in F such that $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, $q i k$ is $q'$ . Therefore, $w (0, i 0)\in L q 0, q'$ and, for all $k \geq0, w (i k, i k +1)\in L q',q' .$ Therefore, $w \in L q 0,q' (L q',q') ω .$

Conversely, suppose

w \in L q,q' (L q',q' - {ε} ) ω

for some

q \in I

and

q'\in F .

Therefore, there is an infinite and strictly increasing sequence i₀,i₁,i₂... such that

w (0, i 0) \in L q,q'

and, for all

k \geq0, w (i k, i k +1)\in L q',q' .

By definition of L_q,q', there is a finite run of

A

from

q

to

q'

on word w(0,i₀). For all k≥0, there is a finite run of

A

from

q'

to

q'

on word w(i_k,i_k+1). By this construction, there is a run of A, which starts from

q

and in which

q'

occurs infinitely often. Hence,

w \in 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.

This page was redesigned at the edge.

Omega-regular language

Formal definition

Equivalence to Büchi automaton

Equivalence to Monadic second-order logic

Further reading