Omega language


An ω-language is a set of infinite-length sequences of symbols.

Formal definition

Let Σ be a set of symbols. 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 → Σ, with the value at i giving the symbol at position i. The infinite words, or ω-words, can likewise be viewed as functions from to Σ. The set of all infinite words over Σ is denoted Σω. The set of all finite and infinite words over Σ is sometimes written Σ.
Thus, an ω-language L over Σ is a subset of Σω.

Operations

Some common operations defined on ω-languages are:
The set Σω can be made into a metric space by definition of the metric as:
where |x| is interpreted as "the length of x", and inf is the infimum over sets of real numbers. If then there is no longest prefix x and so. 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 then the first characters of w and u must be the same so. 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 then the ω-language is a linear time property, which are studied in model checking.