# Semi-deterministic Büchi automaton

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, 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$_{ij}$=R$_{ij}$ and L$_{ij}$≠∅. For all j > 0, let m = i$_j$-i$_{j-1}$. Due to definitions of ∆$_3$ and ∆$_4$, for every q$_m$ ∈ L$_{ij}$, there exist a state q$_0$ ∈ L$_{ij-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 ≤ m, q$_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$_{ij}$ × {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$_{ni}$ },w(n$_i$,k)) ⊃ Pr({ q$_{ni+1}$ },w(n$_{i+1}$,k)). Therefore,Pr({ q$_{np}$ },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').