Omega-regular language

---

title: "Omega-regular language" type: doc version: 1 created: 2026-02-28 author: "Wikipedia contributors" status: active scope: public tags: ["formal-languages"] description: "Class of languages studied in formal language theory in computer science" topic_path: "linguistics" source: "https://en.wikipedia.org/wiki/Omega-regular_language" license: "CC BY-SA 4.0" wikipedia_page_id: 0 wikipedia_revision_id: 0

::summary Class of languages studied in formal language theory in computer science ::

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

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 A1B1ω ∪ ... ∪ AnB**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 , we construct an ω-regular language and then we will show that this language is recognized by A. For an ω-word w = a1a2... let w(i,j) be the finite segment a**i+1...a**j-1a**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 w ∈ L(A) and q0,q1,q2,... is an accepting run of A on w. Therefore, q0 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 i0,i1,i2... such that, for all k≥0, qik is q'. Therefore, and, for all Therefore, :Conversely, suppose for some and Therefore, there is an infinite and strictly increasing sequence i0,i1,i2... such that and, for all 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,i**k+1). By this construction, there is a run of A, which starts from q and in which q' occurs infinitely often. Hence, .

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.

::callout[type=info title="Wikipedia Source"] This article was imported from Wikipedia and is available under the Creative Commons Attribution-ShareAlike 4.0 License. Content has been adapted to SurfDoc format. Original contributors can be found on the article history page. ::