ω-automaton

In automata theory, a branch of theoretical computer science, an ω-automaton (or stream automaton) is a variation of a finite automaton that runs on infinite, rather than finite, strings as input.

They all recognize precisely the regular ω-languages except for the deterministic Büchi automata, which is strictly weaker than all the others.

Formally, a deterministic ω-automaton is a tuple A = (Q,Σ,δ,Q0,Acc) that consists of the following components: An input for A is an infinite string over the alphabet Σ, i.e. it is an infinite sequence α = (a1,a2,a3,...).

The set of accepted input ω-words is called the recognized ω-language by the automaton, which is denoted as L(A).

The definition of Acc as a subset of Qω is purely formal and not suitable for practice because normally such sets are infinite.

This notion of certain states being visited infinitely often will be helpful in defining the following acceptance conditions.

The following ω-language L over the alphabet Σ = {0,1}, which can be recognized by a nondeterministic Büchi automaton: L consists of all ω-words in Σω in which 1 occurs only finitely many times.

Notice that above language cannot be recognized by a deterministic Büchi automaton, which is strictly less expressive than its non-deterministic counterpart.

An ω-language over Σ is said to be recognized by an ω-automaton A (with the same alphabet) if it is the set of all ω-words accepted by A.

The nondeterministic Büchi, parity, Rabin, Streett, and Muller automata, respectively, all recognize exactly the same class of ω-languages.

Using different proofs it can also be shown that the deterministic parity, Rabin, Streett, and Muller automata all recognize the regular ω-languages.

Because nondeterministic Muller, Rabin, Streett, parity, and Büchi automata are equally expressive, they can be translated to each other.

[3] ω-automata can be used to prove decidability of S1S, the monadic second-order (MSO) theory of natural numbers under successor.

Infinite-tree automata extend ω-automata to infinite trees and can be used to prove decidability of S2S, the MSO theory with two successors, and this can be extended to the MSO theory of graphs with bounded (given a fixed bound) treewidth.