5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 91
Текст из файла (страница 91)
As (s1 , s2 ) ∈ R1,2 , it follows that if s1 ∈ Post(s1 ) then(s1 , s2 ) ∈ R1,2 for some s2 ∈ Post(s2 ). Since (s2 , s3 ) ∈ R2,3 , we have (s2 , s3 ) ∈R2,3 for some s3 ∈ Post(s3 ). Hence, (s1 , s3 ) ∈ R.(B.3) Similar to the proof for (B.2).Bisimulation is defined in terms of the direct successors of states. By using an inductiveargument over states, we obtain a relation between (finite or infinite) paths.Lemma 7.5.Bisimulation on PathsLet TS1 and TS2 be transition systems over AP, R a bisimulation for (TS1 , TS2 ), and(s1 , s2 ) ∈ R. Then for each (finite or infinite) path π1 = s0,1 s1,1 s2,1 .
. . ∈ Paths(s1 ) thereexists a path π2 = s0,2 s1,2 s2,2 . . . ∈ Paths(s2 ) of the same length such that (sj,1, sj,2) ∈ Rfor all j.Bisimulation455s1 −R− s2↓s1,1↓s2,1↓...can becompleted tos1 −R− s2↓↓s1,1 −R− s1,2↓↓s2,1 −R− s2,2↓↓......Figure 7.4: Construction of statewise bisimilar paths.Proof: Let π1 = s0,1 s1,1 s2,1 . .
. ∈ Paths(s1 ) be a maximal path fragment in TS1 startingin s1 = s0,1 and assume (s1 , s2 ) ∈ R. We successively define a “corresponding” maximalpath fragment in TS2 starting in s2 = s0,2 , where the transitions si,1 →1 si+1,1 are matchedby transitions si,2 →2 si+1,2 such that (si+1,1 , si+1,2 ) ∈ R. This is done by induction oni, see Figure 7.4 on page 455. For each case we distinguish between si being a terminalstate or not.• Base case: i = 0. In case s1 is a terminal state, it follows directly from (s1 , s2 ) ∈ R(by condition (B.3)) that s2 is a terminal state too. Thus s2 = s0,2 is a maximal pathfragment in TS2 . If s1 is not a terminal state, it follows from (s0,1 , s0,2 ) = (s1 , s2 ) ∈ Rthat the transition s1 = s0,1 →1 s1,1 can be matched by a transition s2 →2 s1,2 suchthat (s1,1 , s1,2 ) ∈ R.
This yields the path fragment s2 s1,2 in TS2 .• Induction step: Assume i 0 and that the path fragment s2 s1,2 s2,2 . . . si,2 is alreadyconstructed with (sj,1, sj,2 ) ∈ R for j = 1, . . . , i.If π1 has length i, then π1 is maximal and si,1 is a terminal state. By condition(B.3), si,2 is terminal too. Thus, π2 = s2 s1,2 s2,2 . . . si,2 is a maximal path fragmentin TS2 which is statewise related to π1 = s1 s1,1 s2,1 . .
. si,1 .Now assume that si,1 is not terminal. We consider the step si,1 →1 si+1,1 in π1 . Since(si,1 , si,2 ) ∈ R, there exists a transition si,2 →2 si+1,2 with (si+1,1 , si+1,2 ) ∈ R. Thisyields a path fragment s2 s1,2 . . . si,2 si+1,2 which is statewise related to the prefixs1 s1,1 . . . si,1 si+1,1 of π1 .By symmetry, for each path π2 ∈ Paths(s2 ) there exists a path π1 ∈ Paths(s1 ) of the samelength which is statewise related to π2 .
As one can construct statewise bisimilar paths,bisimilar transition systems are trace-equivalent. It is mostly easier to prove that twotransition systems are bisimilar rather than prove their trace equivalence. The intuitive456Equivalences and Abstractionreason for this discrepancy is that proving bisimulation equivalence just requires “local”reasoning about state behavior instead of considering entire paths.
The following result isthus of importance in checking trace equivalence as well.Theorem 7.6.Bisimulation and Trace EquivalenceTS1 ∼ TS2 implies Traces(TS1 ) = Traces(TS2 ).Proof: Let R be a bisimulation for (TS1 , TS2 ). By Lemma 7.5, any path π1 = s0,1 s1,1 s2,1 . .
.in TS1 can be lifted to a path π2 = s0,2 s1,2 s2,2 . . . in TS2 such that (si,1 , si,2 ) ∈ Rfor all indices i. According to condition (B.1), L1 (si,1 ) = L2 (si,2 ) for all i. Thus,trace(π1 ) = trace(π2 ). This shows Traces(TS1 ) ⊆ Traces(TS2 ). By symmetry, one obtains that TS1 and TS2 are trace equivalent.As trace-equivalent transition systems fulfill the same linear-time properties, it thus nowfollows that bisimilar transition systems fulfill the same linear-time properties.7.1.1Bisimulation QuotientSo far, bisimulation has been defined as a relation between transition systems.
Thisenables comparing different transition systems. An alternative perspective is to considerbisimulation as a relation between states within a single transition system. By consideringthe quotient transition system under such a relation, smaller models are obtained. Thisminimization recipe can be exploited for efficient model checking. In the following, wedefine bisimulation as a relation on states, relate it to the notion of bisimulation betweentransition systems, and define the quotient transition system under such relation.Definition 7.7.Bisimulation Equivalence as Relation on StatesLet TS = (S, Act, →, I, AP, L) be a transition system.
A bisimulation for TS is a binaryrelation R on S such that for all (s1 , s2 ) ∈ R:1. L(s1 ) = L(s2 ).2. If s1 ∈ Post(s1 ), then there exists an s2 ∈ Post(s2 ) with (s1 , s2 ) ∈ R.3. If s2 ∈ Post(s2 ), then there exists an s1 ∈ Post(s1 ) with (s1 , s2 ) ∈ R.States s1 and s2 are bisimulation-equivalent (or bisimilar), denoted s1 ∼TS s2 , if thereexists a bisimulation R for TS with (s1 , s2 ) ∈ R.Bisimulation457Thus, a bisimulation (on states) for TS is a bisimulation (on transition systems) for thepair (TS, TS), except that condition (A) is not required.
This condition could be ensuredby adding the pairs (s, s) to R for any state s. Moreover, for all states s1 and s2 in TS itholds thats1 ∼TS s2 iffas states of TS (Def. 7.7)TS ∼ TSs2 , s1 in the sense of Def. 7.1where TSsi denotes the transition system obtained from TS by declaring si as the uniqueinitial state. Vice versa, the definition of bisimulation between transition systems (Definition 7.1) arises from Definition 7.7 as follows. Take transition systems TS1 and TS2 overAP, and combine them in a single transition system TS1 ⊕ TS2 , which basically resultsfrom the disjoint union of state spaces (see below). We then subsequently “compare” theinitial states of TS1 and TS2 as states of the composite transition system TS1 ⊕ TS2 toensure condition (A).The formal definition of TS1 ⊕ TS2 is as follows.
For TSi = (Si , Acti , →i , Ii , AP, Li ),i = 1, 2:TS1 ⊕ TS2 = (S1 S2 , Act1 ∪ Act2 , →1 ∪ →2 , I1 ∪ I2 , AP, L)where stands for disjoint union and where L(s) = Li (s) if s ∈ Si . Then TS1 ∼ TS2 ifand only if, for every initial state s1 of TS1 , there exists a bisimilar initial state s2 of TS2 ,and vice versa. That is, s1 ∼TS1 ⊕TS2 s2 . Stated in terms of equivalence classes, TS1 ∼ TS2if and only if∀C ∈ (S1 S2 )/ ∼TS1 ⊕TS2 . I1 ∩ C = ∅iffI2 ∩ C = ∅ .Here, (S1 S2 )/ ∼TS1 ⊕TS2 denotes the quotient space with respect to ∼TS1 ⊕TS2 , i.e., the setof all bisimulation equivalence classes in S1 S2 . The latter observation is based on thefact that ∼TS1 ⊕TS2 is an equivalence relation, see the first part of the following lemma.Lemma 7.8.Coarsest BisimulationFor transition system TS = (S, Act, →, I, AP, L) it holds that:1.
∼TS is an equivalence relation on S.2. ∼TS is a bisimulation for TS.3. ∼TS is the coarsest bisimulation for TS.Proof: The first claim follows directly from the characterization of ∼TS in terms of ∼,and Lemma 7.4 on page 453. The last claim states that each bisimulation R for TS is458Equivalences and Abstractionfiner than ∼TS ; this immediately follows from the definition of ∼TS . It remains to provethat ∼TS is a bisimulation for TS. We show that ∼TS satisfies conditions (1) and (2) ofDefinition 7.7. Condition (3) follows by symmetry. Let s1 ∼TS s2 . Then, there exists abisimulation R that contains (s1 , s2 ). From condition (1), it follows that L(s1 ) = L(s2 ).Condition (2) yields that for any transition s1 → s1 there is a transition s2 → s2 with(s1 , s2 ) ∈ R.
Hence, s1 ∼TS s2 .Stated differently, the relation ∼TS is the coarsest equivalence on the state space of TSsuch that equivalent states are equally labeled and can simulate each other as shown inFigure 7.5.s1 ∼TS s2↓s1can be complemented tos1 ∼TS s2↓↓s1 ∼TS s2Figure 7.5: Condition (2) for bisimulation equivalence ∼TS on states.Remark 7.9.Union of BisimulationsFor finite index set I and (Ri )i∈I a family of bisimulation relations for TS, i∈I Ri is abisimulation for TS too (see Exercise 7.2). Since ∼TS is the coarsest bisimulation for TS,∼TS coincides with the union of all bisimulation relations for TS.As stated before, bisimilar transition systems satisfy the same linear-time properties. Suchproperties—and, as we will see later, all temporal formulae that can be expressed inCTL∗ —can thus be checked on the quotient system instead of on the original (and possiblymuch larger) transition system.
Before providing the definition of quotient transitionsystems with respect to ∼TS , let us first fix some notations.Notation 7.10.Equivalence Classes, Quotient SpaceLet S be a set and R an equivalence on S. For s ∈ S, [s]R denotes the equivalenceclass of state s under R, i.e., [s]R = { s ∈ S | (s, s ) ∈ R }. Note that for s ∈ [s]R wehave [s ]R = [s]R . The set [s]R is often referred to as the R-equivalence class of s. Thequotient space of S under R, denoted by S/R = { [s]R | s ∈ S }, is the set consisting ofall R-equivalence classes.BisimulationDefinition 7.11.459Bisimulation QuotientFor transition system TS = (S, Act, →, I, AP, L) and bisimulation ∼TS , the quotienttransition system TS/ ∼TS is defined byTS/ ∼TS = (S/ ∼TS , { τ }, → , I , AP, L )where:• I = { [s]∼ | s ∈ I },• → is defined byα→ ss −−,τ[s]∼ −→ [s ]∼• L ([s]∼ ) = L(s).In the sequel, TS/ ∼TS is referred to as the bisimulation quotient of TS.
For the sake ofsimplicity, we write TS/ ∼ rather than TS/ ∼TS .The state space of TS/ ∼ is the quotient of S under ∼. The initial states in TS/ ∼ arethe ∼-equivalence classes of the initial states in TS. Each transition s → s in TS inducesa transition [s]∼ → [s ]∼ . As the action label is irrelevant, these labels are omitted fromnow on; this is reflected in the definition by replacing any action α ∈ Act by an arbitraryaction, τ say. The state-labeling function L is well-defined, since all states in [s]∼ areequally labeled (see the definition of bisimulation).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
