↑ arvau

Wikipedia / Omega language

In formal language theory within theoretical computer science, an ω-language is a set of infinite words, where an infinite word is an infinite-length sequence (specifically, an ω-length sequence) of symbols. Here, ω refers to the first infinite ordinal number, modeling a set of natural numbers.

Formal definition

Let Σ be a set of symbols (not necessarily finite). Following the standard definition from formal language theory, Σ* is the set of all finite words over Σ. Every finite word has a length, which is a natural number. Given a word w of length n, w can be viewed as a function from the set {0,1,...,n1} → Σ, with the value at i giving the symbol at position i to Σ. The set of all infinite words over Σ is denoted Σω. The set of all finite and infinite words over Σ is sometimes written Σ∞ or Σ≤ω.

Thus an ω-language L over Σ is a subset of Σω.

Operations

Some common operations defined on ω-languages are:

  1. Intersection and union : Given ω-languages L and M, both and are ω-languages.

  2. Left concatenation : Let L be an ω-language, and K be a language of finite words only. Then K can be concatenated on the left, and only on the left, to L to yield the new ω-language KL.

  3. is the infinite version of the Kleene star operator on finite-length languages. Given a formal language L, Lω is the ω-language of all infinite sequences of words from L.

  4. Prefixes : Let w be an ω-word. Then the formal language Pref(w) contains every finite prefix of w.

  5. Limit : Given a finite-length language L, an ω-word w is in the limit of L if and only if is an infinite set. In other words, for an arbitrarily large natural number n, it is always possible to choose some word in L, whose length is greater than n, and which is a prefix of w. The limit operation on L can be written Lδ.

Distance between ω-words

The set Σω can be made into a metric space by definition of the metric as:

where |x| is interpreted as "the length of x" (number of symbols in x), and inf is the infimum over sets of real numbers then there is no longest prefix x. Symmetry is clear. Transitivity follows from the fact that if w and v have a maximal shared prefix of length m and v and u have a maximal shared prefix of length n characters of w and u. Hence d is a metric.

Important subclasses

The most widely used subclass of the ω-languages is the set of ω-regular languages, which enjoy the useful property of being recognizable by Büchi automata. Thus the decision problem of ω-regular language membership is decidable using a Büchi automaton, and fairly straightforward to compute.

If the language Σ is the power set of a set (called the "atomic propositions") then the ω-language is a linear time property, which are studied in model checking.

Bibliography