5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 96
Текст из файла (страница 96)
Then:Refine(B, C)Refine(Π, C) =B∈Πwhere Refine(B, C) = {B ∩ Pre(C), B \ Pre(C)} \ {∅}.B ∩ Pre(C)B \ Pre(C)block Bsuperblock CFigure 7.12: Refinement operator.The basic scheme of the refinement operator is depicted in Figure 7.12. Refine(B, C) ={ B }, i.e., B is not decomposed with respect to C, if all states in B have a direct Csuccessor or if no state in B has a direct C-successor. In case some states in B have adirect C-successor, while others have not, B is refined accordingly.Bisimulation-Quotienting Algorithms483The following result shows that successive refinements, starting with partition ΠAP , yielda series of partitions Π0 = ΠAP , Π1 , Π2 , Π3 , . .
., which become increasingly finer and whichall are coarser than S/∼. This property is essential for establishing the correctness of theiterative approach for as outlined in Algorithm 28 (see page 477).Lemma 7.36.Correctness of the Refinement OperatorLet Π be a partition of S, which is finer than ΠAP and coarser than S/∼. Further, let Cbe a superblock for Π. Then:(a) Refine(Π, C) is finer than Π.(b) Refine(Π, C) is coarser than S/∼.Proof:(a) This follows directly from the definition of Refine, since every block B ∈ Π is eithercontained in Refine(Π, C) or is decomposed into B ∩ Pre(C) and B \ Pre(C).(b) Let B ∈ S/∼.
We show that B is contained in a block of Refine(Π, C). Since Πis coarser than S/∼, there exists a block B ∈ Π with B ⊆ B . B is of the formB = B ∪ D where D is a (possibly empty) superblock of S/∼. If B ∈ Refine(Π, C),/ Refine(Π, C), then B isthen B ⊆ B ∈ Refine(Π, C). Otherwise, i.e., if B ∈decomposed into the subblocks B ∩ Pre(C) and B \ Pre(C).
We now show thatB is contained in one of these two new subblocks. Condition (ii) of Lemma 7.34implies that either B ∩ Pre(C) = ∅ (thus, B \ Pre(C) = B) or B \ Pre(C) = ∅ (thus,B ∩ Pre(C) = B). Since B = B ∪ D, B is either contained in block• B \ Pre(C) = (B \ Pre(C)) ∪ (D \ Pre(C))• or in B ∩ Pre(C) = (B ∩ Pre(C)) ∪ (D ∩ Pre(C)).Definition 7.37.Splitter, StabilityLet Π be a partition for S and C a superblock of Π.1. C is a splitter for Π if there exists a block B ∈ Π with B ∩ Pre(C) = ∅ andB \ Pre(C) = ∅.484Equivalences and Abstraction2.
Block B is stable with respect to C if B ∩ Pre(C) = ∅ or B \ Pre(C) = ∅.3. Π is stable with respect to C if each block B ∈ Π is stable wrt. C.C is thus a splitter for Π if and only if Π = Refine(Π, C), that is, if and only if Π is notstable for C. B is stable with respect to C whenever { B } = Refine(B, C). Note that S/∼is the coarsest stable partition that is finer than ΠAP .Algorithm 30 Algorithm for computing the bisimulation quotient spaceInput: finite transition system TS over AP with state space SOutput: bisimulation quotient space S/∼Π := ΠAP ;while there exists a splitter for Π dochoose a splitter C for Π;Π := Refine(Π, C);odreturn Π(* Refine(Π, C) is strictly finer than Π *)The refine operator and the concept of a splitter can be effectively exploited in computingS/∼, see Algorithm 30.
Its correctness follows from Lemmas 7.34 and 7.36, Terminationfollows from the following result.Lemma 7.38.Termination Criterion of Algorithm 30Let Π be a partition for S, which is finer than ΠAP and coarser than S/∼. Then, Π isstrictly coarser than S/∼ if and only if there exists a splitter for Π.Proof: Follows immediately from Lemma 7.34 on page 480.Example 7.39.Partition Refinement AlgorithmFigure 7.13 illustrates the principle of the partition refinement algorithm on a small example.
The initial partition ΠAP identifies all equally labeled states:Π0 = ΠAP = {{ s1 , s2 , s3 }, { t1 , t2 , t3 }, { u1 , u2 }, { v1 , v2 }}In the first step, consider C1 = { v1 , v2 }. This leaves the blocks { s1 , s2 , s3 }, { u1 , u2 } and{ v1 , v2 } unaffected, but splits block of the t-states into { t1 } = { t1 , t2 , t3 } \ Pre(C1 ) andBisimulation-Quotienting Algorithms485{ t2 , t3 } = { t1 , t2 , t3 } ∩ Pre(C1 ).
Thus, we obtain the partitionΠ1 = {{ s1 , s2 , s3 }, { t1 }, { t2 , t3 }, { u1 , u2 }, { v1 , v2 }}.In the second refinement step, consider C2 = { t1 }. This splitter divides the s-block into{a, b} s1s2 {a, b}s3 {a, b}s1s2s3t1t2t3u1v1refine{b} t1∅ u1t2 {b}{a} v1t3 {b}∅ u2for C = { v1 , v2 }v2 {a}refines1s2s3t1t2t3u1v1u2v2for C = { t1 }s1s2s3t1t2t3u1v1refineu2for C = { t2 , t3 }v2u2v2Figure 7.13: Execution of the partition refinement algorithm for a small example.{ s1 , s2 } = { s1 , s2 , s3 } ∩ Pre(C2 ) and { s3 } = { s1 , s2 , s3 } \ Pre(C2 ), yieldingΠ2 = {{ s1 , s2 }, { s3 }, { t1 }, { t2 , t3 }, { u1 , u2 }, { v1 , v2 }}.In the third refinement step, consider C3 = { t2 , t3 }.
This splitter distinguishes states s1and s2 —s1 has no transition to C3 , while s2 does—and yields the partitionΠ3 = {{ s1 }, { s2 }, { s3 }, { t1 }, { t2 , t3 }, { u1 , u2 }, { v1 , v2 }}.No further refinements are possible, and Π3 thus agrees with the bisimulation quotient ofthe original transition system.A possible implementation of the operator Refine(Π, C) is based on a list representationof the sets of predecessors Pre(s ), s ∈ S. For any state s ∈ C, the list of predecessorsPre(s ) is traversed, and s ∈ Pre(s ) is “moved” from the (data structure representing the)current block B = [s]Π to the block[s]Refine(Π,C) = B ∩ Pre(C).486Equivalences and AbstractionThe states remaining in B form the subblock B \ Pre(C).
In case all states s ∈ B aremoved from B to B ∩ Pre(C), the set of states in the data structure representing block Bis empty and we have B ∩ Pre(C) = B and B \ Pre(C) = ∅. In case no state is movedfrom B to B ∩ Pre(C), we have, B = B \ Pre(C) and B ∩ Pre(C) = ∅.By means of the above-described technique, every state s ∈ C causes the costs O(|Pre(s )|+1), provided appropriate data structures are used to represent TS (or its state graph), andthe partition Π. (The summand 1 in the complexity bound reflects the case Pre(s ) = ∅;although these summands can be omitted when considering the complexity per state, theymight be relevant when considering the complexity over all states.) Examples of such datastructures are, e.g., an adjacency list representation for Pre(·), and a bit-vector representation of the satisfaction sets Sat(a) = { s ∈ S | a ∈ L(s) } to represent the labelingfunction.
Furthermore, list representations of partition Π and of the blocks B ∈ Π can beused. Using the fact that&O(|Pre(s )| +s ∈C'1) = O (|Pre(C)| + |C|)we obtain for the time complexity of the refinement operator:Lemma 7.40.Time Complexity of the Refinement OperatorRefine(Π, C) can be computed in time O (|Pre(C)| + |C|).7.3.3A First Partition Refinement AlgorithmSo far we presented the partition refinement algorithm without specifying any searchstrategy for the splitters.
Such search strategy prescribes how to determine a splitter Cfor a given partition Πi+1 . A simple strategy that will be pursued in this section, is touse the blocks of the previous partition Πi (where Π−1 = { S }) as splitter candidates forΠi+1 , see Algorithm 31. In every outermost iteration, the refine operator causes for a states ∈ S (as part of Πold ), the cost O(|Pre(s)| + 1), see page 486. The outermost iterationis traversed maximally |S| times; this occurs when in every iteration exactly one state isseparated, i.e., constitutes a separate (singleton) block. This yields for the total costs ofthe iteration:)((|Pre(s )| + 1)= O (|S|·(M + |S|))O |S| ·s ∈SwhereM =s ∈S|Pre(s )|Bisimulation-Quotienting Algorithms487Algorithm 31 A first partition refinement algorithmInput: finite transition system TS with the state space SOutput: bisimulation quotient space S/∼Π := ΠAP ;Πold := { S };(* see Algorithm 29, page 479 *)(* Πold is the previous partition *)(* loop invariant: Π is coarser than S/∼ and finer than ΠAP and Πold *)repeatΠold := Π;for all C ∈ Πold doΠ := Refine(Π, C);oduntil Π = Πoldreturn Πdenotes the number of edges in the state graph G(TS).
Assuming M |S|, this can besimplified to O(|S|·M ). To obtain the total time complexity of Algorithm 31, it remainsto consider the cost of computing ΠAP , which is Θ(|S|·|AP|), as stated in Lemma 7.33 onpage 480. This yields:Theorem 7.41.Time Complexity of Algorithm 31The bisimulation quotient space of TS can be computed by Algorithm 31 with time complexity O(|S| · (|AP| + M )), under the assumption that M |S|, where M is the numberof edges in the state graph G(TS).Computing the bisimulation quotient is thus linear in the number of states of TS. In thenext section, a strategy is presented that improves this such that the time complexity islogarithmic in |S|.7.3.4An Efficiency ImprovementThe crucial observation that allows for an improvement of the time complexity is that itis not necessary to refine with respect to all blocks C ∈ Πold as in Algorithm 31.
Instead,it suffices to only consider roughly half of them, viz. the smaller subblocks of a previousrefinement. More precisely, if a block C of the current partition Π is decomposed intosubblocks C1 = C ∩ Pre(D) and C2 = C \ Pre(D), only the smaller subblock is used as asplitter candidate in the following iteration. Now, let C ∈ { C1 , C2 } such that|C| |C |/2, thus |C| |C \ C|.488Equivalences and AbstractionThe decomposition of the blocks B ∈ Refine(Π, D) with respect to C and C \ C is nowslightly modified by combining the refinement steps with respect to C and C \ C. Tomake such “simultaneous” refinement possible, the algorithm exploits a ternary (insteadof the previous binary) refinement operator:Refine(Π, C, C \ C) = Refine( Refine(Π, C), C \ C )where it is assumed that |C| |C \ C|.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
