ω-automaton

In automata theory, a branch of theoretical computer science, an ω-automaton (or stream automaton) is a variation of finite automatons that runs on infinite, rather than finite, strings as input. Since ω-automata do not stop, they have a variety of acceptance conditions rather than simply a set of accepting states. In automata theory, a branch of theoretical computer science, an ω-automaton (or stream automaton) is a variation of finite automatons that runs on infinite, rather than finite, strings as input. Since ω-automata do not stop, they have a variety of acceptance conditions rather than simply a set of accepting states. ω-automata are useful for specifying behavior of systems that are not expected to terminate, such as hardware, operating systems and control systems. For such systems, one may want to specify a property such as 'for every request, an acknowledge eventually follows', or its negation 'there is a request that is not followed by an acknowledge'. The former is a property of infinite words: one cannot say of a finite sequence that it satisfies this property. Classes of ω-automata include the Büchi automata, Rabin automata, Streett automata, parity automata and Muller automata, each deterministic or non-deterministic. These classes of ω-automata differ only in terms of acceptance condition. They all recognize precisely the regular ω-languages except for the deterministic Büchi automata, which is strictly weaker than all the others. Although all these types of automata recognize the same set of ω-languages, they nonetheless differ in succinctness of representation for a given ω-language. 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 run of A on such an input is an infinite sequence ρ = (r0,r1,r2,...) of states, defined as follows: The main purpose of an ω-automaton is to define a subset of the set of all inputs: The set of accepted inputs. Whereas in the case of an ordinary finite automaton every run ends with a state rn and the input is accepted if and only if rn is an accepting state, the definition of the set of accepted inputs is more complicated for ω-automata. Here we must look at the entire run ρ. The input is accepted if the corresponding run is in Acc. 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. The difference between various types of ω-automata (Büchi, Rabin etc.) consists in how they encode certain subsets Acc of Qω as finite sets, and therefore in which such subsets they can encode. Formally, a nondeterministic ω-automaton is a tuple A = (Q,Σ,Δ,Q0,Acc) that consists of the following components: Unlike a deterministic ω-automaton, which has a transition function δ, the non-deterministic version has a transition relation Δ. Note that Δ can be regarded as a function : Q × Σ → P(Q) from Q × Σ to the power set P(Q). Thus, given a state qn and a symbol an, the next state qn+1 is not necessarily determined uniquely, rather there is a set of possible next states.