# Omega-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$_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 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$_1$a$_2$... let w(i,j) be the finite segment a$_{i+1}$...a$_{j-1}$a$_j$ of w. For every q, q' ∈ 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∈I,q'∈F}$ L$_{q,q'}$ (L$_{q',q'}$ − {ε} )$^ω$.
    Proof: Let's suppose word w ∈ L(A) and q$_0$,q$_1$,q$_2$,... is an accepting run of A on w. Therefore, q$_0$ 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$_0$,i$_1$,i$_2$... such that, for all k≥0, q$_{ik}$ is q'. Therefore, w(0,i$_0$)∈L$_{q0,q'}$ and, for all k≥0, w(i$_k$,i$_{k+1}$)∈L$_{q',q'}$ . Therefore, w ∈ L$_{q0,q'}$ (L$_{q',q'}$ )$^ω$.
    Conversely, suppose w ∈ L$_{q,q'}$ (L$_{q',q'}$ − {ε} )$^ω$ for some q∈I and q'∈F. Therefore, there is an infinite and strictly increasing sequence i$_0$,i$_1$,i$_2$... such that w(0,i$_0$) ∈ L$_{q,q'}$ and, for all k≥0, w(i$_k$,i$_{k+1}$)∈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$_0$). 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 ∈ 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.