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

The vertices of the diagram are relations, and an edge from R to Rmeans that R is strictly finer than R , that is to say, R is more distinctive than R . Recallthat for AP-deterministic transition systems, ∼, - and trace equivalence coincide.7.5Simulation and ∀CTL∗ EquivalenceThe aim of this section is to provide a logical characterization of the simulation order ,.This amounts establishing an analogous result to the theorem stating that bisimulationequivalence coincides with CTL∗ (and CTL) equivalence for finite transition systems without terminal states.

That is to say, given two transition systems TS1 and TS2 , the aimis to characterize the relation , in terms of the satisfaction relations on TS1 and TS2 forsome temporal logic. In fact, from the results of the previous section, it can be inferredthat for transition systems without terminal states, TS1 , TS2 implies trace inclusion ofTS1 and TS2 , and thus whenever TS2 |= ϕ for a LTL formula ϕ, it follows TS1 |= ϕ.

Inthis section, it is shown that this not only applies to any LTL formula, but for a fragment516Equivalences and Abstractionof CTL∗ that includes LTL.Since , is not symmetric, it cannot be expected that , can be characterized by a sublogicof CTL∗ which allows negation of arbitrary state formulae. This can be seen as follows.Let L be a fragment of CTL∗ which is closed under negation, i.e., Φ ∈ L implies ¬Φ ∈ L,such that for any transition system TS without terminal states and states s1 , s2 of TS:s1 ,TS s2ifffor all state formulae Φ of L: s2 |= Φ =⇒ s1 |= Φ.Let s1 ,TS s2 .

Note that s2 |= ¬Φ implies s1 |= ¬Φ, i.e., s1 |= ¬Φ implies s2 |= ¬Φ. Then,for any state formula Φ of L:s1 |= Φ =⇒ s1 |= ¬Φ =⇒ s2 |= ¬Φ =⇒ s2 |= Φ.Hence, s2 ,TS s1 . Thus, a logic that characterizes ,TS cannot be closed under negation,as that would require ,TS to be symmetric which, however, is not the case.The proof of the path-lifting lemma (Lemma 7.55 on page 504) informally explains whyfor every LTL formula ϕ such that s2 |= ϕ we have s1 |= ϕ.

This observation can begeneralized for CTL∗ formulae of the form ∀ϕ, provided that the state formulae in ϕcontain neither negation nor existential quantification. These considerations motivate thedefinition of the universal fragment of CTL∗ , denoted ∀CTL∗ .Definition 7.74.Universal Fragment of CTL∗The universal fragment of CTL∗ , denoted ∀CTL∗ , consists of the state formulae Φ andpath formulae ϕ given, for a ∈ AP, byΦ ::= trueϕ ::= Φfalseϕ¬aΦ1 ∧ Φ2Φ1 ∨ Φ2ϕ1 ∧ ϕ2ϕ1 ∨ ϕ2ϕ1 U ϕ2a∀ϕϕ1 R ϕ2 .State formulae in ∀CTL∗ are required to be in positive normal form, (negations may onlyoccur adjacent to atomic propositions) and do not contain existential path quantifiers.Due to the positive normal form (PNF, for short), the release operator R is considered asa basic operator in the logic.

The universal fragment of CTL, denoted ∀CTL, is obtainedfrom the definition of ∀CTL∗ by restricting the path formulae toϕ ::= ΦΦ1 U Φ2Φ1 R Φ2 .Simulation and ∀CTL∗ Equivalence517The eventually and always operators are obtained by the ∀CTL∗ path formulae ♦ϕ =true U ϕ and ϕ = false R ϕ. Similarly, in ∀CTL these modalities are obtained by ∀♦Φ =∀(true U Φ) and ∀Φ = ∀(false R Φ).∀CTL∗ covers all safety properties that can be expressed in CTL∗ . The following resultshows that for any LTL formula there exists an equivalent ∀CTL∗ formula.Lemma 7.75.∀CTL∗ Includes LTLFor every LTL formula ϕ there exists an equivalent ∀CTL∗ formula.Proof: It follows from Theorem 5.24 (page 257) that for any LTL formula ϕ there existsan equivalent LTL formula in PNF.

From the definition of ∀CTL∗ and positive normalform LTL, it follows directly that any LTL formula in PNF can be regarded as a ∀CTL∗formula.Vice versa, the universal fragment of CTL∗ is more expressive than LTL, as, e.g., ∀♦∀ais a ∀CTL∗ formula that has no equivalent LTL formula. The following theorem indicatesa temporal logic characterization of the simulation order by ∀CTL∗ and ∀CTL.Theorem 7.76.Simulation Order and ∀CTL∗ /∀CTLLet TS be a finite transition system without terminal states and s1 , s2 be states of TS. Thefollowing statements are equivalent:(a) s1 ,TS s2 .(b) For all ∀CTL∗ formulae Φ: s2 |= Φ implies s1 |= Φ.(c) For all ∀CTL formulae Φ: s2 |= Φ implies s1 |= Φ.Proof: The proof technique is analogous to Theorem 7.20 (page 469).(a) =⇒ (b) follows from the following claims that hold for arbitrary (i.e., not necessarilyfinite) transition system TS with state space S:(i) if s1 ,TS s2 , then for all ∀CTL∗ state formulae Φ: s2 |= Φ implies s1 |= Φ.(ii) if π1 ,TS π2 , then for all ∀CTL∗ path formulae ϕ: π2 |= ϕ implies π1 |= ϕ.518Equivalences and AbstractionThe proof of these claims is by structural induction, similar to Lemma 7.26 (page 473),and is omitted here.

See also Exercise 7.14. For the treatment of formulas ∀ϕ in the stepinduction for (i), the assumption that the given transition system does not have terminalstates is crucial, since it permits path lifting rather than just path fragment lifting.(b) =⇒ (c) is obvious since ∀CTL is a sublogic of ∀CTL∗ .(c) =⇒ (a). Let S be the state space of the finite transition system TS.

It suffices to showthatR = { (s1 , s2 ) ∈ S × S | ∀Φ ∈ ∀CTL∗ . s2 |= Φ ⇒ s1 |= Φ }is a simulation for TS. This is proven by checking the conditions of a simulation relation.Let (s1 , s2 ) ∈ R.1. If AP is finite, then we can argue by means of the formulaΦ =a∈L(s2 )a ∧a∈AP\L(s2 )¬a.Note that Φ is a propositional formula in PNF, and hence a ∀CTL formula. Sinces2 |= Φ and (s1 , s2 ) ∈ R, we obtain s1 |= Φ. As Φ uniquely characterizes the labelingof s1 , we have L(s1 ) = L(s2 ).If AP is infinite we need a slightly different argument.

Let a ∈ AP. If a ∈ L(s2 ),then s2 |= a. Since the atomic proposition a is a ∀CTL formula, we get s1 |= a (by/ L(s2 ), then s2 |= ¬a.definition of R), and therefore a ∈ L(s1 ). Similarly, if a ∈Again, as ¬a is a ∀CTL formula and by definition of R, we get s1 |= ¬a, and hencea∈/ L(s1 ). This yields L(s1 ) = L(s2 ).2.

The idea for establishing the condition (2) of simulation relations is to define a ∀CTLmaster formula Φu for the downward closure of state u with respect to R, i.e.,Sat(Φu ) = u↓ = { t ∈ S | (t, u) ∈ R }./ u↓ then, accordingThe definition of Φu is as follows. If u, t are states in TS with t ∈to the definition of u↓ and R, there exists a ∀CTL formula Φu,t such that u |= Φu,tand t |= Φu,t . Let Φu be the conjunction of all formulae Φu,t where t ∈ u↓:Φu,tΦu =t∈S(t,u)∈RAs TS is finite, Φu arises by a finite conjunction, and thus, it is a ∀CTL formula.

Infact, Φu is a master formula for u↓:Sat(Φu ) = u↓Simulation and ∀CTL∗ Equivalence519Let us check this. If v ∈/ u↓ then (v, u) ∈/ R and Φu has the form . . . ∧ Φu,v ∧ . . ../ Sat(Φu ). Vice versa, if v ∈ u↓ thenHence, v |= Φu (as v |= Φu,v ), and therefore v ∈(v, u) ∈ R. As u |= Φu we get v |= Φu (by definition of R). Hence, v ∈ Sat(Φu ).It remains to prove that whenever (s1 , s2 ) ∈ R and s1 → s1 , we have that s2 → s2such that (s1 , s2 ) ∈ R.

Since TS is finite, the set of direct successors of s2 is finite, sayPost(s2 ) = { u1 , . . . , uk }. Let Φi = Φui be the master formula for ui ↓, for 0 < i k.From ui ∈ ui ↓, it follows ui |= Φi . Hence:!Φis2 |= ∀Since (s1 , s2 ) ∈ R and ∀ 0<ik"0<ikΦi is a ∀CTL formula, we have:s1 |= ∀!Φi1ikSince s1 ∈ Post(s1 ), s1 ∈ Sat(Φi ) for some i ∈ { 1, .

. . , k }. Hence, s1 ∈ ui ↓, i.e.,(s1 , ui ) ∈ R. Taking s2 = ui , we obtain s2 → s2 and (s1 , s2 ) ∈ R.Theorem 7.76 can be reformulated for the simulation order between transition systems.This yieldsTS1 , TS2 if and only if TS2 |= Φ ⇒ TS1 |= Φfor any ∀CTL∗ (or ∀CTL) formula Φ. As the proof of Theorem 7.76 does not exploit theuntil operator, this result applies to the fragment of CTL∗ that consists of literals (i.e.,atomic propositions and their negations), conjunction, disjunction, and the modality ∀ .Example 7.77.Distinguishing Nonsimilar Transition SystemsConsider the transition systems TS1 (left) and TS2 (right) in Figure 7.28. TS1 is simulatedby TS2 , but due to the self-loop in the initial state, TS2 , TS1 . This can also be establishedby providing a ∀CTL formula Φ such that, e.g., TS1 |= Φ whereas TS2 |= Φ.

Such a ∀CTLformula isΦ = ∀ (∀ ¬a ∨ ∀ a).An alternative logical characterization of , is obtained by replacing the universal quantifier∀ by the existential quantifier ∃ using the CTL∗ duality rule: ∀ϕ ≡ ¬∃¬ϕ. Theorem 7.76yields:s1 ,TS s2 iff for all formulae ∃ϕ: s1 |= ∃ϕ implies s2 |= ∃ϕ.520Equivalences and Abstraction{ a } s1∅ v1{ a } s2t1 { a }∅ v2t2 { a }Figure 7.28: TS1 , TS2 , but TS2 , TS1 .Here, ϕ is an arbitrary CTL∗ path formula that does not contain universal path quantifiers,and is in PNF.

Such formulae are ∃CTL∗ formulae.Definition 7.78.Existential Fragment of CTL∗The existential fragment of CTL∗ , denoted ∃CTL∗ , consists of the state formulae Φ andpath formulae ϕ given, for a ∈ AP, byΦ ::= trueϕ ::= Φfalseϕ¬aΦ1 ∧ Φ2Φ1 ∨ Φ2ϕ1 ∧ ϕ2ϕ1 ∨ ϕ2ϕ1 U ϕ2a∃ϕϕ1 R ϕ2 .The existential fragment of CTL, denoted ∃CTL, is obtained by restricting the pathformulae in the above definition toϕ ::= ΦΦ1 U Φ2Φ1 R Φ2 .The modalities eventually and always can be derived as for ∀CTL∗ and ∀CTL.Theorem 7.79.Simulation Order and ∃CTL∗ /∃CTLLet TS be a finite transition system without terminal states, and s1 , s2 states of TS.

Then,the following statements are equivalent:(a) s1 ,TS s2 .(b) For all ∃CTL∗ formulae Φ: s1 |= Φ implies s2 |= Φ.(c) For all ∃CTL formulae Φ: s1 |= Φ implies s2 |= Φ.Simulation-Quotienting Algorithms521Proof: Directly from Theorem 7.76, as statements (b) and (c) here are the duals to statements (b) and (c) in Theorem 7.76.Corollary 7.80.Characterizations of Simulation EquivalenceLet TS be a finite transition system without terminal states and s1 , s2 be states in TS.Then the following five statements are equivalent:(a) s1 -TS s2 .(b) s1 and s2 satisfy the same ∀CTL∗ formulae.(c) s1 and s2 satisfy the same ∀CTL formulae.(d) s1 and s2 satisfy the same ∃CTL∗ formulae.(e) s1 and s2 satisfy the same ∃CTL formulae.Proof: From Theorems 7.76 and 7.79.In fact, this result can be strengthened as the listed equivalences coincide with the logicalequivalence on the sublogic of CTL that just contains atomic propositions and their negations, conjunction, disjunction, and the next-step operator , with either a universal orexistential path quantifier.7.6Simulation-Quotienting AlgorithmsThis section presents algorithms for obtaining the simulation quotient TS/ - for finitetransition system TS.

Such algorithms serve two purposes. First, they can be used toverify whether TS1 - TS2 by considering the simulation quotient of TS1 ⊕ TS2 (see page457). Secondly, such algorithms can be used to obtain the abstract (and thus smaller)transition system TS/- in a fully automated manner. As TS - TS/-, it follows thatany verification result for TS/ -, either being negative or positive, carries over to TS.This applies to any formula expressed in either the universal or existential fragment ofCTL or CTL∗ . Since simulation equivalence is coarser than bisimulation equivalence, thequotient TS/- is at most as large as—but maybe significantly smaller than—TS/∼.