5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 101
Текст из файла (страница 101)
(Such ”maximal” elements exist sinceTS is finite.) For each state u ∈ B, we have t - u. Since t , u, there exists a transition→ v withu−→ u with tmax , u . And vice versa, since u , t, there exists a transition t −u , v. But then tmax , v by the transitivity of ,. The maximality of tmax yieldstmax - v. Since tmax , u , v we get tmax - u . We conclude that all states u ∈ B have→ [tmax ] .an outgoing transition leading to a state in [tmax ] . This yields B −We now use the above claim to show (B.2) for R when TS is finite. Let us now suppose→ s is a transition in TS.
We take an arbitrary representativethat (s, B) ∈ R and that s −→ t witht ∈ B. By definition of R , state t simulates s. Thus, there exists a transition t −→ tmax with t , tmax ands , t . The above claim yields the existence of a transition t −B−→ C where C = [tmax ] . But then s , tmax and hence, (s , C) ∈ R .7.4.2Bisimulation, Simulation, and Trace EquivalenceIn this monograph, various equivalences and preorder relations have been defined on transition systems. This section compares bisimulation, simulation, and (infinite and finite)trace equivalence as well as the simulation preorder and trace inclusion. In the sequel ofthis section, let TSi = (Si , Acti , →i , Ii , AP, Li ), i = 1, 2, be transition systems over AP.We first observe that bisimulation equivalence implies simulation equivalence.
This simplySimulation Relations511follows by the symmetry of the conditions required for bisimulations. However, there aresimulation equivalent transition systems which are not bisimulation equivalent. Note thatbisimulation equivalence requires that whenever s1 ∼ s2 , then every transition s1 → s1can be mimicked by a transition s2 → s2 such that s1 ∼ s2 .
Simulation equivalence,however, requires that whenever s1 - s2 , then s1 → s1 can be mimicked by s2 → s2 suchthat s1 , s2 (but not necessarily s1 - s2 !). The fact that TS1 - TS2 does not alwaysimply TS1 ∼ TS2 is illustrated by the following example.Example 7.63.Similar but not Bisimilar Transition SystemsConsider the transition systems TS1 (left) and TS2 (right) in Figure 7.25.
TS1 ∼ TS2 , asthere is no bisimilar state in TS2 that mimics state s2 ; the only candidate would be t2 ,but s2 cannot mimic t2 → t4 . TS1 and TS2 are, however, simulation-equivalent. As TS2is a subgraph (up to isomorphism) of TS1 , we obtain TS2 , TS1 . In addition, TS1 , TS2asR = { (s1 , t1 ), (s2 , t2 ), (s3 , t2 ), (s4 , t3 ), (s5 , t4 ) }is a simulation relation for (TS1 , TS2 ).s1 { a }s2 ∅s4{b}s3 ∅s5 { c }t1 { a }t2 ∅t3 { b }t4 { c }Figure 7.25: Simulation-, but not bisimulation-equivalent transition systems.Theorem 7.64.Bisimulation is Strictly Finer than Simulation EquivalenceTS1 ∼ TS2 implies TS1 - TS2 , but TS1 ∼ TS2 and TS1 - TS2 is possible.Proof: Suppose TS1 ∼ TS2 . Then, there exists a bisimulation R for (TS1 , TS2 ). Itfollows directly that R is a simulation for (TS1 , TS2 ), and that R−1 is a simulation for(TS2 , TS1 ).
Hence, TS1 - TS2 . Example 7.63 provides transition systems TS1 and TS2such that TS1 - TS2 , but TS1 ∼ TS2 .Recall the notion of AP-determinism (see Definition 2.5 on page 24).512Equivalences and AbstractionDefinition 7.65.AP-Deterministic Transition SystemTransition system TS = (S, Act, →, I, AP, L) is AP-deterministic if1.
for A ⊆ AP: |I ∩ { s | L(s) = A }| 1, andαα→ s and s −−→ s and L(s ) = L(s ), then s = s .2. for s ∈ S: if s −−The difference between ∼ and - crucially relies on AP-determinism, e.g., transition systemTS1 in Figure 7.25 (left) is not AP-deterministic as its initial state has two distinct ∅successors.AP-Determinism Implies ∼ and - CoincideTheorem 7.66.If TS1 and TS2 are AP-deterministic, then TS1 ∼ TS2 if and only if TS1 - TS2 .Proof: see Exercise 7.3.This completes the comparison between bisimulation and simulation equivalence.
To enable the comparison with trace equivalence, we first consider the relation between , and(finite and infinite) trace inclusion.Theorem 7.67.Simulation Order vs. Finite Trace InclusionTS1 , TS2 implies Tracesfin (TS1 ) ⊆ Tracesfin (TS2 ).π1 be s1 = s0,1 s1,1 s2,1 . . . sn,1 ∈ Pathsfin (s1 ) whereProof: Assume TS1 , TS2 . Let *s1 ∈ I1 , i.e., s1 is an initial state in TS1 . Since TS1 , TS2 , there exists s2 ∈ I2 such thats1 , s2 . As , can be lifted to finite path fragments (see Lemma 7.55 on page 504), itfollows that there exists *π2 ∈ Pathsfin (s2 ), say, of the form s2 = s0,2 s1,2 s2,2 .
. . s2,n such*2 , i.e., sj,1 , sj,2 for 0 j n. But then L(sj,1) = L(sj,2) for 0 j n, thatthat *π1 , πis, trace(π1 ) = trace(π2 ).Corollary 7.68.Simulation Preserves Safety PropertiesLet Psafe be a safety LT property and TS1 and TS2 transition systems (all over AP) withoutterminal states. Then:TS1 , TS2andTS2 |= PsafeimpliesTS1 |= Psafe .Simulation Relations513Proof: Follows directly from Theorem 7.67 and the fact that Tracesfin (TS2 ) ⊇ Tracesfin (TS1 )implies that if TS2 |= Psafe , then TS1 |= Psafe (see Corollary 3.15 on page 104).Theorem 7.67 relates simulation preorder and finite trace inclusion, and cannot be obtainedfor trace inclusion. That is, in general, TS1 , TS2 does not imply that Traces(TS1 ) ⊆Traces(TS2 ).
This is illustrated by the following example.Example 7.69.Simulation Preorder Does Not Imply Trace InclusionConsider the transition systems TS1 (left) and TS2 (right) depicted in Figure 7.26. Wehave TS1 , TS2 , but Traces(TS1 ) ⊆ Traces(TS2 ) since { a } ∅ ∈ Traces(TS1 ) but { a } ∅ ∈Traces(TS1 ). This is due to the fact that s2 , t2 , but whereas s2 is a terminal state, t2 iss1 { a }s2 ∅t1 { a }s3 ∅t2 ∅s4 { b }t3 { b }Figure 7.26: TS1 , TS2 , but Traces(TS1 ) ⊆ Traces(TS2 ).not.
(Note that terminal states are simulated by any equally labeled state, be it terminalor not). As a result, a trace in TS1 may end in s2 , but a trace in TS2 cannot end in t2 .The example indicates that terminal states are an essential factor of not preserving traceinclusion. Indeed, if terminal states are absent in TS1 and TS1 , TS2 then all paths inTS1 are infinite and the path fragment lifting for simulations yields that each path of TS1can be lifted to an infinite path in TS2 . This yields:Theorem 7.70.Simulation Order and Trace InclusionIf TS1 , TS2 and TS1 does not have terminal states then Traces(TS1 ) ⊆ Traces(TS2 ).Thus, for transition systems without terminal states, the result stated in Corollary 7.68holds for all LT properties and not just the safety properties.514Equivalences and AbstractionFor the class of AP-deterministic transition systems one obtains a similar result.
Here,however, we have to deal with simulation equivalence and trace equivalence (rather thanthe simulation preorder and trace inclusion).Theorem 7.71.Simulation in AP-Deterministic SystemsIf TS1 - TS2 and TS1 and TS2 are AP-deterministic then Traces(TS1 ) = Traces(TS2 ).Proof: See Exercise 7.3.Corollary 7.72.Simulation and (Finite) Trace EquivalenceFor transition systems TS1 and TS2 over AP:(a) If TS1 - TS2 , then Tracesfin (TS1 ) = Tracesfin (TS2 ).(b) If TS1 and TS2 do not have terminal states and TS1 - TS2 , thenTraces(TS1 ) = Traces(TS2 ).(c) If TS1 and TS2 are AP-deterministic, then TS1 - TS2 if and only if Traces(TS1 ) =Traces(TS2 ).Proof: Claim (a) follows from Theorem 7.67, claim (b) from Theorem 7.70. Claim (c)follows from (and only if) Theorem 7.71 and (if) Exercise 7.3.Simulation equivalent transition systems without terminal states satisfy the same LT properties, and hence, the same LTL formulae.
Claim (c) together with Theorem 7.66 yieldthat for AP-deterministic transition systems, ∼, -, and trace equivalence coincide. (Finite) Trace equivalence does not imply simulation equivalence. This is illustrated by thetwo beverage vending machines described in Example 7.48 on page 498.Remark 7.73.Bisimulation and Trace EquivalenceSince ∼ is finer than -, it follows from Theorem 7.67 (page 512) that ∼ is finer than finitetrace equivalence:TS1 ∼ TS2 implies Tracesfin (TS1 ) = Tracesfin (TS2 ).However, bisimulation equivalent transition systems are even trace eqivalent. That is,TS1 ∼ TS2 implies Traces(TS1 ) = Traces(TS2 ).
This applies to any transition systemSimulation and ∀CTL∗ Equivalence515bisimulation equivalenceTS1 ∼ TS2simulation equivalenceTS1 - TS2trace equivalenceTraces(T1 ) = Traces(TS2 )finite trace equivalenceTracesfin (T1 ) = Tracesfin (TS2 )simulation orderTS1 , TS2trace inclusionTraces(T1 ) ⊆ Traces(TS2 )finite trace inclusionTracesfin (T1 ) ⊆ Tracesfin (T2 )Figure 7.27: Relation between equivalences and preorders on transition systems.TS1 , i.e., the absence of terminal states (as in Theorem 7.70 on page 513) is not required.This stems from the fact that a terminal state cannot be bisimilar to a nonterminal state,while terminal states are simulated by any state with the same label.Figure 7.27 summarizes the relationship between bisimulation, simulation, and (finite andinfinite) trace equivalence as well as simulation order and trace inclusion in the form ofa Hasse diagram.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
