5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 70
Текст из файла (страница 70)
As for theuntil-operator, the algorithm for ∃ Φ is based on the characterization in Theorem 6.23,i.e., Sat(∃ Φ) is the largest set T ⊆ S satisfyingT ⊆ Sat(Φ) and (s ∈ T implies T ∩ Post(s) = ∅).The basic idea is to compute Sat(∃ Φ) by means of the iterationT0 = Sat(Φ) andTi+1 = Ti ∩ { s ∈ Sat(Φ) | Post(s) ∩ Ti = ∅ }.Then, for all j 0, it holds thatT0 T1 T2 . . . Tj = Tj+1 = .
. . = T = Sat(∃ Φ).The above iteration can be realized by means of a backward search starting withT = Sat(Φ)andE = S \ Sat(Φ).Here T equals T0 and E contains all states that refute ∃ Φ. During the backward search,states are iteratively removed from T , for which it has been established that they refute∃ Φ.
This applies to any s ∈ T satisfyingPost(s) ∩ T = ∅.Although s |= Φ (as it is in T ), all its successors refute ∃ Φ (as they are not in T ), andtherefore s refutes ∃ Φ. Once such states are encountered, they are inserted in E toenable the possible removal of other states in T .352Computation Tree LogicAlgorithm 16 Enumerative backward search to compute Sat(∃ Φ)Input: finite transition system TS with state set S and CTL formula ∃ ΦOutput: Sat(∃ Φ) = { s ∈ S | s |= ∃ Φ }(* E contains any not visited s with s |= ∃Φ *)E := S \ Sat(Φ);T := Sat(Φ);(* T contains any s for which s |= ∃Φ has not yet been disproven *)for all s ∈ Sat(Φ) do count[s] := | Post(s) |; odwhile E = ∅ do(* initialize array count *)(* loop invariant: count[s] = | Post(s) ∩ (T ∪ E) | *)(* s |= Φ *)(* s has been considered *)let s ∈ E;E := E \ { s };for all s ∈ Pre(s ) do(* update counters count[s] for all predecessors s of s *)if s ∈ T thencount[s] := count[s] − 1;if count[s] = 0 thenT := T \ { s };E := E ∪ { s };fifiododreturn T(* s does not have any successor in T *)The resulting computational procedure is detailed in Algorithm 16 on page 352.
In orderto support the test whether Post(s) ∩ T = ∅, a counter count[s] is exploited that keepstrack of the number of direct successors of s in T ∪ E:count[s] = | Post(s) ∩ (T ∪ E) |.Once count[s] = 0, we have that Post(s) ∩ (T ∪ E) = ∅, and hence Post(s) ∩ T = ∅. Thus,state s is not in Sat(∃ Φ) and therefore can be safely removed from T . On termination,E = ∅, and thus count[s] = | Post(s) ∩ T |.
It follows that any state s ∈ Sat(Φ) for whichcount[s] > 0 satisfies the CTL formula ∃ Φ.It is left to the interested reader to consider how the outlined approach can be modifiedto compute Sat(∃(Φ W Ψ)).CTL Model Checking353Example 6.27.Consider the transition system depicted in Figure 6.11 and the formula ∃ b. Initially,T0 = { s0 , s1 , s2 , s4 } andE = { s3 , s5 , s6 , s7 } and count = [1, 1, 2, 1, 2, 2, 1, 2].Suppose state s3 ∈ E is selected in the first iteration. As s1 ∈ Pre(s3 ) and s1 ∈ T ,count[s1 ] := 0.
Accordingly, s1 is deleted from T and added to E. This yieldsT1 = { s0 , s2 , s4 } andE = { s1 , s5 , s6 , s7 }and count = [1, 0, 2, 1, 2, 2, 1, 2].We also have s7 ∈ Pre(s3 ), but as s7 ∈ T , this affects neither count[s7 ], T nor E.Suppose s6 and s7 are selected in the second and third iteration, respectively. None ofthese states has a predecessor in T1 , so we obtainT3 = { s0 , s2 , s4 }and E = { s1 , s5 } andcount = [1, 0, 2, 1, 2, 2, 1, 2].Now select s1 ∈ E in the next iteration.
As Pre(s1 ) ∩ T3 = { s2 , s4 }, the counters for s2and s4 are decremented. This yieldsT4 = { s0 , s2 , s4 } and E = { s5 } and count = [1, 0, 1, 1, 1, 2, 1, 2].As Pre(s5 ) = ∅, T and count are unaffected in the subsequent iteration. As E = ∅, thealgorithm terminates and returns T = { s0 , s2 , s4 } as the final outcome.This section is concluded by outlining an alternative algorithm for computing Sat(∃ Φ).Since the computation of the satisfaction sets takes place by means of a bottom-up traversalthrough the parse tree of the formula at hand, it is assumed that Sat(Φ) is at our disposal.A possibility to compute Sat(∃ Φ) is to only consider the Φ-states of transition system TSand ignore all ¬Φ-states. The justification of this modification to TS is that all removedstates will not satisfy ∃ Φ (as they violate Φ) and therefore can be safely removed.For TS = (S, Act, →, I, AP, L) let TS[Φ] = (S , Act, → , I , AP, L ) with S = Sat(Φ),→ = → ∩ (S × Act × S ), I = I ∩ S and L (s) = L(s) for all s ∈ S .
Then, allnontrivial strongly connected components (SCCs) 4 in the state graph induced by TS[Φ]are computed. All states in each such SCC C satisfy ∃ Φ, as any state in C is reachablefrom any other state in C, and—by construction—all states in C satisfy Φ. Finally, allstates in TS[Φ] are computed that can reach such SCC. If state s ∈ S and there exists sucha path, then—by construction of TS[Φ]—the property ∃ Φ is satisfied by s; otherwise, itis not.
This can be done by a backward search. The worst-case time complexity of this4A strongly connected component (SCC) of a digraph G is a maximal, connected subgraph of G. Stateddifferently, the SCCs of a graph are the equivalence classes of vertices under the “are mutually reachable”relation. A nontrivial SCC is an SCC that contains at least one transition.354Computation Tree Logic{c}{ a, b, c }∅{a}{ a, c }{b}{ b, c }{ a, b }(a)(c) non-trivial SCC in TS[b](b) TS[b](d)Figure 6.13: Computing Sat(∃ b) using strongly connected components in TS[Φ].alternative algorithm is the same as for Algorithm 16. This approach is illustrated by thefollowing example.Example 6.28.Alternative Algorithm for ∃ ΦConsider the transition system of Figure 6.11 and CTL formula ∃ b.
The modifiedtransition system TS[b] consists of the four states that are labeled with b, see the graystates in Figure 6.13(a). The only nontrivial SCC of this structure is indicated by theblack states, see Figure 6.13(b). As there is only a single b-state (that is not in the SCC)that can reach the nontrivial SCC, this state satisfies ∃ b, and the computation finishes,see Figure 6.13(c).Theorem 6.29.For state s in transition system TS and CTL formula Φ:s |= ∃ Φ iff s |= Φ and there is a nontrivial SCC in TS[Φ] reachable from s.Proof: ⇒: Suppose s |= ∃ Φ. Clearly, s is a state in TS[Φ].
Let π be a path in TSstarting in s such that π |= Φ. As TS is finite, π has a suffix ρ = s1 s2 . . . sk for k > 1,representing a cycle that is traversed infinitely often. As π is also a path in TS[Φ], theCTL Model Checking355states s1 through sk are all in TS[Φ]. Since π is traversed infinitely often, it representsa cycle, and thus any pair of states si and sj is mutually reachable. Stated differently,{ s1 , . . . , sk } is either an SCC or contained in some SCC in TS[Φ].
As π is a path startingin s, these states are reachable from s.⇐: Suppose s is a state in TS[Φ] and there exists an SCC in TS[Φ] reachable from s. Lets be a state in such SCC. As the SCC is nontrivial, s is reachable from itself by a pathof length at least one. Repeating this cycle infinitely often yields an infinite path π withπ |= Φ. The path from s to s followed by π[1..] now satisfies Φ and starts in s. Thus,s |= ∃ Φ.6.4.3Time and Space ComplexityThe time complexity of the CTL model-checking algorithm is determined as follows. LetTS be a finite transition system with N states and K transitions. Under the assumptionthat the sets of predecessors Pre(·) are represented as linked lists, the time complexity ofAlgorithms 15 and 16 lies in O(N +K). Given that the computation of the satisfactionsets Sat(Φ) is a bottom-up traversal over the parse tree of Φ and thus linear in | Φ |, thetime complexity of Algorithm 14 (see page 348) is inO((N +K) · | Φ |).When the initial states of TS are administrated in, e.g., a linked list, checking whetherI ⊆ Sat(Φ) can be done in O(N0 ) where N0 is the cardinality of the set I.
Recall that theCTL model-checking algorithm requires the CTL formula to be checked to be in existentialnormal form. As the transformation of any CTL formula into an equivalent CTL formulain ENF may yield an exponential blowup of the formula, it is recommended to treatthe modalities such as ∀ U, ∀♦ , ∀ , ∃♦ , ∀ W , and ∃ W , analogous to the introducedapproaches for ∃ U and ∃ , by exploiting the characterizations of Sat(∀ Φ), Sat(∃♦ Φ),and so on. The resulting algorithms are all linear in N and K. Thus, we obtain thefollowing theorem:Theorem 6.30.Time Complexity of CTL Model CheckingFor transition system TS with N states and K transitions, and CTL formula Φ, the CTLmodel-checking problem TS |= Φ can be determined in time O ((N +K) · | Φ |).Let us compare this complexity bound with that for LTL model checking. Recall that LTLmodel checking is exponential in the size of the formula.
Although the difference in timecomplexity with respect to the length of the formula seems drastic (exponential for LTL vs.356Computation Tree Logiclinear for CTL), this should not be interpreted as “CTL model checking is more efficientthan LTL model checking”. From Theorem 6.18 it follows that whenever ϕ ≡ Φ for LTLformula ϕ and CTL formula Φ, then ϕ is obtained by removing all path quantifiers in Φ.Thus, CTL formulae are at least as long as their equivalent counterparts in LTL (if theseexist). In fact, if P = NP, then there exist LTL formulae ϕn with | ϕn | ∈ O(poly (n)) forwhich CTL-equivalent formulae do exist, but not of polynomial length.
LTL formulae maybe exponentially shorter than any of their equivalent formulation in CTL. The latter effectis illustrated in the following example. From Lemma 5.45, it follows that the Hamiltonianpath problem for digraphs with n nodes can be encoded in LTL formula ϕn whose lengthis polynomial in n. More precisely, given a digraph G with nodeset { 1, . . . , n } there is anLTL formula ϕn such that (1) G has a Hamiltonian path if and only if ¬ϕn does not holdfor the transition system associated with G and (2) ¬ϕn has an equivalent CTL formula.To express the existence of a Hamiltonian path in CTL requires a CTL formula of exponential length, unless P = NP: if it is assumed that ¬ϕn ≡ ¬Φn for CTL formulae Φnof polynomial length, then the Hamiltonian path problem could be solved by CTL modelchecking, and thus in polynomial time.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
