5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 67
Текст из файла (страница 67)
Consider, for example, the followingstatement:♦ (ϕ ∨ ψ) ≡ ♦ ϕ ∨ ♦ ψ,which is valid for any path. The same is true for:∃♦ (Φ ∨ Ψ) ≡ ∃♦ Φ ∨ ∃♦ Ψ.This can be seen as follows.⇐: Assume that s |= ∃♦ Φ ∨ ∃♦ Ψ. Then, without loss of generality, we may assumethat s |= ∃♦ Φ. This means that there is some state s (possibly s = s ), reachablefrom state s, such that s |= Φ. But then s |= Φ ∨ Ψ. This means that there exists areachable state from s which satisfies Φ ∨ Ψ. By the semantics of CTL it now followsthat s |= ∃♦ (Φ ∨ Ψ).⇒: Let s be an arbitrary state such that s |= ∃♦ (Φ ∨ Ψ).
Then there exists a state s(possibly s = s ) such that s |= Φ ∨ Ψ. Without loss of generality we may assume thats |= Φ. But then we can conclude that s |= ∃♦ Φ, as s is reachable from s. Therefore wealso have s |= ∃♦ Φ ∨ ∃♦ Ψ.However, ∀♦ (Φ ∨ Ψ) ≡ ∀♦ Φ ∨ ∀♦ Ψ since ∀♦ (Φ ∨ Ψ) ⇒ ∀♦ Φ ∨ ∀♦ Ψ is invalid asshown by the following transition system:332Computation Tree Logicsss{a}{b}For each path that starts in state s we have that ♦ (a ∨ b) holds, so s |= ∀♦ (a ∨ b).
Thisfollows directly from the fact that each path visits either state s or state s eventually,and s |= a ∨ b and the same applies to s . However, state s does not satisfy ∀♦ a ∨ ∀♦ b.For instance, path s (s )ω |= ♦ a but s (s )ω |= ♦ b. Thus, s |= ∀♦ b. By a similar reasoningapplied to path s (s )ω it follows that s |= ∀♦ a. Thus, s |= ∀♦ a ∨ ∀♦ b. Stated in words,not all computations that start in state s eventually reach an a-state nor do they alleventually reach a b-state.6.2.4Normal Forms for CTLThe duality law for ∀ Φ shows that ∀ can be treated as a derived operator of ∃ .That is to say, the basic operators ∃ , ∃ U, and ∀ U would have been sufficient to define thesyntax of CTL.
The following theorem demonstrates that we can even omit the universalpath quantifier and define all temporal modalities in CTL using the basic operators ∃ ,∃ U, and ∃ .Definition 6.13.Existential Normal Form (for CTL)For a ∈ AP, the set of CTL state formulae in existential normal form (ENF, for short) isgiven byΦ ::= trueTheorem 6.14.aΦ 1 ∧ Φ2¬Φ∃ Φ∃(Φ1 U Φ2 )Existential Normal Form for CTLFor each CTL formula there exists an equivalent CTL formula in ENF.∃ Φ.Computation Tree Logic333Proof: The following duality laws allow elimination of the universal path quantifier andthus provide a translation of CTL formulae into equivalent ENF formulae:∀ Φ≡ ¬∃ ¬Φ,∀(Φ U Ψ) ≡ ¬∃(¬Ψ U (¬Φ ∧ ¬Ψ)) ∧ ¬∃ ¬Ψ.Recall that the basis syntax of CTL only uses ∃ , ∃ U and ∀ and ∀ U.
Thus, the tworules used in the proof of Theorem 6.14 allow the removal of all universal quantifiers froma given CTL formula. However, when implementing the translation from CTL formulaeto ENF formulae one might use analogous rules for the derived operators, such as∀♦ Φ ≡¬ ∃ ¬ Φ,∀ Φ ≡¬ ∃♦ ¬ Φ = ¬ ∃(true U Φ).Since the rewrite rule for ∀ U triples the occurrences of the right formula Ψ, the translationfrom CTL to ENF can cause an exponential blowup.Another normal form of importance is the positive normal form. A CTL formula is saidto be in positive normal form (PNF, for short) whenever negations only occur adjacentto atomic propositions.
That is, e.g., ¬∀(a U ¬b) is not in PNF, whereas ∃(¬a ∧ ¬b U a) isin PNF. To ensure that every CTL formula is equivalent to a formula in PNF, for eachoperator a dual operator is necessary. We have that conjunction and disjunction are dual,and that is dual to itself. As for LTL, we adopt the weak until operator W as a dualoperator of U.Definition 6.15.Positive Normal Form (for CTL)The set of CTL state formulae in positive normal form (PNF, for short) is given byΦ ::= true falsea¬a Φ1 ∧ Φ2Φ1 ∨ Φ2∃ϕ ∀ϕwhere a ∈ AP and the path formulae are given byϕ ::= Φ Φ1 U Φ2Theorem 6.16.Φ1 W Φ2 .Existence of Equivalent PNF FormulaeFor each CTL formula there exists an equivalent CTL formula in PNF.334Computation Tree LogicProof: Any CTL formula can be transformed into PNF by successively “pushing” negations“inside” the formula at hand.
This is facilitated by the following equivalence laws:¬true¬¬Φ¬(Φ ∧ Ψ)¬∀ Φ¬∃ Φ¬∀(Φ U Ψ)¬∃(Φ U Ψ)≡≡≡≡≡≡≡falseΦ¬Φ ∨ ¬Ψ∃ ¬Φ∀ ¬Φ∃((Φ ∧ ¬Ψ) W (¬Φ ∧ ¬Ψ))∀((Φ ∧ ¬Ψ) W (¬Φ ∧ ¬Ψ)).Due to the fact that in the rules for ∀ U and ∃ U the number of occurrences of Ψ (and Φ)is doubled, the length of an equivalent CTL formula may be exponentially longer than theoriginal CTL formula.
3 The same phenomenon appeared in defining the PNF for LTLwhen using the weak-until operator. As for LTL, this exponential blowup can be avoided byusing the release operator, which in CTL can be defined by: ∃(Φ R Ψ) = ¬∀((¬Φ) U (¬Ψ))and ∀(Φ R Ψ) = ¬∃((¬Φ) U (¬Ψ)).6.3Expressiveness of CTL vs. LTLAlthough many relevant properties of reactive systems can be specified in LTL and CTL,the logics CTL and LTL are incomparable according to their expressiveness. More precisely, there are properties that one can express in CTL, but that cannot be expressed inLTL, and vice versa.Let us first define what it means for CTL and LTL formulae to be equivalent. Intuitivelyspeaking, equivalent means “express the same thing”.
More precisely:Definition 6.17.Equivalence between CTL- and LTL FormulaeCTL formula Φ and LTL formula ϕ (both over AP) are equivalent, denoted Φ ≡ ϕ, if forany transition system TS over AP:TS |= Φ if and only if TS |= ϕ.3rules for ¬∀“U and ¬∃ U couldbe simplified by ¬∀(Φ U Ψ) ≡“ Although the rewrite””∃ (¬Ψ) W (¬Φ ∧ ¬Ψ) and ¬∃(Φ U Ψ) ≡ ∀ (¬Ψ) W (¬Φ ∧ ¬Ψ) , there is still a duplication of formulaΨ.Expressiveness of CTL vs. LTL335The LTL formula ϕ holds in state s of a transition system whenever all paths starting ins satisfy ϕ. Given this (semantical) universal quantification over paths, it seems naturalthat, e.g., the LTL formula ♦a is equivalent to the CTL formula ∀♦a.
This seems tosuggest that for a given CTL formula, an equivalent LTL formula is obtained by simplyomitting all universal path quantifiers (as these are implicit in LTL). The following resultby Clarke and Draghicescu [85] (for which the proof is omitted) shows that dropping all(universal and existential) quantifiers is a safe way to generate an equivalent LTL formula,provided there are equivalent LTL formulae:Theorem 6.18.LTL FormulaeCriterion for Transforming CTL Formulae into EquivalentLet Φ be a CTL formula, and ϕ the LTL formula that is obtained by eliminating all pathquantifiers in Φ.
Then:Φ ≡ ϕ or there does not exist any LTL formula that is equivalent to Φ.For the following CTL formulae, an equivalent LTL formula is obtained by simply omittingall path quantifiers: a, ∀ a, ∀(a U b), ∀♦ a, ∀ a, and ∀ ∀♦ a. The fact that the CTLformula ∀ ∀♦ a is equivalent to the LTL formula ♦ a has been established earlier inRemark 6.8 (326).
However, ∀♦ ∀ a and ♦ a are not equivalent. The LTL formula ♦aensures that a will eventually forever (i.e., continuously from some point on) hold. Thesemantics of ∀♦ ∀ a is different, however. The CTL formula ∀♦ ∀ a asserts that on anycomputation, eventually some state, s say, is reached such that s |= ∀ a. Note thats |= ∀♦ ∀aΦif and only if for any path π = s0 s1 s2 . .
. ∈ Paths(s), sj |= Φ for some j. For Φ = ∀ a,this entails that for any such path π there is some state sj such that all reachable statesfrom sj satisfy the atomic proposition a.Lemma 6.19.PersistenceThe CTL formula ∀♦∀a and the LTL formula ♦a are not equivalent.Proof: Consider the following transition system TS over AP = { a }:336Computation Tree Logics0s1s2{a}∅{a}The initial state s0 satisfies the LTL formula ♦ a, since each path starting in s0 eventuallyremains forever in one of the two states s0 or s2 , which are both labeled with a.
The CTLformula ∀♦ ∀ a, however, does not hold in s0 , since we have sω0 |= ♦ ∀ a (as s0 |= ∀ a).This is due to the fact that the path s∗0 s1 sω2 passes through the ¬a-state s1 . Thus, sω0is a path starting in s0 which will never reach a state satisfying ∀a, i.e., sω0 |= ♦ ∀ a.Accordingly, it follows thats0 |= ∀♦ ∀ a.Given that the CTL formulae ∀♦ ∀ a and the LTL formula ♦ a are not equivalent andthe fact that ♦ a is obtained from ∀♦ ∀ a by eliminating the universal path quantifiers,it follows from Theorem 6.18 that there does not exist an LTL formula that is equivalentto ∀♦ ∀ a.
In a similar way, it can be shown that the CTL formulae ∀♦ (a ∧ ∀ a)and ♦ (a ∧ a) are not equivalent, and thus, the requirement ∀♦ (a ∧ ∀ a) cannot beexpressed in LTL.Lemma 6.20.Eventually an a-State with only direct a-SuccessorsThe CTL formula ∀♦ (a ∧ ∀ a) and the LTL formula ♦ (a ∧ a) are not equivalent.Proof: Consider the transition system depicted in Figure 6.6. All paths that start in theinitial state s0 have either as prefix the path fragment s0 s1 or s0 s3 s4 . Clearly, all suchpaths satisfy the LTL formula ♦ (a ∧ a), and so, s0 |= ♦ (a ∧ a).
On the otherhand, however, s0 |= ∀♦ (a ∧ ∀ a) as the path s0 s1 (s2 )ω does not satisfy ♦ (a ∧ ∀ a).This follows from the fact that state s0 has the non-a-state s3 as direct successor, i.e.,s0 |= a ∧ ∀ a.These examples show that certain requirements that can be expressed in CTL, cannotbe expressed in LTL. The following theorem provides, in addition, some examples ofLTL formulae for which no equivalent CTL formula exists.
This establishes that theexpressiveness of the temporal logics LTL and CTL are incomparable.Expressiveness of CTL vs. LTL337∅s3s2s1s0∅{a}{a}s4{a}Figure 6.6: Transition system for ∀♦ (a ∧ ∀ a).∅{a}∅{a}s0t0s0t0Figure 6.7: The base transition systems: TS0 (left) and TS0 (right).Theorem 6.21.Incomparable Expressiveness of CTL and LTL(a) There exist LTL formulae for which no equivalent CTL formula exists. This holdsfor, for instance♦aor♦(a ∧ a).(b) There exist CTL formulae for which no equivalent LTL formula exists.
This holdsfor, for instance∀♦ ∀ aand∀♦ (a ∧ ∀ a)and∀ ∃♦ a.Proof:(a) Consider the formula ♦ a. The proof for ♦ (a ∧ a) goes along similar lines andis omitted here. Consider the two series of transition systems TS0 , TS1 , TS2 , . . . andTS0 , TS1 , TS2 , . . . that are inductively defined as follows (see Figures 6.7 and 6.8).338Computation Tree Logic∅{a}sntn∅{a}sntnTSn−1TSn−1Figure 6.8: Inductive construction of TSn (upper) and TSn (lower).For all transition systems, AP = { a }, and the action labels are not important. Let,for n 0,TSn = (Sn , { τ }, →n , { sn }, { a }, Ln )andTSn = (Sn , { τ }, →n , { sn }, { a }, Ln )where S0 = { s0 , t0 }, S0 = { s0 , t0 }, and for n > 0:∪ { sn , tn } and Sn = Sn−1∪ { sn , tn }.Sn = Sn−1The labeling functions are defined such that all states ti are labeled with { a } andall states si are labeled with ∅.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
