For applying the sweep-line method, a state space reduction technique, it is necessary to provide an automatic calculation of a progress measure. In [1], such a calculation has been proposed for Petri nets. The approach presented there may lead to suboptimal results, therefore the author suggested possible optimizations. In this paper, we check whether the proposed optimization goals indeed lead to an improved performance of the sweep-line method.
The sweep-line method is a state space reduction technique that can be used to verify
safety properties (e.g. the existence of deadlocks or reachability of a given state) of the
modelled system. The main idea of this technique is that during state space exploration,
there is some kind of “progress”: States that have been processed and will never be
visited again are no longer needed for further exploration. To quantify this progress,
a progress measure is needed that assigns a progress value to every state. To use the
sweep-line method fully automatically, the progress measure must be calculated
automatically, too. Such an automatic calculation of the progress measure for applying the
sweep-line method to state spaces of Petri nets has been proposed in [
There exist two forms of the sweep-line method: the basic form [
As we stated above, the progress measure assigns a progress value p(s) to every state s of the state space. For the basic sweep-line method, the progress measure is monotonous, i.e., for all states s; s0 and transitions t, s !t s0 implies p(s) p(s0). The state space is explored such that states with low progress values are visited first. Therefore, we can divide the set of states into three classes: (1) states that have been explored including all their successors, (2) states that have been explored, but which’s successors have not been completely explored (we also call this class front) and (3) states that have not been explored yet. As the progress measure is monotonous, all states of class (1) can be deleted; only the states of the front must be stored.
For the generalized sweep-line method, the progress measure does not have to be monotonous, i.e., for an edge s !t s0 of the state space it may hold p(s) > p(s0). Such edges are called regress edges. Applying the basic method would now lead to the following problem: Let s !t s0 be a regress edge with s in class (2) or (3) and s0 in class (1). Because all states of class (1) have been deleted, we have no information that we have explored s0 yet. The exploration would be continued from this state and s0 will eventually be explored again as an unknown state – the method would not terminate. That is why in the generalized sweep-line method target states of regress edges are marked as persistent and stored permanently in memory. In the current iteration (sweep) of the sweep-line method, successors of persistent states are not explored, and newly marked persistent states are initial states of the next sweep. Therefore, it is guaranteed that the method terminates and explores all states at least once.
It is obvious that a large number of persistent states increases memory consumption and can lead to a large number of sweeps.
The sweep-line method can be combined with stubborn sets, another state space
reduction method; the computation method for stubborn sets described in [
The progress measure required for the sweep-line method needs to be generated for each
system which’s state space should be explored. The automatic calculation of a progress
measure for Petri nets described in [
Using this approach for calculating a consistent progress measure, offset values must preserve the linear dependencies of all vectors D t.
with transitions T . An offset function o is linear dependency preserving if for all t 2 T , ft0; : : : ; tng T n ftg, l0; : : : ; ln 2 Q with D t = l0D t0 + + lnD tn it holds o(t) = l0o(t0) + + lno(tn).
The method for computing offset values suggested in [
The computation method for offset values described in Sect. 4 is suitable for the purpose of optimization, as for attaining any optimization goal, only one vector a 2 QjPj must be chosen properly to calculate the offset value o(t) = a D t for any transition t of a Petri net. As we already mentioned, we want to attain two optimization goals: First, the number of RTs should be minimized (as one could expect that this reduces the number of persistent states and thus the number of sweeps) and second, chains of RTs should be avoided (as such chains could lead to an unneccessary re-exploration of huge parts of the state space). In our approach described in the following, at first we will compute several sets of RTs which are as small as possible, and afterwards choose a set R which promises to avoid chains of RTs the most. Afterwards, we can calculate a vector a such that o(t) < 0 iff t 2 R. 5.1
For this subsection, let N = [P; T; F;W; s0] be a Petri net. Minimizing the number of RTs means that we want to compute as few negative offset values as possible for all transitions t 2 T . Furthermore, we decide that we do not want to assign the offset value o(t) = 0 to any transition t 2 T . Therefore, with regard to the computation method described in Sect. 4, for every transition t 2 T we set up the inequality a D t > 0. Thus, we obtain a system of linear inequalities which we call L .
Obviously, if L is feasible, we can calculate positive offset values for all transitions t 2 T . We may choose any vector a 2 QjPj from the set of feasible solutions described by L (which can be done by a Linear Programming solver) to obtain offset values without RTs. Of course, in this case we do not have to avoid chains of RTs as there are none.
If L is not feasible, things become more difficult. To minimize the number of RTs,
we are looking for a feasible subsystem of L containing as many inequalities as
possible. This almost equates to solving an instance of the Maximum Feasible Subsystem
Problem (MAXFS) [
As we are now able to generate multiple sets of RTs, in this section we want to develop a heuristic that should select the set which avoids chains of RTs the most. In contrast to the minimization of RTs which can be performed prior to state space exploration, chains of RTs are initially detected during state space exploration. As offset values are calculated prior to state space exploration, we have to think about how to optimize offset value calculation to avoid chains of RTs anyway. To attain this optimization goal, we introduce the enabling graph.
Definition 2 (Enabling Graph). Let N = [P; T; F;W; s0] be a Petri net. G = [V; E] is the enabling graph of N, where V = T , and (t; t0) 2 E iff 9 p 2 P : t 2 p ^ t0 2 p .
If there is an edge from t to t0 in the enabling graph, then firing t creates at least one token on a place p 2 t0. Therefore, firing t supports enabling t0. In our heuristic for avoiding chains of RTs, we use shortest paths within the enabling graph to decide whether a set of RTs is likely to avoid chains or not. Although this approach has some weaknesses (for example, it does not take account of concurrency of transitions and of the actual marking of the net), we consider it to be appropriate for avoiding chains of RTs prior to state space exploration. For a given Petri Net N = [P; T; F;W; s0] and its enabling graph G = [V; E], our heuristic for avoiding chains of RTs chooses a set R of RTs that satisfies the criteria described in the following. 1. Shortest paths from each t to each t0 with t; t0 2 R should be as long as possible. 2. Shortest paths from each transition t enabled in s0 to each t0 2 R should be as long as possible. 3. For each t 2 R and each p 2 t, it should hold p 2= t0 for as many t0 2 R n ftg and p 2 t00 for as many t00 2 T n R with D t00( p) < 0 as possible.
Criterion 1 aims at maximizing the number of explored states between any two regress transitions. Especially, t0 should not fire immediately after t has fired. Furthermore, in our implementation used for the case study in Sect. 6, we demand that the shortest path among all shortest paths between RTs should be preferably long. It is obvious that this criterion helps us to avoid chains of RTs.
Criterion 2 states that during the first sweep, as many transitions as possible should fire before a regress edge is explored. This does not avoid chains of RTs immediately, but it has the effect that a large part of the state space should be already explored in the first sweep.
Criterion 3 takes account of shared places. We want to avoid that a RT t shares a place p with another RT, because if the marking of p is sufficiently big, then these two transitions could fire one after another, which would exactly yield a chain of RTs. On the other hand, if t shares a place with a transition t0 that is not a RT and t0 consumes more tokens from p than it produces on this place, the firing of t0 may disable t. Therefore, such transitions should preferably be chosen as RTs.
In our heuristic, we weight these criteria and combine them to a function f that
assigns a value to every set of RTs (see [
In our case study, we checked whether the computation of progress values given in [
Table 1 shows a summary of our test results. The state space was too large to be computed completely by LoLA O for 6 nets with stubborn sets and for 10 nets without stubborn sets. In the table, these nets are not considered except for the columns complete and #RT.
From the results, we conclude that our optimization goals do not lead to an improved
performance of the sweep-line method in general. Moreover, as stated in [
As the computation of the offset values does not depend on stubborn sets, we obtain the same number of regress transitons for state space exploration with and without stubborn sets.
Although the results for the combination of the sweep-line method and stubborn sets look more promising than those obtained without stubborn sets, note that our optimization goals did not include special improvements for stubborn sets. Especially, computation of stubborn sets combined with the sweep-line method in LoLA depends on the offset values of all transitions; thus, one should not reason about these results without taking a closer look at LoLA. 7
The case study in Sect. 6 revealed that the optimization goals examined in Sect. 5 do not improve the performance of the sweep-line method in general. Different optimization goals must be found to achieve this aim.
For estimating the number of persistent states, it turns out that it would be important to know how often RTs are enabled during state space exploration and how many distinct target states they lead to. Furthermore, even offset values of transitions which are no RTs influence the peak value. It would be appropriate to provide an offset value calculation that exploits this fact. Finally, as mentioned above, when using LoLA, the implementation of stubborn sets should be taken into consideration when trying to optimize the sweep-line method.