Semi-deterministic büchi automaton
Encyclopedia
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 semi-deterministic Büchi automaton can be constructed
such that both recognize the same ω-language. But, a deterministic Büchi automaton may not exist for the same ω-language.
(Q,Σ,∆,Q0,F) is called semi-deterministic if Q has two disjoint partitions N and D such that F ⊆ D and, for every d ∈ D, automaton (D,Σ,∆,{d},F) is deterministic.
.
Suppose A=(Q,Σ,∆,Q0,F) is a Büchi automaton. Let Pr be a projection function which takes a set of states S and a symbol a ∈ Σ and returns set of states {q' | ∃q ∈ S and (q,a,q') ∈ ∆ }. The equivalent semi-deterministic Büchi automaton is A=(N ∪ D,Σ,∆',Q'0,F'), where
Note the structure of states and transitions of A′. States of A′ are partitioned into N and D. An N-state is defined as an element of the power set of states of A. A D-state is defined as a pair of elements of power set of states of A. The transition relation of A' is the union of four parts: ∆1, ∆2, ∆3, and ∆4. The ∆1-transitions only take A' from a N-state to a N-state. Only the ∆2-transitions can take A' from an N-state to a D-state. Note that only the ∆2-transitions can cause non-determinism in A' . The ∆3 and ∆4-transitions take A' from a D-state to a D-state. By construction, A' is a semi-deterministic Büchi automaton. The proof of L(A')=L(A) as follows.
For an ω-word w=a1,a2,... , let w(i,j) be the finite segment ai+1,...,aj-1,aj of w.
By definition of ∆2, L0 must be a singleton set. Let L0 = {s}. Due to definitions of ∆1 and ∆2, there exist a run prefix s0,...,sn-1,s of A on word w(0,n) such that sj ∈ Sj. Since ρ' is an accepting run of A' , some states in F' are visited infinitely often. Therefore, there exist a strictly increasing and infinite sequence of indexes i0,i1,... such that i0=0 and, for each j > 0, Lij=Rij and Lij≠∅. For all j > 0, let m = ij-ij-1. Due to definitions of ∆3 and ∆4, for every qm ∈ Lij, there exist a state q0 ∈ Lij-1 and a run segment q0,...,qm of A on the word segment w(n+ij-1,n+ij) such that, for some 0 < k ≤ m, qk ∈ F. We can organize the run segments collected so for via following definitions.
Now the above run segments will be put together to make an infinite accepting run of A. Consider a tree whose set of nodes is ∪j≥0 Lij × {j}. The root is (s,0) and parent of a node (q,j) is (predecessor(q,j), j-1).
This tree is infinite, finitely branching, and fully connected. Therefore, by König's lemma
, there exists an infinite path (q0,0),(q1,1),(q2,2),... in the tree. Therefore, following is an accepting run of A
Hence, w is accepted by A.
Lemma 1
In any run, A' can only once make a non-deterministic choice that is when it chooses to take a Δ2 transition and rest of the execution of A' is deterministic. Let n be such that it satisfies lemma 1. We make A' to take Δ2 transition at nth step. So, we define a run ρ'=S0,...,Sn-1,({qn},∅),(L1,R1),(L2,R2),... of A' on word w. We will show that ρ' is an accepting run. Li ≠ ∅ because there is an infinite run of A passing through qn. So, we are only left to show that Li=Ri occurs infinitely often. Suppose contrary then there exists an index m such that, for all i ≥ m, Li≠Ri. Let j > m such that qj+n ∈ F therefore qj+n ∈ Rj. By lemma 1, there exist k > j such that Lk = Pr({ qn },w(n,k+n)) = Pr({ qj+n },w(j+n,k+n)) ⊆ Rk. So, Lk=Rk.
A contradiction has been derived. Hence, ρ' is an accepting run and w ∈ L(A').
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 semi-deterministic Büchi automaton is a special type of Büchi automaton
Büchi automaton
In computer science and automata theory, a Büchi automaton is a type of ω-automaton, which extends a finite automaton to infinite inputs. It accepts an infinite input sequence iff there exists a run of the automaton that visits one of the final states infinitely often. Büchi automata recognize the...
. 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 semi-deterministic Büchi automaton can be constructed
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...
such that both recognize the same ω-language. But, a deterministic Büchi automaton may not exist for the same ω-language.
Formal definition
A Büchi automatonBüchi automaton
In computer science and automata theory, a Büchi automaton is a type of ω-automaton, which extends a finite automaton to infinite inputs. It accepts an infinite input sequence iff there exists a run of the automaton that visits one of the final states infinitely often. Büchi automata recognize the...
(Q,Σ,∆,Q0,F) is called semi-deterministic if Q has two disjoint partitions N and D such that F ⊆ D and, for every d ∈ D, automaton (D,Σ,∆,{d},F) is deterministic.
Transformation from a Büchi automaton
Any given Büchi automaton can be transformed into a semi-deterministic Büchi automaton that recognizes the same language, using following constructionAutomata construction
In automata theory, automata construction is an important mathematical technique used to demonstrate the existence of an automaton with a certain desired property...
.
Suppose A=(Q,Σ,∆,Q0,F) is a Büchi automaton. Let Pr be a projection function which takes a set of states S and a symbol a ∈ Σ and returns set of states {q' | ∃q ∈ S and (q,a,q') ∈ ∆ }. The equivalent semi-deterministic Büchi automaton is A=(N ∪ D,Σ,∆',Q'0,F'), where
- N = 2Q and D = 2Q×2Q
- Q'0 = {Q0}
- ∆' = ∆1 ∪ ∆2 ∪ ∆3 ∪ ∆4
- ∆1 = {( S, a, S' ) | S'=Pr(S,a) }
- ∆2 = {( S, a, ({q'},∅) ) | ∃q ∈ S and (q,a,q') ∈ ∆ }
- ∆3 = {( (L,R), a, (L',R') ) | L≠R and L'=Pr(L,a) and R'=(L'∩F)∪Pr(R,a) }
- ∆4 = {( (L,L), a, (L',R') ) | L'=Pr(L,a) and R'=(L'∩F) }
- F' = {(L,L) | L≠∅ }
Note the structure of states and transitions of A′. States of A′ are partitioned into N and D. An N-state is defined as an element of the power set of states of A. A D-state is defined as a pair of elements of power set of states of A. The transition relation of A' is the union of four parts: ∆1, ∆2, ∆3, and ∆4. The ∆1-transitions only take A' from a N-state to a N-state. Only the ∆2-transitions can take A' from an N-state to a D-state. Note that only the ∆2-transitions can cause non-determinism in A' . The ∆3 and ∆4-transitions take A' from a D-state to a D-state. By construction, A' is a semi-deterministic Büchi automaton. The proof of L(A')=L(A) as follows.
For an ω-word w=a1,a2,... , let w(i,j) be the finite segment ai+1,...,aj-1,aj of w.
L(A') ⊆ L(A)
Proof: Let w ∈ L(A'). The initial state of A' is an N-state and all the accepting states in F' are D-states. Therefore, any accepting run of A' must follow ∆1 for finitely many transitions at start, then take a transition in ∆2 to move into D-states, and then take ∆3 and ∆4 transitions for ever. Let ρ' = S0,...,Sn-1,(L0,R0),(L1,R1),... be such accepting run of A' on w.By definition of ∆2, L0 must be a singleton set. Let L0 = {s}. Due to definitions of ∆1 and ∆2, there exist a run prefix s0,...,sn-1,s of A on word w(0,n) such that sj ∈ Sj. Since ρ' is an accepting run of A' , some states in F' are visited infinitely often. Therefore, there exist a strictly increasing and infinite sequence of indexes i0,i1,... such that i0=0 and, for each j > 0, Lij=Rij and Lij≠∅. For all j > 0, let m = ij-ij-1. Due to definitions of ∆3 and ∆4, for every qm ∈ Lij, there exist a state q0 ∈ Lij-1 and a run segment q0,...,qm of A on the word segment w(n+ij-1,n+ij) such that, for some 0 < k ≤ m, qk ∈ F. We can organize the run segments collected so for via following definitions.
- Let predecessor(qm,j) = q0.
- Let run(s,0)= s0,...,sn-1,s and, for j > 0, run(qm,j)= q1,...,qm
Now the above run segments will be put together to make an infinite accepting run of A. Consider a tree whose set of nodes is ∪j≥0 Lij × {j}. The root is (s,0) and parent of a node (q,j) is (predecessor(q,j), j-1).
This tree is infinite, finitely branching, and fully connected. Therefore, by König's lemma
König's lemma
König's lemma or König's infinity lemma is a theorem in graph theory due to Dénes Kőnig . It gives a sufficient condition for an infinite graph to have an infinitely long path. The computability aspects of this theorem have been thoroughly investigated by researchers in mathematical logic,...
, there exists an infinite path (q0,0),(q1,1),(q2,2),... in the tree. Therefore, following is an accepting run of A
- run(q0,0)⋅run(q1,1)⋅run(q2,2)⋅...
Hence, w is accepted by A.
L(A) ⊆ L(A')
Proof: The definition of projection function Pr can be extended such that in the second argument it can accept a finite word. For some set of states S, finite word w, and symbol a, let Pr(S,aw) = Pr(Pr(S,a),w) and Pr(S,ε) = S. Let w ∈ L(A) and ρ=q0,q1,... be an accepting run of A on w. First, we will prove following useful lemma.Lemma 1
- There is an index n such that qn ∈ F and, for all m ≥ n there exist a k > m, such that Pr({ qn },w(n,k)) = Pr({ qm },w(m,k)).
- Proof: Pr({ qn },w(n,k)) ⊇ Pr({ qm },w(m,k)) holds because there is a path from qn to qm. We will prove the converse by contradiction. Lets assume for all n, there is a m ≥ n such that for all k > m, Pr({ qn },w(n,k)) ⊃ Pr({ qm },w(m,k)) holds. Lets suppose p is the number of states in A. Therefore, there is a strictly increasing sequence of indexes n0,n1,... ,np such that, for all k > np, Pr({ qni },w(ni,k)) ⊃ Pr({ qni+1 },w(ni+1,k)). Therefore,Pr({ qnp },w(np,k)) = ∅. Contradiction.
In any run, A' can only once make a non-deterministic choice that is when it chooses to take a Δ2 transition and rest of the execution of A' is deterministic. Let n be such that it satisfies lemma 1. We make A' to take Δ2 transition at nth step. So, we define a run ρ'=S0,...,Sn-1,({qn},∅),(L1,R1),(L2,R2),... of A' on word w. We will show that ρ' is an accepting run. Li ≠ ∅ because there is an infinite run of A passing through qn. So, we are only left to show that Li=Ri occurs infinitely often. Suppose contrary then there exists an index m such that, for all i ≥ m, Li≠Ri. Let j > m such that qj+n ∈ F therefore qj+n ∈ Rj. By lemma 1, there exist k > j such that Lk = Pr({ qn },w(n,k+n)) = Pr({ qj+n },w(j+n,k+n)) ⊆ Rk. So, Lk=Rk.
A contradiction has been derived. Hence, ρ' is an accepting run and w ∈ L(A').