Overview
In automata theory, a semi-deterministic Büchi automaton (also known as Büchi automaton deterministic in the limit, or limit-deterministic Büchi automaton ) is a special type of Büchi automaton. In such an automaton, the set of states can be partitioned into two subsets: one subset forms a deterministic automaton and 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.
Motivation
In standard model checking against linear temporal logic (LTL) properties, it is sufficient to translate an LTL formula into a non-deterministic Büchi automaton. But, in probabilistic model checking, LTL formulae are typically translated into deterministic Rabin automata (DRA), as for instance in the PRISM tool. However, a fully deterministic automaton is not needed. Indeed, semi-deterministic Büchi automata are sufficient in probabilistic model checking.
Formal definition
A Büchi automaton (Q,Σ,∆,Q 0 ,F) is called semi-deterministic if Q is the union of two disjoint subsets N and D such that F ⊆ D and, for every d ∈ D, the 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 construction. Suppose A=(Q,Σ,∆,Q 0 ,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 = 2 Q and D = 2 Q ×2 Q * Q' 0 = Q 0 * ∆' = ∆ 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) follows. For an ω-word w=a 1 ,a 2 ,... , let w(i,j) be the finite segment a i+1 ,...,a j-1 ,a j 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 ρ' = S 0 ,...,S n-1 ,(L 0 ,R 0 ),(L 1 ,R 1 ),... be such accepting run of A' on w. By definition of ∆ 2 , L 0 must be a singleton set. Let L 0 = s . Due to definitions of ∆ 1 and ∆ 2 , there exist a run prefix s 0 ,...,s n-1 ,s of A on word w(0,n) such that s j ∈ S j . 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 i 0 ,i 1 ,... such that i 0 =0 and, for each j > 0, L i j =R i j and L i j ≠∅.
For all j > 0, let m = i j -i j-1 . Due to definitions of ∆ 3 and ∆ 4 , for every q m ∈ L i j , there exist a state q 0 ∈ L i j-1 and a run segment q 0 ,...,q m of A on the word segment w(n+i j-1 ,n+i j ) such that, for some 0 k ∈ F. We can organize the run segments collected so for via following definitions. * Let predecessor(q m ,j) = q 0 . * Let run(s,0)= s 0 ,...,s n-1 ,s and, for j > 0, run(q m ,j)= q 1 ,...,q m 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 L i j × 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 (q 0 ,0),(q 1 ,1),(q 2 ,2),... in the tree.
Therefore, following is an accepting run of A : run(q 0 ,0)⋅run(q 1 ,1)⋅run(q 2 ,2)⋅... Hence, by infinite pigeonhole principle, 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 ρ=q 0 ,q 1 ,... be an accepting run of A on w. First, we will prove following useful lemma. ;Lemma 1 :There is an index n such that q n ∈ F and, for all m ≥ n there exist a k > m, such that Pr( q n ,w(n,k)) = Pr( q m ,w(m,k)). :Proof: Pr( q n ,w(n,k)) ⊇ Pr( q m ,w(m,k)) holds because there is a path from q n to q m . We will prove the converse by contradiction.
Lets assume for all n, there is a m ≥ n such that for all k > m, Pr( q n ,w(n,k)) ⊃ Pr( q m ,w(m,k)) holds. Lets suppose p is the number of states in A. Therefore, there is a strictly increasing sequence of indexes n 0 ,n 1 ,... ,n p such that, for all k > n p , Pr( q n i ,w(n i ,k)) ⊃ Pr( q n i+1 ,w(n i+1 ,k)). Therefore,Pr( q n p ,w(n p ,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 ρ'=S 0 ,...,S n-1 ,( q n ,∅),(L 1 ,R 1 ),(L 2 ,R 2 ),... of A' on word w. We will show that ρ' is an accepting run.
L i ≠ ∅ because there is an infinite run of A passing through q n . So, we are only left to show that L i =R i occurs infinitely often. Suppose contrary then there exists an index m such that, for all i ≥ m, L i ≠R i . Let j > m such that q j+n ∈ F therefore q j+n ∈ R j . By lemma 1, there exist k > j such that L k = Pr( q n ,w(n,k+n)) = Pr( q j+n ,w(j+n,k+n)) ⊆ R k . So, L k =R k . A contradiction has been derived. Hence, ρ' is an accepting run and w ∈ L(A').