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

Since s1 ≡CTL s2 , it follows that s2 |= Φ. As Φ characterizesthe labeling of state s1 , we immediately get L(s1 ) = L(s2 ). Thus, condition (1) ofDefinition 7.7 holds.2. For any equivalence class C ∈ S/R, let CTL formula ΦC be such that(∗)Sat (ΦC ) = C.ΦC is obtained as follows. For every pair (C, D) of equivalence classes C, D ∈ S/Rwith C = D, let CTL formula ΦC,D be such that Sat (ΦC,D ) ⊇ C and Sat (ΦC,D ) ∩D = ∅. Since TS is finite, there are only finitely many equivalence classes under R.Hence, ΦC can be defined as the conjunction of all formulae ΦC,D :Bisimulation and CTL∗ Equivalence471ΦC=ΦC,D .D∈S/RD=CClearly, condition (∗) is satisfied.Let B ∈ S/R and s1 , s2 ∈ B, i.e., (s1 , s2 ) ∈ R and B is the equivalence class ofs1 , s2 with respect to R. Further, let s1 ∈ Post(s1 ) and C be the equivalence classof s1 with respect to R, i.e., C = [s1 ]R .

Now we show the existence of a transitions2 → s2 with (s1 , s2 ) ∈ R.Due to s1 ∈ Post(s1 ) ∩ C and (∗), we have s1 |= ∃ ΦC . Since s1 ≡CTL s2 , weget s2 |= ∃ ΦC . Thus, there is a state s2 ∈ Post(s2 ) with s2 |= ΦC . But thenequation (∗) yields s2 ∈ C. Since C = [s1 ]R , we obtain (s1 , s2 ) ∈ R.Remark 7.22.Master FormulaeThe proof of Lemma 7.21 relies on establishing so-called master formulae ΦC for equivalence class C such that Sat(ΦC ) = C.

To indicate how to obtain such master formulae,consider the bisimulation quotient of the Bakery algorithm (see Figure 7.9 on page 464),and let AP = { crit1 , crit2 }. Instead of considering the conjunction of formulae ΦC,D ,master formulae can be obtained by inspecting the transition system. The equivalenceclass C = wait1 , wait2 , x1 > x2 > 0 is, given the atomic propositions in AP, uniquelycharacterized by the fact that none of the processes is currently in the critical section andthe second process acquires access to the critical section immediately. A master formulaΦC for C thus isΦC = ¬crit1 ∧ ¬crit2 ∧ ∀ crit2 .A master formula for the equivalence class D = wait1 , crit2 , −− isΦD = crit2 ∧ ∀ ¬crit2 .It is easy to check that none of the other equivalence classes under bisimulation satisfiesΦD .Remark 7.23.Logical Characterization by a Sublogic of CTLWe stress that the proof of Lemma 7.21 only exploits the propositional fragment of CTL,i.e., atomic propositions, conjunction, and negation, and the modal operator ∃ .

It doesnot, however, rely on the presence of the until operator. Thus, bisimulation equivalence(and CTL∗ equivalence) agrees with the equivalence induced by a simple logic that onlycontains atomic propositions, negation, conjunction and ∃ . In particular, any two472Equivalences and Abstractionnonbisimilar states can be distinguished by a CTL formula that does contain neither theuntil operator U nor one of the derived operators ♦, , W or R .Remark 7.24.Infinite Transition SystemsLemma 7.21 is restricted to finite transition systems. This restriction is reflected in theproof as follows. The master formula for equivalence class C, formula ΦC is defined asthe conjunction of CTL formulae for the form ΦC,D with C = D.

As CTL only allows forfinite conjunctions, there should only be finitely many equivalence classes D = C. This isguaranteed, of course, if the transition system is finite. An extension of CTL with infiniteconjunctions would be needed to obtain a similar result for infinite transition systems.An example of an infinite transition system TS where CTL equivalence is not finer thanbisimulation equivalence is as follows. Assume the set AP of atomic propositions is infinite.The states in TS are s1 , s2 and the states tA where A is a subset of AP. States s1 , s2 arelabelled with ∅, while the label of state tA is A.

State s1 has a transition to all states tAwhere A = AP, while state s2 has transitions to all states tA , including A = AP. Thus,Post(s1 ) = {tA | A ⊆ AP, A = AP} and Post(s2 ) = {tA | A ⊆ AP}. States tA havea single outgoing transition which leads to s1 . Clearly, s1 and s2 are not bisimulationequivalent as s2 has a transition to state tAP but there is no successor of s1 with thelabel L(tAP ) = AP. On the other hand, s1 and s2 are CTL equivalent with respect toAP. This follows from the fact that (1) the set of atomic propositions that appear ina given CTL formula over AP is finite and (2) s1 , s2 are bisimulation-equivalent whenshrinking the set AP of atomic propositions to any finite subset of AP. Note that thenR = {(s1 , s2 )} ∪ {(tA , tB ) : A ∩ AP = B ∩ AP } is a bisimulation.

But then Lemma 7.26yields that s1 , s2 satisfy the same CTL formulae over AP .However, the result stated in Lemma 7.21 can also be established for (possibly infinite)transition systems that are finitely branching. This is shown in the following lemma.Recall that a transition system is finitely branching if (i) the set of initial states is finiteand (ii) for each state s the set of successors (i.e., the set Post(s)) is finite.Lemma 7.25.CTL Equivalence is Finer Than Bisimulation (Revisited)Let TS = (S, Act, →, I, AP, L) be a finitely branching transition system without terminalstates, and s1 , s2 states in TS.

Then s1 ≡CTL s2 implies s1 ∼TS s2 .Proof: As in the proof of Lemma 7.25 we show thatR = { (s1 , s2 ) ∈ S × S | s1 ≡CTL s2 }Bisimulation and CTL∗ Equivalence473is a bisimulation for TS. Let (s1 , s2 ) ∈ R. These states are equally labeled, since for anyatomic proposition a we have s1 |= a iff s2 |= a, i.e., a ∈ L(s1 ) if and only if a ∈ L(s2 ).Condition (2) is proven by contraposition. Let (s1 , s2 ) ∈ R and s1 ∈ Post(s1 ).

Assumethere is no s2 ∈ Post(s2 ) with (s1 , s2 ) ∈ R. Since TS is finitely branching, the set Post(s2 )/ R and the definition ofis finite, say it agrees with { t1 , . . . , tk }. The assumption (s1 , tj ) ∈R yields the existence of a CTL formula Ψj such thats1 |= Ψjand tj |= Ψj for 0 < j k.Now consider the formulaΦ = ∃ (Ψ1 ∧ . . . ∧ Ψk ).Clearly, we have s1 |= Ψ1 ∧ .

. . ∧ Ψk . Hence, s1 |= Φ. On the other hand, tj |= Ψ1 ∧ . . . ∧ Ψkfor 0 < j k. This yields s2 |= Φ. But then (s1 , s2 ) ∈/ R. Contradiction.The following lemma asserts that bisimilar states are CTL∗ equivalent, and is not restrictedto finite transition systems. Let π1 ∼TS π2 denote that the path fragments π1 and π2 arestatewise bisimilar, i.e., for π1 = s0,1 s1,1 s2,1 . . . and π2 = s0,2 s1,2 s2,2 . . ., we havesj,1 ∼TS sj,2 for all j 0.Lemma 7.26.Bisimulation is Finer Than CTL∗ EquivalenceLet TS be a transition system TS (over AP) without terminal states, s1 , s2 be states inTS, and π1 , π2 infinite path fragments in TS. Then:(a) If s1 ∼TS s2 , then for any CTL∗ formula Φ: s1 |= Φ if and only if s2 |= Φ.(b) If π1 ∼TS π2 , then for any CTL∗ path formula ϕ: π1 |= ϕ if and only if π2 |= ϕ.Proof: We simultaneously prove (a) and (b) by means of induction over the structure ofthe formula.Induction basis.

Let s1 ∼TS s2 . For Φ = true, statement (a) obviously holds. SinceL(s1 ) = L(s2 ), it follows that for Φ = a ∈ AP:s1 |= a iff a ∈ L(s1 ) iff a ∈ L(s2 ) iff s2 |= a .Induction step(a) Assume Φ1 , Φ2 , Ψ are CTL∗ state formulae for which proposition (a) holds, and ϕto be a CTL∗ path formula for which proposition (b) holds. Let s1 ∼TS s2 . Theproof is by structural induction on Φ:474Equivalences and AbstractionCase 1: Φ = Φ1 ∧ Φ2 .

The induction hypothesis for Φ1 and Φ2 providess1 |= Φ1 ∧ Φ2 iff s1 |= Φ1 and s1 |= Φ2iff s2 |= Φ1 and s2 |= Φ2iff s2 |= Φ1 ∧ Φ2 .Case 2: Φ = ¬Ψ. By applying the induction hypothesis for Ψ, one obtainss1 |= ¬Ψ iff s1 |= Ψiff s2 | = Ψiff s2 |= ¬Ψ.Case 3: Φ = ∃ϕ. For symmetry reasons, it suffices to shows1 |= ∃ϕ=⇒s2 |= ∃ϕ.Assume s1 |= ∃ϕ. Then there exists π1 = s0,1 s1,1 s2,1 . . . ∈ Paths(s1 ) startingin s1 = s0,1 , with π1 |= ϕ. According to the path-lifting lemma (Lemma 7.5on page 454) there exists a path π2 = s0,2 s1,2 s2,2 . . .

∈ Paths(s2 ) starting ins2 = s0,2 , such that π1 ∼TS π2 . From the induction hypothesis (on part (b)), itfollows that π2 |= ϕ. Thus, s2 |= ∃ϕ.(b) Assume statement (a) holds for CTL∗ state formula Φ, and (b) holds for CTL∗ pathformulae ϕ1 , ϕ2 , and ψ. Let π1 ∼TS π2 . Recall that πi [j .

. .] denotes the suffixsj,i sj+1,i sj+2,i . . . of πi . The proof proceeds by structural induction on ϕ:Case 1: ϕ = Φ. It follows from the CTL∗ semantics and the induction hypothesison Φ thatπ1 |= ϕ iff s0,1 |= Φ iff s0,2 |= Φ iff π2 |= ϕ.Case 2: ϕ = ϕ1 ∧ ϕ2 . By applying the induction hypothesis to ϕ1 and ϕ2 we obtainπ1 |= ϕ1 ∧ ϕ2 iff π1 |= ϕ1 and π1 |= ϕ2iff π2 |= ϕ1 and π2 |= ϕ2iff π2 |= ϕ1 ∧ ϕ2 .Case 3: ϕ = ¬ψ.

We apply the induction hypothesis to ψ and obtainπ1 |= ¬ψ iff π1 |= ψiff π2 | = ψiff π2 |= ¬ψ.Case 4: ϕ = ψ. The induction hypothesis for ψ and the path fragments πl [1 . . .],l = 1, 2, providesπ1 |= ψ iff π1 [1 . . .] |= ψiff π2 [1 . . .] |= ψiff π2 |= ψ.Bisimulation and CTL∗ Equivalence475Case 5: ϕ = ϕ1 U ϕ2 . The induction hypothesis for ϕ1 and ϕ2 and the path fragments πl [i .

. .], l = 1, 2, i = 0, 1, 2, . . ., providesπ1 |= ϕ1 U ϕ2 iff there exists an index j ∈ IN withπ1 [j . . .] |= ϕ2 andπ1 [i . . .] |= ϕ1 , i = 0, 1, . . . , j−1iff there exists an index j ∈ IN withπ2 [j . . .] |= ϕ2 andπ2 [i . . .] |= ϕ1 , i = 0, 1, . . .

, j−1iff π2 |= ϕ1 U ϕ2 .Corollary 7.27.CTL∗ /CTL- vs. Bisimulation EquivalenceFor finite transition systems TS1 , TS2 (over AP) without terminal states, the followingthree statements are equivalent:(a) TS1 ∼ TS2(b) TS1 ≡CTL TS2 , i.e., TS1 and TS2 satisfy the same CTL formulae.(c) TS1 ≡CTL TS2 , i.e., TS1 and TS2 satisfy the same CTL∗ formulae.Thus, bisimilar transition systems are equivalent with respect to all formulae that can beexpressed in CTL∗ . The fact that CTL equivalence is finer than bisimulation equivalenceproves that bisimulation equivalence is the coarsest equivalence which preserves all CTLformulae.

Stated differently, a relation which is strictly coarser than ∼ may yield a smallerquotient transition system, but cannot guarantee the preservation of all CTL formulae.The fact that CTL equivalence is finer than ∼ is useful to prove that two finite transitionsystems are not bisimilar—it suffices to indicate a single CTL formula which holds for onetransition system, but not for the other.Example 7.28.Distinguishing Nonbisimilar Systems by CTL FormulaeConsider the beverage vending machines TS1 and TS2 in Figure 7.3 on page 453. ForAP = { pay, beer, soda }, we have TS1 ∼TS TS2 .