Menu
Home
People
Places
Arts
History
Plants & Animals
Science
Life & Culture
Technology
Reference.org
Büchi automaton
open-in-new
<h2 id="formal-definition">Formal definition</h2> <p>Formally, a deterministic Büchi automaton is a tuple <i>A</i> = (<i>Q</i>,Σ,δ,<i>q</i>0,F) that consists of the following components: </p> <ul><li><i>Q</i> is a <a href="/facts/Finite_set/za1newlP">finite set</a>. The elements of <i>Q</i> are called the <i>states</i> of <i>A</i>.</li> <li>Σ is a finite set called the <i>alphabet</i> of <i>A</i>.</li> <li>δ: <i>Q</i> × Σ → <i>Q</i> is a function, called the <i>transition function</i> of <i>A</i>.</li> <li><i>q</i>0 is an element of <i>Q</i>, called the <i>initial state</i> of <i>A</i>.</li> <li>F⊆<i>Q</i> is the <i>acceptance condition</i>. <i>A</i> accepts exactly those runs in which at least one of the infinitely often occurring states is in F.</li></ul> <p>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 <i>q</i>0 is replaced by a set <i>I</i> of initial states. Generally, the term Büchi automaton without qualifier refers to non-deterministic Büchi automata. </p><p>For more comprehensive formalism see also <a href="/facts/%25CE%25A9-automaton/wXtY3hVu">ω-automaton</a>. </p> <h2 id="closure-properties">Closure properties</h2> <p>The set of Büchi automata is <a href="/facts/Closed_under/Ct6r2fJz">closed under</a> the following operations. </p><p>Let A = ( Q A , Σ , Δ A , I A , F A ) {\displaystyle \scriptstyle A=(Q_{A},\Sigma ,\Delta _{A},I_{A},{F}_{A})} and B = ( Q B , Σ , Δ B , I B , F B ) {\displaystyle \scriptstyle B=(Q_{B},\Sigma ,\Delta _{B},I_{B},{F}_{B})} be Büchi automata and C = ( Q C , Σ , Δ C , I C , F C ) {\displaystyle \scriptstyle C=(Q_{C},\Sigma ,\Delta _{C},I_{C},{F}_{C})} be a <a href="/facts/Finite_automaton/GMusWd0a">finite automaton</a>. </p> <ul><li>Union: <i>There is a Büchi automaton that recognizes the language L ( A ) ∪ L ( B ) . {\displaystyle \scriptstyle L(A)\cup L(B).} </i></li></ul> Proof: If we assume, <i><a href="/facts/W.l.o.g./gVP4dmEe">w.l.o.g.</a></i>, Q A ∩ Q B {\displaystyle \scriptstyle Q_{A}\cap Q_{B}} is empty then L ( A ) ∪ L ( B ) {\displaystyle \scriptstyle 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 \scriptstyle (Q_{A}\cup Q_{B},\Sigma ,\Delta _{A}\cup \Delta _{B},I_{A}\cup I_{B},{F}_{A}\cup {F}_{B}).} <ul><li>Intersection: <i>There is a Büchi automaton that recognizes the language L ( A ) ∩ L ( B ) . {\displaystyle \scriptstyle L(A)\cap L(B).} </i></li></ul> Proof: The Büchi automaton A ′ = ( Q ′ , Σ , Δ ′ , I ′ , F ′ ) {\displaystyle \scriptstyle A'=(Q',\Sigma ,\Delta ',I',F')} recognizes L ( A ) ∩ L ( B ) , {\displaystyle \scriptstyle L(A)\cap L(B),} where <ul><li> Q ′ = Q A × Q B × { 1 , 2 } {\displaystyle \scriptstyle Q'=Q_{A}\times Q_{B}\times \{1,2\}} </li> <li> Δ ′ = Δ 1 ∪ Δ 2 {\displaystyle \scriptstyle \Delta '=\Delta _{1}\cup \Delta _{2}} <ul><li> Δ 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 \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\}} </li> <li> Δ 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 \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\}} </li></ul></li> <li> I ′ = I A × I B × { 1 } {\displaystyle \scriptstyle I'=I_{A}\times I_{B}\times \{1\}} </li> <li> F ′ = { ( q A , q B , 2 ) | q B ∈ F B } {\displaystyle \scriptstyle F'=\{(q_{A},q_{B},2)|q_{B}\in F_{B}\}} </li></ul> By construction, r ′ = ( q A 0 , q B 0 , i 0 ) , ( q A 1 , q B 1 , i 1 ) , … {\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 <i>w</i> if r A = q A 0 , q A 1 , … {\displaystyle \scriptstyle r_{A}=q_{A}^{0},q_{A}^{1},\dots } is run of A on <i>w</i> and r B = q B 0 , q B 1 , … {\displaystyle \scriptstyle r_{B}=q_{B}^{0},q_{B}^{1},\dots } is run of B on <i>w</i>. r A {\displaystyle \scriptstyle r_{A}} is accepting and r B {\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'. <ul><li>Concatenation: <i>There is a Büchi automaton that recognizes the language L ( C ) ⋅ L ( A ) . {\displaystyle \scriptstyle L(C)\cdot L(A).} </i></li></ul> Proof: If we assume, <i>w.l.o.g.</i>, Q C ∩ Q A {\displaystyle \scriptstyle Q_{C}\cap Q_{A}} is empty then the Büchi automaton A ′ = ( Q C ∪ Q A , Σ , Δ ′ , I ′ , F A ) {\displaystyle \scriptstyle A'=(Q_{C}\cup Q_{A},\Sigma ,\Delta ',I',F_{A})} recognizes L ( C ) ⋅ L ( A ) {\displaystyle \scriptstyle L(C)\cdot L(A)} , where <ul><li> Δ ′ = Δ A ∪ Δ C ∪ { ( q , a , q ′ ) | q ′ ∈ I A and ∃ f ∈ F C . ( q , a , f ) ∈ Δ C } {\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}\}} </li> <li> if I C ∩ F C is empty then I ′ = I C otherwise I ′ = I C ∪ I A {\displaystyle \scriptstyle {\text{ if }}I_{C}\cap F_{C}{\text{ is empty then }}I'=I_{C}{\text{ otherwise }}I'=I_{C}\cup I_{A}} </li></ul> <ul><li>ω-closure: <i>If L ( C ) {\displaystyle \scriptstyle L(C)} does not contain the empty word then there is a Büchi automaton that recognizes the language L ( C ) ω . {\displaystyle \scriptstyle L(C)^{\omega }.} </i></li></ul> Proof: The Büchi automaton that recognizes L ( C ) ω {\displaystyle \scriptstyle L(C)^{\omega }} is constructed in two stages. First, we construct a finite automaton A' such that A' also recognizes L ( C ) {\displaystyle \scriptstyle L(C)} but there are no incoming transitions to initial states of A'. So, A ′ = ( Q C ∪ { q new } , Σ , Δ ′ , { q new } , F C ) , {\displaystyle \scriptstyle 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 \scriptstyle \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 \scriptstyle L(C)=L(A')} because L ( C ) {\displaystyle \scriptstyle L(C)} does not contain the empty string. Second, we will construct the Büchi automaton A" that recognize L ( C ) ω {\displaystyle \scriptstyle L(C)^{\omega }} by adding a loop back to the initial state of A'. So, A ″ = ( Q C ∪ { q new } , Σ , Δ ″ , { q new } , { q new } ) {\displaystyle \scriptstyle 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 \scriptstyle \Delta ''=\Delta '\cup \{(q,a,q_{\text{new}})|\exists q'\in F_{C}.(q,a,q')\in \Delta '\}.} <ul><li>Complementation:<i>There is a Büchi automaton that recognizes the language Σ ω / L ( A ) . {\displaystyle \scriptstyle \Sigma ^{\omega }/L(A).} </i></li></ul> Proof: The proof is presented <a href="/facts/Complementation_of_B%25C3%25BCchi_automaton/5jpnnL6h">here</a>. <h2 id="recognizable-languages">Recognizable languages</h2> <p>Büchi automata recognize the <a href="/facts/%25CE%25A9-regular_language/P20uz0Dd">ω-regular languages</a>. 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 <a href="/facts/%25CE%25A9-regular_language/P20uz0Dd">construction of a ω-regular language</a> for a Büchi automaton. </p> <h3>Deterministic versus non-deterministic Büchi automata</h3> <p>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 ω {\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 <i>A</i> is a deterministic Büchi automaton that recognizes ( 0 ∪ 1 ) ∗ 0 ω {\displaystyle (0\cup 1)^{*}0^{\omega }} with final state set <i>F</i>. <i>A</i> accepts 0 ω {\displaystyle 0^{\omega }} . So, <i>A</i> will visit some state in <i>F</i> after reading some finite prefix of 0 ω {\displaystyle 0^{\omega }} , say after the i 0 {\displaystyle i_{0}} th letter. <i>A</i> also accepts the ω-word 0 i 0 10 ω . {\displaystyle 0^{i_{0}}10^{\omega }.} Therefore, for some i 1 {\displaystyle i_{1}} , after the prefix 0 i 0 10 i 1 {\displaystyle 0^{i_{0}}10^{i_{1}}} the automaton will visit some state in <i>F</i>. Continuing with this construction the ω-word 0 i 0 10 i 1 10 i 2 … {\displaystyle 0^{i_{0}}10^{i_{1}}10^{i_{2}}\dots } is generated which causes A to visit some state in <i>F</i> infinitely often and the word is not in ( 0 ∪ 1 ) ∗ 0 ω . {\displaystyle (0\cup 1)^{*}0^{\omega }.} Contradiction. </p><p>The class of languages recognizable by deterministic Büchi automata is characterized by the following lemma. </p> Lemma: <i>An ω-language is recognizable by a deterministic Büchi automaton if it is the <a href="/facts/Omega_language/sJwjxW2U">limit language</a> of some <a href="/facts/Regular_language/ahxw67T1">regular language</a>.</i> 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 ) {\displaystyle L(A)} is the limit language of L ( A ′ ) {\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, L ( A ) {\displaystyle L(A)} is a limit language of L ( A ′ ) {\displaystyle L(A')} . <h2 id="algorithms">Algorithms</h2> <p><a href="/facts/Model_checking/FwvKMlw9">Model checking</a> 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. </p> Determinization <p>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, <a href="/facts/McNaughton%2527s_Theorem/w4TnLN1Q">McNaughton's Theorem</a> and Safra's construction provide algorithms that can translate a Büchi automaton into a deterministic <a href="/facts/Muller_automaton/J7qbapPG">Muller automaton</a> or deterministic <a href="/facts/Rabin_automaton/wXtY3hVu">Rabin automaton</a>.<a class="footnote-ref" id="fnref:2" href="#fn:2"><sup>2</sup></a> </p> Emptiness checking <p>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. </p><p>An effective algorithm that can check emptiness of a Büchi automaton: </p> <ol><li>Consider the automaton as a <a href="/facts/Directed_graph/YBdfQ0um">directed graph</a> and decompose it into <a href="/facts/Strongly_connected_component/P6rBqb7W">strongly connected components</a> (SCCs).</li> <li>Run a search (e.g., the <a href="/facts/Depth-first_search/luxJKVph">depth-first search</a>) to find which SCCs are reachable from the initial state.</li> <li>Check whether there is a non-trivial SCC that is reachable and contains a final state.</li></ol> <p>Each of the steps of this algorithm can be done in time linear in the automaton size, hence the algorithm is clearly optimal. </p> Minimization <p>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.<a class="footnote-ref" id="fnref:3" href="#fn:3"><sup>3</sup></a> This is in contrast to <a href="/facts/DFA_minimization/qASLWje9">DFA minimization</a>, which can be done in polynomial time. </p> <h2 id="variants">Variants</h2> <ul><li><a href="/facts/Co-B%25C3%25BCchi_automaton/zR2k8RAD">Co-Büchi automaton</a></li> <li><a href="/facts/Weak_B%25C3%25BCchi_automaton/LgCTMvlT">Weak Büchi automaton</a></li> <li><a href="/facts/Semi-deterministic_B%25C3%25BCchi_automaton/FvGsHrXm">Semi-deterministic Büchi automaton</a></li> <li><a href="/facts/Generalized_B%25C3%25BCchi_automaton/Hz9uLoK4">Generalized Büchi automaton</a></li></ul> <h2 id="transforming-from-other-models-of-description-to-non-deterministic-bchi-automata">Transforming from other models of description to non-deterministic Büchi automata</h2> <h3>From <a href="/facts/Generalized_B%25C3%25BCchi_automaton/Hz9uLoK4">generalized Büchi automata</a> (GBA)</h3> 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 <i>A</i> = (Q,Σ,∆,q0,{F1,...,Fn}) is a GBA, where F1,...,Fn are sets of accepting states then the equivalent Büchi automaton is <i>A'</i> = (Q', Σ, ∆',q'0,F'), where <ul><li>Q' = Q × {1,...,n}</li> <li>q'0 = ( q0,1 )</li> <li>∆' = { ( (q,i), a, (q',j) ) | (q,a,q') ∈ ∆ and if q ∈ Fi then j=((i+1) mod n) else j=i }</li> <li>F'=F1× {1}</li></ul> <h3>From <a href="/facts/Linear_temporal_logic/Gh5yxXK7">Linear temporal logic</a> formula</h3> A translation from a Linear temporal logic formula to a generalized Büchi automaton is given <a href="/facts/Linear_temporal_logic_to_B%25C3%25BCchi_automaton/7LsWGyy5">here</a>. And, a translation from a generalized Büchi automaton to a Büchi automaton is presented above. <h3>From <a href="/facts/Muller_automaton/J7qbapPG">Muller automata</a></h3> A given Muller automaton can be transformed into an equivalent Büchi automaton with the following automata construction. Let's suppose <i>A</i> = (Q,Σ,∆,Q0,{F0,...,Fn}) is a Muller automaton, where F0,...,Fn are sets of accepting states. An equivalent Büchi automaton is <i>A'</i> = (Q', Σ, ∆',Q0,F'), where <ul><li>Q' = Q ∪ ∪ni=0 {i} × Fi × 2Fi</li> <li>∆'= ∆ ∪ ∆1 ∪ ∆2, where <ul><li>∆1 ={ ( q, a, (i,q',∅) ) | (q, a, q') ∈ ∆ and q' ∈ Fi }</li> <li>∆2={ ( (i,q,R), a, (i,q',R') ) | (q,a,q')∈∆ and q,q' ∈ Fi and if R=Fi then R'= ∅ otherwise R'=R∪{q} }</li></ul></li> <li>F'=∪ni=0 {i} × Fi × {Fi}</li></ul> <i>A' </i> keeps original set of states from <i>A</i> and adds extra states on them. The Büchi automaton <i>A' </i> simulates the Muller automaton <i>A</i> as follows: At the beginning of the input word, the execution of <i>A'</i> follows the execution of <i>A</i>, since initial states are same and ∆' contains ∆. At some non-deterministically chosen position in the input word, <i>A' </i> decides of jump into newly added states via a transition in ∆1. Then, the transitions in ∆2 try to visit all the states of <i>Fi</i> and keep growing <i>R</i>. Once <i>R</i> becomes equal to <i>Fi</i> then it is reset to the empty set and ∆2 try to visit all the states of <i>Fi</i> states again and again. So, if the states <i>R</i>=<i>Fi</i> are visited infinitely often then <i>A' </i> accepts corresponding input and so does <i>A</i>. This construction closely follows the first part of the proof of <a href="/facts/McNaughton%2527s_Theorem/w4TnLN1Q">McNaughton's Theorem</a>. <h3>From Kripke structures</h3> Let the given <a href="/facts/Kripke_structure/WYQk8U5T">Kripke structure</a> be defined by <i>M</i> = ⟨<i>Q</i>, <i>I</i>, <i>R</i>, <i>L</i>, <i>AP</i>⟩ where <i>Q</i> is the set of states, I is the set of initial states, <i>R</i> is a relation between two states also interpreted as an edge, <i>L</i> is the label for the state and <i>AP</i> are the set of atomic propositions that form <i>L</i>. The Büchi automaton will have the following characteristics: Q final = Q ∪ { init } {\displaystyle Q_{\text{final}}=Q\cup \{{\text{init}}\}} Σ = 2 A P {\displaystyle \Sigma =2^{AP}} I = { init } {\displaystyle I=\{{\text{init}}\}} F = Q ∪ { init } {\displaystyle F=Q\cup \{{\text{init}}\}} δ = q a → p {\displaystyle \delta =q{\overrightarrow {a}}p} if (<i>q</i>, <i>p</i>) belongs to <i>R</i> and <i>L</i>(<i>p</i>) = <i>a</i> and init a → {\displaystyle {\overrightarrow {a}}} <i>q</i> if <i>q</i> belongs to I and <i>L</i>(<i>q</i>) = <i>a</i>. 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. <h2 id="complementation">Complementation</h2> <p>In <a href="/facts/Automata_theory/Q6BmPv63">automata theory</a>, complementation of a Büchi automaton is the task of <a href="/facts/Complementation_of_automata/WBWDGUh3">complementing</a> a Büchi automaton, i.e., constructing another automaton that recognizes the complement of the <a href="/facts/%25CE%25A9-regular_language/P20uz0Dd">ω-regular language</a> recognized by the given Büchi automaton. Existence of algorithms for this construction proves that the set of ω-regular languages is <a href="/facts/Closed_under/Ct6r2fJz">closed under</a> complementation. </p><p>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.<a class="footnote-ref" id="fnref:4" href="#fn:4"><sup>4</sup></a> Later, other constructions were developed that enabled efficient and optimal complementation.<a class="footnote-ref" id="fnref:5" href="#fn:5"><sup>5</sup></a><a class="footnote-ref" id="fnref:6" href="#fn:6"><sup>6</sup></a><a class="footnote-ref" id="fnref:7" href="#fn:7"><sup>7</sup></a><a class="footnote-ref" id="fnref:8" href="#fn:8"><sup>8</sup></a><a class="footnote-ref" id="fnref:9" href="#fn:9"><sup>9</sup></a> </p> <h3>Büchi's construction</h3> <p>Büchi presented<a class="footnote-ref" id="fnref:10" href="#fn:10"><sup>10</sup></a> a doubly exponential complement construction in a logical form. Here, we have his construction in the modern notation used in automata theory. Let <i>A</i> = (<i>Q</i>,Σ,Δ,<i>Q</i>0,F) be a Büchi automaton. Let ~<i>A</i> be an equivalence relation over elements of Σ+ such that for each <i>v,w</i> ∈ Σ+, <i>v</i> ~<i>A</i> <i>w</i> if and only if for all <i>p,q</i> ∈ <i>Q</i>, <i>A</i> has a run from <i>p</i> to <i>q</i> over <i>v</i> if and only if this is possible over <i>w</i> and furthermore <i>A</i> has a run via F from <i>p</i> to <i>q</i> over <i>v</i> if and only if this is possible over <i>w</i>. Each class of ~<i>A</i> defines a map <i>f</i>:<i>Q</i> → 2<i>Q</i> × 2<i>Q</i> in the following way: for each state <i>p</i> ∈ <i>Q</i>, we have (<i>Q</i>1,<i>Q</i>2)= <i>f</i>(<i>p</i>), where <i>Q</i>1 = {<i>q</i> ∈ <i>Q</i> | <i>w</i> can move automaton <i>A</i> from <i>p</i> to <i>q</i>} and <i>Q</i>2 = {<i>q</i> ∈ <i>Q</i> | <i>w</i> can move automaton <i>A</i> from <i>p</i> to <i>q</i> via a state in F}. Note that <i>Q</i>2 ⊆ <i>Q</i>1. If <i>f</i> is a map definable in this way, we denote the (unique) class defining <i>f</i> by <i>L</i><i>f</i>. </p><p>The following three theorems provide a construction of the complement of <i>A</i> using the equivalence classes of ~<i>A</i>. </p><p>Theorem 1: ~<i>A</i> has finitely many equivalent classes and each class is a <a href="/facts/Regular_language/ahxw67T1">regular language</a>. Proof: Since there are finitely many <i>f</i>:<i>Q</i> → 2<i>Q</i> × 2<i>Q</i>, the relation ~<i>A</i> has finitely many equivalence classes. Now we show that <i>L</i><i>f</i> is a regular language. For <i>p</i>,<i>q</i> ∈ <i>Q</i> and <i>i</i> ∈ {0,1}, let <i>A</i><i>i</i>,<i>p</i>,<i>q</i> = ( {0,1}×<i>Q</i>, Σ, Δ1∪Δ2, {(0,<i>p</i>)}, {(<i>i</i>,<i>q</i>)} ) be a <a href="/facts/Nondeterministic_finite_automaton/fW600oAl">nondeterministic finite automaton</a>, where Δ1 = { ((0,<i>q</i>1),(0,<i>q</i>2)) | (<i>q</i>1,<i>q</i>2) ∈ Δ} ∪ { ((1,<i>q</i>1),(1,<i>q</i>2)) | (<i>q</i>1,<i>q</i>2) ∈ Δ}, and Δ2 = { ((0,<i>q</i>1),(1,<i>q</i>2)) | <i>q</i>1 ∈ F ∧ (<i>q</i>1,<i>q</i>2) ∈ Δ }. Let Q' ⊆ <i>Q</i>. Let α<i>p</i>,Q' = ∩{ <i>L</i>(<i>A</i>1,<i>p</i>,<i>q</i>) | <i>q</i> ∈ Q'}, which is the set of words that can move <i>A</i> from <i>p</i> to all the states in Q' via some state in F. Let β<i>p</i>,Q' = ∩{ <i>L</i>(<i>A</i>0,<i>p</i>,<i>q</i>)-<i>L</i>(<i>A</i>1,<i>p</i>,<i>q</i>)-{ε} | <i>q</i> ∈ Q'}, which is the set of non-empty words that can move <i>A</i> from <i>p</i> to all the states in Q' and does not have a run that passes through any state in F. Let γ<i>p</i>,Q' = ∩{ Σ+-<i>L</i>(<i>A</i>0,<i>p</i>,<i>q</i>) | <i>q</i> ∈ Q'}, which is the set of non-empty words that cannot move <i>A</i> from <i>p</i> to any of the states in Q'. Since the regular languages are closed under finite intersections and under relative complements, every α<i>p</i>,Q', β<i>p</i>,Q', and γ<i>p</i>,Q' is regular. By definitions, <i>L</i><i>f</i> = ∩{ α<i>p</i>,<i>Q</i>2∩ β<i>p</i>,<i>Q</i>1-<i>Q</i>2∩ γ<i>p</i>,<i>Q</i>-<i>Q</i>1 | (<i>Q</i>1,<i>Q</i>2)=<i>f</i>(<i>p</i>) ∧ <i>p</i> ∈ <i>Q</i>}. </p><p>Theorem 2: For each <i>w</i> ∈ Σω, there are ~<i>A</i> classes <i>L</i><i>f</i> and <i>L</i><i>g</i> such that <i>w</i> ∈ <i>L</i><i>f</i>(<i>L</i><i>g</i>)ω. Proof: We will use the <a href="/facts/Ramsey%2527s_Theorem/VS6K8jGk">infinite Ramsey theorem</a> to prove this theorem. Let <i>w</i> =<i>a</i>0<i>a</i>1... and <i>w</i>(<i>i</i>,<i>j</i>) = <i>a</i><i>i</i>...<i>a</i><i>j</i>-1. Consider the set of natural numbers N. Let equivalence classes of ~<i>A</i> be the colors of subsets of N of size 2. We assign the colors as follows. For each <i>i</i> < <i>j</i>, let the color of {<i>i</i>,<i>j</i>} be the equivalence class in which <i>w</i>(<i>i</i>,<i>j</i>) occurs. By the infinite Ramsey theorem, we can find an infinite set <i>X</i> ⊆ N such that each subset of <i>X</i> of size 2 has same color. Let 0 < <i>i</i>0 < <i>i</i>1 < <i>i</i>2 .... ∈ <i>X</i>. Let <i>f</i> be a defining map of an equivalence class such that <i>w</i>(0,<i>i</i>0) ∈ <i>L</i><i>f</i>. Let <i>g</i> be a defining map of an equivalence class such that for each <i>j</i>>0,<i>w</i>(<i>i</i><i>j</i>-1,<i>i</i><i>j</i>) ∈ <i>L</i><i>g</i>. Then <i>w</i> ∈ <i>L</i><i>f</i>(<i>L</i><i>g</i>)ω. </p><p>Theorem 3: Let <i>L</i><i>f</i> and <i>L</i><i>g</i> be equivalence classes of ~<i>A</i>. Then <i>L</i><i>f</i>(<i>L</i><i>g</i>)ω is either a subset of <i>L</i>(<i>A</i>) or disjoint from <i>L</i>(<i>A</i>). Proof: Suppose there is a word <i>w</i> ∈ <i>L</i>(<i>A</i>) ∩ <i>L</i><i>f</i>(<i>L</i><i>g</i>)ω, otherwise the theorem holds trivially. Let <i>r</i> be an accepting run of <i>A</i> over input <i>w</i>. We need to show that each word w' ∈ <i>L</i><i>f</i>(<i>L</i><i>g</i>)ω is also in <i>L</i>(<i>A</i>), i.e., there exists a run r' of <i>A</i> over input w' such that a state in F occurs in r' infinitely often. Since <i>w</i> ∈ <i>L</i><i>f</i>(<i>L</i><i>g</i>)ω, let <i>w</i>0w1<i>w</i>2... = <i>w</i> such that <i>w</i>0 ∈ <i>L</i><i>f</i> and for each <i>i</i> > 0, <i>w</i><i>i</i> ∈ <i>L</i><i>g</i>. Let <i>s</i><i>i</i> be the state in <i>r</i> after consuming <i>w</i>0...<i>w</i><i>i</i>. Let <i>I</i> be a set of indices such that <i>i</i> ∈ <i>I</i> if and only if the run segment in <i>r</i> from <i>s</i><i>i</i> to <i>s</i><i>i</i>+1 contains a state from F. <i>I</i> must be an infinite set. Similarly, we can split the word w'. Let w'0w'1w'2... = w' such that w'0 ∈ <i>L</i><i>f</i> and for each <i>i</i> > 0, w'<i>i</i> ∈ <i>L</i><i>g</i>. We construct r' inductively in the following way. Let the first state of r' be same as <i>r</i>. By definition of <i>L</i><i>f</i>, we can choose a run segment on word w'0 to reach <i>s</i>0. By induction hypothesis, we have a run on w'0...w'<i>i</i> that reaches to <i>s</i><i>i</i>. By definition of <i>L</i><i>g</i>, we can extend the run along the word segment w'<i>i</i>+1 such that the extension reaches si+1 and visits a state in F if <i>i</i> ∈ <i>I</i>. The r' obtained from this process will have infinitely many run segments containing states from F, since <i>I</i> is infinite. Therefore, r' is an accepting run and w' ∈ <i>L</i>(<i>A</i>). </p><p>By the above theorems, we can represent Σω-<i>L</i>(<i>A</i>) as finite union of <a href="/facts/%25CE%25A9-regular_language/P20uz0Dd">ω-regular languages</a> of the form <i>L</i><i>f</i>(<i>L</i><i>g</i>)ω, where <i>L</i><i>f</i> and <i>L</i><i>g</i> are equivalence classes of ~<i>A</i>. Therefore, Σω-<i>L</i>(<i>A</i>) is an ω-regular language. We can <a href="/facts/%25CE%25A9-regular_language/P20uz0Dd">translate the language</a> into a Büchi automaton. This construction is doubly exponential in terms of size of <i>A</i>. </p> <ul><li>Bakhadyr Khoussainov; <a href="/facts/Anil_Nerode/5dfjh20g">Anil Nerode</a> (6 December 2012). <a href="https://books.google.com/books?id=wR_oBwAAQBAJ"><i>Automata Theory and its Applications</i></a>. Springer Science & Business Media. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 978-1-4612-0171-7.</li> <li>Thomas, Wolfgang (1990). "Automata on infinite objects". In Van Leeuwen (ed.). <i>Handbook of Theoretical Computer Science</i>. Elsevier. pp. 133–164.</li></ul> <h2 id="external-links">External links</h2> Wikimedia Commons has media related to Büchi automaton. <ul><li><a href="http://www.imsc.res.in/~madhavan/papers/pdf/tcs-96-2.pdf">"Finite-state Automata on Infinite Inputs"</a> (PDF).</li> <li><a href="/facts/Moshe_Y._Vardi/Sz9AoseQ">Vardi, Moshe Y.</a> "An automata-theoretic approach to linear temporal logic". <a href="/facts/CiteSeerX_(identifier)/SceDmd3c">CiteSeerX</a> <a href="https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.125.8126">10.1.1.125.8126</a>.</li></ul> <h2 id="references">References</h2> <ol> <li id="fn:1"><p>Büchi, J.R. (1962). "On a Decision Method in Restricted Second Order Arithmetic". The Collected Works of J. Richard Büchi. Stanford: Stanford University Press. pp. 425–435. doi:10.1007/978-1-4613-8928-6_23. ISBN 978-1-4613-8930-9. {{cite book}}: ISBN / Date incompatibility (help); |journal= ignored (help) <a href="978-1-4613-8930-9" target="_blank">978-1-4613-8930-9</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></p></li> <li id="fn:2"><p>Safra, S. (1988), "On the complexity of ω-automata", Proceedings of the 29th Annual Symposium on Foundations of Computer Science (FOCS '88), Washington DC, US: IEEE Computer Society, pp. 319–327, doi:10.1109/SFCS.1988.21948, ISBN 0-8186-0877-3, S2CID 206559211. <a href="0-8186-0877-3" target="_blank">0-8186-0877-3</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></p></li> <li id="fn:3"><p>Schewe, Sven (2010). "Minimisation of Deterministic Parity and Büchi Automata and Relative Minimisation of Deterministic Finite Automata". arXiv:1007.1333 [cs.FL]. <a href="/wiki/ArXiv_(identifier)" target="_blank">/wiki/ArXiv_(identifier)</a> <a href="#fnref:3" class="footnote-back-ref">↩</a></p></li> <li id="fn:4"><p>Büchi, J. R. (1962), "On a decision method in restricted second order arithmetic", Proc. International Congress on Logic, Method, and Philosophy of Science, Stanford, 1960, Stanford: Stanford University Press, pp. 1–12. <a href="/wiki/Julius_Richard_B%C3%BCchi" target="_blank">/wiki/Julius_Richard_B%C3%BCchi</a> <a href="#fnref:4" class="footnote-back-ref">↩</a></p></li> <li id="fn:5"><p>McNaughton, R. (1966), "Testing and generating infinite sequences by a finite automaton", Information and Control, 9 (5): 521–530, doi:10.1016/s0019-9958(66)80013-x. <a href="/wiki/Robert_McNaughton" target="_blank">/wiki/Robert_McNaughton</a> <a href="#fnref:5" class="footnote-back-ref">↩</a></p></li> <li id="fn:6"><p>Sistla, A. P.; Vardi, M. Y.; Wolper, P. (1987), "The complementation problem for Büchi automata with applications to temporal logic", Theoretical Computer Science, 49 (2–3): 217–237, doi:10.1016/0304-3975(87)90008-9. <a href="/wiki/Moshe_Vardi" target="_blank">/wiki/Moshe_Vardi</a> <a href="#fnref:6" class="footnote-back-ref">↩</a></p></li> <li id="fn:7"><p>Safra, S. (October 1988), "On the complexity of ω-automata", Proc. 29th IEEE Symposium on Foundations of Computer Science, White Plains, New York, pp. 319–327. <a href="/wiki/Shmuel_Safra" target="_blank">/wiki/Shmuel_Safra</a> <a href="#fnref:7" class="footnote-back-ref">↩</a></p></li> <li id="fn:8"><p>Kupferman, O.; Vardi, M. Y. (July 2001), "Weak alternating automata are not that weak", ACM Transactions on Computational Logic, 2 (3): 408–429, doi:10.1145/377978.377993. <a href="/wiki/Orna_Kupferman" target="_blank">/wiki/Orna_Kupferman</a> <a href="#fnref:8" class="footnote-back-ref">↩</a></p></li> <li id="fn:9"><p>Schewe, Sven (2009). Büchi Complementation Made Tight. STACS. <a href="https://inria.hal.science/inria-00360108/document" target="_blank">https://inria.hal.science/inria-00360108/document</a> <a href="#fnref:9" class="footnote-back-ref">↩</a></p></li> <li id="fn:10"><p>Büchi, J. R. (1962), "On a decision method in restricted second order arithmetic", Proc. International Congress on Logic, Method, and Philosophy of Science, Stanford, 1960, Stanford: Stanford University Press, pp. 1–12. <a href="/wiki/Julius_Richard_B%C3%BCchi" target="_blank">/wiki/Julius_Richard_B%C3%BCchi</a> <a href="#fnref:10" class="footnote-back-ref">↩</a></p></li> </ol>