5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 68
Текст из файла (страница 68)
Thus, L0 (s0 ) = ∅ and L0 (t0 ) = { a }, and for n > 0,the labels of all states in TSn−1 remain the same and are extended withLn (sn ) = Ln (sn ) = ∅and Ln (tn ) = Ln (tn ) = { a }.Finally, the transition relations →n and →n contain →n−1 (where →−1 = ∅), as wellas the transitionsTSn : sn →n tn , tn →n tn , tn →n sn−1 , tn →n snTSn : sn →n tn , tn →n tn , tn →n sn−1where the action labels are omitted for simplicity.Thus, the only difference between TSn and TSn is the fact that TSn includes theedge tn → sn , whereas this edge is absent in TSn . Some example instantiations ofTSn and TSn are indicated in Figure 6.9.Expressiveness of CTL vs.
LTL339∅{a}∅{a}s1t1s0t0∅{a}∅{a}s1t1s0t0Figure 6.9: The transition systems TS1 (upper) and TS1 (lower).It follows from the construction of TSn and TSn thatTSn |= ♦a andTSn |= ♦a for all n 0.This can be proven as follows. TSn contains the initial path (sn tn )ω that visits snand tn in an alternating fashion. We have thattrace((sn tn )ω ) = ∅ { a } ∅ { a } ∅ . . .thus trace((sn tn )ω ) |= ♦ a.As the considered path is initial, it follows that TSn |= ♦ a. On the other hand, asTSn has no opportunity to infinitely often return to an ¬a-state, each initial pathin TSn is of the following form:πi = sn tn . .
. si (ti )ωfor some i. Due to the fact thattrace(πi ) = ∅ { a } ∅ . . . ∅ ({ a })ωit follows that trace(πi ) |= ♦ a. As this applies to any initial path of TSn , we haveTSn |= ♦ a.By means of induction on n, it can be proven that TSn and TSn cannot be distinguished by any CTL formula of length at most n. That is to say, for all n 0,∀CTL formula Φ with |Φ| n : TSn |= Φif and only if TSn |= Φ.(The proof of this fact is left to the interested reader.)340Computation Tree Logic∅{a}∅sss(a)(b)Figure 6.10: Two transition systems for ∀ ∃♦ a.The final step of the proof is now as follows. Assume there is a CTL formula Φ thatis equivalent to ♦ a. Let n = |Φ| be the length of the formula Φ andTS = TSn , TS = TSn .On the one hand, it follows from TS |= ♦ a and TS |= ♦ a thatTS |= Φ and TS |= Φ.On the other hand, it results from the fact that TSn and TSn cannot be distinguishedby a CTL formula (of length at most n) that Φ has the same truth-value under TSand under TS .
This yields a contradiction.(b) We concentrate on the proof that there does not exist an equivalent formulation ofthe CTL formula ∀ ∃♦ a in LTL. The fact that there do not exist equivalent LTLformulations of the CTL formulae ∀♦ ∀ a and ∀♦ (a ∧ ∀ a) follows directly fromLemmas 6.19 and 6.20 respectively, and Theorem 6.18. The proof for ∀ ∃♦ a is bycontraposition. Let ϕ be an LTL formula that is equivalent to ∀ ∃♦ a. Consider thetransition system TS depicted in Figure 6.10(a). As TS |= ∀ ∃♦ a, and ϕ ≡ ∀♦ ∃♦ a,it follows that TS |= ϕ, and thereforeTraces(TS) ⊆ Words(ϕ).Since π = sω is a path in TS, it follows thattrace(π) = ∅ ∅ ∅ ∅ .
. . ∈ Traces(TS) ⊆ Words(ϕ).Now consider the transition system TS depicted in Figure 6.10(b). Note that TS ispart of transition system TS. The paths starting in s in TS are also paths startingfrom s in TS, so we have s |= ϕ in TS and thus TS |= ϕ. However, s |= ∀ ∃♦ a,since ∃♦ a is never valid along the only path sω , and thus TS |= ∀ ∃♦ a.
This is acontradiction.CTL Model Checking341Note that the CTL formula ∀ ∃♦ a is of significant practical use, since it expresses thefact that it is possible to reach a state for which a holds irrespective of the current state.If a characterizes a state where a certain error is repaired, the formula expresses the factthat it is always possible to recover from that error.6.4CTL Model CheckingThis section is concerned with CTL model checking, which means a decision algorithm thatchecks whether TS |= Φ for a given transition system TS and CTL formula Φ. Throughoutthis section, it is assumed that TS is finite, and has no terminal states.
We will seethat CTL-model checking can be performed by a recursive procedure that calculates thesatisfaction set for all subformulae of Φ and finally checks whether all initial states belongto the satisfaction set of Φ.Throughout this section, we consider CTL formulae in ENF, i.e., CTL formulae built bythe basic modalities ∃ , ∃ U, and ∃ . This requires algorithms that generate Sat(∃ Φ),Sat(∃(Φ U Ψ)), and Sat(∃ Φ) when Sat(Φ) and Sat(Ψ) are given.
Although each CTL formula can be transformed algorithmically into an equivalent ENF formula, for an implementation of the CTL model-checking algorithm it is recommended to use similar techniquesto handle universal quantification, i.e., to design algorithms that generate Sat(∀ Φ),Sat(∀(Φ U Ψ)), and Sat(∀ Φ) directly from Sat(Φ) and Sat(Ψ). (The same holds forother derived operators such as W or R .)6.4.1Basic AlgorithmThe model-checking problem for CTL is to verify for a given transition system TS andCTL formula Φ whether TS |= Φ. That is, we need to establish whether the formula Φ isvalid in each initial state s of TS.
The basic procedure for CTL model checking is ratherstraightforward:• the set Sat(Φ) of all states satisfying Φ is computed recursively, and• it follows that TS |= Φ if and only if I ⊆ Sat(Φ)where I is the set of initial states of TS. Note that by computing Sat(Φ) a more generalproblem than just checking whether TS |= Φ is solved. In fact, it checks for any states in S whether s |= Φ, and not just for the initial states. This is sometimes referred342Computation Tree Logicto as a global model-checking procedure. The basic idea of the algorithm is sketched inAlgorithm 13 where Sub(Φ) is the set of subformulae of Φ. In the sequel of this section itis assumed that TS is finite and has no terminal states.Algorithm 13 CTL model checking (basic idea)Input: finite transition system TS and CTL formula Φ (both over AP)Output: TS |= Φfor all i | Φ | dofor all Ψ ∈ Sub(Φ) with | Ψ | = i docompute Sat(Ψ) from Sat(Ψ )ododreturn I ⊆ Sat(Φ)(* compute the sets Sat(Φ) = { s ∈ S | s |= Φ } *)(* for maximal genuine Ψ ∈ Sub(Ψ) *)The recursive computation of Sat(Φ) basically boils down to a bottom-up traversal ofthe parse tree of the CTL state formula Φ.
The nodes of the parse tree represent thesubformulae of Φ. The leaves stand for the constant true or an atomic proposition a ∈ AP.All inner nodes are labeled with an operator. For ENF formulae the labels of the innernodes are ¬, ∧, ∃ , ∃ U, or ∃ .For each node of the parse tree, i.e., for each subformula Ψ of Φ, the set Sat(Ψ) of statesis computed for which Ψ holds. This computation is carried out in a bottom-up fashion,starting from the leaves of the parse tree and finishing at the root of the tree, the (unique)node in the parse tree that corresponds to Φ. At an intermediate node, the results of thecomputations of its children are used and combined in an appropriate way to establish thestates of its associated subformula. The type of computation at such node, v say, dependson the operator (e.g., ∧, ∃, or ∃ U) that is at the “top level” of the subformula treated.The children of node v stand for the maximal genuine subformulae of the formula Ψv that isrepresented by v.
As soon as Sat(Ψ) is computed, subformula Ψ is (theoretically) replacedby a new atomic proposition aΨ , and the labeling function L is adjusted as follows: aΨ isadded to L(s) if and only if s ∈ Sat(Ψ). Once the bottom-up computations continue withthe father, w say, of node v, Ψ = Ψv is a maximal genuine subformula of Ψw , and all statesthat are labeled with aΨ are known to satisfy Ψ. In fact, one might say that Ψ is replacedin the formula by the atomic proposition aΨ . This technique will be of importance whentreating the model checking of CTL with fairness.CTL Model Checking343Example 6.22.Consider the following state formula over AP = { a, b, c }:Φ = ∃ a ∧ ∃(b U ∃ ¬c) Ψ Ψ .ΨThe indicated formulae Ψ and Ψ are the maximal proper subformulae of Φ, while Ψ isa maximal proper subformula of Ψ.
The syntax tree for Φ is of the following form:∧Sat(Φ)∃ U Sat(Ψ )Sat(Ψ) ∃b∃ Sat(Ψ )a¬cThe satisfaction sets for the leaves result directly from the labeling function L. The treatment of subformula ¬c only needs the satisfaction set for Sat(c) to be complemented. UsingSat(¬c), the set Sat(∃ ¬c) can be computed. The subformula Ψ can now be replacedby the fresh atomic proposition a3 where a3 ∈ L(s) if and only if s ∈ Sat(∃ ¬c). Thecomputation now continues with determining Sat(∃(b U a3 )). In a similar way, Sat(∃ a)can be computed by means of Sat(a).Once the subformulae Ψ and Ψ are treated, they can be replaced by the atomic propositions a1 , a2 , respectively, such thata1 ∈ L(s) iffs |= ∃ a and a2 ∈ L(s)iffs |= ∃(b U a3 ).The formula that is to be treated for the root node simply thus is: Φ = a1 ∧ a2 . Sat(Φ )results from intersecting Sat(a1 ) = Sat(Ψ) and Sat(a2 ) = Sat(Ψ ).
Note that a1 , a2 , anda3 are fresh atomic propositions, i.e., { a1 , a2 , a3 } ∩ AP = ∅. The above procedure thusis considered over AP = AP ∪ { a1 , a2 , a3 }.Theorem 6.23.Characterization of Sat(·) for CTL formulae in ENFLet TS = (S, Act, →, I, AP, L) be a transition system without terminal states. For all CT Lformulae Φ, Ψ over AP it holds that344Computation Tree Logic(a) Sat(true) = S,(b) Sat(a) = { s ∈ S | a ∈ L(s) }, for any a ∈ AP,(c) Sat(Φ ∧ Ψ) = Sat(Φ) ∩ Sat(Ψ),(d) Sat(¬Φ) = S \ Sat(Φ),(e) Sat(∃ Φ) = { s ∈ S | Post(s) ∩ Sat(Φ) = ∅ },(f ) Sat(∃(Φ U Ψ)) is the smallest subset T of S, such that(1) Sat(Ψ) ⊆ T and (2) s ∈ Sat(Φ) and Post(s) ∩ T = ∅ implies s ∈ T ,(g) Sat(∃ Φ) is the largest subset T of S, such that(3) T ⊆ Sat(Φ) and (4) s ∈ T implies Post(s) ∩ T = ∅.In the clauses (f) and (g), the terms “smallest” and “largest” should be interpreted withrespect to the partial order induced by set inclusion.Proof: The validity of the claims indicated in (a) through (e) is straightforward.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
