5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 73
Текст из файла (страница 73)
Then there exists a fair path π = s0 s1 s2 s3 . . . ∈Paths(s) with s1 |= a. Since π is fair, the path π[1..] = s1 s2 s3 . . . is fair too. Thus,s = s1 ∈ Post(s) satisfies the indicated property.⇐: Assume s |= a and FairPaths(s ) = ∅ for some s ∈ Post(s). Thus there exists a fairpathπ = s s1 s2 s3 . . .starting in s . Therefore, π = s s s1 s2 s3 . . . is a fair path starting s such that π |= a.Thus, s |=fair ∃ a.Using analogous arguments we obtain:Lemma 6.38.Until for Fair Satisfaction Relations |=fair ∃(a1 U a2 ) if and only if there exists a finite path fragments0 s1 s2 s3 . . .
sn ∈ Pathsfin (s)with n 0such that si |= a1 for 0 i < n, sn |= a2 , and FairPaths(sn ) = ∅.The results of the previous two lemmas lead to the following approach. As a first step,the setSatfair (∃ true) = { s ∈ S | FairPaths(s) = ∅ }366Computation Tree Logicis computed. (The algorithmic way to do so is explained later in this chapter.) That is,all states are determined for which it is guaranteed that at least one fair path emanates.Once such a state is visited, it is thus guaranteed that a fair continuation is possible. Thelabels of the thus computed states are extended with the new atomic proposition afair ,i.e.:afair ∈ L(s) if and only if s ∈ Satfair (∃ true).The sets Satfair (∃ a) and Satfair (∃(a U a )) result from= Sat (∃ (a ∧ afair )) ,Satfair (∃ a)Satfair(∃(a U a ))= Sat (∃(a U (a ∧ afair ))) .As a result, these satisfaction sets can be computed using an ordinary CTL model checker.These considerations lead to Algorithm 17 on page 364 and provide the basis for thefollowing result:Theorem 6.39.Model-Checking CTL with FairnessThe model-checking problem for CTL with fairness can be reduced to• the model-checking problem for CTL (without fairness), and• the problem of computing Satfair (∃a) for the atomic proposition a.Note that the set Satfair (∃ true) corresponds to Satfair (∃ a) whenever every state islabeled with a.
Thus, an algorithm to compute Satfair (∃ a) can also be used to computeSatfair (∃ true).In the following, we explain how to compute the satisfaction set Satfair (∃ a) for a ∈ APin case fair is a strong CTL fairness assumption. Weak fairness assumptions can betreated in an analogous way. As we will see, unconditional fairness assumptions are aspecial case. Arbitrary fairness assumptions with unconditional, strong, and weak fairnessconstraints can be treated by using algorithms in which the corresponding techniques areappropriately combined.Consider the strong CTL fairness assumption over the atomic propositions ai and bi (0 <i k):( ♦ ai → ♦ bi ).sfair =0<ikThe following lemma provides a graph-theoretical characterization of the fair satisfactionset Satsfair (∃ a) where a is an atomic proposition.Fairness in CTLLemma 6.40.367Characterization of Satsfair (∃a)s |=sfair ∃ a if and only if there exists a finite path fragment s0 s1 .
. . sn and a cycles0 s1 . . . sr such that(1) s0 = sandsn = s0 = sr ,(2) si |= a, for any 0 i n, and sj |= a, for any 0 < j r, and(3) Sat(ai ) ∩ { s1 , . . . , sr } = ∅ or Sat(bi ) ∩ { s1 , . . . , sr } = ∅ for all 1 i k.Proof: ⇐: Assume there exists a finite path fragment s0 s1 . . . sn and a cycle s0 s1 . . . srsuch that the conditions (1) through (3) hold for state s. Consider the infinite pathfragment π = s0 s1 . . .
sn s1 . . . sr s1 . . . sr . . . ∈ Paths(s) which is obtained by traversingthe cycle s0 s1 . . . sr infinitely often. From constraints (1) and (3), it follows that π is fair,i.e., π |= sfair . From (2), it follows that π |= a. Thus, s |=sfair ∃ a.⇒: Assume s |=sfair ∃ a. Since s |=sfair ∃ a, there exists an infinite path fragmentπ = s0 s1 s2 . . . with π |= a and π |= sfair . Let i ∈ { 1, . .
. , k }. Distinguish betweentwo cases:1. π |= ♦ai . Since π |= sfair , there is a state s ∈ Sat(bi ) which is infinitely oftenvisited in π . Let n ∈ IN such that sn = s and s ∈ { s0 , s1 , . . . , sn−1 }. That is,sn is the first occurrence of s in π.
Further, let r > n such that sn = sr . Thensn sn+1 . . . sr−1 sr = sn is a cycle withsn ∈ Sat(bi ) ∩ { sn , sn+1 , . . . , sr−1 , sr }.2. π |= ♦ai . Then there exists an index n such that sn , sn+1 , sn+2 . . . ∈ Sat(ai ). Assume without loss of generality that sn occurs infinitely often in π. Since there arefinitely many states, there exists an r > n such that sn = sr .
Thus, sn sn+1 . . . sr−1 sr =sn is a cycle with Sat(ai ) ∩ { sn , sn+1 , . . . , sr−1 , sr } = ∅.From both cases it follows that there exists a finite path fragment s0 s1 . . . sn and a cycles0 . . . sr satisfying the constraints (1) through (3).This characterization is used to compute Satsfair (∃ a) in the following way. Consider thedirected graph G[a] = (S, Ea ) whose set of edges Ea is defined as(s, s ) ∈ Eaif and only if s ∈ Post(s) ∧ s |= a ∧ s |= a.368Computation Tree LogicStated in words, G[a] is obtained from the state graph GTS by eliminating all edges (s, s )for which either s |= a or s |= a.
(Thus, G[a] is the state graph of the transition systemTS[a].) Apparently, each infinite path in G[a] (that starts in s ∈ I) corresponds to aninfinite path in the transition system TS satisfying a. Conversely, each infinite pathfragment π of TS with π |= a is a path in G[a]. In particular,s |=sfair ∃aif and only if there exists a nontrivial, strongly connected set of nodes D in G[a] that isreachable from s, such that for all 1 i k:D ∩ Sat(ai ) = ∅orD ∩ Sat(bi ) = ∅.Let T be the union of all nontrivial strongly connected components C in the graph G[a]such that sfair is realizable in C, i.e., there exists a nontrivial strongly connected subsetD of C satisfying D ∩ Sat(ai ) = ∅ or D ∩ Sat(bi ) = ∅, for all 1 i k. It then followsthatSatsfair (∃ a) = { s ∈ S | ReachG[a] (s) ∩ T = ∅ }.Here, ReachG[a] (s) is the set of states that is reachable from s in G[a].
Note that as SCCD is contained in SCC C, D can be reached from any state in C; reachability of C is thusof relevance.The key part of the model-checking algorithm is now the computation of the set T . Thisamounts to investigating the SCCs C of G[a] and checking for which SCC sfair is realizable.As the computation of T for the general case is slightly involved, we first consider twospecial (and simpler) cases: ai = true for all i, i.e., unconditional fairness, and the casefor which k=1, i.e., a single strong fairness constraint.In the sequel, each set C of nodes in G[a] is identified with the subgraph (C, EC ) whereEC results from the edge relation in G[a] by removing all edges with starting or targetvertex not in C.Unconditional Fairness Let ai = true for all 1 i k.
In this case ♦ bi .sfair ≡1ikObviously, s |=sfair ∃ a if and only if there exists a nontrivial SCC C in G[a] that isreachable from s, such that C contains at least one bi -state for any i. In that case, ♦ biis realizable in SCC C, for any i. Let T be the set union of all nontrivial SCCs C of G[a]satisfying C ∩ Sat(bi ) = ∅ for all 1 i k. It now follows thats |=sfair ∃ a if and only if ReachG[a] (s) ∩ T = ∅.Fairness in CTL369The following example illustrates this.Example 6.41.Consider the transition systems TS (upper) and TS (lower) in which it is implicitly assumed that all states are labeled with the atomic proposition a:{ b1 }s1s0s3s2s4{ b2 }s3s1s0s2{ b1 }s4{ b2 }(Due to this assumption, TS[a] = TS and TS [a] = TS .) Consider the unconditionalfairness assumption:sfair = ♦b1 ∧ ♦b2 .The transition system TS contains the reachable nontrivial SCC C = { s2 , s3 , s4 } suchthat C ∩ Sat(b1 ) = ∅ and C ∩ Sat(b2 ) = ∅.
We thus have s0 |=sfair ∃ a, and henceTS |=sfair ∃ a. On the other hand, TS contains two non-trivial SCCs, but none thatcontains a b1 -state and a b2 -state. Therefore s0 |=sfair ∃ a and hence TS |=sfair ∃ a.Strong Fairness with a Single Fairness Constraintassumed to be of the formsfair = ♦a1 → ♦b1 .Assume k=1. i.e., sfair isWe have that s |=sfair ∃a if and only if there exists a nontrivial strongly connectedcomponent C of G[a] with C ⊆ ReachG[a] (s) such that at least one of the following twoconditions (1) or (2) holds:(1) C ∩ Sat(b1 ) = ∅, or(2) D ∩ Sat(a1 ) = ∅ for some nontrivial SCC D of C.370Computation Tree LogicAlgorithm 18 Computation of Satsfair (∃a)Input: A finite TS without terminal states, a ∈ AP and fair = ♦ biOutput: { s ∈ S | s |=fair ∃ a }0<iksfair i with sfair i = ♦ ai →compute the SCCs of the state graph G[a] of TS[a];T := ∅;for all nontrivial SCCs C in G[a] do(* check whether the fairness assumption sfair can be realized in C *)if CheckFair (C, k, sfair 1 , .
. . , sfair k ) thenT := T ∪ C;fiodreturn { s ∈ S | ReachG[a] (s) ∩ T = ∅ }(* e.g., backwards reachability *)Intuitively, in case (1) C stands for a cyclic set of states that realizes ♦ b1 , while D in (2)represents a cyclic set of states for which ¬a1 continuously holds. The SCCs D of C thatdo not contain any a1 -state can easily be computed by determining the nontrivial SCCsin the graph that is obtained from C by eliminating all a1 -states.
(Stated differently, Crealizes the unconditional fairness constraint ♦ b1 , while D realizes the unconditionalfairness constraint ♦ true in the transition system induced by C after eliminating all a1 states. This characterization is helpful to understand the general algorithm below.) Everypath that has a suffix consisting of the infinite repetition of a cycle that runs through allstates of C (case (1)) or that eventually reaches D and stays there forever satisfies thefairness assumption sfair . Accordingly, we may define T as the union of all nontrivialSCCs C of G[a] satisfying the above constraints (1) and (2). Then, s |=sfair ∃a if andonly if ReachG[a] (s) ∩ T = ∅.Strong Fairness with k > 1 Fairness Constraints In this case, sfair is defined fork > 1 bysfair i with sfair i = ♦ ai → ♦ bi .sfair =1ikAs for the other cases, the initial step is to determine G[a] and its set of SCCs.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
