ωautomaton

In automata theory, a branch of theoretical computer science, an ωautomaton (or stream automaton) is a deterministic or nondeterministic 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, you may want to specify a property such as "for every request, an acknowledge eventually follows", or its negation "there is a request which is not followed by an acknowledge". The latter 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 nondeterministic. 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.
Contents
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. 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_{n1},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},F) that consists of the following components:
 Q is a finite set. 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 nondeterministic 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 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_{n1},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 condition may be an infinite set of omega words. So, people mostly study acceptance conditions that are only finitely representable. The following lists a variety of popular acceptance conditions.
Before discussing the list, let's make 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 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 ρ.
 Since F is finite, this is equivalent to the condition that ρ_{n} is accepting for infinitely many natural numbers n.
 A Rabin automaton is an ωautomaton A that uses the following acceptance condition, for some set Ω of pairs (E_{i},F_{i}) of sets of states:

 Rabin condition
 A accepts exactly those runs ρ for which there exists a pair (E_{i},F_{i}) in Ω such that E_{i} ∩ Inf(ρ) is empty and F_{i} ∩ Inf(ρ) is not empty.
 A Streett automaton is an ωautomaton A that uses the following acceptance condition, for some set Ω of pairs (E_{i},F_{i}) of sets of states:

 Streett condition
 A accepts exactly those runs ρ such that for all pairs (E_{i},F_{i}) in Ω, E_{i} ∩ Inf(ρ) is not empty or F_{i} ∩ Inf(ρ) is empty.
The Streett condition is the negation of the Rabin condition. Therefore a deterministic Streett automaton accepts exactly the complement of the language accepted by the deterministic Rabin automaton consisting of the same data with all L_{i} and U_{i} exchanged.
 A parity automaton is an automaton A whose set of states is Q = {0,1,2,...,k} for some natural number k, and which has the following acceptance condition:

 Parity condition
 A accepts ρ if and only if the smallest number in Inf(ρ) is even.
 A Muller automaton is an ωautomaton A that uses the following acceptance condition, for a subset F of P(Q) (the power set 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 Σ = {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. A nondeterministic 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 = {q_{1}}. For any input α in which 1 occurs only finitely many times, there is a run which 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 can not be recognized by a deterministic büchi automaton, which can be shown using the fact that there are only finitely many states in the automaton.
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 which 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.
References
 Farwer, Berndt (2002), "ωAutomata", in Grädel, Erich; Thomas, Wolfgang; Wilke, Thomas, Automata, Logics, and Infinite Games, Lecture Notes in Computer Science, Springer, pp. 3–21, ISBN 9783540003885.
 Automata on Infinite Words Slides for a tutorial by Paritosh K. Pandya.
Further reading
 Perrin, Dominique; Pin, JeanÉric (2004), Infinite Words: Automata, Semigroups, Logic and Games, Elsevier, ISBN 9780125321112
 Thomas, Wolfgang (1990), "Automata on infinite objects", in van Leeuwen, Jan, Handbook of Theoretical Computer Science, vol. B, MIT Press, pp. 133–191, ISBN 9780262220392
Categories:
Wikimedia Foundation. 2010.
Look at other dictionaries:
Automaton (disambiguation) — Automaton may refer to:* Automaton, a self operating machine * Automaton , a song by London s Neo New Wave Band The Rakes * An automaton, a mathematical model for a finite state machine (see automata theory) … Wikipedia
automaton — (n.) 1610s, from L. automaton (Suetonius), from Gk. automaton, neut. of automatos self acting, from autos self (see AUTO (Cf. auto )) + matos thinking, animated, willing, from PIE *mn to , from root *men to think (see MIND … Etymology dictionary
Automaton — Au*tom a*ton, n.; pl. L. {Automata}, E. {Automatons}. [L. fr. Gr. ?, neut. of ? self moving; ? self + a root ma, man, to strive, think, cf. ? to strive. See {Mean}, v. i.] 1. Any thing or being regarded as having the power of spontaneous motion… … The Collaborative International Dictionary of English
AUTOMATON LOGICUM — (лат. – логический производящий автомат) название мозга, введенное Отто Либманом для характеристики (парадоксального) факта, что в отношении совершающихся в нервной системе, в мозгу и т. д. процессов действительны физические и химические законы,… … Философская энциклопедия
Automaton spirituale — (лат.) духовный механизм (Лейбниц). Философский энциклопедический словарь. М.: Советская энциклопедия. Гл. редакция: Л. Ф. Ильичёв, П. Н. Федосеев, С. М. Ковалёв, В. Г. Панов. 1983 … Философская энциклопедия
Automaton — [engl.], Automat … UniversalLexikon
AUTOMATON — quibusdam idem cum pegmate, de quo suô locô: Sueton. tamen in Claudio c. 34. distinguit: Si autαὐτόματον, aut pegma, vel tale quid aliud parum cessisset: de Automato in Physicis, vide infra, ubi de Perpetuo motu; ubi de Αὐτοματοποιητικῇ, seu… … Hofmann J. Lexicon universale
automaton — has the plural form automata when understood collectively and automatons when understood individually. See Latin plurals … Modern English usage
automaton — ► NOUN (pl. automata or automatons) 1) a moving mechanical device resembling a human being. 2) a machine which operates according to coded instructions. ORIGIN Greek, from automatos acting of itself … English terms dictionary
automaton — [ô täm′ə tän΄, ô täm′ətən] n. pl. automatons or automata [ô täm′ətə] [L < Gr, neut. of automatos: see AUTOMATIC] 1. anything that can move or act of itself 2. an apparatus that automatically performs certain actions by responding to preset… … English World dictionary
Automaton — This article is about a self operating machine. For other uses of Automaton, see Automaton (disambiguation) or Automata (disambiguation). An automaton (plural: automata or automatons ) is a self operating machine. The word is sometimes used to… … Wikipedia