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. 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.
Deterministic ω-automata Formally, a deterministic ω-automaton is a tuple A = ( Q , Σ , δ , Q 0 , A a c c ) {\textstyle A=(Q,\Sigma ,\delta ,Q_{0},A_{acc})} , that consists of the following components:
Q {\textstyle Q} , is a finite set. The elements of Q {\textstyle Q} are called the states of A {\textstyle A} .
Σ {\textstyle \Sigma } , is a finite set called the alphabet of A {\textstyle A} .
δ : Q × Σ → Q {\textstyle \delta \colon Q\times \Sigma \rightarrow Q} is a function, called the transition function of A {\textstyle A} .
Q 0 {\textstyle Q_{0}} is an element of Q {\textstyle Q} , called the initial state.
A a c c {\textstyle A_{acc}} is a set of accepting states of A {\textstyle A} , formally a subset of Q ω {\textstyle Q^{\omega }} . An input for A {\textstyle A} is an infinite string over the alphabet Σ {\textstyle \Sigma } , i.e. it is an infinite sequence α = ( a 1 , a 2 , a 3 , … ) {\textstyle \alpha =(a_{1},a_{2},a_{3},\ldots )} . The run of A {\textstyle A} on such an input is an infinite sequence ρ = ( r 0 , r 1 , r 2 , … ) {\textstyle \rho =(r_{0},r_{1},r_{2},\ldots )} of states, defined as follows:
r 0 = q 0 {\textstyle r_{0}=q_{0}} .
r 1 = δ ( r 0 , a 1 ) {\textstyle r_{1}=\delta (r_{0},a_{1})} .
… excerpt ends here. Continue reading the full article.
