5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 85
Текст из файла (страница 85)
In the case of an iterated preimage computation by T0 = B andTj+1 = Tj ∪ Pre(Tj ) for the symbolic computation of Pre∗ (B), one might also switch fromTj to any set T̃ such that Tj \ Tj−1 ⊆ T̃ ⊆ Tj and compute Tj ∪ Pre(T̃ ). For such advancedtechniques, we refer the interested reader to [92, 292, 374] and the literature mentionedthere.Summary We now have all ingredients for a symbolic realization of the standard CTLmodel-checking approach which recursively computes the satisfaction sets of the subformulae by means of shared OBDDs. Initially, one has to construct the ROBDD representationof the transition system to be analyzed.
This can be done in a compositional way bymeans of synthesis operators (disjunction, conjunction, etc.) as mentioned in Remark6.59. Furthermore, we assume that ROBDD representations of the satisfaction sets forthe atomic propositions are given. This assumption is justified since often the atomicpropositions can serve as variables for the encoding of the states.
(And in this case theirsatisfaction set is just given by a projection function.) The CTL model-checking procedurecan then be performed by means of the ITE algorithm (to treat the propositional logicfragment of CTL) and the symbolic BFS-based algorithms sketched in Algorithms 20 and21. Both rely on an iterative preimage computation. Techniques to do this efficiently havebeen discussed above. The termination condition requires checking the equality of twoswitching functions.
This, in fact, is trivial for shared OBDDs since it simply amounts tothe comparison of the corresponding nodes and can be performed in constant time.4226.8Computation Tree LogicCTL∗We saw in Theorem 6.21 on page 337 that CTL and LTL have incomparable expressiveness.An extension of CTL, proposed by Emerson and Halpern, called CTL∗ , combines thefeatures of both logics, and thus is more expressive than either of them.6.8.1Logic, Expressiveness, and EquivalenceCTL∗ is an extension of CTL as it allows path quantifiers ∃ and ∀ to be arbitrarily nestedwith linear temporal operators such as and U. In contrast, in CTL each linear temporaloperator must be immediately preceded by a path quantifier.
As in CTL, the syntax ofCTL∗ distinguishes between state and path formulae. The syntax of CTL∗ state formulaeis roughly as in CTL, while the CTL∗ path formulae are defined as LTL formulae, the onlydifference being that arbitrary CTL∗ state formulae can be used as atoms. For example,∀ a is a legal CTL∗ formula, but does not belong to CTL. The same applies to theCTL∗ formulae ∃ ♦ a and ∀ ♦ a. (However, ∀ ♦ a is equivalent to the CTL formula∀ ∀♦ a.)Definition 6.80.Syntax of CTL∗CTL∗ state formulae over the set AP of atomic propositions, briefly called CTL∗ formulae,are formed according to the following grammar:Φ ::= trueaΦ1 ∧ Φ2¬Φ∃ϕwhere a ∈ AP and ϕ is a path formula.
The syntax of CTL∗ path formulae is given bythe following grammar:ϕ ::= Φϕ1 ∧ ϕ2¬ϕϕϕ1 U ϕ2where Φ is a state formula, and ϕ, ϕ1 , and ϕ2 are path formulae.As for LTL or CTL, we use derived propositional logic operators like ∨, →, .
. . and let♦ϕ = true U ϕandϕ = ¬♦¬ϕ.The universal path quantifier ∀ can be defined in CTL∗ by existential quantification andnegation:∀ϕ = ¬∃¬ϕ.(Note that this is not the case for CTL.)CTL∗423For example, the following formulae are syntactically correct CTL∗ formulae:∀ ( ♦a ∧ ¬(b U c) )and∀ ¬a ∧ ∃♦ (a ∨ ∀(b U a)).Note that these formulae are not CTL formulae.Definition 6.81.Satisfaction Relation for CTL∗Let a ∈ AP be an atomic proposition, TS = (S, Act, →, I, AP, L) be a transition systemwithout terminal states, state s ∈ S, Φ, Ψ be CTL∗ state formulae, and ϕ, ϕ1 and ϕ2 beCTL∗ path formulae.
The satisfaction relation |= is defined for state formulae bys |= aiffa ∈ L(s),s |= ¬ Φiffnot s |= Φ,s |= Φ ∧ Ψiff(s |= Φ) and (s |= Ψ),s |= ∃ϕiffπ |= ϕ for some π ∈ Paths(s).For path π, the satisfaction relation |= for path formulae is defined by:π |= Φiffs0 |= Φ,π |= ϕ1 ∧ ϕ2iffπ |= ϕ1 and π |= ϕ2 ,π |= ¬ϕiffπ |= ϕ,π |= ϕiffπ[1..] |= ϕ,π |= ϕ1 U ϕ2iff∃ j 0.
(π[j..] |= ϕ2 ∧ (∀ 0 k < j. π[k..] |= ϕ1 ))where for path π = s0 s1 s2 . . . and integer i 0, π[i..] denotes the suffix of π from indexi on.Definition 6.82.CTL∗ Semantics for Transition SystemsFor CTL∗ -state formula Φ, the satisfaction set Sat(Φ) is defined bySat(Φ) = { s ∈ S | s |= Φ }.The transition system TS satisfies CTL∗ formula Φ if and only if Φ holds in all initialstates of TS:TS |= Φ if and only if ∀s0 ∈ I.
s0 |= Φ.424Computation Tree LogicThus, TS |= Φ if and only if all initial states of TS satisfy the formula Φ.LTL formulae are CTL∗ path formulae in which the elementary state formulae Φ are restricted to atomic propositions. Apparently, the interpretation of LTL over the paths of atransition system (see Definition 5.7, page 237) corresponds to the semantics of LTL obtained as a sublogic of CTL∗ . The following theorem demonstrates that the correspondingclaim also holds for states.
Thereby, every LTL formula ϕ is identified with the CTL∗formula ∀ϕ, and the semantics of LTL over states is taken as a reference. Recall thataccording to the LTL semantics in paths, s |= ϕ if and only if π |= ϕ for all π ∈ Paths(s).Theorem 6.83.Embedding of LTL in CTL∗Let TS = (S, Act, →, I, AP, L) be a transition system without terminal states. For eachLTL formula ϕ over AP and for each s ∈ S:s |= ϕ if and only ifLTL semanticss |= ∀ϕ .CTL∗ semanticsIn particular, TS |= ϕ (with respect to the LTL semantics) if and only if TS |= ∀ϕ (withrespect to the CTL∗ semantics)As a result, it is justified to understand LTL (with interpretation over the states of atransition system) as a sublogic of CTL∗ .
Theorem 6.21 (page 337) stated that the expressivenesses of LTL and CTL are incomparable. Since LTL is a sublogic of CTL∗ , it nowfollows that CTL∗ subsumes LTL and CTL, i.e., there exist CTL∗ formulae which can beexpressed neither in LTL nor in CTL.Theorem 6.84.CTL∗ is More Expressive Than LTL and CTLFor the CTL∗ formula over AP = { a, b },Φ = (∀♦ a) ∨ (∀ ∃♦ b),there does not exist any equivalent LTL or CTL formula.Proof: This follows directly from the fact that ∀ ∃♦ b is a CTL formula that cannot beexpressed in LTL, whereas ♦ a is an LTL formula that cannot be expressed in CTL.Both these facts follow from Theorem 6.21 (page 337).The relationship between LTL, CTL, and CTL∗ is depicted in Figure 6.27.CTL∗425CTL∗CTLLTL♦ (a ∧ a)∨∀ ∃♦ a♦ (a ∧ a)♦a∀ ∃♦ aFigure 6.27: Relationship between LTL CTL and CTL∗ .One of the consequences of this fact, is that—as in LTL—fairness assumptions can beexpressed syntactically in CTL∗ .
For instance, for fairness assumption fair , formulae ofthe form∀(fair → ϕ) or ∃(fair ∧ ϕ)are legal CTL∗ formulae. As for CTL or LTL, semantic equivalence ≡ can be defined forCTL∗ formulae. Apart from the equivalence laws for CTL and the laws resulting from theequivalence laws for LTL, there exists a series of other important laws that are specific toCTL∗ . This includes, among others, the laws listed in Figure 6.28.Example instances of the duality laws for the path quantifiers are¬∀♦a ≡ ∃♦¬a and¬∃♦a ≡ ∀♦¬a.As usual, universal quantification does not distribute over disjunction, and the same applies to existential quantification and conjunction:∀(ϕ ∨ ψ) ≡ ∀ϕ ∨ ∀ψand ∃(ϕ ∧ ψ) ≡ ∃ϕ ∧ ∃ψ.Path quantifier elimination should also be considered with care.
For instance,∀♦ ϕ ≡ ∀♦ ∀ ϕ and∃ ♦ Φ ≡ ∃ ∃♦ ϕ.Finally, we remark that for CTL∗ -state formula Φ we have that∃Φ ≡ Φ and∀Φ ≡ Φ.This is illustrated by means of an example. Consider the CTL∗ formula ∃∀♦ a. Thisformula holds in state s whenever there exists an infinite path fragment π = s0 s1 s2 .
. . ∈Paths(s), such that π |= ∀♦ a. Since π |= ∀♦ a holds if and only if s = s0 |= ∀♦ a, theformula ∃∀♦a is equivalent to ∀♦a.426Computation Tree Logicduality laws for path quantifiers¬∀ϕ ≡ ∃¬ϕ¬∃ϕ ≡ ∀¬ϕdistributive laws∀(ϕ1 ∧ ϕ2 ) ≡ ∀ϕ1 ∧ ∀ϕ2∃(ϕ1 ∨ ϕ2 ) ≡ ∃ϕ1 ∨ ∃ϕ2quantifier absorption laws∀♦ϕ ≡ ∀ ∀♦ϕ∃♦ϕ ≡ ∃♦ ∃ϕFigure 6.28: Some equivalence laws for CTL∗ .Remark 6.85.Extending CTL with Boolean Connectors for Path Formulae (CTL+ )Consider the following fragment, called CTL+ , of CTL∗ , which extends CTL by allowingBoolean operators in path formulae.
CTL+ state formulae over the set AP of atomicproposition are formed according to the following grammar:Φ ::= trueaΦ1 ∧ Φ2¬Φ∃ϕ∀ϕwhere a ∈ AP and ϕ is a path formula. CTL+ path formulae are formed according to thefollowing grammar:¬ϕΦΦ1 U Φ2ϕ ::= ϕ1 ∧ ϕ2where Φ, Φ1 , and Φ2 are state formulae, and ϕ1 , ϕ2 are path formulae. Surprisingly, CTL+is as expressive as CTL, i.e., for any CTL+ state formula Φ+ there exists an equivalentCTL formula Φ. For example:∃(a W b) ≡ ∃( (a U b) ∨ a ) CTL formulaCTL+ formulaor∃(♦a ∧ ♦b) ≡ ∃♦(a ∧ ∃♦b) ∧ ∃♦(b ∧ ∃♦a) .
CTL+ formulaCTL formulaCTL∗427We do not provide here a full proof for transforming CTL+ formulae into equivalent CTLformulae. The transformation relies on equivalence laws such as∃(¬ Φ) ≡ ∃ ¬Φ∃(¬(Φ1 U Φ2 )) ≡ ∃( (Φ1 ∧ ¬Φ2 ) U (¬Φ1 ∧ ¬Φ2 ) ) ∨ ∃¬Φ2∃( Φ1 ∧ Φ2 ) ≡ ∃ (Φ1 ∧ Φ2 )∃( Φ ∧ (Φ1 U Φ2 )) ≡ (Φ2 ∧ ∃ Φ) ∨ (Φ1 ∧ ∃ (Φ ∧ ∃(Φ1 U Φ2 )))∃((Φ1 U Φ2 ) ∧ (Ψ1 U Ψ2 )) ≡ ∃((Φ1 ∧ Ψ1 ) U (Φ2 ∧ ∃(Ψ1 U Ψ2 ))) ∨∃((Φ1 ∧ Ψ1 ) U (Ψ2 ∧ ∃(Φ1 U Φ2 )))...Thus, CTL can be expanded by means of a Boolean operator for path formulae withoutchanging the expressiveness.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
