5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 60
Текст из файла (страница 60)
Intuitively, the first componentq ∈ Q∪{ ∗ } of state (q, A, i) in the ith copy indicates whether the cursor points to cell i (inwhich case q ∈ Q is the current state) or to some other tape cell (in which case q = ∗). Thesymbol A ∈ Σ in state (q, A, i) stands for the current symbol in cell i.
The path fragmentsfrom state 0 to state P (n) serve to represent the possible configurations of M. Moreprecisely, the configuration in which the current content of the tape is A1 A2 . . . AP (n) , thecurrent state is q, and the cursor points to cell i is encoded by the path fragment:0 (∗, A1 , 1) 1 (∗, A 2 , 2) 2 . . . i−1 (q, Ai , i) i (∗, A i+1 , i+1) i+1 . . . P (n)Accordingly, the computation of M for an input word of length n can be described by theconcatenation of such path fragments.292Linear Temporal Logic012P(n)Figure 5.23: Transition system TS(M, n) for Turing machine M and input length n.We use the state identities as atomic propositions. In addition, proposition begin is usedto identify state 0, while proposition end is used for state P (n). That is, AP = S ∪{ begin, end } with the obvious labeling function.
Let ΦQ denote the disjunction over allatoms (q, A, i) where q ∈ Q (i.e., q = ∗) and A ∈ Σ, 0 < i P (n). The LTL formulae:whereϕConf = begin −→ ϕ1Conf ∧ ϕ2Conf"ϕ1Conf =ϕ2Conf 2i−1 ΦQ1iP (n)= 2i−1 ΦQ −→1iP (n) 2j−1 ¬ΦQ1jP (n)j=icharacterize any path π in TS such that all path fragments of π that lead from 0 via1, . .
. , P (n−1) to P (n) encode a configuration of M. Note that ϕ1Conf ∧ϕ2Conf ensures that thecursor points exactly to one of the positions 1, . . . , P (n). Thus, any path π in TS such thatπ |= ϕConf can be viewed as a sequence of configurations in M. However, this sequence neednot be a computation of M, since the configurations might not be consecutive accordingto M’s operational behavior. For this, we need additional constraints that formalize M’sstepwise behavior.The transition relation δ of M can be encoded by an LTL formula ϕδ that arises througha conjunction of formulae ϕq,A describing the semantics of δ(q, A).
Here, q ranges over allstates in Q and A over the tape-symbols in Σ. For instance, if δ(q, A) = (p, B, L) thenϕq,A = 1iP (n) 2i−1 (q, A, i) −→ ψ(q,A,i,p,B,L)Automata-Based LTL Model Checking293where ψ(q,A,i,p,B,L) is defined as1jP (n)j=i,C∈Σ( 2j−1 C ↔ 2j−1+2P (n)+1 C ) ∧ 2i−1+2P (n)+1 B ∧ 2i−1+2P (n)+1−2 p .
content of all cells j = i unchangedoverwrite A by B in cell imove to state pand cursor to cell i−1Here, C denotes the disjunction of the atoms (r, C, j) where r ∈ Q∪{ ∗ } and 1 j P (n),and p for the disjunction of all atoms (p, D, j) where D ∈ Σ and 1 j P (n).The starting configuration of M for a given input word w = A1 . . . An ∈ Σ∗ is given bythe formula 2i−1 Ai ∧ 2i−1 $ .ϕwstart = q0 ∧1inn<iP (n)The first conjunct q0 asserts that M starts in its starting state; the other conjunctsassert that A1 . . .
An $P (n)−n is the content of the tape where $ denotes the blank symbol.The accepting configurations are formalized by the formula!q.ϕaccept = ♦q∈FFor a given input word w = A1 . . . An of length n for M, letϕw = ϕwstart ∧ ϕConf ∧ ϕδ ∧ ϕaccept .Note that the length of ϕw is polynomial in the size of M and the length n of w. Thus,TS = TS(M, n) and ϕw can be constructed from (M, w) in polynomial time. Moreover,it also follows that there exists a path π |= ϕw in TS if and only if M accepts the inputword w.For real applications, the aforementioned theoretical complexity result is less dramaticthan it seems at first sight, since the complexity is linear in the size of the transitionsystem and exponential in formula length. In practice, typical requirement specificationsyield short LTL formulae.
In fact, the exponential growth in the length of the formulais not decisive for the practical application of LTL model checking. Instead, the lineardependency on the size of the transition system is the critical factor. As has been discussedat the end of Chapter 2 (page 77), the size of transition systems may be huge evenfor relatively simple systems—the state-space explosion problem. In later chapters ofthis monograph, various techniques will be treated to combat this state-space explosionproblem.We mentioned before that the LTL model-checking problem is PSPACE-complete.
Theprevious result showed PSPACE-hardness. It remains to show that it belongs to thecomplexity class PSPACE.294Linear Temporal LogicTo prove that the LTL model-checking problem is in PSPACE, we resort (again) to theexistential variant of the LTL model-checking problem. This is justified by the fact thatPSPACE – as any other deterministic complexity class – is closed under complementation.That is, the LTL model-checking problem is in PSPACE iff its complement is in PSPACE.This is equivalent to the statement that the existential variant of the LTL model-checkingproblem is solvable by a polynomial space-bounded algorithm. By Savitch’s theorem(PSPACE agrees with NPSPACE), it suffices to provide a nondeterministic polynomialspace-bounded algorithm that solves the existential LTL model-checking problem.Lemma 5.47.The existential LTL model-checking problem is solvable by a nondeterministic space-bounded algorithm.Proof: In the sequel, let ϕ be an LTL formula and TS = (S, Act, →, I, AP, L) a finitetransition system.
The goal is to check nondeterministically whether TS has a path πwith π |= ϕ, while the memory requirements are bounded by O( poly(size(TS), |ϕ|) ). Thetechniques discussed in Section 5.2 (page 270 ff) suggest to build an NBA Aϕ for ϕ,construct the product transition system TS ⊗ Aϕ and check whether this product containsa reachable cycle containing an accept state of Aϕ . We now modify this approach toobtain an NPSPACE algorithm.
Instead of an NBA for ϕ, we deal here with the GNBAGϕ for ϕ. Recall that states in this automaton are elementary subsets of the closure of ϕ(see Definition 5.34 on page 276). The goal is to guess nondeterministically a finite pathu0 u1 . . . un−1 v0 v1 . . . vm−1 in TS ⊗ Gϕ and to check whether the components of Gϕ inthe infinite pathu0 u1 . . .
un−1 (v0 v1 . . . vm−1 )ωconstitute an accepting run in Gϕ . This, of course, requires that v0 is a successor of vm−1 .The states ui , vj in the infinite path in TS ⊗ Gϕ are pairs consisting of a state in TSand an elementary set of formulae. For the lengths of the prefix u0 . . . un−1 and the cyclev0 v1 . . . vm−1 vm we can deal with n k and m k ·|ϕ| where k is the number of reachablestates in TS ⊗ Gϕ . (Note that |ϕ| is an upper bound for the number of acceptance sets inGv arphi.) An upper bound for the value k is given byK = NTS · 2Nϕwhere NTS denotes the number of states in TS and Nϕ = |closure(ϕ)|. Note thatK = O( size(TS) · exp(|ϕ|) ).The algorithm now works as follows.
We first nondeterministically choose two naturalnumbers n, m with n K and m K · |ϕ| (by guessing %log K& = O(log(size(TS)) · |ϕ|)Automata-Based LTL Model Checking295bits for n and %log K&+%log |ϕ|& = O(log(size(TS)) · |ϕ|) bits for m). Then the algorithmguesses nondeterministically a sequence u0 . . . un−1 , un . .
. un+m where the ui ’s are pairssi , Bi consisting of a state si in TS and a subset Bi of closure(ϕ). For each such stateui = si , Bi , the algorithm checks whether1. si is a successor of si−1 , provided that i 1,2. Bi is elementary,3. Bi ∩ AP = L(si ),4. Bi ∈ δ(Bi−1 , L(si )), provided that i 1.For i = 0, the algorithm checks whether s0 ∈ I is an initial state of TS and whether B0 ∈δ(B, L(s0 )) for some elementary set B which contains ϕ. Here, δ denotes the transitionrelation of the GNBA Gϕ .
(Recall that the sets B where ϕ ∈ B are the initial states inthe GNBA for ϕ.) Conditions 1-4 are local and simple to check. If one of these fourconditions is violated for some i, the algorithm rejects and halts. Otherwise u0 . . . un+mis a finite path in TS ⊗ Gϕ . We finally check whether un agrees with the last stateun+m . Again, the algorithm rejects and halts if this condition does not hold. Otherwise,u0 . . . un−1 (un . .
. un+m−1 )ω is an infinite path in TS ⊗ Gϕ , and it finally amounts to checkwhether the acceptance condition of Gϕ is fulfilled. This means we have to verify thatwhenever ψ1 U ψ2 ∈ Bi for some i ∈ {n, . . . , n + m − 1}, then there is some j ∈ {n, . . . , n +m − 1} such that ψ2 ∈ Bj . If this condition holds, then the algorithm terminates with theanswer “yes”.This algorithm is correct since if TS has a path where ϕ holds, then there is a computationof the above algorithm that returns “yes”. Otherwise, i.e., if TS does not have a pathwhere ϕ holds, then all computations of the algorithm are rejecting.It remains to explain how the sketched algorithm can be realized such that the memoryrequirements are polynomial in the size of TS and length of ϕ. Although the length n + mof the path u0 .
. . un+m might be exponentially in the length of ϕ (note that, e.g., n = Kis possible and that K grows exponentially in the length of ϕ), this procedure can berealized with only polynomial space requirements. This is due to the observation that forchecking the above conditions 1-4 for ui = si , Bi , we only need state ui−1 = si−1 , Bi−1 .Thus, there is no need to store all states uj for 0 j n + m. Instead, the actual andprevious states are sufficient. Moreover, to verify that Gϕ ’s acceptance condition holds,we only need to remember the subformulae ψ1 U ψ2 of ϕ that are contained in some of thesets Bn , . .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
