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

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 69)

We onlyprove the propositions (f) and (g):Proof of (f): The proof of this claim consists of two parts:(i) Show that T = Sat(∃(Φ U Ψ)) satisfies (1) and (2). From the expansion law∃(Φ U Ψ) ≡ Ψ ∨ (Φ ∧ ∃ ∃(Φ U Ψ)),it directly follows that T satisfies the properties (1) and (2).(ii) Show that for any T satisfying properties (1) and (2) we haveSat(∃(Φ U Ψ)) ⊆ T.This is proven as follows. Let s ∈ Sat(∃(Φ U Ψ)). Distinguish between s ∈ Sat(Ψ)and s ∈ Sat(Ψ). If s ∈ Sat(Ψ), it follows from (1) that s ∈ T . In case s ∈/ Sat(Ψ),there exists a path π = s0 s1 s2 .

. . starting in s=s0 , such that π |= Φ U Ψ. Letn > 0, such that si |= Φ, 0 i < n, and sn |= Ψ. Then:• sn ∈ Sat(Ψ) ⊆ T ,• sn−1 ∈ T , since sn ∈ Post(sn−1 ) ∩ T and sn−1 ∈ Sat(Φ),• sn−2 ∈ T , since sn−1 ∈ Post(sn−2 ) ∩ T and sn−2 ∈ Sat(Φ),CTL Model Checking345• . . . . .

.,• s1 ∈ T , since s2 ∈ Post(s1 ) ∩ T and s1 ∈ Sat(Φ), and finally• s0 ∈ T , since s1 ∈ Post(s0 ) ∩ T and s0 ∈ Sat(Φ).It thus follows that s = s0 ∈ T .Proof of (g): The proof of this claim consists of two parts:(i) Show that T = Sat(∃Φ) satisfies (3) and (4). From the expansion law∃ Φ ≡ Φ ∧ ∃ ∃ Φ,it directly follows that T satisfies the properties (3) and (4).(ii) Show that for any T satisfying properties (3) and (4)T ⊆ Sat(∃Φ).This proof goes as follows.

Let T ⊆ S satisfy (3) and (4) and s ∈ T . Let π =s0 s1 s2 . . . be a path starting in s=s0 . (As TS has no terminal states, such a pathexists.) Then we derive• s0 = s.• Since s0 ∈ T , there exists a state s1 ∈ Post(s0 ) ∩ T .• Since s1 ∈ T , there exists a state s2 ∈ Post(s1 ) ∩ T .• ......Here, property (4) is exploited in every step. From property (3), it follows thatsi ∈ T ⊆ Sat(Φ),i 0.Thus, π = s0 s1 s2 . .

. satisfies Φ. It follows thats ∈ Sat(∃Φ).As this reasoning applies to any s ∈ T , it follows that T ⊆ Sat(∃ Φ).Remark 6.24.Alternative Formulation of Sat(∃(Φ U Ψ) and Sat(∃ Φ)The characterizations of the sets Sat(∃(Φ U Ψ)) and Sat(∃ Φ) indicated in Theorem 6.23346Computation Tree Logicare based upon the fixed-point equation induced by the expansion laws for ∃(Φ U Ψ) and∃ Φ, respectively.

Consider, for instance, the expansion law∃(Φ U Ψ) ≡ Ψ ∨ (Φ ∧ ∃ ∃(Φ U Ψ)).The recursive nature of this law suggests to considering the CTL formula ∃(Φ U Ψ) as afixed point of the logical equationF ≡ Ψ ∨ (Φ ∧ ∃ F ).By the expansion law F = ∃(Φ U Ψ) is a solution, but there are also other solutions that arenot equivalent to ∃(Φ U Ψ), such as F = ∃(Φ W Ψ) (see Remark 6.25). However, a uniquecharacterization of ∃(Φ U Ψ) is obtained by the fact that ∃(Φ U Ψ) is the least solutionof F ≡ Ψ ∨ (Φ ∧ ∃ F ). Using a set-theoretical counterpart by means of Sat(·), weobtain the following equivalent formulation of constraint (f) in Theorem 6.23:(f ) Sat(∃(Φ U Ψ)) is the smallest set T ⊆ S satisfyingSat(Ψ) ∪ { s ∈ Sat(Φ) | Post(s) ∩ T = ∅ } ⊆ T.In fact, “⊆” may be replaced by “=”.In a similar way, ∃ Φ can be considered as the greatest fixed point of the logical equationF = Φ ∧ ∃ F.Using a set-theoretical counterpart of this equation we obtain the following equivalentformulation of constraint (g) in Theorem 6.23:(g ) Sat(∃Φ) is the largest set T ⊆ S satisfyingT ⊆ { s ∈ Sat(Φ) | Post(s) ∩ T = ∅ }.Also in this characterization “⊆” may be replaced by “=”.Characterizations of the satisfaction sets for universally quantified CTL formulae can beobtained using the result in Theorem 6.23.

This yields(h) Sat(∀ Φ) = { s ∈ S | Post(s) ⊆ Sat(Φ) }.CTL Model Checking347(i) Sat(∀(Φ U Ψ)) is the smallest set T ⊆ S satisfyingSat(Ψ) ∪ { s ∈ Sat(Φ) | Post(s) ⊆ T } ⊆ T.(j) Sat(∀ Φ) is the largest set T ⊆ S satisfyingT ⊆ { s ∈ Sat(Φ) | Post(s) ⊆ T }.Remark 6.25.Weak UntilThe weak-until operator satisfies the same expansion laws as the until operator.∃(Φ W Ψ) ≡ Ψ ∨ (Φ ∧ ∃ ∃(Φ W Ψ)),∀(Φ W Ψ) ≡ Ψ ∨ (Ψ ∧ ∀ ∀(Φ W Ψ)).The difference, however, is that the weak-until operator represents the largest solution(i.e., fixed point) of the expansion law, whereas the until operator denotes the smallestsolution.

The satisfaction sets for weak until are characterized as follows:(k) Sat(∃(Φ W Ψ)) is the largest set T ⊆ S satisfyingT ⊆ Sat(Ψ) ∪ { s ∈ Sat(Φ) | Post(s) ∩ T = ∅ }.(l) Sat(∀(Φ W Ψ)) is the largest set T ⊆ S satisfyingT ⊆ Sat(Ψ) ∪ { s ∈ Sat(Φ) | Post(s) ⊆ T }.Without loss of generality, we may assume that the CTL formula Φ to be verified is inENF (see Theorem 6.14, page 332). That is, the model-checking algorithm is supposed tobe preceded by transforming the CTL formula at hand into ENF. The characterizationsof the satisfaction sets indicated in Theorem 6.23 are exploited to compute the sets Sat(·).The essential steps for computing the satisfaction sets are summarized in Algorithm 14on page 348.6.4.2The Until and Existential Always OperatorTo treat constrained reachability properties, given by CTL formulae of the form ∃(Φ U Ψ),the characterization in Theorem 6.23 is exploited. Recall that Sat(∃(Φ U Ψ)) is character-348Computation Tree LogicAlgorithm 14 Computation of the satisfaction setsInput: finite transition system TS with state set S and CTL formula Φ in ENFOutput: Sat(Φ) = { s ∈ S | s |= Φ }(* recursive computation of the sets Sat(Ψ) for all subformulae Ψ of Φ *)switch(Φ):trueaΦ1 ∧ Φ2¬Ψ::::returnreturnreturnreturnS;{ s ∈ S | a ∈ L(s) };Sat(Φ1 ) ∩ Sat(Φ2 );S \ Sat(Ψ);∃ Ψ:return { s ∈ S | Post(s) ∩ Sat(Ψ) = ∅ };∃(Φ1 U Φ2 ):T := Sat(Φ2 ); (* compute the smallest fixed point *)while { s ∈ Sat(Φ1 ) \ T | Post(s) ∩ T = ∅ } = ∅ dolet s ∈ { s ∈ Sat(Φ1 ) \ T | Post(s) ∩ T = ∅ };T := T ∪ { s };od;return T ;∃ Φ:T := Sat(Φ); (* compute the greatest fixed point *)while { s ∈ T | Post(s) ∩ T = ∅ } = ∅ dolet s ∈ { s ∈ T | Post(s) ∩ T = ∅ };T := T \ { s };od;return T ;end switchized as the smallest set T ⊆ S, where S is the set of states in the transition system underconsideration, such that(1) Sat(Ψ) ⊆ T and (2) (s ∈ Sat(Φ) and Post(s) ∩ T = ∅) ⇒ s ∈ T.(6.1)This characterization suggests adopting the following iterative procedure to computeSat(∃(Φ U Ψ)):T0 = Sat(Ψ) and Ti+1 = Ti ∪ { s ∈ Sat(Φ) | Post(s) ∩ Ti = ∅ }.Intuitively speaking, the set Ti contains all states that can reach a Ψ-state in at most isteps via a Φ-path.

This is to be understood as follows. From the fact that Sat(∃(Φ U Ψ))satisfies the conditions (1) and (2) in (6.1), it can be demonstrated by induction on j thatT0 ⊆ T1 ⊆ T2 ⊆ . . . ⊆ Tj ⊆ Tj+1 ⊆ . . . ⊆ Sat(∃(Φ U Ψ)).Since we assume a finite transition system TS, there exists a j 0 such thatTj = Tj+1 = Tj+2 = . . ..CTL Model Checking349ThereforeTj = Tj ∪ { s ∈ Sat(Φ) | Post(s) ∩ Tj = ∅ }and, hence:{ s ∈ Sat(Φ) | Post(s) ∩ Tj = ∅ } ⊆ Tj .Hence, Tj satisfies property (2). Further,Sat(Ψ) = T0 ⊆ Tj .These considerations show that Tj possesses the properties (1) and (2). Since Sat(∃(Φ U Ψ))is the smallest set of states satisfying the properties (1) and (2), it follows thatSat(∃(Φ U Ψ)) ⊆ Tjand thus Sat(∃(Φ U Ψ)) = Tj . Hence, for any j 0 we haveT0 T1 T2 .

. . Tj = Tj+1 = . . . = Sat(∃(Φ U Ψ)).Algorithm 15 (see page 351) shows a more detailed version of the backward search indicatedearlier in Algorithm 14 (see page 348). As each Ψ-state obviously satisfies ∃(Φ U Ψ),all states in Sat(Ψ) are initially considered to satisfy ∃(Φ U Ψ)). This conforms to theinitialization to the variable E. An iterative procedure is subsequently started that canbe considered to systematically check the state space in a “backward” manner. In eachiteration, all Φ-states are determined that can move by a single transition to (one of) thestates of which we already know to satisfy ∃(Φ U Ψ)).

Thus, in the ith iteration of theprocedure, all Φ-states are considered that can move to a Ψ-state in at most i steps. Thiscorresponds to the set Ti . Termination of the algorithm intuitively follows, as the numberof states in the transition system is finite. Note that the algorithm assumes a transitionsystem representation (or its state graph) by means of “inverse” adjacency lists, i.e., listrepresentations for the sets of predecessors Pre(s ) = { s ∈ S | s ∈ Post(s) }.Example 6.26.Consider the transition system depicted in Figure 6.11, and suppose we are interested inchecking the formula ∃♦ Φ with Φ = ((a = c) ∧ (a = b)). Recall that ∃♦ Φ = ∃(true U Φ).To check ∃♦ Φ we invoke Algorithm 14 (see page 348). This algorithm recursively computesSat(true) and Sat((a = c) ∧ (a = b)). This corresponds to the situation depicted inFigure 6.12(a), where all states in the set T are colored black, and white otherwise.

In thefirst iteration, we select and delete s5 from E, but as Pre(s5 ) = ∅, T remains unaffected.On considering s4 ∈ E, Pre(s4 ) = { s6 } is added to T (and E), see Figure 6.12(b).During the next iteration, the only predecessor of s6 is added, yielding the snapshot inFigure 6.12(c). After the fourth iteration, the algorithm terminates as there are no newpredecessors of Φ-states encountered, i.e., E = ∅ (see Figure 6.12(d)).350Computation Tree Logic∅{c}s7s6{ a, b, c } s0s3s4{ b, c } s2{a}{b}s5s1{ a, c }{ a, b }Figure 6.11: An example of a transition system.(a)(b)(c)(d)Figure 6.12: Example of backward search for ∃(true U (a=c) ∧ (a=b)).CTL Model Checking351Algorithm 15 Enumerative backward search for computing Sat(∃(Φ U Ψ))Input: finite transition system TS with state set S and CTL formula ∃(Φ U Ψ)Output: Sat(∃(Φ U Ψ)) = { s ∈ S | s |= ∃(Φ U Ψ) }E := Sat(Ψ);(* E administers the states s with s |= ∃(Φ U Ψ) *)T := E;(* T contains the already visited states s with s |= ∃(Φ U Ψ) *)while E = ∅ dolet s ∈ E;E := E \ { s };for all s ∈ Pre(s ) doif s ∈ Sat(Φ) \ T then E := E ∪ { s }; T := T ∪ { s } fiododreturn TLet us now consider the computation of Sat(∃ Φ) for the transition system TS.

Характеристики

Список файлов книги