In formal language theory within theoretical computer science, an infinite word is an infinite-length sequence (specifically, an ω-length sequence) of symbols, and an ω-language is a set of infinite words.
Let Σ be a set of symbols (not necessarily finite).
Given a word w of length n, w can be viewed as a function from the set {0,1,...,n−1} → Σ, with the value at i giving the symbol at position i.
The infinite words, or ω-words, can likewise be viewed as functions from
The set of all infinite words over Σ is denoted Σω.
The set of all finite and infinite words over Σ is sometimes written Σ∞ or Σ≤ω.
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.