5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 46

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 46)

Consider the scenario in which s2 is considered as a firstsuccessor of s0 , i.e., s2 is considered in the outer depth-first search prior to consideringstate s1 . This means that the order in which the states are put by Algorithm 8 on thestack U equals s1 , s3 , s2 , s0 where we write the stack content from the top to the bottom,i.e., s1 is the top element (the last element that has been pushed on the stack). Besides,R = S.

Thus, the outer DFS takes s1 as the top element of U and verifies Post(s1 ) ⊆ R.As s1 |= Φ, the invocation cycle check(s1 ) takes place and s1 is deleted from stack U for theouter DFS. This yields that s1 is put on the stack V for the inner DFS, followed by its onlysuccessor s3 . Then the cycle s1 → s3 → s1 is detected, cycle check(s1 ) yields true, andas a result, reachable cycle(s0 ) terminates with the conclusion that Ppers on Φ is refuted.An error indication is obtained by first concatenating the content of V = s1 , s3 , s1 andU = s3 , s2 , s0 and then reversing the order.

This yields the path s0 s2 s3 s1 s3 s1 , whichis indeed a prefix of a run refuting “eventually always Φ”.The soundness of the nested depth-first search is no longer trivial because – by thetreatment of T as a global variable – not all states reachable from s are explored incycle check(s), but only those states that have not been visited before in the inner depthfirst search. Thus, we could imagine that there is a cycle with ¬Φ-states which will notbe found with the nested depth-first search: this cycle might have been explored duringcycle check(u) where u does not belong to this or any other cycle. Then, none of thefollowing procedure calls of cycle check(·) will find this cycle. The goal is now to showModel-Checking ω-Regular Properties213s0s2s1s3Figure 4.25: An example of a transition system for nested DFS.that this cannot happen, i.e., if there is a reachable cycle with ¬Φ-states, then the nesteddepth-first search will find such a cycle.In fact, things are more tricky than it seems.

In Algorithm 8 it is important that theinvocations to the procedure cycle check(s) for s ∈ Reach(TS) and s |= Φ occur in appropriate order. Let s |= Φ. Then cycle check(s) is only invoked if Post(s) ⊆ R, i.e.,when all states reachable from s have been encountered and visited.6 So, the invocationcycle check(s) is made immediately once all states that are reachable from s have beenvisited and expanded in the outer depth-first search.

As a result, Algorithm 8 satisfies thefollowing property: if s is a successor of state s in the visit-order of the outer depth-firstsearch and s |= Φ and s |= Φ, then the invocation cycle check(s ) occurs prior to theinvocation cycle check(s).Example 4.68.Modifying the Nested DFSLet us illustrate by an example that the nested depth-first search algorithm would bewrong if the outer and inner DFS are interleaved in an arbitrary way.

We consider againthe transition system in Figure 4.25 on page 213. We start the outer DFS with the initialstate s0 and assume that state s2 is visited prior to s1 . Let us see what happens if wedo not wait until s2 has been fully expanded in the outer DFS and start cycle check(s2 )immediately.

Then, cycle check(s2 ) visits s3 and s1 and returns f alse, since there is nobackward edge leading to state s2 . Thus, cycle check(s2 ) yields T = {s2 , s3 , s1 } (andV = ε). Now the outer DFS proceeds and visits s3 and s1 . It calls cycle check(s1 ) whichfails to find the cycle s1 s3 s1 . Note that cycle check(s1 ) immediately halts and returnsf alse since s1 ∈ T = {s2 , s3 , s1 }.

Thus, the nested depth-first search would return thewrong answer ”yes”.6For a recursive formulation of the outer depth-first search, this is the moment where the depth-firstsearch call for s terminates.214Regular PropertiesTheorem 4.69.Correctness of the Nested DFSLet TS be a finite transition system over AP without terminal states, Φ a propositionalformula over AP, and Ppers the persistence property ”eventually forever Φ”.

Then:Algorithm 8 returns the answer ”no” if and only if TS |= Ppers .Proof:⇒: This follows directly from the fact that the answer “false” is only obtained when aninitial path fragment of the form s0 . . . s . . . s has been encountered for some s0 ∈ I ands |= Φ. But then, TS |= Ppers .⇐: To establish this direction, we first prove that the following condition holds:(*) On invoking cycle check(s), there is no cycle s0 s1 . . . sk in TS such that:{ s0 , s1 , . . .

, sk } ∩ T = ∅and s ∈ { s0 , . . . , sk }.So, on invoking cycle check(s), there is no cycle containing s and a state in T . Statement(*) ensures that in the inner DFS, all already visited states in T —the states that werevisited during an earlier cycle detection—can be safely ignored during the next cyclesearch. In other words, if s belongs to a cycle then cycle check(s) has to find one such cycle.We prove the statement (*) by contradiction. Consider the invocation cycle check(s).Assume there exists a cycle s0 s1 .

. . sk such thats0 = sk = sand s |= Φand { s0 , s1 , . . . , sk } ∩ T = ∅.Without loss of generality we assume that s is the first state for which this condition holdson invoking cycle check(s). More precisely, we assume:s) has been invoked prior to cy(+) For all states s with s |= Φ where cycle check(cle check(s), there is no cycle containing s and a state in T , on invoking cycle check(s).Let t ∈ { s0 , . .

. , sk } ∩ T , i.e., t is a state on a cycle with state s. Since t ∈ T on theinvocation cycle check(s), there must be a state, u say, for which cycle check(·) has beeninvoked earlier and during this search t has been encountered (and added to T ). Thus, wehave u |= Φ and the following conditions (4.1) and (4.2):cycle check(u) was invoked prior to cycle check(s)(4.1)Model-Checking ω-Regular Properties215as a result of cycle check(u), t was visited and added to T(4.2)Obviously, from (4.2), it follows that state t is reachable from u.

As the states s and t areon a cycle, and t is reachable from u, we have that s is reachable from u. This situationis sketched in the following figure:s¬Φu¬Φt ∈ RinΦNow consider the outer depth-first search, i.e., reachable cycle(·), and discuss the followingcases 1 and 2:1. u has been visited prior to s in the outer DFS, i.e., s has been pushed on stack Uafter u.Since s is reachable from u, state s is visited during the expansion of u in the outerDFS and taken from stack U before u.

Hence, cycle check(s) is invoked prior tocycle check(u) which contradicts (4.1).2. u has been visited after s in the outer DFS, i.e., s has been pushed on stack U beforeu.By (4.1), s is still in stack U when cycle check(u) is invoked. This yields that u isreachable from s.

But as s is reachable from u, this means that s and u are on acycle. This cycle or another cycle with state u would have been encountered during cycle check(u) because of (+) and Algorithm 8 would have terminated withoutinvoking cycle check(s).It remains to discuss the complexity of the nested depth-first search algorithm. Since Tis increasing during the execution of the nested depth-first search (i.e., we insert states inT , but never take them out) any state in TS is visited at most once in the inner depthfirst search, when ranging over all procedure calls of cycle check(·).

The same holds forthe outer depth-first search since it is roughly a standard depth-first search. Thus, eachreachable state s in TS is taken216Regular Properties• at most once7 as the top element of stack U in the outer depth-first search;• at most once as the top element of stack V in the inner depth-first search (whenranging over all calls of cycle check).In particular, this observation yields the termination of Algorithm 8. The cost caused bythe top-element s for the body of the repeat loop in cycle check (inner depth-first search)and in reachable cycle (outer depth-first search) is O(|Post(s )|). Thus, the worst-casetime complexity of Algorithm 8 is linear in the size of the reachable fragment of TS, buthas the chance to terminate earlier when a cycle has been found. In the following theoremwe also take into account that Φ might be a complex formula and evaluating the truthvalue of Φ for a given state (by means of its label) requires O(|Φ|) steps.Theorem 4.70.Time Complexity of Persistence CheckingThe worst-case time complexity of Algorithm 8 is in O((N +M ) + N ·| Φ |) where N is thenumber of reachable states, and M the number of transitions between the reachable states.The space complexity is bounded above by O(|S| + | → |) where S is the state space ofTS and | → | the number of transitions in TS.

This is an adequate bound if we assumea representation of TS by adjacency lists. However, in the context of model checkingthe starting point is typically not an explicit representation of the composite transitionsystem, but a syntactic description of the concurrent processes, e.g., by high-level modelinglanguages with a program graph or channel system semantics. Such syntactic descriptionsare typically much smaller than the resulting transition system.

Характеристики

Список файлов книги