5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 59
Текст из файла (страница 59)
The reader isreferred to Exercise 5.22 (on page 308) for more details.288Linear Temporal LogicAn interesting aspect of the LTL model-checking algorithm is that it can be executed onthe-fly, i.e., while constructing the NBA A¬ϕ . This may avoid the need for constructing theentire automaton A¬ϕ . This on-the-fly procedure works as follows. Suppose we are given ahigh-level description of the transition system TS, e.g., by means of a syntactic descriptionof the concurrent processes (as in Spin’s input language Promela).
The generation ofthe reachable states of TS can proceed in parallel with the construction of the relevantfragment of A¬ϕ . Simultaneously, the reachable fragment of the product transition systemTS ⊗ A¬ϕ is constructed in a DFS-manner. (This, in fact, yields the outermost DFS inthe nested DFS for checking persistence in TS ⊗ A¬ϕ .) So the entire LTL model-checkingprocedure can be interleaved with the generation of the relevant fragments of TS and A¬ϕ .In this way, the product transition system TS ⊗ A¬ϕ is constructed “on demand”, so tospeak. A new vertex is only considered if no accepting cycle has been encountered yetin the partially constructed product transition system TS ⊗ A¬ϕ . When generating thesuccessors of a state in A¬ϕ , it suffices to only consider the successors matching the currentstate TS (rather than all possible successors).
It is thus possible that an accepting cycleis found, i.e., a violation of ϕ (with corresponding counterexample), without the need forgenerating the entire automaton A¬ϕ .This on-the-fly generation of Reach(TS), A¬ϕ , and TS ⊗ A¬ϕ is adopted in practicalLTL model checkers (such as Spin) and for many examples yields an efficient verificationprocedure. From a theoretical point of view, though, the LTL model-checking problemremains computationally hard and is ”probably” not efficiently solvable.
It is shown inthe sequel of this section that the LTL model-checking problem is PSPACE-complete.We assume some familiarity with basic notions of complexity theory and the complexityclasses coNP and PSPACE; see, e.g., the textbooks [160, 320] and the Appendix.Before proving the PSPACE-hardness of the LTL model-checking problem, a weaker resultis provided. To that end, let us recall the so-called Hamiltonian path problem.
Consider afinite directed graph G = (V, E) with set V of vertices and set E ⊆ V × V of edges. TheHamiltonian path problem is a decision problem that yields an affirmative answer when Ghas a Hamiltonian path, i.e., a path which passes through every vertex in V exactly once.The next ingredient needed for the following result is the complement of the LTL modelchecking problem. This decision problem takes as input a finite transition system TS andan LTL formula ϕ and asks whether TS |= ϕ. Thus, whenever the LTL model-checkingproblem provides an affirmative answer, its complement yields “no”, and whenever theresult of the LTL model-checking problem is negative, its complement yields “yes”.Lemma 5.45.The Hamiltonian path problem is polynomially reducible to the complement of the LTLmodel-checking problem.Automata-Based LTL Model Checking289Proof: To establish a polynomial reduction from the Hamiltonian path problem to thecomplement of the LTL model-checking problem, a mapping is needed from instances ofthe Hamiltonian path problem onto instances for the complement model-checking problem.That is, we need to map a finite directed graph G onto a pair (TS, ϕ) where TS is a finitetransition system and ϕ is an LTL formula, such that(i) G has a Hamiltonian path if and only if TS |= ϕ, and(ii) the transformation G (TS, ϕ) can be performed in polynomial time.The basic concept of the mapping is as follows.
Essentially, TS corresponds to G, i.e., thestates of TS are the vertices in G and the transitions in TS correspond to the edges inG. For technical reasons, G is slightly modified to ensure that TS has no terminal states.More precisely, the state graph of TS arises from G by inserting a new vertex b to G, whichis reachable from every vertex v via an edge and which is only equipped with a self-loopb → b (i.e., b has no further outgoing edges). Formally, for G = (V, E) the associatedtransition system isTS = (V { b }, { τ }, →, V, V, L)where L(v) = { v } for any vertex v ∈ V and L(b) = ∅. The atomic propositions for TSare thus obtained by taking the identities of the vertices in G.
The transition relation →is defined as follows:v ∈ V ∪ {b}(v, w) ∈ Eand.ττv −→ wv −→bThis completes the mapping of directed graph G onto transition system TS. It remains toformalize the negation of the existence (i.e., the absence) of a Hamiltonian path by meansof an LTL formula. Let( ♦v ∧ (v → ¬v) ).ϕ = ¬v∈VStated in words, ϕ asserts that it is not the case that each vertex v ∈ V is eventuallyvisited and never visited again. Note that the conjunction does not quantify over b ∈ V .It is evident that TS and ϕ can be constructed in polynomial time for a given directedgraph G. As a last step, we need to show that G has a Hamiltonian path if and only ifTS |= ϕ.⇐: Assume TS |= ϕ.
Then there exists a path π in TS such that( ♦v ∧ (v → ¬v) ).π |=v∈V290As π |=Linear Temporal Logicv∈V♦v, each vertex v ∈ V occurs at least once in the path π. Since(v → ¬v),π |=v∈Vthere is no vertex that occurs more than once in π. Thus, π is of the form v1 . . . vn b b b . .
.where V = { v1 , . . . , vn } and |V | = n. In particular, v1 . . . vn is a Hamiltonian path in G.⇒: Each Hamiltonian path v1 . . . vn in G can be extended to a path π = v1 . . . vn b b b . . .in TS. Thus, π |= ϕ and, hence, TS |= ϕ.Since the Hamiltonian path problem is known to be NP-complete, it follows from the previous lemma that the LTL model-checking problem is coNP-hard.
The following complexityresult states that the LTL model-checking problem is PSPACE-hard.Theorem 5.46.Lower Bound for LTL Model CheckingThe LTL model-checking problem is PSPACE–hard.Proof: Let TS be a finite transition system and ϕ an LTL formula. As a first observation,note that it suffices to show the PSPACE-hardness of the existential variant of the LTLmodel-checking problem.
This existential decision problem takes as input TS and ϕ andyields “yes” if π |= ϕ for some (initial, infinite) path π in TS, and “no” otherwise. GiventhatTS |= ϕif and only ifπ |= ϕ for all paths πif and only ifnot (π |= ¬ϕ for some path π)it follows that the output for the instance (TS, ϕ) of the LTL model-checking problemyields ”yes” if and only if the output for the instance (TS, ¬ϕ) of the existential variant of the LTL model-checking problem yields ”no”. Thus, the PSPACE-hardness ofthe existential variant of the LTL model-checking problem yields the PSPACE-hardnessof the complement of the existential variant of the LTL model checking problem whichagain induces the PSPACE-hardness of the LTL model-checking problem.
Recall thatPSPACE = coPSPACE, thus, the complement of any PSPACE-hard problem is PSPACEhard.In the remainder of the proof we concentrate on showing the PSPACE–hardness of theexistential LTL model-checking problem. This is established by providing a polynomialreduction from any decision problem K ∈ PSPACE to the existential LTL model-checkingproblem. Let M be a polynomial space-bounded deterministic Turing machine that accepts exactly the words w ∈ K. The goal is now to transform (M, w) by a deterministicAutomata-Based LTL Model Checking291polynomial-time bounded procedure into a pair (TS, ϕ) such that M accepts w if and onlyif TS contains a path π with π |= ϕ.The following proof, adopted from [372], has some similarities with Cook’s theorem statingthe NP-completeness of the satisfiability problem for propositional logic.
The rough ideais to encode the initial configurations, possible transitions, and accepting configurationsof a given Turing machine M by LTL formulae. In the sequel, let M be a deterministicsingle-tape Turing machine with state-space Q, starting state q0 ∈ Q, the set F of acceptstates, the tape alphabet Σ, and the transition function δ : Q × Σ → Q × Σ × { L, R, N }.The intuitive meaning of δ is as follows.
Suppose δ(q, A) = (p, B, L). Then, whenever thecurrent state is q and the current symbol in cell i under the cursor is A, then M changesto state p, overwrites the symbol A by B in cell i, and moves the cursor one position tothe left, i.e., it positions the cursor under cell i−1. For R or N , the cursor moves oneposition to the right, or does not move at all, respectively. (For our purposes, there is noneed to distinguish between the input and the tape alphabet.)For technical reasons, it is required that the accept states are absorbing, i.e., δ(q, A) =(q, A, N ) for all q ∈ F .
Moreover, it is assumed that M is polynomially space-bounded,i.e., there is a polynomial P such that the computation for an input word A1 . . . An ∈ Σ∗of length n visits at most the first P (n) cells on the tape. Without loss of generality, thecoefficients of P are assumed to be natural numbers and P (n) n.To encode M’s possible behaviors by LTL formulae for an input word of length n, theTuring machine is transformed into a transition system TS = TS(M, n) with the followingstate space:S = {0, 1, . . . , P (n)} ∪ {(q, A, i) | q ∈ Q ∪ { ∗ }, A ∈ Σ, 0 < i P (n)}.The structure of TS is shown in Figure 5.23. TS consists of P (n) copies of “diamonds”.The ith copy starts in state i−1, ends in state i, and contains the states (q, A, i) whereq ∈ Q ∪ { ∗ } and A ∈ Σ “between” state i−1 and state i.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
