5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 66
Текст из файла (страница 66)
Therefore, ∃ ais valid in these states. Since a ∈ L(s2 ) there is no path starting at s2 for which a isglobally valid.• ∀ a is only valid for s3 since its only path, sω3 , always visits a state in which aholds. For all other states it is possible to have a path which contains s2 that doesnot satisfy a. So for these states ∀ a is not valid.Computation Tree Logic325s1s0TS{a}s3{a}{ a, b }s2{b}(a)∃ a∀ a∃ a∀ a∃♦ (∃ a)∀(a U b)∃ (a U ( ¬ a ∧ ∀( ¬ a U b)))Figure 6.4: Interpretation of several CTL formulae.326Computation Tree Logic• ∃♦ (∃ a) is valid for all states since from each state another state (either s0 , s1 , ors3 ) can be eventually reached from which some computation can start along whicha is globally valid.• ∀(a U b) is not valid in s3 since its only computation (sω3 ) never reaches a state forwhich b holds.
In state s0 proposition a holds until b holds, and in states s1 and s2proposition b holds immediately. So, for these states the formula is true.• Finally, ∃(a U ( ¬ a ∧ ∀( ¬ a U b))) is not valid in s3 , since from s3 a b-state can neverbe reached. For the states s0 and s1 the formula is valid, since state s2 can be reachedfrom these states via an a-path; ¬ a is valid in s2 , and from s2 all possible pathssatisfy ¬ a U b, since s2 is a b-state. For instance, for state s0 the path (s0 s2 s1 )ωsatisfies a U ( ¬ a ∧ ∀( ¬ a U b)) since a ∈ L(s0 ), a ∈ L(s2 ), and b ∈ L(s1 ).
For states2 the property is valid since a is invalid in s2 and for all paths starting at s2 thefirst state is a b-state.Remark 6.8.Infinitely OftenFor a better comprehension of the semantics of CTL, let us prove that:s |= ∀∀♦a if and only if ∀π ∈ Paths(s). π[i] |= a for infinitely many i .⇒: Let s be a state, such that s |= ∀ ∀♦ a. The proof obligation is to show that everyinfinite path fragment π starting in s passes through an a-state infinitely often. Letπ = s0 s1 s2 . .
. ∈ Paths(s) and j 0. We demonstrate that there exists an index i jwith si |= a. Since s |= ∀∀♦a, we haveπ |= ∀♦a.In particular, sj |= ∀♦a. From π[j..] = sj sj+1 . . . ∈ Paths(sj ) it follows thatsj sj+1 sj+2 . . . |= ♦a.Thus, there exists an index i j with si |= a. As this reasoning applies to any index j,path π visits an a-state infinitely often.⇐: Let s be a state such that every infinite path fragment starting in s visits infinitelymany a-states.
Let π = s0 s1 s2 . . . ∈ Paths(s). To show that s |= ∀∀♦a, it has to beproven that π |= ∀♦a, i.e.:sj |= ∀♦a,for any j 0.Computation Tree Logic327Let j 0 and π = sj sj+1 sj+2 . . . ∈ Paths(sj ). To show that sj |= ∀♦a, it suffices toprove that π visits at least one a-state. It is not difficult to infer thatπ = s0 s1 s2 . . . sj sj+1 sj+2 . . . ∈ Paths(s) . prefix of ππ ∈ Paths(sj )By assumption, π visits infinitely many a-states. In particular, there is an i > j suchthat si |= a. It now follows thatπ = sj sj+1 .
. . si−1 si si+1 , . . . |= ♦aand, as this holds for any path π ∈ Paths(sj ), thus sj |= ∀♦a. This yields π |= ∀♦a forall paths π ∈ Paths(s). Thus, we have s |= ∀ ∀♦ a.Remark 6.9.Weak UntilAs for LTL (see Section 5.1.5), a slight variant of the until operator can be defined, viz.the weak-until operator, denoted W. The intuition behind this operator is that path πsatisfies Φ W Ψ, for state formulae Φ and Ψ, if either Φ U Ψ or Φ holds.
That is, thedifference between until and weak until is that the latter does not require a Ψ-state to bereached eventually.The weak-until operator in CTL cannot be defined directly starting from the LTL definitionϕ W ψ = ϕ U ψ ∨ ϕ,since ∃(ϕ U ψ ∨ ϕ) is not a syntactically correct CTL formula. However, using the LTLequivalence law ϕ W ψ ≡ ¬((ϕ ∧ ¬ψ) U (¬ϕ ∧ ¬ψ)) and the duality between universal andexistential quantification, the weak-until operator can be defined in CTL by∃(Φ W Ψ) = ¬∀((Φ ∧ ¬Ψ) U (¬Φ ∧ ¬Ψ)),∀(Φ W Ψ) = ¬∃((Φ ∧ ¬Ψ) U (¬Φ ∧ ¬Ψ)).Let us now check the semantics of ∃ W .
From the above-defined duality, it follows thats |= ∃(Φ W Ψ) if and only if there exists a path π = s0 s1 s2 . . . that starts in s (i.e., s0 = s)such thatπ |= (Φ ∧ ¬Ψ) U (¬Φ ∧ ¬Ψ).Such path exists if and only if• either sj |= Φ ∧ ¬Ψ for all j 0, i.e., π |= (Φ ∧ ¬Ψ), or• there exists an index j such that328Computation Tree Logic– sj |= Φ ∧ ¬Ψ and sj |= ¬Φ ∧ ¬Ψ, i.e., sj |= Ψ, and– si |= Φ ∧ ¬Ψ for all 0 i < j.This is equivalent to π |= Φ U Ψ.Gathering these results yieldsπ |= Φ W Ψif and only ifπ |= Φ U Ψ or π |= (Φ ∧ ¬Ψ),if and only ifπ |= Φ U Ψ or π |= Φ.Thus, the CTL formula ∃(Φ W Ψ) is equivalent to ∃(Φ U Ψ) ∨ ∃Φ.
In the same way, onecan check that the meaning of ∀(Φ W Ψ) is as expected, i.e., s |= ∀(Φ W Ψ) if and only ifall paths starting in s fulfill Φ W Ψ according to the LTL semantics of W .Remark 6.10.The Semantics of NegationFor state s, we have s |= Φ if and only if s |= ¬Φ. This, however, does not hold in generalfor transition systems. That is to say, it is possible that the statements TS |= Φ andTS |= ¬Φ both hold. This stems from the fact that there might be two initial states, s0and s0 , say, such that s0 |= Φ and s0 |= Φ. Furthermore:TS |= ¬∃ϕ iff there exists a path π ∈ Paths(TS) with π |= ϕ.This—at first glance surprising—equivalence is justified by the fact that the interpretationof CTL state formulae over transition systems is based on a universal quantification overthe initial states.
The statement TS |= ¬∃ϕ thus holds if and only if there exists an initialstate s0 ∈ I with s0 |= ¬∃ϕ, i.e., s0 |= ∃ϕ. On the other hand, TS |= ∃ϕ requires thats0 |= ∃ϕ for all s0 ∈ I. Consider the following transition system:s0s0{a}∅It follows that s0 |= ∃ a, whereas s0 |= ∃ a. Accordingly, TS |= ¬∃ a and TS |= ∃ a.The semantics of CTL has been defined for a transition system without terminal states.This has the (technically) pleasant effect that all paths are infinite and simplifies theComputation Tree Logic329definition of |= for paths. In the following remark it is shown how to adapt the pathsemantics in case transition systems are considered with terminal states, i.e., when finitepaths are possible.Remark 6.11.CTL Semantics for Transition Systems with Terminal StatesFor finite maximal path fragment π = s0 s1 s2 .
. . sn of length n, i.e., sn is a terminalstate, letπ |= Φiff n > 0 and s1 |= Φ,π |= Φ U Ψ iff there exists an index j ∈ IN with j n, andsi |= Φ, for i = 0, 1, . . . , j−1, and sj |= Ψ.Then, s |= ∀ false if and only if s is a terminal state. For the derived operators ♦ and we obtainπ |= ♦Φ iff there exists an index j n with sj |= Φ,π |= Φ iff for all j ∈ IN with j n we have sj |= Φ.6.2.3Equivalence of CTL FormulaeCTL formulae Φ and Ψ are called equivalent whenever they are semantically identical,i.e., when for any state s it holds that2 s |= Φ if and only if s |= Ψ.Definition 6.12.Equivalence of CTL FormulaeCTL formulae Φ and Ψ (over AP) are called equivalent, denoted Φ ≡ Ψ, if Sat(Φ) =Sat(Ψ) for all transition systems TS over AP.Accordingly, Φ ≡ Ψ if and only if for any transition system TS we have:TS |= Φif and only ifTS |= Ψ .Besides the standard equivalence laws for the propositional logic fragment of CTL, thereexist a number of equivalence rules for temporal modalities in CTL.
An important set ofequivalence laws is indicated in Figure 6.5.To understand the expansion laws, let usreconsider the expansion law for the until operator in LTL:ϕ U ψ ≡ ψ ∨ (ϕ ∧ (ϕ U ψ)).2Recall that the notion CTL formula is used for a CTL state formula.330Computation Tree Logicduality laws for path quantifiers∀ Φ ≡ ¬∃ ¬Φ∃ Φ ≡ ¬∀ ¬Φ∀♦Φ ≡ ¬∃¬Φ∃♦Φ ≡ ¬∀¬Φ∀(Φ U Ψ) ≡ ¬∃(¬Ψ U (¬Φ ∧ ¬Ψ)) ∧ ¬∃¬Ψ≡ ¬∃((Φ ∧ ¬Ψ) U (¬Φ ∧ ¬Ψ)) ∧ ¬∃(Φ ∧ ¬Ψ)≡ ¬∃((Φ ∧ ¬Ψ) W (¬Φ ∧ ¬Ψ))expansion laws∀(Φ U Ψ) ≡ Ψ ∨ (Φ ∧ ∀ ∀(Φ U Ψ))∀♦Φ ≡ Φ ∨ ∀ ∀♦Φ∀Φ ≡ Φ ∧ ∀ ∀Φ∃(Φ U Ψ) ≡ Ψ ∨ (Φ ∧ ∃ ∃(Φ U Ψ))∃♦Φ ≡ Φ ∨ ∃ ∃♦Φ∃Φ ≡ Φ ∧ ∃ ∃Φdistributive laws∀(Φ ∧ Ψ) ≡ ∀Φ ∧ ∀Ψ∃♦(Φ ∨ Ψ) ≡ ∃♦Φ ∨ ∃♦ΨFigure 6.5: Some equivalence rules for CTL.Computation Tree Logic331In CTL, similar expansion laws for ∃(Φ U Ψ) and ∀(Φ U Ψ) exist.
For instance, we havethat ∃(Φ U Ψ) is equivalent to the fact that the current state either satisfies Ψ, or it satisfiesΦ, and for some direct successor state, ∃(Φ U Ψ) holds. The expansion laws for ∃♦ Φ and∃ Φ can be simply derived from the expansion laws for ∃ U. The basic idea behind theselaws—as for LTL—is to express the validity of a formula by a statement about the currentstate (without the need to use temporal operators) and a statement about the directsuccessors of this state (using either ∃ or ∀ depending on whether an existential ora universally quantified formula is treated). For instance, ∃ Φ is valid in state s if Φ isvalid in s (a statement about the current state) and Φ holds for all states along some pathstarting at s (a statement about the successor states).Not any law in LTL can be easily lifted to CTL.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
