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

If, however, π1 is a finiteSimulation Relations505s1 −R− s2↓s1,1↓s2,1↓...can becompleted to↓sn,1s1 −R− s2↓↓s1,1 −R− s1,2↓↓s2,1 −R− s2,2↓↓......↓↓sn,1 −R− sn,2Figure 7.22: Path fragment lifting for simulations.path from s1 then π2 is a finite path fragment from s2 , but possibly not maximal (i.e., thelast state of π2 might be nonterminal). Hence, state s1 can have finite traces, which aretrace fragments, but not traces of s2 .7.4.1Simulation EquivalenceThe simulation relation , is transitive and reflexive, but not symmetric. An examplewhere TS1 , TS2 , but TS2 , TS1 , was provided in Example 7.48 (page 498).

However,as any preorder, , induces an equivalence relation, the so-called kernel of ,, which isdefined by - = , ∩ ,−1 . It consists of all pairs (TS1 , TS2 ) of transition systems thatcan mutually simulate each other. The relation - is called simulation equivalence.Definition 7.56.Simulation EquivalenceTransition systems TS1 and TS2 (over AP) are simulation-equivalent, denoted TS1 - TS2 ,if TS1 , TS2 and TS2 , TS1 .Example 7.57.Simulation Equivalent Transition SystemsThe transition systems TS1 (left) and TS2 (right) in Figure 7.23 are simulation-equivalent.This can be seen as follows.

Since TS1 is a subgraph of TS2 (up to isomorphism, i.e., stateidentities), it is clear that TS1 , TS2 . Consider now the reverse direction. The transitiont1 → t2 in TS2 is simulated by s1 → s2 . Formally,R = { (t1 , s1 ), (t2 , s2 ), (t3 , s2 ), (t4 , s3 ) }is a simulation for (TS2 , TS1 ). From this, we derive TS2 , TS1 and obtain TS1 - TS2 .506Equivalences and Abstractions1 { a }s2 ∅t1 { a }t2 ∅s3 { b }t3 ∅t4 { b }Figure 7.23: Simulation-equivalent transition systems.The beverage vending machines described in Example 7.48 (page 498) are not simulationequivalent if (as before) the set of propositions AP = { pay, beer, soda } is used.

However,TS1 - TS2 holds for AP = { pay } or for AP = { pay, drink }.The simulation preorder , and its induced equivalence may also be adopted to comparestates of a single transition system.Definition 7.58.Simulation Order as a Relation on StatesLet TS = (S, Act, →, I, AP, L) be a transition system. A simulation for TS is a binaryrelation R ⊆ S × 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.State s1 is simulated by s2 (or s2 simulates s1 ), denoted s1 ,TS s2 , if there exists asimulation R for TS with (s1 , s2 ) ∈ R. States s1 and s2 of TS are simulation-equivalent,denoted s1 -TS s2 , if s1 ,TS s2 and s2 ,TS s1 .For state s, let SimTS (s) denote the simulator set of s, i.e., the set of states that simulates.

Formally:SimTS (s) = { s ∈ S | s ,TS s } .For convenience, the branching-time relations introduced so far are summarized in Figure7.24.As stated on page 457 for bisimulations, the relation ,TS on S × S results from , vias1 ,TS s2if and only if TSs1 , TSs2Simulation Relations507simulation orders1 ,TS s2 :⇔ there exists a simulation R for TS with (s1 , s2 ) ∈ Rsimulation equivalences1 -TS s2 :⇔ s1 ,TS s2 and s2 ,TS s1bisimulation equivalences1 ∼TS s2 :⇔ there exists a bisimulation R for TS with (s1 , s2 ) ∈ RFigure 7.24: Summary of the relations ,TS , ∼TS , and -TS .where TSs arises from TS by declaring s as the unique initial state. Vice versa, TS1 , TS2if each initial state s1 of TS1 is simulated by an initial state of TS2 in the transitionsystem TS1 ⊕ TS2 . Analogous observations hold for the simulation equivalence.

Theseobservations allow us to say that a state s1 in a transition system TS1 is simulated by astate s2 of another transition system TS2 , provided that the pair (s1 , s2 ) is contained insome simulation for (TS1 , TS2 ).In analogy to Lemma 7.8, ,TS is the coarsest simulation. Moreover, the simulation orderon TS is a preorder (i.e., transitive and reflexive) on TS’s state space and is the union ofall simulations on TS.Lemma 7.59.,TS is a Preorder and the Coarsest SimulationFor transition system TS = (S, Act, →, I, AP, L) it holds that:1.

,TS is a preorder on S.2. ,TS is a simulation on TS.3. ,TS is the coarsest simulation for TS.Proof: The first claim follows from Lemma 7.49 (page 453). To prove the second statementwe show ,TS fulfills conditions (1) and (2) of simulations on TS (Definition 7.58). Lets1 ,TS s2 for s1 , s2 states in TS. Then, there exists a simulation R that contains (s1 , s2 ).Since conditions (1) and (2) of Definition 7.58 hold for all pairs in R, L(s1 ) = L(s2 ) andfor any transition s1 → s1 , there exists a transition s2 → s2 with (s1 , s2 ) ∈ R. Hence,s1 ,TS s2 .

Thus, ,TS is a simulation on TS.508Equivalences and AbstractionThe third claim follows immediately from the second statement (,TS is a simulation) andthe fact that s1 ,TS s2 if there exists some simulation containing (s1 , s2 ). Hence, eachsimulation R is contained in ,TS .Let us now define the quotient transition system under simulation equivalence for transition system TS = (S, Act, →, I, AP, L). For simplicity, we omit the subscript TS andsimply write , rather than ,TS and - rather than -TS .Definition 7.60.Simulation Quotient SystemFor transition system TS = (S, Act, →, I, AP, L), the simulation quotient transition systemTS/ - is defined as follows:TS/ - = (S/ -, { τ }, → , I , AP, L )where I = { [s] | s ∈ I }, L ([s] ) = L(s), and→ is defined by:αs −−→ sτ[s] −→ [s ]Note that the transition relation in Definition 7.60 is similar to that of the bisimulation quotient of TS, but considers equivalence classes under - rather than ∼.

From thedefinition of → it follows thatB−→ Cif and only if ∃s ∈ B. ∃s ∈ C. s −→ s .In contrast to the bisimulation quotient, this is not equivalent toB−→ Cif and only if ∀s ∈ B. ∃s ∈ C. s −→ s .Stated in words, B −→ C does not imply that Post(s) ∩ C = ∅ for any s ∈ B. Thus, ingeneral, we have TS ∼ TS/ -. However, simulations can be established for TS and TS/ in both directions. That is to say, TS and TS/ - are simulation equivalent:Theorem 7.61.Simulation equivalence of TS and TS/ -For any transition system TS it holds that TS - TS/ -.Proof: TS , TS/ - follows directly from the fact that the relation R = { (s, [s] ) | s ∈ S }is a simulation for (TS, TS/ -). We show that TS/ - , TS by establishing a simulationSimulation Relations509R for (TS/-, TS).

First, observe that R = R−1 = { ([s] , s) | s ∈ S } is not adequate,as it is possible that s - s, s → t , but [t ] ∩ Post(s) = ∅. Instead,R = { ([s] , t) | s , t }is a simulation for (TS/ -, TS). This is proven as follows. Each initial state [s0 ] in TS/ is simulated by an initial state in TS, since [s0 ] , s0 and s0 ∈ I. In addition, [s] and t areequally labeled as s , t and all states in the simulator set SimTS (s) = { s ∈ S | s ,TS s }of s are equally labeled.

It remains to check whether each transition of [s] is mimicked→ C be a transition inby a transition of t for s , t. Let B ∈ S/ -, (B, t) ∈ R , and B −TS/ -. By definition of −→ , there exists a state s ∈ B and a transition s → s in TS suchthat C = [s ] . As (B, t) ∈ R , t simulates some state u ∈ B, i.e., u , t for some u ∈ B.Since s, u ∈ B, and all states in B are simulation-equivalent, we get u , t and s , u (andu , s).

By transitivity of ,, we have s , t. There is thus a transition t −→ t in TS withs , t . By definition of R , (C, t ) = ([s ] , t ) ∈ R .Remark 7.62.Alternative Definition of the Simulation Quotient SystemLet us consider the following alternative definition of the simulation quotient system. LetTS be a transition system as before andTS/ - = (S/ -, {τ }, → , I , AP, L )where I and L are as in Definition 7.60 and where the transitions in TS/ - arise bythe rule→ sB, B ∈ S/ - ∧ ∀s ∈ B ∃s ∈ B . s −[s] −→ [s ](where the action labels are omitted since they are not of importance here). Clearly,TS/ - is simulated by TS as R = {([s] , s) | s ∈ S} is a simulation for (TS/ - , TS).However, we cannot guarantee that the reverse holds, i.e., that TS is simulated by TS/ - .Let us illustrate this by means of an example. Assume that TS has two initial states s1and s2 with Post(s1 ) = {2i + 1 | i 0} and Post(s2 ) = {2i | i 0}.

Moreover, assumethat1 , 2 , 3 , ...while state n+1 , n for all n ∈ IN. For instance, the state space of TS could be {s1 , s2 } ∪→ 2i+ j for all i 0, j = 1, 2, n −→ tn and tn+1 −→ tn for all n 0,IN∪ {tn | n ∈ IN} with sj −while state t0 is terminal. Moreover, we deal with AP = { a, b } and L(s1 ) = L(s2 ) = { a },L(n) = { b } and L(tn ) = ∅ for all n 0. Then ti ,TS tj if and only if i < j which yieldsi ,TS j if and only if i < j510Equivalences and Abstractionand s1 -TS s2 .

In the quotient system TS/ - , states s1 and s2 are collapsed into their simulation equivalence class B = { s1 , s2 }. Since the states in IN are pairwise not simulationequivalent and since s1 and s2 do not have any common direct successor, B is a terminalstate in TS/ - . In particular, the reachable fragment of TS/ - just consists of the initial state B and does not have any transition. Thus, TS/ - and TS are not simulationequivalent.In the above example, TS is infinite. If, however, we are given a finite transition system,then TS/ - simulates TS, which yields the simulation equivalence of TS and TS/ - .

Tosee why it suffices to establish a simulation for (TS, TS/ - ). LetR = {(s, [t] ) | s , t}and show that R is a simulation for (TS, TS/ - ). Conditions (A) and (B.1) are obvious.Let us check condition (B.2). We use the following claim:→ tmax such thatClaim. If B ∈ S/ -, t ∈ B and t −→ t , then there exists a transition t −→ [tmax ] .t , tmax and B −Proof of the claim. Let tmax be such that tmax is ”maximal” in the sense that for anytransition t −→ v where tmax , v we have tmax - v.