Büchi automaton

A Büchi automaton with two states, $q_0$ and $q_1$, the former of which is the start state and the latter of which is accepting. Its inputs are infinite words over the symbols $\{a,b\}$. As an example, it accepts the infinite word $(ab{)}^{\omega }$, where $x^{\omega }$ denotes the infinite repetition of a string $x$. It rejects the infinite word $aaa{b}^{\omega }$.

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 machine should move to from its current state when it reads the next input character. Some states are accepting states and one state is the start state. The machine accepts an input if and only if it will pass through an accepting state infinitely many times as it reads the input.

A non-deterministic Büchi automaton, later referred to just as a Büchi automaton, has a transition function which may have multiple outputs, leading to many possible paths for the same input; it accepts an infinite input if and only if some possible path is accepting. Deterministic and non-deterministic Büchi automata generalize deterministic finite automata and nondeterministic finite automata to infinite inputs. Each are types of ω-automata. Büchi automata recognize the ω-regular languages, the infinite word version of regular languages. They are named after the Swiss mathematician Julius Richard Büchi, who invented them in 1962.

Büchi automata are often used in model checking as an automata-theoretic version of a formula in linear temporal logic.

Formal definition

Formally, a deterministic Büchi automaton is a tuple Template:Nowrap that consists of the following components:

• Template:Nowrap is a finite set. The elements of Template:Nowrap are called the states of Template:Nowrap.
• Template:Nowrap is a finite set called the alphabet of Template:Nowrap.
• Template:Nowrap is a function, called the transition function of Template:Nowrap.
• Template:Nowrap is an element of Template:Nowrap, called the initial state of Template:Nowrap.
• Template:Nowrap is the acceptance condition.

A run $\underset{\_}{i}=i_0{i}_1{i}_2\cdots \in {\mathrm{\Sigma }}^{\omega }$ is an infinite string of inputs of $A$. By calling $\delta$ recursively, we can extend it to a function ${\delta }^{\omega }:{\mathrm{\Sigma }}^{\omega }\to Q^{\omega }$. A state $q\in Q$ is said to occur infinitely often for a run $\underset{\_}{i}$ when the set $\{n\in \mathbb{N}\mid {\delta }^{\omega }(\underset{\_}{i}{)}_n=q\}$ is infinite. Let $\mathrm{I}\mathrm{n}\mathrm{f}(\underset{\_}{i})$ be the set of states occurring infinitely often for $\underset{\_}{i}$. The language of $A$ is then the set of runs of $A$ in which at least one of the infinitely-often occurring states is in Template:Nowrap; in symbols: $$L(A)=\{\underset{\_}{i}\in {\mathrm{\Sigma }}^{\omega }\mid \mathrm{I}\mathrm{n}\mathrm{f}(\underset{\_}{i})\cap 𝐅\ne \varnothing \}.$$

In a (non-deterministic) Büchi automaton, the transition function Template:Nowrap is replaced with a transition relation Template:Nowrap that returns a set of states, and the single initial state Template:Nowrap is replaced by a set Template:Nowrap of initial states. Generally, the term Büchi automaton without qualifier refers to non-deterministic Büchi automata.

For more comprehensive formalism see also ω-automaton.

Closure properties

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

Let $A=(Q_A,\mathrm{\Sigma },{\mathrm{\Delta }}_A,I_A,F_A)$ and $B=(Q_B,\mathrm{\Sigma },{\mathrm{\Delta }}_B,I_B,F_B)$ be Büchi automata and $C=(Q_C,\mathrm{\Sigma },{\mathrm{\Delta }}_C,I_C,F_C)$ be a finite automaton.

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

Proof: If we assume, w.l.o.g., $Q_A\cap Q_B$ is empty then $L(A)\cup L(B)$ is recognized by the Büchi automaton $(Q_A\cup Q_B,\mathrm{\Sigma }\cup \mathrm{\Sigma },{\mathrm{\Delta }}_A\cup {\mathrm{\Delta }}_B,I_A\cup I_B,F_A\cup F_B).$

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

Proof: The Büchi automaton $A^{\prime }=(Q^{\prime },\mathrm{\Sigma },{\mathrm{\Delta }}^{\prime },I^{\prime },F^{\prime })$ recognizes $L(A)\cap L(B),$ where

• $Q^{\prime }=Q_A\times Q_B\times \{1,2\}$
• ${\mathrm{\Delta }}^{\prime }={\mathrm{\Delta }}_1\cup {\mathrm{\Delta }}_2$
  • ${\mathrm{\Delta }}_1=\{((q_A,q_B,1),a,(q{\text{'}}_A,q{\text{'}}_B,i))|(q_A,a,q{\text{'}}_A)\in {\mathrm{\Delta }}_A\text{ and }(q_B,a,q{\text{'}}_B)\in {\mathrm{\Delta }}_B\text{ and if }{q}_A\in F_A\text{ then }i=2\text{ else }i=1\}$
  • ${\mathrm{\Delta }}_2=\{((q_A,q_B,2),a,(q{\text{'}}_A,q{\text{'}}_B,i))|(q_A,a,q{\text{'}}_A)\in {\mathrm{\Delta }}_A\text{ and }(q_B,a,q{\text{'}}_B)\in {\mathrm{\Delta }}_B\text{ and if }{q}_B\in F_B\text{ then }i=1\text{ else }i=2\}$
• $I^{\prime }=I_A\times I_B\times \{1\}$
• $F^{\prime }=\{(q_A,q_B,2)|q_B\in F_B\}$

By construction, $r^{\prime }=(q_A^0,q_B^0,i^0),(q_A^1,q_B^1,i^1),\dots$ is a run of automaton A' on input word Template:Nowrap if $r_A=q_A^0,q_A^1,\dots$ is run of Template:Nowrap on Template:Nowrap and $r_B=q_B^0,q_B^1,\dots$ is run of Template:Nowrap on Template:Nowrap. Template:Nowrap is accepting and Template:Nowrap is accepting if Template:Nowrap 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 Template:Nowrap if Template:Nowrap is accepted by Template:Nowrap.

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

Proof: If we assume, w.l.o.g., $Q_C\cap Q_A$ is empty then the Büchi automaton $A^{\prime }=(Q_C\cup Q_A,\mathrm{\Sigma },{\mathrm{\Delta }}^{\prime },I^{\prime },F_A)$ recognizes $L(C)\cdot L(A)$, where

• ${\mathrm{\Delta }}^{\prime }={\mathrm{\Delta }}_A\cup {\mathrm{\Delta }}_C\cup \{(q,a,q^{\prime })|q^{\prime }\in I_A\text{ and }\mathrm{\exists }f\in F_C.(q,a,f)\in {\mathrm{\Delta }}_C\}$
• $\text{ if }{I}_C\cap F_C\text{ is empty then }{I}^{\prime }=I_C\text{ otherwise }{I}^{\prime }=I_C\cup I_A$

• ω-closure: If $L(C)$ does not contain the empty word then there is a Büchi automaton that recognizes the language $L(C{)}^{\omega }.$

Proof: The Büchi automaton that recognizes $L(C{)}^{\omega }$ is constructed in two stages. First, we construct a finite automaton Template:Nowrap such that Template:Nowrap also recognizes $L(C)$ but there are no incoming transitions to initial states of Template:Nowrap. So, $A^{\prime }=(Q_C\cup \{q_{\text{new}}\},\mathrm{\Sigma },{\mathrm{\Delta }}^{\prime },\{q_{\text{new}}\},F_C),$ where ${\mathrm{\Delta }}^{\prime }={\mathrm{\Delta }}_C\cup \{(q_{\text{new}},a,q^{\prime })|\mathrm{\exists }q\in I_C.(q,a,q^{\prime })\in {\mathrm{\Delta }}_C\}.$ Note that $L(C)=L(A^{\prime })$ because $L(C)$ does not contain the empty string. Second, we will construct the Büchi automaton Template:Nowrap that recognize $L(C{)}^{\omega }$ by adding a loop back to the initial state of Template:Nowrap. So, $A^{″}=(Q_C\cup \{q_{\text{new}}\},\mathrm{\Sigma },{\mathrm{\Delta }}^{″},\{q_{\text{new}}\},\{q_{\text{new}}\})$, where ${\mathrm{\Delta }}^{″}={\mathrm{\Delta }}^{\prime }\cup \{(q,a,q_{\text{new}})|\mathrm{\exists }{q}^{\prime }\in F_C.(q,a,q^{\prime })\in {\mathrm{\Delta }}^{\prime }\}.$

• Complementation:There is a Büchi automaton that recognizes the language ${\mathrm{\Sigma }}^{\omega }/L(A).$

Proof: The proof is presented here.

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

A non-deterministic Büchi automaton that recognizes Template:Tmath

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 Template:Tmath, which contains exactly words in which 1 occurs only finitely many times. We can demonstrate it by contradiction that no such deterministic Büchi automaton exists. Let us suppose Template:Nowrap is a deterministic Büchi automaton that recognizes Template:Tmath with final state set Template:Nowrap. Template:Nowrap accepts Template:Nowrap. So, Template:Nowrap will visit some state in Template:Nowrap after reading some finite prefix of Template:Nowrap, say after the Template:Nowrapth letter. Template:Nowrap also accepts the ω-word Template:Nowrap. Therefore, for some Template:Nowrap, after the prefix Template:Nowrap the automaton will visit some state in Template:Nowrap. Continuing with this construction the ω-word Template:Nowrap is generated which causes Template:Nowrap to visit some state in Template:Nowrap infinitely often and the word is not in Template:Tmath 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 if it is the limit language of some regular language.

Proof: Any deterministic Büchi automaton Template:Nowrap can be viewed as a deterministic finite automaton Template:Nowrap 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 Template:Nowrap is the limit language of Template:Nowrap. An ω-word is accepted by Template:Nowrap if it will force Template:Nowrap to visit final states infinitely often. Thus, infinitely many finite prefixes of this ω-word will be accepted by Template:Nowrap. Hence, Template:Nowrap is a limit language of Template:Nowrap.

Algorithms

Model checking 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 for the 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 and Safra's construction provide algorithms that can translate a Büchi automaton into a deterministic Muller automaton 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 and decompose it into strongly connected components (SCCs).
2. Run a search (e.g., the depth-first search) to find which SCCs are reachable from the initial state.
3. Check whether there is a non-trivial SCC that is 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

Minimizing deterministic Büchi automata (i.e., given a deterministic Büchi automaton, finding a deterministic Büchi automaton recognizing the same language with a minimal number of states) is an NP-complete problem. This is in contrast to DFA minimization, which can be done in polynomial time.

Variants

• Co-Büchi automaton
• Weak Büchi automaton
• Semi-deterministic Büchi automaton
• Generalized Büchi automaton

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

From generalized Büchi automata (GBA)

Multiple sets of states in acceptance condition can be translated into one set of states by an automata construction, which is known as "counting construction". Let's say Template:Nowrap is a GBA, where Template:Nowrap are sets of accepting states then the equivalent Büchi automaton is Template:Nowrap, where

• Template:Nowrap
• Template:Nowrap
• Template:Nowrap
• Template:Nowrap

From Linear temporal logic formula

A translation from a Linear temporal logic formula to a generalized Büchi automaton is given here. And, a translation from a generalized Büchi automaton to a Büchi automaton is presented above.

From Muller automata

A given Muller automaton can be transformed into an equivalent Büchi automaton with the following automata construction. Let's suppose Template:Nowrap is a Muller automaton, where Template:Nowrap are sets of accepting states. An equivalent Büchi automaton is Template:Nowrap, where

• Template:Nowrap
• Template:Nowrap, where
  • Template:Nowrap
  • Template:Nowrap
• Template:Nowrap

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

From Kripke structures

Let the given Kripke structure be defined by Template:Nowrap where Template:Nowrap is the set of states, Template:Nowrap is the set of initial states, Template:Nowrap is a relation between two states also interpreted as an edge, Template:Nowrap is the label for the state and Template:Nowrap are the set of atomic propositions that form Template:Nowrap.

The Büchi automaton will have the following characteristics:

$Q_{\text{final}}=Q\cup \{\text{init}\}$

$\mathrm{\Sigma }=2^{AP}$

$I=\{\text{init}\}$

$F=Q\cup \{\text{init}\}$

$\delta =q\overrightarrow{a}p$ if Template:Nowrap belongs to Template:Nowrap and Template:Nowrap

and Template:Nowrap if Template:Nowrap belongs to Template:Nowrap and Template:Nowrap.

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.

Complementation

In automata theory, complementation of a Büchi automaton is the task of complementing a Büchi automaton, i.e., constructing another automaton that recognizes the complement of the ω-regular language recognized by the given Büchi automaton. Existence of algorithms for this construction proves that the set of ω-regular languages is closed under complementation.

This construction is particularly hard relative to the constructions for the other closure properties of Büchi automata. The first construction was presented by Büchi in 1962. Later, other constructions were developed that enabled efficient and optimal complementation.

Büchi's construction

Büchi presented a doubly exponential complement construction in a logical form. Here, we have his construction in the modern notation used in automata theory. Let Template:Nowrap be a Büchi automaton. Let Template:Nowrap be an equivalence relation over elements of Template:Nowrap such that for each Template:Nowrap, Template:Nowrap if and only if for all Template:Nowrap, Template:Nowrap has a run from Template:Nowrap to Template:Nowrap over Template:Nowrap if and only if this is possible over Template:Nowrap and furthermore Template:Nowrap has a run via Template:Nowrap from Template:Nowrap to Template:Nowrap over Template:Nowrap if and only if this is possible over Template:Nowrap. Each class of Template:Nowrap defines a map Template:Nowrap in the following way: for each state Template:Nowrap, we have Template:Nowrap, where Template:Nowrap and Template:Nowrap. Note that Template:Nowrap. If Template:Nowrap is a map definable in this way, we denote the (unique) class defining Template:Nowrap by Template:Nowrap.

The following three theorems provide a construction of the complement of Template:Nowrap using the equivalence classes of Template:Nowrap.

Theorem 1: Template:Nowrap has finitely many equivalent classes and each class is a regular language.
Proof: Since there are finitely many Template:Nowrap, the relation Template:Nowrap has finitely many equivalence classes. Now we show that Template:Nowrap is a regular language. For Template:Nowrap and Template:Nowrap, let Template:Nowrap be a nondeterministic finite automaton, where Template:Nowrap, and Template:Nowrap. Let Template:Nowrap. Let Template:Nowrap, which is the set of words that can move Template:Nowrap from Template:Nowrap to all the states in Template:Nowrap via some state in Template:Nowrap. Let Template:Nowrap, which is the set of non-empty words that can move Template:Nowrap from Template:Nowrap to all the states in Template:Nowrap and does not have a run that passes through any state in Template:Nowrap. Let Template:Nowrap, which is the set of non-empty words that cannot move Template:Nowrap from Template:Nowrap to any of the states in Template:Nowrap. Since the regular languages are closed under finite intersections and under relative complements, every Template:Nowrap, Template:Nowrap, and Template:Nowrap is regular. By definitions, Template:Nowrap.

Theorem 2: For each Template:Nowrap, there are Template:Nowrap classes Template:Nowrap and Template:Nowrap such that Template:Nowrap.
Proof: We will use the infinite Ramsey theorem to prove this theorem. Let Template:Nowrap and Template:Nowrap. Consider the set of natural numbers Template:Nowrap. Let equivalence classes of Template:Nowrap be the colors of subsets of Template:Nowrap of size 2. We assign the colors as follows. For each Template:Nowrap, let the color of Template:Nowrap be the equivalence class in which Template:Nowrap occurs. By the infinite Ramsey theorem, we can find an infinite set Template:Nowrap such that each subset of Template:Nowrap of size 2 has same color. Let Template:Nowrap. Let Template:Nowrap be a defining map of an equivalence class such that Template:Nowrap. Let Template:Nowrap be a defining map of an equivalence class such that for each Template:Nowrap, Template:Nowrap. Then Template:Nowrap.

Theorem 3: Let Template:Nowrap and Template:Nowrap be equivalence classes of Template:Nowrap. Then Template:Nowrap is either a subset of Template:Nowrap or disjoint from Template:Nowrap.
Proof: Suppose there is a word Template:Nowrap, otherwise the theorem holds trivially. Let Template:Nowrap be an accepting run of Template:Nowrap over input Template:Nowrap. We need to show that each word Template:Nowrap is also in Template:Nowrap, i.e., there exists a run Template:Nowrap of Template:Nowrap over input Template:Nowrap such that a state in Template:Nowrap occurs in Template:Nowrap infinitely often. Since Template:Nowrap, let Template:Nowrap such that Template:Nowrap and for each Template:Nowrap, Template:Nowrap. Let Template:Nowrap be the state in Template:Nowrap after consuming Template:Nowrap. Let Template:Nowrap be a set of indices such that Template:Nowrap if and only if the run segment in Template:Nowrap from Template:Nowrap to Template:Nowrap contains a state from Template:Nowrap. Template:Nowrap must be an infinite set. Similarly, we can split the word Template:Nowrap. Let Template:Nowrap such that Template:Nowrap and for each Template:Nowrap, Template:Nowrap. We construct Template:Nowrap inductively in the following way. Let the first state of Template:Nowrap be same as Template:Nowrap. By definition of Template:Nowrap, we can choose a run segment on word Template:Nowrap to reach Template:Nowrap. By induction hypothesis, we have a run on Template:Nowrap that reaches to Template:Nowrap. By definition of Template:Nowrap, we can extend the run along the word segment Template:Nowrap such that the extension reaches Template:Nowrap and visits a state in Template:Nowrap if Template:Nowrap. The Template:Nowrap obtained from this process will have infinitely many run segments containing states from Template:Nowrap, since Template:Nowrap is infinite. Therefore, Template:Nowrap is an accepting run and Template:Nowrap.

By the above theorems, we can represent Template:Nowrap as finite union of ω-regular languages of the form Template:Nowrap, where Template:Nowrap and Template:Nowrap are equivalence classes of Template:Nowrap. Therefore, Template:Nowrap is an ω-regular language. We can translate the language into a Büchi automaton. This construction is doubly exponential in terms of size of Template:Nowrap.

References

• Template:Cite book
• Template:Cite book

External links

• Template:Cite web
• Template:Cite CiteSeerX