Büchi automaton

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 of A.
• 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 the single initial state q₀ is replaced by a set I 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.

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

Let ${\displaystyle \scriptstyle A=(Q_{A},\Sigma ,\Delta _{A},I_{A},{F}_{A})}$ and ${\displaystyle \scriptstyle B=(Q_{B},\Sigma ,\Delta _{B},I_{B},{F}_{B})}$ be Büchi automata and ${\displaystyle \scriptstyle C=(Q_{C},\Sigma ,\Delta _{C},I_{C},{F}_{C})}$ be a finite automaton.

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

Proof: If we assume, w.l.o.g., ${\displaystyle \scriptstyle Q_{A}\cap Q_{B}}$ is empty then ${\displaystyle \scriptstyle L(A)\cup L(B)}$ is recognized by the Büchi automaton ${\displaystyle \scriptstyle (Q_{A}\cup Q_{B},\Sigma ,\Delta _{A}\cup \Delta _{B},I_{A}\cup I_{B},{F}_{A}\cup {F}_{B}).}$

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

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

• ${\displaystyle \scriptstyle Q'=Q_{A}\times Q_{B}\times \{1,2\}}$
• ${\displaystyle \scriptstyle \Delta '=\Delta _{1}\cup \Delta _{2}}$
  • ${\displaystyle \scriptstyle \Delta _{1}=\{((q_{A},q_{B},1),a,(q'_{A},q'_{B},i))|(q_{A},a,q'_{A})\in \Delta _{A}{\text{ and }}(q_{B},a,q'_{B})\in \Delta _{B}{\text{ and if }}q_{A}\in F_{A}{\text{ then }}i=2{\text{ else }}i=1\}}$
  • ${\displaystyle \scriptstyle \Delta _{2}=\{((q_{A},q_{B},2),a,(q'_{A},q'_{B},i))|(q_{A},a,q'_{A})\in \Delta _{A}{\text{ and }}(q_{B},a,q'_{B})\in \Delta _{B}{\text{ and if }}q_{B}\in F_{B}{\text{ then }}i=1{\text{ else }}i=2\}}$
• ${\displaystyle \scriptstyle I'=I_{A}\times I_{B}\times \{1\}}$
• ${\displaystyle \scriptstyle F'=\{(q_{A},q_{B},2)|q_{B}\in F_{B}\}}$

By construction, ${\displaystyle \scriptstyle r'=(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 w if ${\displaystyle \scriptstyle r_{A}=q_{A}^{0},q_{A}^{1},\dots }$ is run of A on w and ${\displaystyle \scriptstyle r_{B}=q_{B}^{0},q_{B}^{1},\dots }$ is run of B on w. ${\displaystyle \scriptstyle r_{A}}$ is accepting and ${\displaystyle \scriptstyle r_{B}}$ is accepting if 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' if r' is accepted by A'.

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

Proof: If we assume, w.l.o.g., ${\displaystyle \scriptstyle Q_{C}\cap Q_{A}}$ is empty then the Büchi automaton ${\displaystyle \scriptstyle A'=(Q_{C}\cup Q_{A},\Sigma ,\Delta ',I',F_{A})}$ recognizes ${\displaystyle \scriptstyle L(C)\cdot L(A)}$, where

• ${\displaystyle \scriptstyle \Delta '=\Delta _{A}\cup \Delta _{C}\cup \{(q,a,q')|q'\in I_{A}{\text{ and }}\exists f\in F_{C}.(q,a,f)\in \Delta _{C}\}}$
• ${\displaystyle \scriptstyle {\text{ if }}I_{C}\cap F_{C}{\text{ is empty then }}I'=I_{C}{\text{ otherwise }}I'=I_{C}\cup I_{A}}$

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

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

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

Proof: The proof is presented here.

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 ${\displaystyle (0\cup 1)^{*}0^{\omega }}$

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 ${\displaystyle (0\cup 1)^{*}0^{\omega }}$, 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 A is a deterministic Büchi automaton that recognizes ${\displaystyle (0\cup 1)^{*}0^{\omega }}$ with final state set F. A accepts ${\displaystyle 0^{\omega }}$. So, A will visit some state in F after reading some finite prefix of ${\displaystyle 0^{\omega }}$, say after the ${\displaystyle i_{0}}$th letter. A also accepts the ω-word ${\displaystyle 0^{i_{0}}10^{\omega }.}$ Therefore, for some ${\displaystyle i_{1}}$, after the prefix ${\displaystyle 0^{i_{0}}10^{i_{1}}}$ the automaton will visit some state in F. Continuing with this construction the ω-word ${\displaystyle 0^{i_{0}}10^{i_{1}}10^{i_{2}}\dots }$ is generated which causes A to visit some state in F infinitely often and the word is not in ${\displaystyle (0\cup 1)^{*}0^{\omega }.}$ 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 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 ${\displaystyle L(A)}$ is the limit language of ${\displaystyle L(A')}$. An ω-word is accepted by A if it will force A to visit final states infinitely often. Thus, infinitely many finite prefixes of this ω-word will be accepted by A'. Hence, ${\displaystyle L(A)}$ is a limit language of ${\displaystyle L(A')}$.

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.[2]

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.[3] This is in contrast to DFA minimization, which can be done in polynomial time.

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

• Bakhadyr Khoussainov; Anil Nerode (6 December 2012). Automata Theory and its Applications. Springer Science & Business Media. ISBN 978-1-4612-0171-7.
• Thomas, Wolfgang (1990). "Automata on infinite objects". In Van Leeuwen (ed.). Handbook of Theoretical Computer Science. Elsevier. pp. 133–164.

Wikimedia Commons has media related to Büchi automaton.

• "Finite-state Automata on Infinite Inputs" (PDF).
• Vardi, Moshe Y. "An automata-theoretic approach to linear temporal logic". CiteSeerX 10.1.1.125.8126.