Omega-regular Language
Get Omega-regular Language essential facts below. View Videos or join the Omega-regular Language discussion. Add Omega-regular Language to your topic list for future reference or share this resource on social media.
Omega-regular Language

The ?-regular languages are a class of ω-languages that generalize the definition of regular languages 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, 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 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 = a1a2... let w(i,j) be the finite segment ai+1...aj-1aj of w. For every q, q' ? Q, we define a regular language 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 a 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).


  • W. Thomas, "Automata on infinite objects." In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, pages 133-192. Elsevier Science Publishers, Amsterdam, 1990.

  This article uses material from the Wikipedia page available here. It is released under the Creative Commons Attribution-Share-Alike License 3.0.



Music Scenes