Ω-automaton
Encyclopedia
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 non-deterministic. These classes of ω-automata differ only in terms of acceptance condition. They all recognize precisely the regular ω-language
s 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.
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.
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.
A run of A on the input α = (a1,a2,a3,...) is any infinite sequence ρ = (r0,r1,r2,...) of states that satisfies the following conditions:
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.
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.
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 Li and Ui exchanged.
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.
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 q0 (the initial state) and q1. Δ consists of the triples (q0,0,q0), (q0,1,q0), (q0,0,q1) and (q1,0,q1).
F = {q1}. For any input α in which 1 occurs only finitely many times, there is a run which stays in state q0 as long as there are 1s to read, and goes to state q1 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 q0. (Once the machine has left q0 and reached q1, 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.
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.
Automata theory
In theoretical computer science, automata theory is the study of abstract machines and the computational problems that can be solved using these machines. These abstract machines are called automata...
, a branch of theoretical computer science
Theoretical computer science
Theoretical computer science is a division or subset of general computer science and mathematics which focuses on more abstract or mathematical aspects of computing....
, an ω-automaton (or stream automaton) is a deterministic
Deterministic finite state machine
In the theory of computation and automata theory, a deterministic finite state machine—also known as deterministic finite automaton —is a finite state machine accepting finite strings of symbols. For each state, there is a transition arrow leading out to a next state for each symbol...
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
Büchi automaton
In computer science and automata theory, a Büchi automaton is a type of ω-automaton, which extends a finite automaton to infinite inputs. It accepts an infinite input sequence iff there exists a run of the automaton that visits one of the final states infinitely often. Büchi automata recognize the...
, Rabin automata, Streett automata, parity automata and Muller automata
Muller automaton
In automata theory, a Muller automaton is a type of an ω-automaton.The acceptance condition separates a Muller automomaton from other ω-automata....
, each deterministic or non-deterministic. These classes of ω-automata differ only in terms of acceptance condition. They all recognize precisely the regular ω-language
Omega-regular language
The ω-regular languages are a class of ω-languages which generalize the definition of regular languages to infinite words. Büchi showed in 1962 that ω-regular languages are precisely the ones definable in a particular monadic second-order logic called S1S.- Formal definition :An...
s 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,Σ,δ,q0,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.
- q0 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 α = (a1,a2,a3,...).
The run of A on such an input is an infinite sequence ρ = (r0,r1,r2,...) of states, defined as follows:
- r0 = q0.
- r1 = δ(r0,a1).
- r2 = δ(r1,a2).
-
- ...
- rn = δ(rn-1,an).
- ...
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.
Nondeterministic ω-automata
Formally, a nondeterministic ω-automaton is a tuple A = (Q,Σ,Δ,Q0,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.
- Q0 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 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.
A run of A on the input α = (a1,a2,a3,...) is any infinite sequence ρ = (r0,r1,r2,...) of states that satisfies the following conditions:
- r0 is an element of Q0.
- r1 is an element of Δ(r0,a1).
- r2 is an element of Δ(r1,a2).
-
- ...
- rn is an element of Δ(rn-1,an).
- ...
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 automatonBüchi automatonIn computer science and automata theory, a Büchi automaton is a type of ω-automaton, which extends a finite automaton to infinite inputs. It accepts an infinite input sequence iff there exists a run of the automaton that visits one of the final states infinitely often. Büchi automata recognize the...
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 (Ei,Fi) of sets of states:
-
- Rabin condition: A accepts exactly those runs ρ for which there exists a pair (Ei,Fi) in Ω such that Ei ∩ Inf(ρ) is empty and Fi ∩ Inf(ρ) is not empty.
- A Streett automaton is an ω-automaton A that uses the following acceptance condition, for some set Ω of pairs (Ei,Fi) of sets of states:
-
- Streett condition: A accepts exactly those runs ρ such that for all pairs (Ei,Fi) in Ω, Ei ∩ Inf(ρ) is not empty or Fi ∩ 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 Li and Ui 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 automatonMuller automatonIn automata theory, a Muller automaton is a type of an ω-automaton.The acceptance condition separates a Muller automomaton from other ω-automata....
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
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 non-deterministic Büchi automaton recognizing L needs only two states q0 (the initial state) and q1. Δ consists of the triples (q0,0,q0), (q0,1,q0), (q0,0,q1) and (q1,0,q1).
F = {q1}. For any input α in which 1 occurs only finitely many times, there is a run which stays in state q0 as long as there are 1s to read, and goes to state q1 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 q0. (Once the machine has left q0 and reached q1, 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
Büchi automaton
In computer science and automata theory, a Büchi automaton is a type of ω-automaton, which extends a finite automaton to infinite inputs. It accepts an infinite input sequence iff there exists a run of the automaton that visits one of the final states infinitely often. Büchi automata recognize the...
, 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
Omega-regular language
The ω-regular languages are a class of ω-languages which generalize the definition of regular languages to infinite words. Büchi showed in 1962 that ω-regular languages are precisely the ones definable in a particular monadic second-order logic called S1S.- Formal definition :An...
.
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.