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 A = ( Q , Σ , δ , q 0 , F ) {\textstyle A=(Q,\Sigma ,\delta ,q_{0},\mathbf {F} )} that consists of the following components: Q {\textstyle Q} is a finite set. The elements of Q {\textstyle Q} are called the states of A {\textstyle A} . Σ {\textstyle \Sigma } is a finite set called the alphabet of A {\textstyle A} . δ : Q × Σ → Q {\textstyle \delta \colon Q\times \Sigma \to Q} is a function, called the transition function of A {\textstyle A} . q 0 {\textstyle q_{0}} is an element of Q {\textstyle Q} , called the initial state of A {\textstyle A} . F ⊆ Q {\textstyle \mathbf {F} \subseteq Q} is the acceptance condition. A run i _ = i 0 i 1 i 2 ⋯ ∈ Σ ω {\displaystyle {\underline {i}}=i_{0}i_{1}i_{2}\cdots \in \Sigma ^{\omega }} is an infinite string of inputs of A {\displaystyle A} . By calling δ {\displaystyle \delta } recursively, we can extend it to a function δ ω : Σ ω → Q ω {\displaystyle \delta ^{\omega }:\Sigma ^{\omega }\to Q^{\omega }} . A state q ∈ Q {\displaystyle q\in Q} is said to occur infinitely often for a run i _ {\displaystyle {\underline {i}}} when the set { n ∈ N ∣ δ ω ( i _ ) n = q } {\displaystyle \{n\in \mathbb {N} \mid \delta ^{\omega }({\underline {i}})_{n}=q\}} is infinite. Let I n f ( i _ ) {\displaystyle \mathrm {Inf} ({\underline {i}})} be the set of states occurring infinitely often for i _ {\displaystyle {\underline {i}}} . The language of A {\displaystyle A} is then the set of runs of A {\displaystyle A} in which at least one of the infinitely-often occurring states is in F {\textstyle \mathbf {F} } ; in symbols: L ( A ) = { i _ ∈ Σ ω ∣ I n f ( i _ ) ∩ F ≠ ∅ } . {\displaystyle L(A)=\{{\underline {i}}\in \Sigma ^{\omega }\mid \mathrm {Inf} ({\underline {i}})\cap \mathbf {F} \neq \varnothing \}.} In a (non-deterministic) Büchi automaton, the transition function δ {\textstyle \delta } is replaced with a transition relation Δ {\textstyle \Delta } that returns a set of states, and the single initial state q 0 {\textstyle q_{0}} is replaced by a set I {\textstyle 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. == Closure properties == The set of Büchi automata is closed under the following operations. Let A = ( Q A , Σ , Δ A , I A , F A ) {\displaystyle A=(Q_{A},\Sigma ,\Delta _{A},I_{A},{F}_{A})} and B = ( Q B , Σ , Δ B , I B , F B ) {\displaystyle B=(Q_{B},\Sigma ,\Delta _{B},I_{B},{F}_{B})} be Büchi automata and C = ( Q C , Σ , Δ C , I C , F C ) {\displaystyle 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 L ( A ) ∪ L ( B ) . {\displaystyle L(A)\cup L(B).} Proof: If we assume, w.l.o.g., Q A ∩ Q B {\displaystyle Q_{A}\cap Q_{B}} is empty then L ( A ) ∪ L ( B ) {\displaystyle L(A)\cup L(B)} is recognized by the Büchi automaton ( Q A ∪ Q B , Σ ∪ Σ , Δ A ∪ Δ B , I A ∪ I B , F A ∪ F B ) . {\displaystyle (Q_{A}\cup Q_{B},\Sigma \cup \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 L ( A ) ∩ L ( B ) . {\displaystyle L(A)\cap L(B).} Proof: The Büchi automaton A ′ = ( Q ′ , Σ , Δ ′ , I ′ , F ′ ) {\displaystyle A'=(Q',\Sigma ,\Delta ',I',F')} recognizes L ( A ) ∩ L ( B ) , {\displaystyle L(A)\cap L(B),} where Q ′ = Q A × Q B × { 1 , 2 } {\displaystyle Q'=Q_{A}\times Q_{B}\times \{1,2\}} Δ ′ = Δ 1 ∪ Δ 2 {\displaystyle \Delta '=\Delta _{1}\cup \Delta _{2}} Δ 1 = { ( ( 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 } {\displaystyle \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\}} Δ 2 = { ( ( 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 } {\displaystyle \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\}} I ′ = I A × I B × { 1 } {\displaystyle I'=I_{A}\times I_{B}\times \{1\}} F ′ = { ( q A , q B , 2 ) | q B ∈ F B } {\displaystyle F'=\{(q_{A},q_{B},2)|q_{B}\in F_{B}\}} By construction, r ′ = ( q A 0 , q B 0 , i 0 ) , ( q A 1 , q B 1 , i 1 ) , … {\displaystyle 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 {\textstyle w} if r A = q A 0 , q A 1 , … {\displaystyle r_{A}=q_{A}^{0},q_{A}^{1},\dots } is run of A {\textstyle A} on w {\textstyle w} and r B = q B 0 , q B 1 , … {\displaystyle r_{B}=q_{B}^{0},q_{B}^{1},\dots } is run of B {\textstyle B} on w {\textstyle w} . r A {\textstyle r_{A}} is accepting and r B {\textstyle r_{B}} is accepting if r ′ {\textstyle 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 ′ {\textstyle r'} if r ′ {\textstyle r'} is accepted by A ′ {\textstyle A'} . Concatenation: There is a Büchi automaton that recognizes the language L ( C ) ⋅ L ( A ) . {\displaystyle L(C)\cdot L(A).} Proof: If we assume, w.l.o.g., Q C ∩ Q A {\displaystyle Q_{C}\cap Q_{A}} is empty then the Büchi automaton A ′ = ( Q C ∪ Q A , Σ , Δ ′ , I ′ , F A ) {\displaystyle A'=(Q_{C}\cup Q_{A},\Sigma ,\Delta ',I',F_{A})} recognizes L ( C ) ⋅ L ( A ) {\displaystyle L(C)\cdot L(A)} , where Δ ′ = Δ A ∪ Δ C ∪ { ( q , a , q ′ ) | q ′ ∈ I A and ∃ f ∈ F C . ( q , a , f ) ∈ Δ C } {\displaystyle \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}\}} if I C ∩ F C is empty then I ′ = I C otherwise I ′ = I C ∪ I A {\displaystyle {\text{ if }}I_{C}\cap F_{C}{\text{ is empty then }}I'=I_{C}{\text{ otherwise }}I'=I_{C}\cup I_{A}} ω-closure: If L ( C ) {\displaystyle L(C)} does not contain the empty word then there is a Büchi automaton that recognizes the language L ( C ) ω . {\displaystyle L(C)^{\omega }.} Proof: The Büchi automaton that recognizes L ( C ) ω {\displaystyle L(C)^{\omega }} is constructed in two stages. First, we construct a finite automaton A ′ {\textstyle A'} such that A ′ {\textstyle A'} also recognizes L ( C ) {\displaystyle L(C)} but there are no incoming transitions to initial states of A ′ {\textstyle A'} . So, A ′ = ( Q C ∪ { q new } , Σ , Δ ′ , { q new } , F C ) , {\displaystyle A'=(Q_{C}\cup \{q_{\text{new}}\},\Sigma ,\Delta ',\{q_{\text{new}}\},F_{C}),} where Δ ′ = Δ C ∪ { ( q new , a , q ′ ) | ∃ q ∈ I C . ( q , a , q ′ ) ∈ Δ C } . {\displaystyle \Delta '=\Delta _{C}\cup \{(q_{\text{new}},a,q')|\exists q\in I_{C}.(q,a,q')\in \Delta _{C}\}.} Note that L ( C ) = L ( A ′ ) {\displaystyle L(C)=L(A')} because L ( C ) {\displaystyle L(C)} does not contain the empty string. Second, we will construct the Büchi automaton A ″ {\textstyle A''} that recognize L ( C ) ω {\displaystyle L(C)^{\omega }} by adding a loop back to the initial state of A ′ {\textstyle A'} . So, A ″ = ( Q C ∪ { q new } , Σ , Δ ″ , { q new } , { q new } ) {\displaystyle A''=(Q_{C}\cup \{q_{\text{new}}\},\Sigma ,\Delta '',\{q_{\text{new}}\},\{q_{\text{new}}\})} , where Δ ″ = Δ ′ ∪ { ( q , a , q new ) | ∃ q ′ ∈ F C . ( q , a , q ′ ) ∈ Δ ′ } . {\displaystyle \Delta ''=\Delta '\cup \{(q,a,q_{\text{new}})|\exists q'\in F_{C}.(q,a,q')\in \Delta '\}.} Complementation:
Read more →
