In computer science

Computer science

Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...

 and automata theory

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 Büchi automaton is a type of ω-automaton

Ω-automaton

In automata theory, a branch of theoretical computer science, an ω-automaton is a deterministic or nondeterministic automaton that runs on infinite, rather than finite, strings as input...

, which extends a finite automaton to infinite inputs. It accepts an infinite input sequence iff

IFF

IFF, Iff or iff may refer to:Technology/Science:* Identification friend or foe, an electronic radio-based identification system using transponders...

 there exists a run of the automaton that visits (at least) one of the final states infinitely often. Büchi automata recognize the omega-regular languages, the infinite word version of regular languages. It is named after the Swiss mathematician Julius Richard Büchi

Julius Richard Büchi

Julius Richard Büchi was a Swiss logician and mathematician.He received his Dr. sc. nat. in 1950 at the ETH Zürich under supervision of Paul Bernays and Ferdinand Gonseth. Shortly afterwards he went to Purdue University, Lafayette, Indiana...

 who invented this kind of automaton in 1962.

Büchi automata are often used in Model checking

Model checking

In computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....

 as an automata-theoretic version of a formula in linear temporal logic

Linear temporal logic

In logic, Linear temporal logic is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths such as that a condition will eventually be true, that a condition will be true until another fact becomes true, etc. It is a fragment of the more...

.

Formal definition

Formally, a deterministic Büchi automaton is a tuple A = (Q,Σ,δ,q₀,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.
• δ: Q × Σ → Q is a function, called the transition function of A.
• q₀ is an element of Q, called the initial state.
• F⊆Q is the acceptance condition. A accepts exactly those runs in which at least one of the infinitely often occurring states is in F.

In a non-deterministic Büchi automaton, the transition function δ is replaced with a transition relation Δ that returns a set of states and initial state is q₀ is replaced by a set of initial states Q₀. Generally, Büchi automaton refers to non-deterministic Büchi automaton.

For more comprehensive formalism see also ω-automaton

Ω-automaton

In automata theory, a branch of theoretical computer science, an ω-automaton is a deterministic or nondeterministic automaton that runs on infinite, rather than finite, strings as input...

.

Closure properties

The set of Büchi automata is closed under following operations.

Let A=(Q_A,Σ,Δ_A,I_A,F_A) and B=(Q_B,Σ,Δ_B,I_B,F_B) be Büchi automata and C=(Q_C,Σ,Δ_C,I_C,F_C) be a finite automaton.

• Union: There is a Büchi automaton that recognizes the language L(A)∪L(B).

Proof: If we assume, w.l.o.g., Q_A∩Q_B is empty then L(A)∪L(B) is recognized by the Büchi automaton (Q_A∪Q_B, Σ, Δ_A∪Δ_B, I_A∪I_B, F_A∪F_B).

• Intersection: There is a Büchi automaton that recognizes the language L(A)∩L(B).

Proof: The Büchi automaton A'=(Q',Σ,Δ',I',F') recognizes L(A)∩L(B), where

• Q' = Q_A × Q_B × {1,2}
• Δ' = Δ₁ ∪ Δ₂
  • Δ₁ = {( (q_A,q_B,1), a, (q'_A,q'_B,i) ) | (q_A,a,q'_A)∈Δ_A and (q_B,a,q'_B)∈Δ_B and if q_A∈F_A then i=2 else i=1 }
  • Δ₂ = {( (q_A,q_B,2), a, (q'_A,q'_B,i) ) | (q_A,a,q'_A)∈Δ_A and (q_B,a,q'_B)∈Δ_B and if q_B∈F_B then i=1 else i=2 }
• I' = I_A × I_B × {1}
• F' = { (q_A,q_B,2) | q_B∈F_B }

By construction, r'=(q_A⁰,q_B⁰,i⁰),(q_A¹,q_B¹,i¹),... is a run of automaton A' on input word w iff r_A=q_A⁰,q_A¹,... is run of A on w and r_B=q_B⁰,q_B¹,... is run of B on w. r_A is accepting and r_B is accepting iff r' is concatenation of an infinite series of finite segments of 1-states(states with third component 1) and 2-states(states with third component 2) alternatively. There is such a series of segments of r' iff r' is accepted by A'.

• Concatenation: There is a Büchi automaton that recognizes the language L(C)⋅L(A).

Proof: If we assume, w.l.o.g., Q_C∩Q_A is empty then the Büchi automaton A'=(Q_C∪Q_A,Σ,Δ',I',F_A) recognizes L(C)⋅L(A), where

• Δ' = Δ_A ∪ Δ_C ∪ { (q,a,q') | q'∈I_A and ∃f∈F_C. (q,a,f)∈Δ_C }
• if I_C∩F_C is empty then I' = I_C otherwise I' = I_C ∪ I_A
• ω-closure: If L(C) does not contain empty word then there is a Büchi automaton that recognizes the language L(C)^ω.

Proof: The Büchi automaton that recognizes L(C)^ω is constructed in two stages. First, we construct a finite automaton A' such that A' also recognizes L(C) but there are no incoming transitions to initial states of A'. So, A'=(Q_C ∪ {q_new},Σ,Δ',{q_new},F_C), where Δ' = Δ_C ∪ { (q_new,a,q') | ∃q∈I_C. (q,a,q')∈Δ_C}. Note that L(C)=L(A') because L(C) does not contain the empty string. Second, we will construct the Büchi automaton A' ' that recognize L(C)^ω by adding a loop back to the initial state of A'. So, A' '=(Q_C ∪ {q_new},Σ,Δ' ',{q_new},{q_new}), where Δ' ' = Δ' ∪ { (q,a,q_new) | ∃q'∈F_C. (q,a,q')∈Δ'}.

• Complementation:There is a Büchi automaton that recognizes the language Σ*/L(A).

Proof: The proof is presented here

Complementation of Büchi automaton

In automata theory, complementation of a Büchi automaton is construction of another Büchi automaton that recognizes complement of the ω-regular language recognized by the given Büchi automaton...

.

Recognizable languages

Büchi automata recognize the ω-regular languages. Using the definition of ω-regular language and the above closure properties of Büchi automata, it can be easily shown that a Büchi automaton can be constructed such that it recognizes any given ω-regular language. For converse, see construction of a ω-regular language for a Büchi automaton.

Deterministic versus non-deterministic Büchi automata

The class of deterministic Büchi automata does not suffice to encompass all omega-regular languages. In particular, there is no deterministic Büchi automaton that recognizes the language (0+1)*0^ω (Any word that has an infinite suffix consisting of only 0's). We can demonstrate it by contradiction that no such deterministic Büchi automaton exists. Let us suppose A is a deterministic Büchi automaton that recognize (0+1)*0^ω with final state set F. A accepts 0^ω. So, A will visit some state in F after reading some finite prefix of 0^ω, say after the i₀th letter. A also accepts the ω-word 0^i₀10^ω. Therefore, for some i₁, after the prefix 0^i₀10^i₁ the automaton will visit some state in F. Continuing with this construction the ω-word 0^i₀10^i₁10^i₂... is generated which causes A to visit some state in F infinitely often and the word is not in (0+1)*0^ω. Contradiction.

The class of languages recognizable by deterministic Büchi automata is characterized by the following lemma.

Lemma: An ω-language is recognizable by a deterministic Büchi automaton iff it is the limit language of some regular language

Regular language

In theoretical computer science and formal language theory, a regular language is a formal language that can be expressed using regular expression....

.

Proof: Any deterministic Büchi automaton A can be viewed as a deterministic finite automaton A' and vice-versa, since both types of automaton are defined as 5-tuple of the same components, only the interpretation of acceptance condition is different. We will show that L(A) is the limit language of L(A'). An ω-word is accepted by A iff it will force A to visit final states infinitely often. Iff, infinitely many finite prefixes of this ω-word will be accepted by A'. Hence, L(A) is a limit language of L(A').

Algorithms

Model checking

Model checking

In computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....

 of finite state systems can often be translated into various operations on Büchi automata.
In addition to the closure operations presented above,
the following are some useful operations in applications of Büchi automata.

Determinization

Since deterministic Büchi automata are strictly less expressive than non-deterministic automata, there can not be an algorithm for determinization of Büchi automata.
But, McNaughton's Theorem

McNaughton's Theorem

In automata theory, McNaughton's theorem refers to a theorem that asserts that the set of ω-regular languages is identical to the set of languages recognizable by deterministic Muller automata....

 and Safra's construction provide algorithms that can translate a Büchi automaton into a deterministic Muller automaton

Muller automaton

In automata theory, a Muller automaton is a type of an ω-automaton.The acceptance condition separates a Muller automomaton from other ω-automata....

 or deterministic Rabin automaton.

Emptiness checking

The language recognized by a Büchi automaton is non-empty if and only if there is a final state that is both reachable from the initial state, and lies on a cycle.

An effective algorithm that can check emptiness of a Büchi automaton:

1. Consider the automaton as a directed graph
   Directed graph
   A directed graph or digraph is a pair G= of:* a set V, whose elements are called vertices or nodes,...
   
    and decompose it into strongly connected component
   Strongly connected component
   A directed graph is called strongly connected if there is a path from each vertex in the graph to every other vertex. In particular, this means paths in each direction; a path from a to b and also a path from b to a....
   
   s.
2. Run a search (e.g., the depth-first search
   Depth-first search
   Depth-first search is an algorithm for traversing or searching a tree, tree structure, or graph. One starts at the root and explores as far as possible along each branch before backtracking....
   
   ) to find which components are reachable from the initial state.
3. Check whether there is a non-trivial strongly connected component that is both reachable and contains a final state.

Each of the steps of this algorithm can be done in time linear in the automaton size, hence the algorithm is clearly optimal.

Minimization

The algorithm for minimizing nondeterministic finite automaton also correctly minimizes a Büchi automaton.
The algorithm does not guarantee minimum Büchi automaton.
Note that algorithms for minimizing deterministic finite automaton does not work for deterministic Büchi automaton.

Variants

• Co-Büchi automaton
  Co-Büchi automaton
  In automata theory, a co-Büchi automaton is a variant of Büchi automaton. The only difference is the accepting condition: a Co-Büchi automaton accepts an infinite word w if there exist a run, such that all the states occurring infinitely often in the run are not in the acceptance condition...
  
  
• Semi-deterministic Büchi automaton
  Semi-deterministic büchi automaton
  In automata theory, a semi-deterministic Büchi automaton is a special type of Büchi automaton. In such an automaton, states can be divided into two partitions such that one part forms a deterministic automaton and this part also contains all the accepting states.For every Büchi automaton, a...
  
  
• Generalized Büchi automaton
  Generalized Büchi automaton
  In automata theory, generalized Büchi automaton is a variant of Büchi automaton. The difference with the Büchi automaton is its accepting condition, i.e., a set of sets of states. A run is accepted by the automaton if it visits at least one state of every set of the accepting condition infinitely...
  
  

Transforming from other models of description to non-deterministic Büchi automata

From generalized Büchi automata

Generalized Büchi automaton

In automata theory, generalized Büchi automaton is a variant of Büchi automaton. The difference with the Büchi automaton is its accepting condition, i.e., a set of sets of states. A run is accepted by the automaton if it visits at least one state of every set of the accepting condition infinitely...

(GBA)

Multiple sets of states in acceptance condition can be translated into one set of states by an automata construction

Automata construction

In automata theory, automata construction is an important mathematical technique used to demonstrate the existence of an automaton with a certain desired property...

, which is known as "counting construction". Lets say A = (Q,Σ,∆,q₀,{F₀,...,F_n}) is a GBA, where F₀,...,F_n are sets of accepting states then the equivalent Büchi automaton is A = (Q', Σ, ∆',q'₀,F'), where

• Q' = Q × {1,...,n}
• q'₀ = ( q₀,1 )
• ∆' = { ( (q,i), a, (q',j) ) | (q,a,q') ∈ ∆ and if q ∈ F_i then j=(i mod n)+1 else j=i }
• F'=F₁× {1}

From Linear temporal logic

Linear temporal logic

In logic, Linear temporal logic is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths such as that a condition will eventually be true, that a condition will be true until another fact becomes true, etc. It is a fragment of the more...

 formula

A translation from a Linear temporal logic formula to a generalized Büchi automaton is given here

Linear temporal logic to Büchi automaton

In formal verification,the model checking method needs to obtain a Büchi automaton from a Linear temporal logic formula.There are algorithms that translates a LTL formula to an equivalent BA...

. And, a translation from a generalized Büchi automaton to a Büchi automaton is presented above.

From 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....

A given Muller automaton can be transformed into an equivalent Büchi automaton with following automata construction

Automata construction

In automata theory, automata construction is an important mathematical technique used to demonstrate the existence of an automaton with a certain desired property...

. Lets suppose A = (Q,Σ,∆,Q₀,{F₀,...,F_n}) is a Muller automaton, where F₀,...,F_n are sets of accepting states. An equivalent Büchi automaton is A = (Q', Σ, ∆',Q₀,F'), where

• Q' = Q ∪  ∪ⁿ_i=0 {i} × F_i × 2^F_i
• ∆'= ∆ ∪ ∆₁ ∪ ∆₂, where
  • ∆₁ ={ ( q, a, (i,q',∅) ) | (q, a, q') ∈ ∆ and q' ∈ F_i }
  • ∆₂={ ( (i,q,R), a, (i,q',R') ) | (q,a,q')∈∆ and q,q' ∈ F_i and if R=F_i then R'= ∅ otherwise R'=R∪{q} }
• F'=∪ⁿ_i=0 {i} × F_i × {F_i}

A' keeps original set of states from A and adds extra states on them. The Büchi automaton A' simulates the Muller automaton A as follows: At the beginning of the input word, the execution of A follows the execution of A, since initial states are same and ∆' contains ∆. At some non-deterministically chosen position in the input word, A' decides of jump into newly added states via a transition in ∆₁. Then, the transitions in ∆₂ try to visit all the states of F_i and keep growing R. Once R becomes equal to F_i then it is reset to the empty set and ∆₂ try to visit all the states of F_i states again and again. So, if the states R=F_i are visited infinitely often then A' accepts corresponding input and so does A. This construction closely follows the first part of the proof of McNaughton's Theorem

McNaughton's Theorem

In automata theory, McNaughton's theorem refers to a theorem that asserts that the set of ω-regular languages is identical to the set of languages recognizable by deterministic Muller automata....

.

From Kripke structures

Let the given Kripke structure

Kripke structure

A Kripke structure is a type of nondeterministic finite state machine proposed by Saul Kripke , used in model checking to represent the behavior of a system.It is a simple abstract machine to capture an idea of a computing machine,...

be defined by M = where Q is the set of states, I is the set of initial states, R is a relation between two states also interpreted as an edge, L is the label for the state and AP are the set of atomic propositions that form L.

The Büchi automaton will have the following characteristics:

if (q, p) belongs to R and L(p) = a

and init q if q belongs to I and L(q) = a.

Note however that there is a difference in the interpretation between Kripke structures and Büchi automata. While the former explicitly names every state variable's polarity for every state, the latter just declares the current set of variables holding or not holding true. It says absolutely nothing about the other variables that could be present in the model.

External links

• Finite-state Automata on Infinite Inputs
• Moshe Y. Vardi: An automata-theoretic approach to linear temporal logic