5. Principles of Model Checking. Baier_ Joost (2008) (5. Principles of Model Checking. Baier_ Joost (2008).pdf), страница 97

This modification of the refinement operator isnecessary to ensure that the decomposed blocks are stable with respect to C and C \ C.As before, the ternary refinement operator decomposes each block into subblocks:Refine(B, C, C \ C)Refine(Π, C, C \ C) =B∈ΠThe effect of the refinement operator Refine(B, C, C \ C) is schematically depicted forB ⊆ Pre(C ) in Figure 7.14.

Thus, every block B ∈ Π with B ⊆ Pre(C ) is decomposedB2CB1B3C+ \Cblock BFigure 7.14: Ternary refinement operator.into maximally three subblocks: states in B that only have direct successors in C, thosethat only have such direct successors in C , and the rest, i.e., states that have directsuccessors in both C and C . Formally:Refine(B, C, C \ C) = { B1 , B2 , B3 } \ { ∅ },whereB1 = B ∩ Pre(C) ∩ Pre(C \ C),B2 = (B ∩ Pre(C)) \ Pre(C \ C),B3 = (B ∩ Pre(C \ C)) \ Pre(C).Note that the blocks B1 , B2 , B3 are stable with respect to C and C \ C.If B ∩ Pre(C ) = ∅, then B is stable with respect to C and C \ C, in which caseRefine(B, C, C \ C) = { B }.

This suggests as loop invariant of the algorithm:each block B ∈ Π is stable with respect to all blocks in ΠoldBisimulation-Quotienting Algorithms489From this invariant it follows that only the two cases B ∩ Pre(C ) = ∅ and B ⊆ Pre(C )are possible.Algorithm 32 outlines the main steps of the improved partition refinement algorithm.To establish the aforementioned loop invariant, the initial partition is Refine(ΠAP , S),i.e., each block only contains equally-labeled states that are all either terminal or not.This is based on the observation that Pre(S) = { s ∈ S | s is nonterminal }.

Insteadof first computing ΠAP and then applying the refinement operator, Refine(ΠAP , S) canbe obtained by executing Algorithm 29 with AP extended with a special symbol whichidentifies nonterminal states. The initial partition can thus (as before) be determined intime Θ(|S| · |AP|).Algorithm 32 An improved partition refinement algorithmInput: finite transition system TS with state space SOutput: bisimulation quotient space S/∼Πold := { S };Π := Refine(ΠAP , S);(* similar to Algorithm 29, page 479 *)(* loop invariant: Π is coarser than S/∼ and finer than ΠAP and Πold , *)(* and Π is stable with respect to any block in Πold *)repeatΠold := Π;choose block C ∈ Πold \ Π and block C ∈ Π with C ⊆ C and |C| Π := Refine(Π, C, C \ C);until Π = Πoldreturn ΠExample 7.42.|C |2 ;Abstract Example of Algorithm 32Consider the quotienting of the transition system in Figure 7.15.

Since all black states areterminal, and all white states are not, we have ΠAP = Refine(ΠAP , S).In the first iteration, one may split with respect to the white or the black states. As|{ u1 , . . . , u8 , w1 , w2 , w3 }| > |S|2 , the set of white states is not a suitable splitter. In fact,the only splitter candidate is block C = { v1 , v2 }.Refine(ΠAP , { v1 , v2 }, { u1 , u2 , . . .

, u8 , w1 , w2 , w3 }) CC \C490Equivalences and AbstractionAPw1u1u2u6w2w3u7u8v2v1Figure 7.15: Example of a transition system.(with C = S), decomposes block B = { u1 , u2 , . . . , u6 , u7 , u8 , w1 , w2 , w3 } into= { u7 },B1 = B ∩ Pre(C) ∩ Pre(C \ C)B2 = (B ∩ Pre(C)) \ Pre(C \ C) = { u1 , u2 , .

. . , u6 } ∪ { u8 },B3 = (B ∩ Pre(C \ C)) \ Pre(C) = { w1 , w2 , w3 }.This yields Πold = { C, C \ C } and Π = { C, B1 , B2 , B3 }.In the second iteration, the blocks B1 = { u7 } and B3 = { w1 , w2 , w3 } are potentialsplitters. C is not considered as C ∈ Πold \ Π. Block B2 is not considered as splitter, sinceit is too large with respect to its superblock in Πold : |B2 | = 7 > 11/2 = |C 2\C| . SupposeB1 (called D) is selected as splitter; its superblock in Πold equals D = C \ C ∈ Πold .Figure 7.16 illustrates the partition obtained byRefine(Π, { u7 }, { u1 , .

. . , u6 , u8 , w1 , w2 , w3 }). =D=D \DThe blocks C = { v1 , v2 } and B2 remain unchanged, since they do not have any directsuccessor in D \ D. Block B3 is refined as follows:Refine({ w1 , w2 , w3 }, { u7 }, { u1 , . . . , u6 , u8 , w1 , w2 , w3 }) = { { w1 }, { w2 }, { w3 } }since w1 has only direct successors in D \ D, w2 can only move to D, and w3 can moveBisimulation-Quotienting Algorithms491w1u1u2u6w2w3u7u8v2v1Figure 7.16: Example for Algorithm 32.to D as well as to D \ D.

Thus, at the end of the second iteration:Π= {{ v1 , v2 }, { u7 }, { u1 , . . . , u6 , u8 }, { w1 }, { w2 }, { w3 }},Πold= {{ v1 , v2 }, { u7 }, { u1 , . . . , u6 , u8 , w1 , w2 , w3 }}. =C=D=D \DThe next refinement does not impose any further splittings, and Π = S/ ∼.Refine(Π, C, C \C) can be realized with time complexity O(|Pre(C)|+ |C|) provided everystate s ∈ Pre(C) causes the costs O(|Pre(s )| + 1). This can be established as follows.

Forevery pair (s, C ) with s ∈ Pre(C ), C ∈ Πold , a counter δ(s, C ) is introduced that keepstrack of the number of direct successors of s in C :δ(s, C ) = |Post(s) ∩ C | .During the execution of Refine(Π, C, C \ C), the values δ(s, C) and δ(s, C \ C) are computed for any s ∈ Pre(C) as follows:for all s ∈ C dofor all s ∈ Pre(s ) doδ(s, C) := δ(s, C) + 1;ododfor all s ∈ Pre(C) doδ(s, C \ C) := δ(s, C ) − δ(s, C);odwhere it is assumed that initially δ(s, C) = 0.492Equivalences and AbstractionLet B ∈ Π be a block with B ⊆ Pre(C ), which should be decomposed into B1 , B2 , B3 bymeans of Refine(B, C, C \ C). Then B1 , B2 , and B3 are obtained as follows:B1 = B ∩ Pre(C) ∩ Pre(C \ C) = { s ∈ B | δ(s, C) > 0, δ(s, C \ C) > 0 }B2 = B ∩ Pre(C) \ Pre(C \ C) = { s ∈ B | δ(s, C) > 0, δ(s, C \ C) = 0 }B3 = B ∩ Pre(C \ C) \ Pre(C) = { s ∈ B | δ(s, C) = 0, δ(s, C \ C) > 0 }The decomposition of block B ∈ Π is realized by ”moving” the states s ∈ Pre(C) fromblock B to block B1 or B2 .

The states remaining in B represent block B3 .The initial values δ(s, C) and δ(s, C \C) need only be determined for the states in Pre(C).The initial values of counters for s ∈ Pre(C )\Pre(C) are derived by δ(s, C \C) = δ(s, C ),and δ(s, C) = 0. For these states, the variable δ(s, C) is not needed. Variable δ(s, C ) forstate s ∈ Pre(C ) \ Pre(C) and block C can be identified with variable δ(s, C \ C) for thenew block C \ C.

These considerations lead to the following lemma:Lemma 7.43.Time Complexity of the Ternary Refinement OperatorThe time complexity of Refine(Π, C, C \ C) is in O(|Pre(C)| + |C|).As asserted by the following theorem, the time complexity of the improved quotientingalgorithm (see Algorithm 32) is logarithmic in the number of states.Theorem 7.44.Time Complexity of Algorithm 32The bisimulation quotient of a finite transition system TS = (S, Act, →, I, AP, L) can becomputed with Algorithm 32 in O (|S|·|AP| + M · log |S|).Proof: The time complexity of Algorithm 32 is bounded above byK(s) · (|Pre(s)| + 1)O |S| · |AP| +s∈Swhere K(s ) denotes the number of blocks C containing s for which Refine(Π, C .

. .) isinvoked.The first summand represents the asymptotic time needed to compute the initial partitionRefine(ΠAP , S). This partition can be computed in the same way as ΠAP by extendingthe set of atomic propositions with a new label that indicates the terminal states. Recallfrom Lemma 7.33 (page 480) that ΠAP can be computed in Θ(|S|·|AP|). The fact that anadditional atomic proposition is needed is not relevant.Bisimulation-Quotienting Algorithms493The second summand stands for the cost of the refinement steps; recall that state s ∈ Cinduces the costs O(|Pre(s)| + 1) on executing Refine(Π, C, C \ C), see Lemma 7.43 (page492).

This summand can be bounded from above as follows. We first observe thatK(s) log |S| + 1for any state s.This is proven as follows. Let s ∈ S and Ci be the ith block with s ∈ Ci , for whichRefine(Π, Ci , . . .) is executed. Then:|Ci+1 | |Ci |2and|C1 | |S|.Let K(s) = k. Then:1 |Ck | |Ck−2 ||Ck−i ||Ck−1 ||C1 ||S| ... . . . k−1 k−1242i22From this, we conclude 2k−1 |S|, or equivalently k−1 log |S|. This yields K(s) =k log |S| + 1.Let M = s∈S |Pre(s)| and assume that a representation of the sets Pre(·) can be obtainedin time O(M ). Thus:K(s ) · (|Pre(s )| + 1) (log |S| + 1)s ∈S(|Pre(s )| + 1)s ∈S= (log |S| + 1) · (M + |S|) 2 · (log |S| + 1) · M7.3.5= O(M · log |S|)Equivalence Checking of Transition SystemsThe partition refinement algorithms can be used to verify the bisimilarity of the finitetransition systems TS1 and TS2 . To that end, the bisimulation quotient space of thecomposite transition system TS = TS1 ⊕ TS2 (see page 457) is computed.

Subsequently,it is checked whetherC ∩ I1 = ∅if and only if C ∩ I2 = ∅for each bisimulation equivalence class C of the composite system TS. Here, Ii denotesthe set of initial states of TSi , i = 1, 2.494Equivalences and AbstractionCorollary 7.45.Complexity of Checking Bisimulation EquivalenceChecking whether TS1 ∼ TS2 for finite transition systems TS1 and TS2 over AP with thestate spaces S1 and S2 , respectively, can be performed in timeO ((|S1 |+|S2 |)·|AP| + (M1 +M2 )· log(|S1 |+|S2 |)) .Here, Mi denotes the number of edges in G(TSi ) and is assumed to be at least |Si | (i = 1, 2).Checking whether two transition systems are trace-equivalent is much harder.