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

All results andconcepts presented for ∼ can be adapted for ∼Act in a straightforward manner. Forfor the statesinstance, ∼Act is an equivalence and can be adapted to an equivalence ∼ActTSof a single transition system TS in a similar way as before. The action-based bisimulationquotient system TS/ ∼Act is defined as TS/ ∼ except that we deal with an empty set ofαα→ s to an equally labeled transition B −−→ Batomic propositions and lift any transition s −−466Equivalences and Abstractionwhere B and B denote the action-based bisimulation equivalence classes of states s ands , respectively.In the context of process calculi, an important aspect of bisimulation is whether it enjoysa substitutivity property with respect to syntactic operators in the process calculus, suchas parallel composition. The following result states that action-based bisimulation is acongruence for the parallel composition H with synchronization over handshaking actions, see Definition 2.26 on page 48.Lemma 7.16.Congruence w.r.t.

HandshakingFor transition systems TS1 , TS1 over Act1 , TS2 , TS2 over Act2 , and H ⊆ Act1 ∩ Act2 itholds thatTS1 ∼Act TS1andTS2 ∼Act TS2implies TS1 H TS2 ∼Act TS1 H TS2 .Proof: Let TSi = (Si , Acti , →i , Ii , AP, Li ) and TSi = (Si , Acti , →i , Ii , AP, Li ) and letRi ⊆ Si × Si be an action-based bisimulation for (TSi , TSi ), i=1, 2.

Then, the relation:R = { (s1 , s2 , s1 , s2 ) | (s1 , s1 ) ∈ R1 ∧ (s2 , s2 ) ∈ R2 }is an action-based bisimulation for (TS1 H TS2 , TS1 H TS2 ). This can be seen as follows.The fulfillment of condition (A) is obvious. To check condition (B.2’), assume that (1) thereα→ t1 , t2 in TS1 H TS2 , and (2) (s1 , s2 , t1 , t2 ) in R. Distinguishis a transition s1 , s2 −−two cases.α→ t1 , t2 arises by an individual move of either TS11.

α ∈ Act \ H. Then s1 , s2 −−αor TS2 . By symmetry, we may assume that s1 −−→ 1 t1 and s2 = t2 . Since (s1 , s1 )α → 1 t1 in TS1 with (t1 , t1 ) ∈belongs to bisimulation R1 , there exists a transition s1 −−α→ t1 , s2 is a transition in TS1 H TS2 and (t1 , s2 , t1 , s2 ) ∈ R.R1 . Thus, s1 , s2 −−α→ t1 , t2 arises by synchronizing transitions in TS1 and TS2 .2. α ∈ H. Then s1 , s2 −−αα→ 2 t2 a transition in TS2 . SinceThat is, s1 −−→ 1 t1 is a transition in TS1 and s2 −−α → i ti in TSi (for i = 1, 2) with (ti , ti ) ∈ Ri .(si , si ) ∈ Ri , there exists a transition si −−α→ t1 , t2 is a transition in TS1 H TS2 and (t1 , t2 , t1 , t2 ) ∈ R.Thus, s1 , s2 −−The fulfillment of condition (B.3’) follows by a symmetric argument.Let us now consider the relation between state-based and action-based bisimulation inmore detail.

We first discuss how an action-based bisimulation can be obtained fromBisimulation467a state-based bisimulation, and the reverse. This is done for transition system TS =(S, Act, →, I, AP, L).Consider the bisimulation ∼TS on S. The intention is to define a transition systemTSact = (Sact , Act, →act , Iact , APact , Lact )coincide. As our interest is in actionsuch that ∼TS and the action-based bisimulation ∼ActTSbased bisimulation on TSact , APact and Lact are irrelevant, and can be taken as AP and/ S).

TSact has the sameL, respectively. Let Sact = S ∪ { t } where t is a new state (i.e., t ∈initial states as TS, i.e., Iact = I, and is equipped with the action set Act = 2AP ∪ { τ }.The transition relation →act is given by the rules:s −→ sL(s)s −−−→ act sands is a terminal state in TSτs −→act tThus, the new state t serves to characterize the terminal states in TS. For bisimulationR for TS, Ract = R ∪ { (t, t) } is an action-based bisimulation for TSact . Vice versa, foraction-based bisimulation Ract for TSact , Ract ∩ (S × S) is a bisimulation for TS. Thus,for all states s1 , s2 ∈ S:s1 ∼TS s2if and only if s1 ∼ActTSact s2 .Let us now consider the reverse direction.

Consider the action-based bisimulation ∼ActTSon S. The intention is to define a transition systemTSstate = (Sstate , Actstate , →state , Istate , APstate , Lstate )and the bisimulation ∼TSstate coincide. As our interest is in a state-basedsuch that ∼ActTSbisimulation, the action-set Actstate is not of importance. Let Sstate = S ∪ (S × Act)where it is assumed that S ∩ (S × Act) = ∅. (Such construction is also used to compareaction-based vs. state-based fairness on page 263) Take Istate = I. The actions of TS serveas atomic propositions in TSstate , i.e., APstate = Act.

The labeling function of Lstate isdefined by L(s) = ∅ and L(s, α) = { α }. The transition relation →state is defined bythe rules:ααs −−→ s→ s , β ∈ Acts −−ands −→state s , αs, β −→state s , αThat is, state s, α in TSstate serves to simulate state s in TS. In fact, the secondcomponent α indicates the action via which s is entered. It now follows that for all statess1 , s2 ∈ S (see Exercise 7.5):s2s1 ∼ActTSif and only if s1 ∼TSstate s2 .4687.2Equivalences and AbstractionBisimulation and CTL∗ EquivalenceThis section considers the equivalence relations induced by the temporal logics CTL andCTL∗ and discusses their connection to bisimulation equivalence.

As in the chapters ontemporal logic, this section is restricted to transition systems that do not have any terminalstates. These transition systems thus only have infinite paths.States in a transition system are equivalent with respect to a logic whenever these statescannot be distinguished by the truth value of any of such formulae. Stated differently,whenever there is a formula in the logic that holds in one state, but not in the other, thesestates are not equivalent.Definition 7.17.CTL∗ EquivalenceLet TS, TS1 , and TS2 be transition systems over AP without terminal states.1.

States s1 , s2 in TS are CTL∗ -equivalent, denoted s1 ≡CTL∗ s2 , ifs1 |= Φiffs2 |= Φfor all CTL∗ state formulae over AP.2. TS1 and TS2 are CTL∗ -equivalent, denoted TS1 ≡CTL∗ TS2 , ifTS1 |= ΦiffTS2 |= Φfor all CTL∗ state formulae over AP.States s1 and s2 are CTL∗ equivalent if there does not exist a CTL∗ state formula thatholds in s1 and not in s2 , or, vice versa, holds in s2 , but not in s1 . This definition can easilybe adapted to any subset of CTL∗ , e.g., s1 and s2 are CTL equivalent, denoted s1 ≡CTL s2 ,if for all CTL formulae Φ over AP, { s1 , s2 } ⊆ Sat(Φ) or { s1 , s2 } ∩ Sat(Φ) = ∅. Similarly,s1 and s2 are LTL-equivalent, denoted s1 ≡LTL s2 , if s1 and s2 satisfy the same LTLformula over AP.The fact that trace-equivalent transition systems satisfy the same LTL formulae (see Theorem 3.15 on page 104) can now be stated as follows:Theorem 7.18.≡trace ⊆ ≡LTL.Trace Equivalence is Finer Than LTL EquivalenceBisimulation and CTL∗ EquivalenceRemark 7.19.469Distinguishing Nonequivalent States by FormulaeLet TS be a transition system without terminal states and s1 , s2 states in TS.

If s1 ≡CTLs2 , then there exists a CTL state formula Φ with s1 |= Φ and s2 |= Φ. This follows fromthe definition of CTL equivalence which yields the existence of a formula Φ with (i) s1 |= Φand s2 |= Φ or (ii) s1 |= Φ and s2 |= Φ. In case (ii), one may switch from Φ to ¬Φ andobtain s1 |= ¬Φ and s2 |= ¬Φ.A corresponding result holds for CTL∗ , but not for LTL.

This can be seen as follows.Assume that s1 ≡LTL s2 and Traces(s1 ) is a proper subset of Traces(s2 ). Then, all LTLformulae that hold for s2 also hold for s1 . However, since there are traces in Traces(s2 )that are not in Traces(s1 ), there exists an LTL formula ϕ (e.g., characterizing such trace)with s2 |= ϕ, but s1 |= ϕ.The main result of this section is stated in Theorem 7.20 (see below). It asserts that CTLequivalence, CTL∗ equivalence, and bisimulation equivalence coincide. This theorem hasvarious important consequences. First, and for all, it relates the notion of bisimulationequivalence to logical equivalences. As a result, bisimulation equivalence preserves allformulae that can be formulated in CTL∗ or CTL.

In principle this result allows performingmodel checking on the bisimulation quotient transition system—assuming that we canobtain this in an algorithmic manner—while preserving both affirmative and negativeoutcomes of the model checking. If a CTL∗ formula holds for the quotient, it also holdsfor the original transition system. Moreover, if the formula is refuted by the quotient, theoriginal transition system refutes it too. On the other hand, it indicates that a single CTL∗formula that holds for one but not for the other state suffices to show the nonbisimilarityof the states.Secondly, the fact that CTL and CTL∗ equivalence coincide is perhaps surprising as CTL∗is strictly more expressive than CTL as CTL∗ subsumes LTL, but the expressivenessesof CTL and LTL are incomparable, see Theorem 6.21 on page 337.

So, although theexpressiveness of CTL∗ is strictly larger than that of CTL, their logical equivalence is thesame. In particular, to show CTL∗ equivalence it suffices to show CTL equivalence!Theorem 7.20.CTL∗ /CTL and Bisimulation EquivalenceFor finite transition system TS without terminal states:∼TS=≡CTL=≡CTL∗ .Proof: The proof of this central result is divided into three steps. First, it is shown thatCTL equivalence is finer than bisimulation equivalence, i.e., ≡CTL ⊆ ∼TS ; see Lemma470Equivalences and Abstraction7.21 below. Subsequently, it is proven that bisimulation equivalence is finer than CTL∗equivalence, i.e., ∼TS ⊆ ≡CTL∗ ; see Lemma 7.26 on page 473.

The obvious fact that CTL∗equivalence is finer than CTL equivalence (since CTL∗ subsumes CTL) completes theproof. Summarizing, we have:∼TS ⊆ ≡CTL∗and≡CTL∗ ⊆ ≡CTLandLemma 7.21Lemma 7.26Lemma 7.21.≡⊆ ∼TS CTL CTL Equivalence is Finer Than BisimulationFor finite transition system TS without terminal states, and s1 , s2 states in TS:s1 ≡CTL s2impliess1 ∼TS s2 .Proof: It suffices to show that the relation:R = { (s1 , s2 ) ∈ S × S | s1 ≡CTL s2 }is a bisimulation for TS. This is proven by checking the conditions of being a bisimulation(see Definition 7.7 on page 456). As R is, by definition, an equivalence relation, it sufficesto consider the first two conditions. Let (s1 , s2 ) ∈ R, i.e., s1 ≡CTL s2 .1. Consider the following CTL state formula Φ over AP:Φ =a∈L(s1 )a∧a∈AP\L(s1 )¬a.Clearly, s1 |= Φ.