ω-automaton
   HOME

TheInfoList



OR:

In
automata theory Automata theory is the study of abstract machines and automata, as well as the computational problems that can be solved using them. It is a theory in theoretical computer science. The word ''automata'' comes from the Greek word αὐτόματο ...
, a branch of
theoretical computer science Theoretical computer science (TCS) is a subset of general computer science and mathematics that focuses on mathematical aspects of computer science such as the theory of computation, lambda calculus, and type theory. It is difficult to circumsc ...
, an ω-automaton (or stream automaton) is a variation of
finite automata A finite-state machine (FSM) or finite-state automaton (FSA, plural: ''automata''), finite automaton, or simply a state machine, is a mathematical model of computation. It is an abstract machine that can be in exactly one of a finite number o ...
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 An operating system (OS) is system software that manages computer hardware, software resources, and provides common services for computer programs. Time-sharing operating systems schedule tasks for efficient use of the system and may also inc ...
and
control systems A control system manages, commands, directs, or regulates the behavior of other devices or systems using control loops. It can range from a single home heating controller using a thermostat controlling a domestic boiler to large industrial c ...
. 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 Buchi can mean: __NOTOC__ Items *Bachi, special Japanese drumsticks *Butsi, the Hispanised term for jin deui (pastry made from glutinous rice) in the Philippines *Büchi automaton, finite state automata extended to infinite inputs * Büchi arithmet ...
, 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
ω-language 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. Here, ω refers to the first ordinal ...
s, they nonetheless differ in succinctness of representation for a given ω-language.


Deterministic ω-automata

Formally, a deterministic ω-automaton is a tuple ''A'' = (''Q'',Σ,δ,''Q''0,''Acc'') that consists of the following components: * ''Q'' is a
finite set In mathematics, particularly set theory, a finite set is a set that has a finite number of elements. Informally, a finite set is a set which one could in principle count and finish counting. For example, :\ is a finite set with five elements. Th ...
. The elements of ''Q'' are called the ''states'' of ''A''. * Σ is a finite set called the ''alphabet'' of ''A''. * δ: ''Q'' × Σ → ''Q'' is a function, called the ''transition function'' of ''A''. * ''Q''0 is an element of ''Q'', called the initial state. * ''Acc'' is the ''acceptance condition'', formally a subset of ''Q''ω. An ''input'' for ''A'' is an infinite string over the alphabet Σ, i.e. it is an infinite sequence α = (''a''1,''a''2,''a''3,...). The ''run'' of ''A'' on such an input is an infinite sequence ρ = (''r''0,''r''1,''r''2,...) of states, defined as follows: * ''r''0 = ''q''0. * ''r''1 = δ(''r''0,''a''1). * ''r''2 = δ(''r''1,''a''2). :: ... * ''r''''n'' = δ(''r''''n''-1,''a''''n''). 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 ''r''''n'' and the input is accepted if and only if ''r''''n'' 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.


Nondeterministic ω-automata

Formally, a nondeterministic ω-automaton is a tuple ''A'' = (''Q'',Σ,Δ,''Q''0,''Acc'') that consists of the following components: * ''Q'' is a
finite set In mathematics, particularly set theory, a finite set is a set that has a finite number of elements. Informally, a finite set is a set which one could in principle count and finish counting. For example, :\ is a finite set with five elements. Th ...
. The elements of ''Q'' are called the ''states'' of ''A''. * Σ is a finite set called the ''alphabet'' of ''A''. * Δ is a subset of ''Q'' × Σ × ''Q'' and is called the ''transition relation'' of ''A''. * ''Q''0 is a subset of ''Q'', called the initial set of states. * ''Acc'' is the ''acceptance condition'', a subset of ''Q''ω. 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 In mathematics, the power set (or powerset) of a set is the set of all subsets of , including the empty set and itself. In axiomatic set theory (as developed, for example, in the ZFC axioms), the existence of the power set of any set is po ...
P(''Q''). Thus, given a state ''q''''n'' and a symbol ''a''''n'', the next state ''q''''n''+1 is not necessarily determined uniquely, rather there is a set of possible next states. A ''run'' of ''A'' on the input α = (''a''1,''a''2,''a''3,...) is any infinite sequence ρ = (''r''0,''r''1,''r''2,...) of states that satisfies the following conditions: * ''r''0 is an element of ''Q''0. * ''r''1 is an element of Δ(''r''0,''a''1). * ''r''2 is an element of Δ(''r''1,''a''2). :: ... * ''r''''n'' is an element of Δ(''r''''n''-1,''a''''n''). A nondeterministic ω-automaton may admit many different runs on any given input, or none at all. The input is accepted if at least one of the possible runs is accepting. Whether a run is accepting depends only on ''Acc'', as for deterministic ω-automata. Every deterministic ω-automaton can be regarded as a nondeterministic ω-automaton by taking Δ to be the graph of δ. The definitions of runs and acceptance for deterministic ω-automata are then special cases of the nondeterministic cases.


Acceptance conditions

Acceptance conditions may be infinite sets of ω-words. However, people mostly study acceptance conditions that are finitely representable. The following lists a variety of popular acceptance conditions. Before discussing the list, let's make the following observation. In the case of infinitely running systems, one is often interested in whether certain behavior is repeated infinitely often. For example, if a network card receives infinitely many ping requests, then it may fail to respond to some of the requests but should respond to an infinite subset of received ping requests. This motivates the following definition: For any run ρ, let Inf(ρ) be the set of states that occur infinitely often in ρ. This notion of certain states being visited infinitely often will be helpful in defining the following acceptance conditions. *A
Büchi automaton In computer science and automata theory, a deterministic Büchi automaton is a theoretical machine which either accepts or rejects infinite inputs. Such a machine has a set of states and a transition function, which determines which state the machi ...
is an ω-automaton ''A'' that uses the following acceptance condition, for some subset ''F'' of ''Q'': :;Büchi condition:''A'' accepts exactly those runs ρ for which Inf(ρ) ∩ ''F'' is not empty, i.e. there is an accepting state that occurs infinitely often in ρ. *A is an ω-automaton ''A'' that uses the following acceptance condition, for some set Ω of pairs (B''i'',G''i'') of sets of states: :;Rabin condition: ''A'' accepts exactly those runs ρ for which there exists a pair (B''i'',G''i'') in Ω such that B''i'' ∩ Inf(ρ) is empty and G''i'' ∩ Inf(ρ) is not empty. *A Streett automaton is an ω-automaton ''A'' that uses the following acceptance condition, for some set Ω of pairs (B''i'',G''i'') of sets of states: :;Streett condition: ''A'' accepts exactly those runs ρ such that for all pairs (B''i'',G''i'') in Ω, B''i'' ∩ Inf(ρ) is empty or G''i'' ∩ Inf(ρ) is not empty. *A parity automaton is an automaton ''A'' whose set of states is ''Q'' =  for some natural number ''k'', and that has the following acceptance condition: :;Parity condition: ''A'' accepts ρ if and only if the smallest number in Inf(ρ) is even. *A
Muller automaton In automata theory, a Muller automaton is a type of an ω-automaton. The acceptance condition separates a Muller automaton from other ω-automata. The Muller automaton is defined using a Muller acceptance condition, i.e. the set of all states visi ...
is an ω-automaton ''A'' that uses the following acceptance condition, for a subset ''F'' of P(''Q'') (the
power set In mathematics, the power set (or powerset) of a set is the set of all subsets of , including the empty set and itself. In axiomatic set theory (as developed, for example, in the ZFC axioms), the existence of the power set of any set is po ...
of ''Q''): :;Muller condition:''A'' accepts exactly those runs ρ for which Inf(ρ) is an element of ''F''. Every Büchi automaton can be regarded as a Muller automaton. It suffices to replace ''F'' by ''F''' consisting of all subsets of ''Q'' that contain at least one element of ''F''. Similarly every Rabin, Streett or parity automaton can also be regarded as a Muller automaton.


Example

The following ω-language ''L'' over the alphabet Σ = , which can be recognized by a nondeterministic Büchi automaton: ''L'' consists of all ω-words in Σω in which 1 occurs only finitely many times. A non-deterministic Büchi automaton recognizing ''L'' needs only two states ''q''0 (the initial state) and ''q''1. Δ consists of the triples (''q''0,0,''q''0), (''q''0,1,''q''0), (''q''0,0,''q''1) and (''q''1,0,''q''1). ''F'' = . For any input α in which 1 occurs only finitely many times, there is a run that stays in state ''q''0 as long as there are 1s to read, and goes to state ''q''1 afterwards. This run is successful. If there are infinitely many 1s, then there is only one possible run: the one that always stays in state ''q''0. (Once the machine has left ''q''0 and reached ''q''1, it cannot return. If another 1 is read, there is no successor state.) Notice that above language cannot be recognized by a deterministic
Büchi automaton In computer science and automata theory, a deterministic Büchi automaton is a theoretical machine which either accepts or rejects infinite inputs. Such a machine has a set of states and a transition function, which determines which state the machi ...
, which is strictly less expressive than its non-deterministic counterpart.


Expressive power of ω-automata

An ω-language over a finite alphabet Σ is a set of ω-words over Σ, i.e. it is a subset of Σω. 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 expressive power of a class of ω-automata is measured by the class of all ω-languages that can be recognized by some automaton in the class. The nondeterministic Büchi, parity, Rabin, Streett, and Muller automata, respectively, all recognize exactly the same class of ω-languages. These are known as the ''ω-Kleene closure of the regular languages'' or as the regular ω-languages. Using different proofs it can also be shown that the deterministic parity, Rabin, Streett, and Muller automata all recognize the regular ω-languages. It follows from this that the class of regular ω-languages is closed under complementation. However, the example above shows that the class of deterministic Büchi automata is strictly weaker.


Conversion between ω-automata

Because nondeterministic Muller, Rabin, Streett, parity, and Büchi automata are equally expressive, they can be translated to each other. Let us use the following abbreviation \\times\: for example, ''NB'' stands for nondeterministic Büchi ω-automaton, while ''DP'' stands for deterministic parity ω-automaton. Then the following holds. * Clearly, any deterministic automaton can be viewed as a nondeterministic one. * NB \rightarrow NR/NS/NP with no blow-up in the state space. * NR \rightarrow NB with a polynomial blow-up in the state space, i.e., the number of states in the resulting ''NB'' is 2nm+1, where n is the number of states in the ''NB'' and m is the number of Rabin acceptance pairs (see, for example, ). * NS/NM/NP \rightarrow NB with exponential blow-up in the state space. * NB \rightarrow DR/DP with exponential blow-up in the state space. This determinization result uses Safra's construction. A comprehensive overview of translations can be found on the referenced web source.


Further reading

* . * * *


References

{{reflist Finite automata