5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 71
Текст из файла (страница 71)
Since, however, the Hamiltonian path problem isNP-complete, this is only possible for the case of PTIME = NP.Example 6.31.The Hamiltonian Path ProblemConsider the NP-complete problem of finding a Hamiltonian path in an arbitrary, connected, directed graph G = (V, E) where V denotes the set of vertices and E ⊆ V × V ,the set of edges. Let V = { v1 , . .
. , vn }. A Hamiltonian path is a (finite) path through thegraph G which visits each state exactly once. Starting from graph G, a transition systemTS(G) is derived as well as a CTL formula Φn , such thatG contains a Hamiltonian path if and only if TS |= ¬Φn .The transition system TS is defined as followsTS = (V ∪ { b }, { τ }, →, V, V, L)with L(vi ) = { vi }, L(b) = ∅.
The transition relation → is defined by(vi , vj ) ∈ Eτvi −→vjandvi ∈ V ∪ { b }.τvi −→bAll vertices of G are states in the transition system TS. A new state b is introducedthat is a direct successor of any state (including b). Figure 6.14 shows (a) an exampleof a directed graph G and (b) its transition system TS(G). The sole purpose of the newstate b is to ensure that the transition system has no terminal states.
Note that TS(G)is defined as in the proof for the existence of a polynomial reduction of the HamiltonianCTL Model Checkingv1357v2v3v4{v3 }v3{v2 }v2{v1 } v1{b}(a)v4 {v4 }b(b)Figure 6.14: Example of encoding the Hamiltonian path problem as a transition system.path problem onto the complement of the LTL model-checking problem; see Lemma 5.45on page 288.It remains to give a recipe for the construction of Φn , a CTL formula that captures theexistence of a Hamiltonian path. Let Φn be defined as follows:!Ψ(vi1 , vi2 , . . . , vin )Φn =(i1 ,...,in )permutation of (1, . . .
, n)such that Ψ(vi1 , . . . , vin ) is a CTL formula that is satisfied if and only if vi1 , vi2 ,. . . , vin isa Hamiltonian path in G. The formulae Ψ(vi1 , . . . , vin ) are inductively defined as follows:Ψ(vi ) = viΨ(vi1 , vi2 , . . . , vin ) = vi1 ∧ ∃ Ψ(vi2 , . . . , vin )if n > 1.Stated in words, Ψ(vi1 , . . . , vin ) holds if there exists a path on which vi1 , vi2 , vi3 successivelyhold. Since each state has a transition to the b state, the trace { vi1 } { vi2 } . . . { vin } canbe extended with { b }ω .
An example of an instantiation of Ψn isΦ2 = (v1 ∧ ∃ v2 ) ∨ (v2 ∧ ∃ v1 )andΦ3 =(v1 ∧ ∃ (v2 ∧ ∃ v3 ))∨(v1 ∧ ∃ (v3 ∧ ∃ v2 ))∨ (v2 ∧ ∃ (v1 ∧ ∃ v3 ))∨(v2 ∧ ∃ (v3 ∧ ∃ v1 ))∨ (v3 ∧ ∃ (v1 ∧ ∃ v2 ))∨(v3 ∧ ∃ (v2 ∧ ∃ v1 )).It is not difficult to infer thatSat( Ψ(vi1 , . . . , vin ) ) =Thus: { vi1 }∅if vi1 , . . . , vin is a Hamiltonian path in Gotherwise.358Computation Tree LogicTS |= ¬Φniffthere is an initial state s of TS for which s |= ¬Φniffthere is an initial state s of TS for which s |= Φniff∃v in G and a permutation i1 , . . . , in of 1, . .
. , n withv ∈ Sat(Ψ(vi1 , . . . , vin )),iff∃v in G and a permutation i1 , . . . , in of 1, . . . , n,such that v = vi1 and vi1 , . . . , vin is a Hamiltonian path in GiffG has a Hamiltonian path.Thus, G contains a Hamiltonian path if and only if TS |= ¬Φn .By the explicit enumeration of all possible permutations we obtain a formula with a lengththat is exponential in the number of vertices in the graph. This does not prove that theredoes not exist an equivalent, but shorter, CTL formula which describes the Hamiltonianpath problem.
Actually, shorter formalizations in CTL cannot be expected, since the CTLmodel-checking problem is polynomially solvable whereas the Hamiltonian path problemis NP-complete.6.5Fairness in CTLRecall that fairness assumptions (see Section 3.5) are used to rule out certain computationsthat are considered to be unrealistic for the system under consideration.
These unreasonable computations that ignore certain transition alternatives forever are the “unfair” ones;the remaining computations are thus the “fair” ones. As there are different notions of fairness, various distinct forms of fairness can be imposed: unconditional, strong, and weakfairness constraints.An important distinction between LTL and CTL is that fairness assumptions can beincorporated into LTL without any specific changes while a special treatment of fairnessis required for CTL. That is to say, fairness assumptions can be added as premise to theLTL formula to be verified.
The LTL model-checking problem where only fair paths areconsidered (i.e., considering the fair satisfaction relation |=fair ) can thus be reduced tothe traditional LTL model-checking problem, i.e., with respect to the common satisfactionrelation |=. In this case, the LTL formula ϕ to be verified is replaced by fair → ϕ:TS |=fair ϕ if and only if TS |= (fair → ϕ).55This observation is mainly of theoretical interest since it is more efficient to design special LTL model-Fairness in CTL359For more details we refer to Section 5.1.6 (see page 257).An analogous approach is not possible for CTL. This stems from the fact that mostfairness constraints cannot be encoded in a CTL formula.
An indication of this is the factthat persistence properties ♦a are inherent in, e.g., strong fairness conditions ♦b →♦c ≡ ♦¬b ∨ ♦c and cannot be expressed in CTL. To be a bit more precise: fairnessconstraints operate on the path level and replace the standard meaning “for all paths”of universal quantification with “for all fair paths” and existential quantification “thereexists a path” with “there exists a fair path”. Thus, if fair expresses the fairness conditionon the path level, then CTL formulae that encode the intuitive meaning of ∀(fair → ϕ)and ∃(fair ∧ ϕ) would be needed. However, these are not legal CTL formulae since (1) theBoolean connectives → and ∧ are not allowed on the level of CTL path formulae and (2)fairness conditions cannot be described by CTL path formulae.Therefore, an alternative approach is taken to treat fairness in CTL.
In order to deal withfairness constraints in CTL, the semantics of CTL is slightly modified such that the stateformulae ∀ϕ and ∃ϕ are interpreted over all fair paths rather than over all possible paths.A fair path is a path that satisfies a set of fairness constraints. It is assumed that thegiven fixed fairness constraint is described by a formula as in LTL.Definition 6.32.CTL Fairness AssumptionsA strong CTL fairness constraint (over AP) is a term of the form( ♦ Φi → ♦ Ψi )sfair =1ikWeak and unconditionalwhere Φi and Ψi (for 1 i k) are CTL formulae over AP.CTL fairness constraints are defined analogously by conjunctions of terms of the form(♦ Φi → ♦ Ψi ) and ♦ Ψi , respectively.
A CTL fairness assumption is a conjunctionof strong, weak, and unconditional CTL fairness constraints.Note that CTL fairness assumptions are not CTL path formulae, but they can be viewedas LTL formulae using CTL state formulaeinstead of atomic propositions. For instance,( ♦ Φi → ♦ Ψi ) on paths means that aimposing the strong fairness constraint1ikpath must either have only finitely many states satisfying Φi or infinitely many statessatisfying Ψi , for any 1 i k (or both).Let TS = (S, Act, →, I, AP, L) be a transition system without terminal states, π be aninfinite path fragment in TS, and fair a fixed CTL fairness assumption. π |= fair denoteschecking algorithms when dealing with fairness assumptions than to apply the reduction to the standardsemantics |=.360Computation Tree Logicthat π satisfies the formula fair , where |= should be read as the LTL semantics.
Consider,for example, strong fairness. For an infinite path π = s0 s1 s2 . . ., we have( ♦ Φi → ♦ Ψi )π |=1ikif and only if for every i ∈ { 1, . . . , k } either sj |= Φi for finitely many indices j, orsj |= Ψi for infinitely many j (or both). Here, the statement sj |= Φi should be interpretedaccording to the CTL semantics, that is, the semantics without taking any fairness intoaccount.The semantics of CTL under fairness assumption fair is identical to the semantics givenearlier (see Definition 6.4), except that the path quantifications range over all fair pathsrather than over all paths.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
