5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 95
Текст из файла (страница 95)
In fact, they can be distinguished by theCTL formulaΦ = ∃ (∃ beer ∧ ∃ soda)as TS1 |= Φ, but TS2 |= Φ.4767.3Equivalences and AbstractionBisimulation-Quotienting AlgorithmsThis section presents algorithms for obtaining the bisimulation quotient for a finite transition system TS. Such an algorithm serves two purposes. First, it can be used to verifythe bisimilarity of two finite transition systems TS1 and TS2 by considering the quotientof TS1 ⊕ TS2 (see page 457). Since bisimulation is finer than trace equivalence, algorithmsthat verify whether TS1 ∼ TS2 can also be used as a sound, though incomplete, prooftechnique for proving the trace equivalence of TS1 and TS2 .
Secondly, such algorithmscan be used to obtain the abstract (and thus smaller) transition system TS/∼ in a fullyautomated manner. As TS ∼ TS/∼ (see Theorem 7.14 on page 464), it follows fromCorollary 7.27 on page 475 that any verification result for TS/∼—either being negative orpositive—carries over to TS. This applies to any formula expressed in either LTL, CTL,or CTL∗ .This section treats two algorithms for computing the bisimulation quotient TS/∼. Bothalgorithms rely on a partition refinement technique. Roughly speaking, the finite statespace S is partitioned in blocks, i.e., pairwise disjoint sets of states.
Starting from astraightforward initial partition where, e.g., all equally labeled states form a partition,the algorithm successively refines these partitions such that ultimately partitions onlycontain bisimilar states. This strategy strongly resembles minimization algorithms fordeterministic finite automata (DFA).In the sequel, let TS = (S, Act, →, I, AP, L) be a finite transition system with S = ∅.Definition 7.29.Partition, Block, SuperblockA partition for S is a set Π = {B1 , .
. . , Bk } such that Bi = ∅ (for 0 < i k), Bi ∩ Bj = ∅(for 0 < i, j k and i = j), and S = 0<ik Bi .Bi ∈ Π is called a block. C ⊆ S is a superblock of Π if C = Bi1 ∪ . . . ∪ Bi for someBi1 , . . . , Bi ∈ Π.Let [s]Π denote the unique block of partition Π containing s. For partitions Π1 and Π2 ofS, Π1 is called finer than Π2 , or Π2 is called coarser than Π1 , if:∀B1 ∈ Π1 ∃B2 ∈ Π2 . B1 ⊆ B2 .In this case, every block of Π2 can be written as a disjoint union of blocks in Π1 . Π1is strictly finer than Π2 (and Π2 is strictly coarser than Π1 ) if Π1 is finer than Π2 andΠ1 = Π2 .Bisimulation-Quotienting AlgorithmsRemark 7.30.477Partitions and EquivalencesThere is a close connection between equivalence relations and partitions. For equivalencerelation R on S, the quotient space S/R is a partition for S.
Vice versa, partition Π forS induces the equivalence relation:RΠ = { (s1 , s2 ) | ∃B ∈ Π. s1 ∈ B ∧ s2 ∈ B }= { (s1 , s2 ) | [s1 ]Π = [s2 ]Π }such that S/RΠ corresponds to Π. For equivalence relation R, the equivalence relationRΠ induced by Π = S/R corresponds to R.The partition refinement algorithm works with a representation of equivalences by meansof the induced partition (i.e., the quotient space).
In the initial partition Π0 = ΠAP ,each group of equally labeled states forms a block. Subsequently, the current partition Πiis successively replaced with a finer partition Πi+1 , (for details, see Section 7.3.2). Thisiterative refinement procedure is halted as soon as Πi cannot be further refined, i.e., whenΠi = Πi+1 . Such situation is guaranteed to occur as S is finite. The resulting partitionΠi is the bisimulation quotient space.
The main steps are outlined in Algorithm 28.Algorithm 28 Partition refinement algorithm (basic idea)Input: finite transition system TS with state space SOutput: bisimulation quotient space S/∼Π0 := ΠAP ;i := 0;(* see Section 7.3.1 *)(* loop invariant: Πi is coarser than S/∼ and finer than ΠAP *)repeatΠi+1 := Refine(Πi );i := i + 1;until Πi = Πi−1return Πi(* no further refinement possible *)The termination of the partition refinement procedure is clear, as the partition Πi+1 isstrictly finer than Πi . Thus, for the induced equivalence relations RΠi we haveS × S ⊇ RΠ0 RΠ1 RΠ2 .
. . RΠi = ∼TS .Due to the fact that S is finite, a partition Πi with Πi = Πi−1 is reached after at most|S| iterations. After |S| proper refinements, any block in Πi is a singleton, and a furtherrefinement is thus impossible.4787.3.1Equivalences and AbstractionDetermining the Initial PartitionSince bisimilar states are equally labeled, it is rather natural to use this in determiningthe initial partition Π0 = ΠAP .Definition 7.31.The AP PartitionThe AP partition of TS, denoted ΠAP , is the quotient space S/RAP induced by RAP ={ (s1 , s2 ) ∈ S × S | L(s1 ) = L(s2 ) }.The initial partition Π0 = ΠAP can be computed as follows.
The basic idea is to generatea decision tree for a ∈ AP. For AP = { a1 , . . . , ak }, the height of the decision tree forAP is k. The vertices at depth i < k represent the decision “is ai+1 ∈ L(s)?”. The left/ L(s)”, while the right branchbranch of vertex v at depth i < k represents the case “ai+1 ∈represents “ai+1 ∈ L(s)”.
The full decision tree for, e.g., k = 2, a1 = a, and a2 = b is fothe form:abLsLsabLsLsbLsLeaf v represents a set of states. More precisely, states(v) contains the states s ∈ S forwhich L(s) is represented by the path from the root to v. The decision tree for AP isconstructed successively by considering all states in S separately. The initial decision treeconsists only of the root v0 . On considering state s, the tree is traversed in a top-downmanner, and new vertices are inserted when necessary, i.e., when s is the first encounteredstate with labeling L(s).
Once the tree traversal for state s reaches leaf w, states(w) isextended with s. The essential steps are outlined in Algorithm 29.Example 7.32.Determining the Initial PartitionConsider the transition system TS over AP = { a, b } in Figure 7.10. We assume thatL(s0 ) = L(s2 ) = L(s5 ) = L(s6 ) = { a }, L(s1 ) = { a, b }, and L(s3 ) = L(s4 ) = ∅. Thefirst three steps for generating the initial partition and the resulting decision tree areindicated in Figure 7.11.
The resulting partition ΠAP consists of three blocks. BlockB1 = {s0 , s2 , s5 , s6 } represents all states labeled with { a }. The two other blocks standfor the states labeled with { a, b } or ∅.Bisimulation-Quotienting Algorithms479Algorithm 29 Computing the initial partition ΠAPInput: TS = (S, Act, →, I, AP, L) over AP = {a1 , . . . , ak } and finite SOutput: partition ΠAPnew(v0 );for all s ∈ S dov := v0 ;for i = 1, . . .
, k−1 doif ai ∈ L(s) thenif right(v) = nil then new(right(v));v := right(v);elseif left(v) = nil then new(left(v));v := left(v);fiod(* create a root vertex *)(* start a top-down traversal *)(* create a right child of v *)(* create a left child of v *)(* v is a vertex at depth k *)if ak ∈ L(s) thenif right(v) = nil then new(right(v));states(right (v)) := states(right (v)) ∪ { s };elseif left(v) = nil then new(left(v));states(left(v)) := states(left(v)) ∪ { s };fiodreturn {states(w) | w is a leaf}(* create a right child of v *)(* create a left child of v *)480Equivalences and Abstraction∅s4{ a } s5s3s1s0s2s6∅{ a, b }{a}{a}{a}Figure 7.10: Transition system TS over AP = { a, b }.We conclude this section by considering the time complexity of computing the initialpartition.
For each state s in S, the decision tree has to be traversed from root to leaf.This takes Θ(|AP|) time. The overall time complexity is now given as follows.Lemma 7.33.Time Complexity of Computing the Initial PartitionThe initial partition ΠAP can be computed in time Θ(|S|·|AP|).7.3.2Refining PartitionsSince any partition Πi (i 0) is finer than the initial partition ΠAP , each block in Πi isguaranteed to contain only equally labeled states. The initial partition, however, does notconsider the one-step successors of states. This is taken care of in the successive refinementsteps.Lemma 7.34.Coarsest PartitionThe bisimulation quotient space S/∼ is the coarsest partition Π for S such that(i) Π is finer than ΠAP .a¬aa¬b¬bb{s0 }{s0 }{s1 }¬b{s3 }¬aa¬bb{s0 }{s1 }...Figure 7.11: Generating the Partition ΠAP .a¬b¬b{s3 , s4 } {s0 , s2 , s5 , s6 }b{s1 }Bisimulation-Quotienting Algorithms481(ii) for all B, C ∈ Π: B ∩ Pre(C) = ∅ or B ⊆ Pre(C).Moreover, if partition Π fulfills (ii), then B ∩ Pre(C) = ∅ or B ⊆ Pre(C) for all B ∈ Πand all superblocks C of Π.Recall that Pre(C) = { s ∈ S | Post(s) ∩ C = ∅ } denotes the set of states in S, whichhave at least one successor in C.
Thus, for every block B, we have that B ∩ Pre(C) = ∅if and only if no state of B has an immediate successor in C, and B ⊆ Pre(C) if and onlyif all states in B have an immediate successor in C.Proof: Let Π be a partition of S and RΠ the equivalence relation on S induced by Π. Theproof is carried out in two steps. We first show that RΠ is a bisimulation if and only ifthe conditions (i) and (ii) are satisfied. Then, we show that S/ ∼ is the coarsest partitionsatisfying (i) and (ii).⇐: Assume that Π satisfies (i) and (ii). We prove that RΠ induced by Π is a bisimulation.Let (s1 , s2 ) ∈ RΠ and B = [s1 ]Π = [s2 ]Π .1. Since Π is finer than ΠAP (condition (i)), there exists a block B of ΠAP containingB. Thus, s1 , s2 ∈ B ⊆ B ∈ ΠAP , and, therefore, L(s1 ) = L(s2 ).2.
Let s1 ∈ Post(s1 ) and C = [s1 ]Π . Then, s1 ∈ B ∩ Pre(C). By condition (ii), weobtain B ⊆ Pre(C). Hence, s2 ∈ Pre(C). So, there exists a state s2 ∈ Post(s2 ) ∩ C.Since s2 ∈ C = [s1 ]Π , it follows that (s1 , s2 ) ∈ RΠ .⇒: Assume RΠ is a bisimulation. The proof obligation is to show that the conditions (i)and (ii) are satisfied.(i) By contraposition. Assume that Π is not finer than ΠAP . Then, there exist a blockB ∈ Π and states s1 , s2 ∈ B with [s1 ]ΠAP = [s2 ]ΠAP .
Then, L(s1 ) = L(s2 ). Hence,RΠ is not a bisimulation. Contradiction.(ii) Let B, C be blocks of Π. We assume that B ∩ Pre(C) = ∅ and show thatB ⊆ Pre(C). As B ∩ Pre(C) = ∅, there exists a state s1 ∈ B with Post(s1 ) ∩ C = ∅.Let s1 ∈ Post(s1 ) ∩ C and s2 be an arbitrary state of B. We demonstrate thats2 ∈ Pre(C). Since s1 , s2 ∈ B, we get that (s1 , s2 ) ∈ RΠ . Due to s1 → s1 , thereexists a transition s2 → s2 with (s1 , s2 ) ∈ RΠ . But then s1 ∈ C yields s2 ∈ C.Hence, s2 ∈ Post(s2 ) ∩ C. Thus, s2 ∈ Pre(C).482Equivalences and AbstractionAssume Π satisfies (ii). We show that B ∩ Pre(C) = ∅ or B ⊆ Pre(C) for any B ∈ Π andsuperblocks C of Π. The proof is by contraposition.
Let B ∈ Π and C a superblock, i.e., Cis of the form C = C1 ∪ . . . ∪ C for blocks C1 , . . . , C of Π. Assume that B ∩ Pre(C) = ∅and B ⊆ Pre(C). Then, there exists an index i ∈ {1, . . . , } with B ∩ Pre(Ci ) = ∅.Further, it is clear that B ⊆ Pre(Ci ), since otherwise B ⊆ Pre(Ci ) ⊆ Pre(C). Thus,condition (ii) is not satisfied for block Ci ∈ Π. Contradiction.It remains to show that the bisimulation partition Π = S/∼ is the coarsest partition of Ssatisfying the conditions (i) and (ii).
This immediately follows from the fact that ∼TS isthe coarsest bisimulation (Lemma 7.8 on page 457).Let us now consider how partitions are successively refined. Every refinement aims atsatisfying condition (ii). To that end, a superblock C of Π is considered and every blockB of the current partition Πi is decomposed (“splitted”) into the subblocks B ∩ Pre(C)and B \ Pre(C), provided that these subblocks are nonempty. If one of the subblocks isempty, then B satisfies condition (ii) and no decomposition takes place.Definition 7.35.The Refinement OperatorLet Π be a partition for S and C be a superblock of Π.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
