5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 45
Текст из файла (страница 45)
How to check for such reachable cycles? A possibility is to computethe strongly connected components (SCCs, for short) in G(TS) – this can be done in aworst-case time complexity that is linear in the number of states and transitions – and tocheck whether one such SCC is reachable from an initial state, contains at least one edge,and, moreover, contains a ¬Φ-state.
If indeed such a SCC does exist, Ppers is refuted;otherwise the answer is affirmative.Although this SCC-based technique is optimal with respect to the asymptotic worst-casetime complexity, it is more complex and less adequate for an on-the-fly implementation.In that respect, pure cycle-check algorithms are more appropriate.
Therefore, in the sequelwe will detail the standard DFS-based cycle detection algorithm.Let us first recall how for a finite directed graph G and node v, it can be checked witha DFS-based approach whether v belongs to a cycle. For this, one may simply start adepth-first search in node v and check for any visited node w whether there is an edge fromw to v. If so, a cycle has been found: it starts in v and follows the path to node w givenby the current stack content and then takes the edge from w to v.
Vice versa, if no suchedge is found, then v does not belong to a cycle. To determine whether G has a cycle, asimilar technique can be exploited: we perform a depth-first search to visit all nodes in G.Moreover, on investigating the edge from w to v it is checked whether v has already beenvisited and whether v is still on the DFS stack. If so, then a so-called backward edge hasbeen found which closes a cycle.
Otherwise, if no backward edge has been found duringthe DFS in G then G is acyclic. (A detailed description of this DFS-based cycle detectiontechnique can be found in textbooks on algorithms and data structures, e.g., [100].)We now DFS-based cycle checks (by searching for backward edges) for persistence checking.The naive approach works in two phases, as illustrated in Algorithm 6:1. In the first step, all states satisfying ¬Φ that are reachable from some initial stateare determined. This is performed by a standard depth-first search.208Regular Properties2.
In the second step, for each reachable ¬Φ-state s, it is checked whether it belongs toa cycle. This algorithm (called cycle check, see Algorithm 7) relies on the techniquesketched above: we start a depth-first search in s (with initially empty DFS stackV and initially empty set T of visited states) and check for all states reachable froms whether there is an outgoing backward edge leading to s.This yields an algorithm for checking the validity of the persistence property with quadraticworst-case running time. More precisely, its time complexity is in O(N ·(|Φ| + N +M ))where N is the number of reachable states in TS and M the number of transitions betweenthese reachable states.
This can be seen as follows. Visiting all states that are reachablefrom some initial state takes O(N +M +N ·|Φ|) as a depth-first search over all states sufficesand in each reachable state the validity of Φ is checked (which is assumed to be linearin the size of Φ). In the worst case, all states refute Φ, and a depth-first search takesplace (procedure cycle check) for all these states.
This takes O(N ·(N +M )). Togetherthis yields O(N ·(|Φ| + N +M )).Several simple modifications of the suggested technique are possible to increase efficiency.For instance, cycle check(s ) can be invoked inside visit(s) immediately before or after s isinserted into R¬Φ , in which case the whole persistence checking algorithm can abort withthe answer ”no” if cycle check(s ) returns true. However, the quadratic worst-case runningtime cannot be avoided if the cycle check algorithm for the ¬Φ-states relies on separatedepth-first searches. The problem is that certain fragments of TS might be reachablefrom different ¬Φ-states.
These fragments are (re-)explored in the depth-first searches(cycle check) invoked by several ¬Φ-states. To obtain linear running time, we aim at acycle detection algorithm that searches for backward edges leading to one of the ¬Φ-statesand ensures that any state is visited at most once in the depth-first searches for the cycledetection. This will be explained in the following subsection.A Nested Depth-First Search Algorithm The rough idea of the linear-time cycle detection-based persistence checking algorithm is to perform two depth-first searches(DFSs) in TS in an interleaved way. The first (outer) depth-first search serves to encounterall reachable ¬Φ-states.
The second (inner) depth-first search seeks backward edges leading to a ¬Φ-state. The inner depth-first search is nested in the outer one in the followingsense: whenever a ¬Φ-state s has been fully expanded by the outer depth-first search,then the inner depth-first search continues with state s and visits all states s that arereachable from s and that have not yet been visited in the inner depth-first search before.If no backward edge has been found when treating s in the inner DFS, then the outer DFScontinues until the next ¬Φ-state t has been fully expanded, in which case the inner DFSproceeds with t.Model-Checking ω-Regular Properties209Algorithm 6 Naive persistence checkingInput: finite transition system TS without terminal states, and proposition ΦOutput: ”yes” if TS |= ”eventually forever Φ”, otherwise ”no”.set of states R := ∅; R¬Φ := ∅;stack of states U := ε;set of states T := ∅;stack of states V := ε;for all s ∈ I \ R do visit(s); odfor all s ∈ R¬Φ doT := ∅; V := ε;if cycle check(s) then return ”no”odreturn ”yes”procedure visit (state s)push(s, U );R := R ∪ { s };repeats := top(U );if Post(s ) ⊆ R thenpop(U );if s |= Φ then R¬Φ := R¬Φ ∪ { s }; fielselet s ∈ Post(s ) \ Rpush(s , U );R := R ∪ { s };fiuntil (U = ε)endproc(* set of reachable states resp.
¬Φ-states(* DFS stack for first DFS, initial empty(* set of visited states for the cycle check(* DFS stack for the cycle check*)*)*)*)(* a DFS for each unvisited initial state *)(* initialize set T and stack V *)(* s belongs to a cycle *)(* none of the ¬Φ-states belongs to a cycle *)(* push s on the stack *)(* mark s as reachable *)(* state s is a new reachable state *)210Regular PropertiesAlgorithm 7 Cycle detectionInput: finite transition system TS and state s in TS with s |= ΦOutput: true if s lies on a cycle in TS, otherwise false(* T organizes the set of states that have been visited, V serves as DFS stack.(* In the standard approach to check whether there is a backward edge to s,(* T and V are initially empty.procedure boolean cycle check(state s)boolean cycle found := false;push(s, V );T := T ∪ { s };repeats := top(V );if s ∈ Post(s ) thencycle found := true;push(s, V );elseif Post(s ) \ T = ∅ thenlet s ∈ Post(s ) \ T ;push(s , V );T := T ∪ { s };elsepop(V );fifiuntil ((V = ε) ∨ cycle found)return cycle foundendproc*)*)*)(* no cycle found yet *)(* push s on the stack *)(* take top element of V *)(* if s ∈ P ost(s ), a cycle is found *)(* push s on the stack *)(* push an unvisited successor of s *)(* and mark it as reachable *)(* unsuccessful cycle search for s *)Model-Checking ω-Regular Properties211Algorithm 8 Persistence checking by nested depth-first searchInput: transition system TS without terminal states, and proposition ΦOutput: ”yes” if TS |= ”eventually forever Φ”, otherwise ”no” plus counterexampleset of states R := ∅;stack of states U := ε;set of states T := ∅;stack of states V := ε;boolean cycle found := false;while (I \ R = ∅ ∧ ¬cycle found) dolet s ∈ I \ R;reachable cycle(s);odif ¬cycle found thenreturn (”yes”)elsereturn (”no”, reverse(V.U ))fiprocedure reachable cycle (state s)push(s, U );R := R ∪ { s };repeats := top(U );if Post(s ) \ R = ∅ thenlet s ∈ Post(s ) \ R;push(s , U );R := R ∪ { s };elsepop(U );if s |= Φ thencycle found := cycle check(s );fifiuntil ((U = ε) ∨ cycle found)endproc(* set of visited states in the outer(* stack for the outer(* set of visited states in the inner(* stack for the innerDFSDFSDFSDFS*)*)*)*)(* explore the reachable *)(* fragment with outer DFS *)(* TS |= ”eventually forever Φ” *)(* stack contents yield a counterexample *)(* push s on the stack *)(* push the unvisited successor of s *)(* and mark it reachable *)(* outer DFS finished for s *)(* proceed with the inner *)(* DFS in state s *)(* stop when stack for the outer *)(* DFS is empty or cycle found *)212Regular PropertiesThis algorithm is called nested depth-first search.
Algorithm 8 shows the pseudocodefor the outer depth-first search (called reachable cycle) which invokes the inner depth-firstsearch (cycle check, cf. Algorithm 7 on page 210). Later we will explain that it is importantthat cycle check(s) is called immediately after the outer depth-first search has visited allsuccessors of s.
The major difference from the naive approach is that cycle check(s)reuses the information of previous calls of cycle check(·) and ignores all states in T . Whencycle check(s) is invoked then T consists of all states that have been visited in the innerDFS before, i.e., during the execution of cycle check(u) called prior to cycle check(s).An interesting aspect of this nested depth-first strategy is that once a cycle is determinedcontaining a ¬Φ-state s, then a path to s can be computed easily: stack U for the outerDFS contains a path fragment from the initial state s0 ∈ I to s (in reversed order),while stack V for the inner DFS — as maintained by the procedure cycle check(·) —contains a cycle from state s to s (in reversed order). Concatenating these path fragmentsthus provides an error indication in the same vein as described before in the proof ofTheorem 4.65 on page 205.Example 4.67.Running the Nested DFS AlgorithmConsider the transition system depicted in Figure 4.25 and assume that s0 |= Φ, s3 |= Φ,whereas s1 |= Φ and s2 |= Φ.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
