Misplaced Pages

Semi-deterministic Büchi automaton

Article snapshot taken from Wikipedia with creative commons attribution-sharealike license. Give it a read and then ask your questions in the chat. We can research this topic together.
This article needs additional citations for verification. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed.
Find sources: "Semi-deterministic Büchi automaton" – news · newspapers · books · scholar · JSTOR (November 2016) (Learn how and when to remove this message)

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,Σ,∆,Q0,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,Σ,∆,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 = 2 and D = 2×2
  • 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) 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, 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, 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 ρ=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').

References

  1. Courcoubetis, Costas; Yannakakis, Mihalis (July 1995). "The Complexity of Probabilistic Verification". J. ACM. 42 (4): 857–907. doi:10.1145/210332.210339. ISSN 0004-5411. S2CID 17872656.
  2. Sickert, Salomon; Esparza, Javier; Jaax, Stefan; Křetínský, Jan (2016). Chaudhuri, Swarat; Farzan, Azadeh (eds.). "Limit-Deterministic Büchi Automata for Linear Temporal Logic". Computer Aided Verification. Lecture Notes in Computer Science. 9780. Springer International Publishing: 312–332. doi:10.1007/978-3-319-41540-6_17. ISBN 978-3-319-41540-6.
Category: