5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 74
Текст из файла (страница 74)
We haveto compute all nontrivial SCCs C such that for some cyclic subset D of C all fairnessconstraints ♦ ai → ♦ bi are realizable in D, i.e., for 1 i k:D ∩ Sat(ai ) = ∅orD ∩ Sat(bi ) = ∅.Algorithm 18 on page 370 provides the schema for the computation of Satsfair (∃ a). Ituses the recursive procedure CheckFair (see Algorithm 19, page 372) to check the real-Fairness in CTL371izability of sfair in SCC C of G[a].
The inputs of CheckFair are a cyclic strongly connected subgraph D of G[a], index j, and j strong fairnessassumptions sfair i1 , . . . , sfair ij .CheckFair (D, j, sfair i1 , . . . , sfair ij ) returns true if 1j sfair i is realizable in D. Thus,whetherthe invocation CheckFair (C, k, sfair 1 , . .
. , sfair k ) yields an affirmative answerC ⊆ T by returning true if and only if the fairness assumption sfair = 1ik sfair i isrealizable in C.The idea of Algorithm 19, CheckFair (C, k, sfair 1 , . . . , sfair k ), is as follows.
First, it ischecked whether C ∩ Sat(bi ) = ∅ for each fairness constraint sfair i = ♦ai → ♦bi .• If yes, then sfair =0<iksfair i is realizable in C.• Otherwise, there exists an index j ∈ { 1, . . . , k } such that C ∩ Sat(bj ) = ∅. The goalis then to realize the conditionsfair i ∧ ¬aj0<iki=jin C. For this, we investigate the subgraph C[¬aj ] of C that arises by removing allstates where aj holds and their incoming and outgoing edges.
The goal is to checkthe existence of a cyclic subgraph of C[¬aj ] such that the remaining k − 1 fairnessconstraints sfair 1 , . . . , sfair j−1 , sfair j+1 , . . . , sfair k are realizable in this subgraph.This is done by analyzing the nontrivial SCCs D of C[¬aj ].– If there is no nontrivial SCC D of C[¬aj ], then sfair is not realizable in C.– Otherwise, invoke CheckFair (D, k−1, . . .) for each of these nontrivial SCCs Dof C[¬aj ] to check whether the remaining k−1 fairness constraints are realizablein D.The main steps of this procedure are summarized in Algorithm 19 on page 372. Note thatin each recursive call one of the fairness constraints is removed, and thus the recursiondepth is at most k, in which case k = 0 and the condition “∀i ∈ {1, .
. . , k}.C ∩Sat(bj ) = ∅”of the first ifstatement is obviously fulfilled.The cost function for CheckFair (C, k, sfair 1 , . . . , sfair k ), is given by the recurrence equation:T (n , k−1) | n1 , . . . , nr 1, n1 + . . . + nr n}T (n, k) = O(n) + max{1rwhere n is the size (number of vertices and edges) of the subgraph C of G[a]. The valuesn1 , . . . , nr denote the sizes of the nontrivial strongly connected components D1 , . . . , Dr ofC[¬aj ]. It is easy to see that the solution of this recurrence is O(n·k). This yields:372Computation Tree LogicAlgorithm 19 Recursive algorithm CheckFair (C, k, sfair 1 , .
. . , sfair k )Input: nontrivial SCC C in G[a], and strong fairness constraints sfair i = ♦ai → ♦bi , i =1, . . . , k.Output: true if 1ik sfair i is realizable in C. Otherwise false.if ∀i ∈ { 1, . . . , k }. C ∩ Sat(bj ) = ∅ thenreturn true(*1ik♦bi is realizable in C *)elsechoose an index j ∈ {1, . .
. , k} with C ∩ Sat(bj ) = ∅;if C[¬aj ] is acyclic (or empty) thenreturn falseelsecompute the nontrivial SCCs of C[¬aj ];for all nontrivial SCC D of C[¬aj ] doif CheckFair (D, k − 1, sfair 1 , . . . , sfair j−1 , sfair j+1 , . . . , sfair k ) thenreturn truefiodfifireturn falseCounterexamples and WitnessesTheorem 6.42.373Time Complexity of Verifying ∃a under FairnessFor transition system TS with N states and K transitions, and CTL strong fairness assumption fair with k conjuncts, the set Satfair (∃ a) can be computed in O ((N +K) · k).The time complexity is thus linear in the size of the transition system and the numberof imposed fairness constraints.
The set T resulting from all SCCs C of G[a], for whichCheckFair (C, 1) returns the value true, can be computed (with appropriate implementation) in time O(size(G[a]) · k). A reachability analysis (by, e.g., depth-first search) resultsin the setSatfair (∃a) = { s ∈ S | ReachG[a] (s) ∩ T = ∅ }.Gathering these results yields that CTL model checking under strong fairness constraintsand for CTL formulae in ENF can be done in time linear in the size of the transitionsystem, the length of the formula, and the number of (strong) fairness constraints. This,in fact, also holds for arbitrary CTL formulae (with universal quantification which canbe treated by techniques similar as the ones we presented for existential quantification)and weak fairness constraints, or any mixture of unconditional, strong, and weak fairnessconstraints.
We thus obtain:Theorem 6.43.Time Complexity of CTL Model Checking with FairnessFor transition system TS with N states and K transitions, CTL formula Φ, and CTLfairness assumption fair with k conjuncts, the CTL model-checking problem TS |=fair Φcan be determined in time O((N +K) · |Φ| · k).6.6Counterexamples and WitnessesA major strength of model checking is the possibility of generating a counterexample incase a formula is refuted. Let us first explain what is meant by a counterexample.
In thecase of LTL, a counterexample for TS |= ϕ is a sufficiently long prefix of a path π thatindicates why π refutes ϕ. For instance, a counterexample for the LTL formula ♦ a is afinite prefix of just ¬a-states that ends with a single cycle traversal. Such counterexamplesuggests that there is a ¬a-path. Similarly, a counterexample for a consists of a pathπ for which π[1] violates a.For CTL the situation is somewhat more involved due to the existential path quantification. For CTL formulae of the form ∀ϕ a sufficiently long prefix of π with π |= ϕprovides—as in LTL—sufficient information about the source of the refutation.
In the374Computation Tree Logiccase of a path formula of the form ∃ϕ, it is unclear what a counterexample will be: ifTS |= ∃ϕ, then all paths violate ϕ and no path satisfies ϕ. However, if one checks theformula ∃ϕ for a transition system TS, then it is quite natural that for the answer “yes,TS |= ∃ϕ” one aims at an initial path where ϕ holds, while the answer “no” might besufficient.6 Therefore, CTL model checking supports the system diagnosis by providingcounterxamples or witnesses. Intuitively, counterexamples indicate the refutation of universally quantified path formulae, while witnesses indicate the satisfaction of existentiallyquantified path formulae.
From a path-based view, the concepts are counterexamples andwitnesses can be explained as follows:• a sufficiently long prefix of a path π with π |= ϕ is a counterexample for the CTLpath formula ∀ϕ, and• a sufficiently long prefix of a path π with π |= ϕ is a witness of the CTL path formula∃ϕ.To exemplify the idea of generating a witness, consider the following well-known combinatorial problem.Example 6.44.The Wolf-Goat-Cabbage ProblemConsider the problem of bringing a ferryman (f), a goat (g), a cabbage (c) and a wolf(w) from one side of a river to the other side. The only available means to go from oneriverside to another is a small boat that is capable of carrying at most two occupants.
Inorder for the boat to be steered, one of the occupants needs to be the ferryman. Of course,the boat does not need to be fully occupied, and the ferryman can cross the river alone.For obvious reasons, neither the goat and the cabbage nor the goat and the wolf shouldbe left unobserved by the ferryman. The question is whether there exists a series of boatmovements such that all three items can be carried by the ferryman to the other side ofthe river.This problem can be represented as a CTL model-checking problem in a rather naturalway. The behavior of the goat, wolf, and cabbage is provided by a simple two-statetransition system depicted in Figure 6.16. The state identifiers indicate the position ofeach of the items: 0 stands for the current (i.e., starting) riverside, and 1 for the other side6Since the standard CTL model-checking procedure calculates the set of states where the given (state)formula Φ holds, also some information extracted from Sat(Φ) could be returned to the user.
For instance,if TS |= ∃ϕ, then the model checker might return the set of initial states s0 where s0 |= ∃ϕ. Thisinformation could be understood as a counterexample and used for debugging purposes. This issue willnot be addressed here. Instead we will discuss the concept of path-based counterexamples (also often called“error traces”) and their duals, i.e., computations that provide a proof for the existence of computationswith certain properties.Counterexamples and Witnessesg0w0α375αββg1w1c0αf0βα τc1τβf1Figure 6.16: Transition systems for the wolf, goat, cabbage, and ferryman.(i.e., the goal). The synchronization actions α and β are used to describe the boat tripsthat are taking place together with the ferryman. The ferryman behaves very similarly,but has in addition the possibility to cross the river alone.
This corresponds to the twoτ -labeled transitions. The resulting transition system representing the entire “system”TS = (wolf ||| goat ||| cabbage) ferryman,has 24 = 16 states. The resulting transition system is depicted in Figure 6.17. Note thatthe transitions are all bidirectional as each boat movement can be reversed. The existenceof a sequence of boat movements to bring the two animals and the cabbage to the otherriverbank can be expressed as the CTL state formula ∃ϕ where(wi ∧ gi → fi ) ∧ (ci ∧ gi → fi ) U (c1 ∧ f1 ∧ g1 ∧ w1 ).ϕ =i=0,1Here, the left part of the until formula forbids the scenarios in which the wolf and thegoat, or the cabbage and the goat are left unobserved.
A witness of the CTL path formulaϕ is an initial finite path fragment which leads frominitial state c0 , f0 , g0 , w0 to target state c1 , f1 , g1 , w1 and which does not pass through any of the (six) states in which the wolf and the goator the goat and the cabbage are left alone on one riverbank. That is, e.g., the statesc0 , f0 , g1 , w1 and c1 , f0 , g1 , w0 should be avoided. An example witness for ϕ is:c0 , f0 , g0 , w0 c0 , f1 , g1 , w0 c0 , f0 , g1 , w0 c1 , f1 , g1 , w0 c1 , f0 , g0 , w0 c1 , f1 , g0 , w1 c1 , f0 , g0 , w1 c1 , f1 , g1 , w1 goat to riverbank 1ferryman comes back to riverbank 0cabbage to riverbank 1goat back to riverbank 0wolf to riverbank 1ferryman comes back to riverbank 0goat to riverbank 1376Computation Tree Logicc0 , f1 , g0 , w0 c0 , f1 , g0 , w1 c0 , f0 , g0 , w0 c1 , f1 , g0 , w0 c0 , f1 , g1 , w0 c0 , f1 , g1 , w1 c0 , f0 , g1 , w0 c0 , f0 , g0 , w1 c1 , f1 , g1 , w0 c1 , f0 , g0 , w0 c1 , f1 , g0 , w1 c1 , f0 , g0 , w1 c0 , f0 , g1 , w1 c1 , f1 , g1 , w1 c1 , f0 , g1 , w0 c1 , f0 , g1 , w1 Figure 6.17: Transition system of the wolf-goat-cabbage problem.6.6.1Counterexamples in CTLNow we explain how to generate counterexamples or witnesses for CTL (path) formulae.We consider here path formulae of the form Φ, Φ U Ψ, and Φ.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
