Stubborn Set Intuition Explained

Abstract

This study focuses on the differences between stubborn sets and other partial order methods. First a major problem with step graphs is pointed out with an example. Then the deadlock-preserving stubborn set method is compared to the deadlock-preserving ample set and persistent set methods. Next, conditions are discussed whose purpose is to ensure that the reduced state space preserves the ordering of visible transitions, that is, transitions that may change the truth values of the propositions that the formula under verification has been built from. Finally solutions to the ignoring problem are analysed both when the purpose is to preserve only safety properties and when also liveness properties are of interest.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Ample sets [1, 10, 11], persistent sets [5, 6], and stubborn sets [15, 19] are methods for constructing reduced state spaces. In each found state, they compute a subset of transitions and only fire the enabled transitions in it to find more states. We call this subset an aps set.

The choice of aps sets depends on the properties under verification. Attempts to obtain good reduction for various classes of properties have led to the development of many different methods. Even when addressing the same class of properties, stubborn set methods often differ from other aps set methods. The present study focuses on these differences. The goal is to explain the intuition behind the choices made in stubborn set methods.

To get a concrete starting point, Sect. 2 presents a simple (and non-optimal) definition of stubborn sets for Petri nets that suffices for preserving all reachable deadlocks. The section also introduces the $\leadsto _M$-relation that underlies many algorithms for computing stubborn sets, and sketches one good algorithm. This relation and algorithm are one of the major differences between stubborn set and other aps set methods. The section also contains a small new result, namely an example showing that always choosing a singleton stubborn set if one is available does not necessarily guarantee best reduction results.

With Petri nets, it might seem natural to fire sets of transitions called steps, instead of individual transitions. Section 3 discusses why this is not necessarily a good idea. Ample and persistent sets are compared to stubborn sets in Sect. 4, in the context of deadlock-preservation. Furthermore, the difference between weak and strong stubborn sets is explained. The verification of many properties relies on a distinction between visible and invisible transitions. This distinction is introduced in Sect. 5. Its ample and stubborn set versions are compared to each other.

Because of the so-called ignoring problem, deadlock-preserving aps set methods fail to preserve most other classes of properties. For many classes, it suffices to solve the ignoring problem in the terminal strong components of the reduced state space. To this end, two slightly different methods have been suggested. Section 6 first introduces them, and then presents and proves correct a novel idea that largely combines their best features.

The above-mentioned solutions to the ignoring problem do not suffice for so-called liveness properties. Section 7 discusses the stubborn set and ample set methods for liveness. A drawback in the most widely known implementation of the methods is pointed out. Section 8 discusses problems related to fairness. Aps set methods have never been able to appropriately deal with mainstream fairness assumptions. In this section we present some examples that illustrate the difficulties. They are from [22]. Section 9 concludes the study.

2 The Basic Idea of Stubborn Sets

In this section we illustrate the basic idea of stubborn sets and of one good algorithm for computing them.

We use T to denote the set of (all) transitions of a Petri net. Let M be a marking. The set of enabled transitions in M is denoted with $\mathsf {en}(M)$ and defined as $\{ t \in T \mid M \mathrel {[t\rangle } \}$. A deadlock is a marking that has no enabled transitions.

In Fig. 1 left, only firing $t_1$ in the initial marking leads to the loss of the deadlock that is reached by firing $t_3 t_2 t_3 t_1$. To find a subset of transitions that cannot lead to such losses, we first define a marking-dependent relation $\leadsto _M$ between Petri net transitions.

 

PNd.:

If $\lnot (M \mathrel {[t\rangle })$, then choose $p_t \in \bullet t$ such that $M(p_t) < W(p_t,t)$ and declare $t \leadsto _M t'$ for every $t' \in \bullet p_t$ except t itself. (If many such $p_t$ are available, only one is chosen. The correctness of what follows does not depend on the choice.)

PNe.:

If $M \mathrel {[t\rangle }$, then declare $t \leadsto _M t'$ for every $t' \in (\bullet t)\bullet$ except t itself.

 

Fig. 1.

A marked Petri net and its $\leadsto _M$-graph, with $p_{t_5} = p_5$.

On the right in Fig. 1, enabled transitions are shown with double circles, disabled transitions with single circles, and the $\leadsto _M$-relation with arrows. For instance, $t_4$ is enabled, $\bullet t_4 = \{p_4, p_6\}$, and $\{p_4, p_6\}\bullet = \{t_3, t_4, t_5\}$, so PNe declares $t_4 \leadsto _M t_3$ and $t_4 \leadsto _M t_5$. Regarding $t_5$, PNd allows choosing $p_{t_5} = p_3$ or $p_{t_5} = p_5$. In the example $p_5$ was chosen, spanning the arrow $t_5 \leadsto _M t_6$.

Consider any $\leadsto _M$ -closed set $T_M$ of transitions, that is, for every t and $t'$, if $t \in T_M$ and $t \leadsto _M t'$, then also $t' \in T_M$. Assume that $t \in T_M$, $t_i \notin T_M$ for $1 \le i \le n$, and $M \mathrel {[t_1 \cdots t_n\rangle } M'$. PNd guarantees that if t is disabled in M, then t is disabled also in $M'$. This is because every transition that may increase the number of tokens in $p_t$ is in $T_M$. PNe guarantees that if t is enabled in M, then there is $M''$ such that $M' \mathrel {[t\rangle } M''$ and $M \mathrel {[t t_1 \cdots t_n\rangle } M''$. This is because t does not consume tokens from the same places as $t_1 \cdots t_n$.

Let $\hat{M}$ be the initial marking of a Petri net. Let $\mathsf {stubb}(M)$ be a function that, for any marking M that is not a deadlock, returns an $\leadsto _M$-closed set of transitions that contains at least one enabled transition. This set is called stubborn. If M is a deadlock, then it does not matter what $\mathsf {stubb}(M)$ returns. Let the reduced state space be the triple $(S_\mathsf {r}, \varDelta _\mathsf {r}, \hat{M})$, where $S_\mathsf {r}$ and $\varDelta _\mathsf {r}$ are the smallest sets such that (1) $\hat{M} \in S_\mathsf {r}$ and (2) if $M \in S_\mathsf {r}$, $t \in \mathsf {stubb}(M)$, and $M \mathrel {[t\rangle } M'$, then $M' \in S_\mathsf {r}$ and $(M, t, M') \in \varDelta _\mathsf {r}$. It can be constructed like the ordinary state space, except that only the enabled transitions in $\mathsf {stubb}(M)$ are fired in each constructed marking M. We have the following theorem.

Theorem 1

The set $S_\mathsf {r}$ contains all deadlocks that are reachable from $\hat{M}$.

Proof

The proof proceeds by induction. Let $M \in S_\mathsf {r}$ and $M \mathrel {[t_1 \cdots t_n\rangle } M_\mathsf {d}$, where $M_\mathsf {d}$ is a deadlock. If $n=0$, then $M_\mathsf {d} = M \in S_\mathsf {r}$.

If $n > 0$, then $M \mathrel {[t_1\rangle }$. So M is not a deadlock and $\mathsf {stubb}(M)$ contains an enabled transition t. If none of $t_i$ is in $\mathsf {stubb}(M)$, then PNe implies that t is enabled at $M_\mathsf {d}$, contradicting the assumption that $M_\mathsf {d}$ is a deadlock. So there is i such that $t_i \in \mathsf {stubb}(M)$ but $t_j \notin \mathsf {stubb}(M)$ for $1 \le j < i$. Let $M_{i-1}$ and $M_i$ be the markings such that $M \mathrel {[t_1 \cdots t_{i-1}\rangle } M_{i-1} \mathrel {[t_i\rangle } M_i\mathrel {[t_{i+1} \cdots t_n\rangle } M_\mathsf {d}$. PNd implies that $t_i \in \mathsf {en}(M)$, because otherwise $t_i$ would be disabled in $M_{i-1}$. So PNe implies $M \mathrel {[t_i t_1 \cdots t_{i-1}\rangle } M_i \mathrel {[t_{i+1} \cdots t_n\rangle } M_\mathsf {d}$. Let $M'$ be the marking such that $M \mathrel {[t_i\rangle } M'$. Then $M' \in S_\mathsf {r}$ and there is the path $M' \mathrel {[t_1 \cdots t_{i-1} t_{i+1} \cdots t_n\rangle } M_\mathsf {d}$ of length $n-1$ from $M'$ to $M_\mathsf {d}$. By induction, $M_\mathsf {d} \in S_\mathsf {r}$.    $\square$

The next question is how to compute stubborn sets. Clearly only the enabled transitions in $\mathsf {stubb}(M)$ affect the reduced state space. Therefore, we define $T_1 \sqsubseteq _M T_2$ if and only if $T_1 \cap \mathsf {en}(M) \subseteq T_2 \cap \mathsf {en}(M)$. If $\mathsf {stubb}_1(M) \sqsubseteq _M \mathsf {stubb}_2(M)$ for every reachable marking M, then $\mathsf {stubb}_1$ yields a smaller or the same reduced state space as $\mathsf {stubb}_2$. So we would like to use $\sqsubseteq _M$-minimal stubborn sets.

Each $\leadsto _M$-relation spans a directed graph $(T, \text {``}{\leadsto _M}\text {''})$ as illustrated in Fig. 1 right. We call it the $\leadsto _M$ -graph. Let C be a strong component of the $\leadsto _M$-graph such that it contains an enabled transition, but no other strong component that is reachable from C contains enabled transitions. In Fig. 1, $C = \{t_3, t_4\}$ is such a strong component. Let $C'$ be the set of all transitions that are reachable from C. In Fig. 1, $C' = \{t_3, t_4, t_5, t_6\}$. Then $C'$ is an $\sqsubseteq _M$-minimal $\leadsto _M$-closed set that contains an enabled transition. That is, we can choose $\mathsf {stubb}(M) = C'$.

A fast algorithm that is based on this idea was presented in [15, 19, 26], among others. It uses Tarjan’s strong component algorithm [14] (see [3] for an improved version). It has been implemented in the ASSET tool [21] (although not for Petri nets). Its running time is linear in the size of the part of the $\leadsto _M$-graph that it investigates. For instance, if it happens to start at $t_2$ in Fig. 1, then it does not investigate $t_1$ and its output arrow. Although in this example the resulting savings are small, they are often significant.

The algorithm performs one or more depth-first searches in the $\leadsto _M$-graph, until a search finds an enabled transition or all transitions have been tried. The description above leaves open the order in which transitions are used as the starting points of the searches. The same holds on the order in which the output arrows of each transition are investigated. For instance, when in $t_4$ in Fig. 1, the algorithm may follow the arrow $t_4 \leadsto t_5$ before or after the arrow $t_4 \leadsto t_3$. Therefore, the result of the algorithm may depend on implementation details. Furthermore, it may also depend on the choice of $p_t$ if there are more than one alternatives. This is why we sometimes say that the method may produce some result, instead of saying that it does produce it.

The conditions PNd and PNe are not the best possible. For instance, $t \leadsto _M t'$ need not be declared in PNd, if $W(p_t, t') \ge W(t', p_t)$. Extreme optimization of the $\leadsto _M$-relation yields very complicated conditions, as can be seen in [15, 19]. A similar claim holds also with formalisms other than Petri nets. For this reason, and also to make the theory less dependent on the formalism used for modelling systems, aps set methods are usually developed in terms of more abstract conditions than PNd and PNe. We will do so in Sect. 4.

To analyse more properties than just deadlocks, additional conditions on the choice of stubborn sets are needed. Many of them will be discussed in Sects. 5, 6, and 7.

Until the end of Sect. 5 it will be obvious that if $\mathsf {stubb}_1(M) \sqsubseteq _M \mathsf {stubb}_2(M)$, then $\mathsf {stubb}_1(M)$ never yields worse but may yield better reduction results than $\mathsf {stubb}_2(M)$. In Sects. 6 and 7, the choices of $\mathsf {stubb}(M)$ with different M may interfere with each other, making the issue less trivial.

Even in the present section, it is not obvious which one to choose when $\mathsf {stubb}_1(M) \not \sqsubseteq _M \mathsf {stubb}_2(M)$ and $\mathsf {stubb}_2(M) \not \sqsubseteq _M \mathsf {stubb}_1(M)$. It was pointed out already in [16] that choosing the smallest number of enabled transitions does not necessarily guarantee best reduction results. In the remainder of this section we demonstrate that always favouring a set with precisely one enabled transition does not guarantee a minimal result. This strengthened observation is new.

A Petri net is 1-safe if and only if no place contains more than one token in any reachable marking. For simplicity, we express a marking of a 1-safe Petri net by listing the marked places within $\{$ and $\}$.

Fig. 2.

A stubborn set with one enabled transition is not always the best choice.

Consider the 1-safe Petri net in Fig. 2. Initially the only possibility is to fire $t_1$ and $t_2$, yielding $\{2,8\}$ and $\{3,8\}$. In $\{2,8\}$, both $\{t_3, t_4\}$ and $\{t_9\}$ are stubborn. In $\{3,8\}$, both $\{t_5, t_6\}$ and $\{t_9\}$ are stubborn. We now show that $\{t_3, t_4\}$ and $\{t_5, t_6\}$ yield better reduction than $\{t_9\}$.

If $\{t_3, t_4\}$ is chosen in $\{2,8\}$ or $\{t_5, t_6\}$ is chosen in $\{3,8\}$, then $\{4,8\}$ and $\{5,8\}$ are obtained. From them, $\{t_7\}$ and $\{t_8\}$ yield $\{6,8\}$, from which $\{t_9\}$ leads to $\{6,9\}$ which is a deadlock. Altogether seven markings and nine edges are constructed.

If $\{t_9\}$ is chosen in $\{2,8\}$ and $\{3,8\}$, then $\{2,9\}$ and $\{3,9\}$ are obtained. Then $\{t_3, t_4\}$ or $\{t_5, t_6\}$ yields $\{4,9\}$ and $\{5,9\}$, from which $\{t_7\}$ and $\{t_8\}$ produce $\{6,9\}$. Altogether eight markings and ten edges are constructed.

3 Why Not Steps?

Before comparing aps set methods to each other, in this section we compare them to step graphs. For simplicity, we restrict ourselves to executions that lead to deadlocks. That is, the goal is to find all reachable deadlocks and for each of them at least one path that leads to it.

A step is any nonempty subset $\{t_1, \ldots , t_n\}$ of Petri net transitions. It is enabled at M if and only if $M(p) \ge \sum _{i=1}^n W(p,t_i)$ for every place p. Then there is $M'$ such that $M \mathrel {[\pi \rangle } M'$ for every permutation $\pi$ of $t_1 \cdots t_n$. The idea of a step graph is to fire steps instead of individual transitions. Unlike the traditional state space, the order of firing of the transitions within the step is not represented, and intermediate markings between the firings of two successive transitions in $\pi$ are not constructed. This is expected to yield a memory-efficient representation of the behaviour of the Petri net.

To maximize the savings, the steps should be as big as possible. Unfortunately, the following example shows that only firing maximal steps is not correct. By firing $t_3 t_2 t_3 t_1$ in Fig. 1, a deadlock is reached where $M(p_2) = 3$. The maximal steps in the initial marking are $\{t_1, t_3\}$ and $\{t_1, t_4\}$. If only they are fired in the initial marking, no deadlock with $M(p_2) > 2$ is reached.

This problem can be fixed by also firing a sufficient collection of non-maximal steps. If $\{t_1, t_3\}$, $\{t_1, t_4\}$, $\{t_3\}$, and $\{t_4\}$ are fired in the initial marking of our example, then no deadlock is lost although the marking M that satisfies $\hat{M} \mathrel {[t_1\rangle } M$ is not constructed. However, another problem may arise even when it suffices to fire only maximal steps. We will now discuss it.

Fig. 3.

An example of firing steps vs. aps sets.

Consider the Petri net that consists of the black places, transitions, and arcs in Fig. 3 left. It models a system of n concurrent processes. It has $n! 2^n$ different executions, yielding a state space with $3^n$ markings and $2n3^{n-1}$ edges. Its initial marking has $2^n$ different steps of size n, consisting of one transition from each process. They yield a step graph with $2^n+1$ markings and $2^n$ edges.

Any reasonable implementation of any aps set method investigates one process at a time in this example. That is, the implementation picks some i such that $M(p_{i,1}) = 1$, and chooses $\mathsf {aps}(M) = \{t_{i,1}, t_{i,2}\}$. If there is no such i, then $\mathsf {aps}(M) = \emptyset$. This yields $1 + 2 + 4 + 8 + \ldots + 2^n = 2^{n+1} - 1$ markings and $2^{n+1} - 2$ edges.

We see that both methods yield a significant saving over the full state space, and step graphs yield approximately 50 % additional saving over aps sets. Step graphs construct strictly as few markings and edges as necessary in this example.

Assume now that the grey places, transitions, and arcs are added. The step graph now has $2^n + 2$ markings and $2^{n+1}$ edges.

Aps sets may yield many different results depending on what $\mathsf {aps}(M)$ returns for each M. Assume that the algorithm in Sect. 2 is used and transitions are tried as the starting points of depth-first searches in the order $t_{1,1}$, $t_{1,2}$, $t_{1,3}$, $t_{1,4}$, $t_{2,1}$, $t_{2,2}$, .... Then $\mathsf {aps}(M)$ is either $\{t_{i,1}, t_{i,2}\}$, $\{t_{i,3}\}$, or $\{ t_{i,4}\}$, where i is the smallest index such that either $M(p_{i,1}) = 1$, $M(p_{i,2}) = 1$, or $M(p_{i,3}) = 1$. (If there is no such i, then $\mathsf {aps}(M) = \emptyset$.) In that case, the reduced state space shown at right in Fig. 3 is obtained. In $M_{i,j}$, $M(p_{k,4}) = 1$ for $1 \le k < i$, $M(p_{i,j}) = 1$, $M(p_{k,1}) = 1$ for $i < k \le n$, and the remaining places are empty. That is, only $3n + 1$ markings and 4n edges are constructed. This is tremendously better than the result with step graphs.

There is no guarantee that aps sets yield this nice result. If transitions are tried in the order $t_{1,1}$, $t_{2,1}$, ..., $t_{n,1}$, $t_{1,2}$, $t_{2,2}$, ..., then $3 \cdot 2^n-2$ markings and $2^{n+2} - 4$ edges are obtained.

The point is that in this example, it is guaranteed that step graphs do not yield a good result, while aps sets may yield a very good result.

Another issue worth noticing in this example is that when aps sets failed to reduce well, they only generated approximately three times the markings and twice the edges that the step graphs generated. This is because where steps avoided many intermediate markings, aps sets investigated only one path through them and thus only generated a small number of them. For this reason, even when aps sets lose to step graphs, they tend not to lose much.

This example brings forward a problem with comparing different methods. Most of the methods in this research field are nondeterministic in the same sense as the algorithm in Sect. 2. Therefore, the results of a verification experiment may depend on, for instance, the order in which transitions are listed in the input of a tool. Above, the order $t_{1,1}$, $t_{2,1}$, ... gave dramatically worse results than the order $t_{1,1}$, $t_{1,2}$, .... When comparing verification methods or tools, it might be a good idea to repeat experiments with transitions in some other order.

4 Deadlocks with Ample vs. Persistent vs. Stubborn Sets

In this section we relate the ample set, persistent set, strong stubborn set, and weak stubborn set methods to each other when the goal is to preserve all deadlocks. Details of each method vary in the literature. We use the variant of ample sets described in [1], persistent sets in [6], and stubborn sets in [19]. These versions of the methods are mature and widely used.

We will use familiar or obvious notation for states, transitions, and so forth. A set of states is typically denoted with S, a set of transitions with T, and an initial state with $\hat{s}$. Transitions refer to structural transitions such as Petri net transitions or atomic statements of a program. Transition t is deterministic, if and only if for every s, t, $s_1$, and $s_2$, $s \xrightarrow {t} s_1$ and $s \xrightarrow {t} s_2$ imply $s_1 = s_2$.

Ample, persistent, and stubborn set methods compute an aps set $\mathsf {aps}(s)$ in each state s that they encounter. They construct a reduced state space by only firing the enabled transitions in each $\mathsf {aps}(s)$. It is the triple $(S_\mathsf {r}, \varDelta _\mathsf {r}, \hat{s})$, where $S_\mathsf {r}$ and $\varDelta _\mathsf {r}$ are the smallest sets such that (1) $\hat{s} \in S_\mathsf {r}$ and (2) if $s \in S_\mathsf {r}$, $t \in \mathsf {aps}(s)$, and $s \xrightarrow {t} s'$, then $s' \in S_\mathsf {r}$ and $(s,t,s') \in \varDelta _\mathsf {r}$. The full state space $(S, \varDelta , \hat{s})$ is obtained by always choosing $\mathsf {aps}(s) = T$. Obviously $\hat{s} \in S_\mathsf {r}\subseteq S$ and $\varDelta _\mathsf {r}\subseteq \varDelta$.

The ample set method relies on the notion of independence between transitions. It is usually defined as any binary relation on transitions that has the following property:

 

Independence. :

If transitions $t_1$ and $t_2$ are independent of each other, $s \xrightarrow {t_1} s_1$, and $s \xrightarrow {t_2} s_2$, then there is $s'$ such that $s_1 \xrightarrow {t_2} s'$ and $s_2 \xrightarrow {t_1} s'$.

 

Independence is not defined as the largest relation with this property, because it may be difficult to find out whether the property holds for some pair of transitions. In such a situation, the pair may be declared as dependent. Doing so does not jeopardize the correctness of the reduced state space, but may increase its size. This issue is similar to the use of non-optimal $\leadsto _M$-relations in Sect. 2.

Obviously transitions that do not access any variable (or Petri net place) in common can be declared as independent. (Here also the program counter or local state of a process is treated as a variable.) Two transitions that both increment the value of a variable by 42 without testing its value in their enabling conditions can be declared as independent, if they do not access other variables in common. A similar claim holds if they both assign 63 to the variable. Reading from a fifo queue and writing to it can be declared as independent, as can two transitions that are never simultaneously enabled.

An ample set for deadlocks in state $s_0$ is any subset of transitions that are enabled at $s_0$ that satisfies the following two conditions:

 

C0. :

If $\mathsf {en}(s_0) \ne \emptyset$, then $\mathsf {ample}(s_0) \ne \emptyset$.

C1. :

If $s_0 \xrightarrow {t_1 \cdots t_n}$ and none of $t_1$, ..., $t_n$ is in $\mathsf {ample}(s_0)$, then each one of $t_1$, ..., $t_n$ is independent of all transitions in $\mathsf {ample}(s_0)$.

 

We show next that every deadlock of the full state space is present also in the reduced state space.

Theorem 2

Assume that transitions are deterministic, $s \in S_\mathsf {r}$, $s_\mathsf {d}$ is a deadlock, and $s \xrightarrow {t_1 \cdots t_n} s_\mathsf {d}$ in the full state space. If C0 and C1 are obeyed, then there is a permutation $t'_1 \cdots t'_n$ of $t_1 \cdots t_n$ such that $s \xrightarrow {t'_1 \cdots t'_n} s_\mathsf {d}$ in the reduced state space.

Proof

We only present the parts where the proof differs from the proof of Theorem 1. If $n > 0$, then $\mathsf {ample}(s)$ contains an enabled transition t by C0 and $\mathsf {ample}(s) \subseteq \mathsf {en}(s)$. If none of $t_1$, ..., $t_n$ is in $\mathsf {ample}(s)$, then $s_\mathsf {d} \xrightarrow {t}$ by C1, contradicting the assumption that $s_\mathsf {d}$ is a deadlock. So there is a smallest i such that $t_i \in \mathsf {ample}(s)$. Let $s_{i-1}$ and $s_i$ be the states such that $s \xrightarrow {t_1 \cdots t_{i-1}} s_{i-1} \xrightarrow {t_i} s_i$. Since $\mathsf {ample}(s) \subseteq \mathsf {en}(s)$, there is $s'$ such that $s \xrightarrow {t_i} s'$. By C1, applying independence $i-1$ times, there is $s'_i$ such that $s' \xrightarrow {t_1 \cdots t_{i-1}} s'_i$ and $s_{i-1} \xrightarrow {t_i} s'_i$. Because transitions are deterministic, $s'_i = s_i$. As a consequence, $s \xrightarrow {t_i} s' \xrightarrow {t_1 \cdots t_{i-1}} s_i \xrightarrow {t_{i+1} \cdots t_n} s_\mathsf {d}$.    $\square$

Strong stubborn sets are defined such that they may contain both enabled and disabled transitions. Deadlock-preserving strong stubborn sets satisfy the following three conditions. D0 is essentially the same as C0. D1 and D2 will be motivated and related to C1 after the definition.

 

D0. :

If $\mathsf {en}(s_0) \ne \emptyset$, then $\mathsf {stubb}(s_0) \cap \mathsf {en}(s_0) \ne \emptyset$.

D1. :

If $t \in \mathsf {stubb}(s_0)$, $t_i \notin \mathsf {stubb}(s_0)$ for $1 \le i \le n$, and $s_0 \xrightarrow {t_1 \cdots t_n t} s'_n$, then $s_0 \xrightarrow {t t_1 \cdots t_n} s'_n$.

D2. :

If $t \in \mathsf {stubb}(s_0)$, $t_i \notin \mathsf {stubb}(s_0)$ for $1 \le i \le n$, $s_0 \xrightarrow {t_1 \cdots t_n} s_n$, and $s_0 \xrightarrow {t}$, then $s_n \xrightarrow {t}$.

 

This formulation was suggested by Marko Rauhamaa [12]. The most important reason for its use is that D1 works well even if transitions are not necessarily deterministic. (For deadlocks, also D2 can be used as such.) This is important for applying stubborn sets to process algebras, please see, e.g., [18, 23, 26]. In the proof of Theorem 2, the assumption that transitions are deterministic was explicitly used. Already the definition of independence relies on determinism. This issue makes ample and persistent set theories difficult to apply to process algebras.

Second, D1 can be used as such and D2 with a small change in the definition of weak stubborn sets towards the end of this section.

Third, D1 and D2 are slightly easier to use in proofs than C1. Let $s = s_0 \xrightarrow {t_1} s_1 \xrightarrow {t_2} \cdots \xrightarrow {t_n} s_n = s_\mathsf {d}$. D0 and D2 yield an i such that $t_i \in \mathsf {stubb}(s)$ and $t_j \notin \mathsf {stubb}(s)$ for $1 \le j < i$. Then the existence of $s'$ such that $s \xrightarrow {t_i} s' \xrightarrow {t_1 \cdots t_{i-1}} s_i$ is immediate by D1. This last piece of reasoning is repeated frequently in stubborn set theory, so it is handy that D1 gives it as a ready-made step. We have proven the following generalization of Theorem 2.

Theorem 3

Theorem 2 remains valid, if D0, D1, and D2 replace C0 and C1. Then transitions need not be deterministic.

This is a generalization, because it applies to also nondeterministic transitions, and because, as will be seen in Theorem 5, in the case of deterministic transitions C0 and C1 imply D0, D1, and D2.

In the case of deterministic transitions, D1 and D2 have the following equivalent formulation:

 

Dd. :

If $t \in \mathsf {stubb}(s_0)$, $\lnot (s_0 \xrightarrow {t})$, $t_i \notin \mathsf {stubb}(s_0)$ for $1 \le i \le n$, and $s_0 \xrightarrow {t_1 \cdots t_n} s_n$, then $\lnot (s_n \xrightarrow {t})$.

De. :

If $t \in \mathsf {stubb}(s_0)$, $s_0 \xrightarrow {t} s'_0$, $t_i \notin \mathsf {stubb}(s_0)$ for $1 \le i \le n$, and $s_0 \xrightarrow {t_1 \cdots t_n} s_n$, then there is $s'_n$ such that $s_n \xrightarrow {t} s'_n$ and $s'_0 \xrightarrow {t_1 \cdots t_n} s'_n$.

 

Dd says that disabled transitions in the stubborn set remain disabled, while outside transitions occur. De says that enabled transitions in the stubborn set commute with sequences of outside transitions. It is immediately obvious that PNd and PNe imply Dd and De. Let us show that for deterministic transitions, this formulation indeed is equivalent to D1 and D2.

Theorem 4

If transitions are deterministic, then D1 $\wedge$ D2 is equivalent to Dd $\wedge$ De.

Proof

Assume first that D1 and D2 hold. Then Dd follows immediately from D1. If $s_0 \xrightarrow {t} s'_0$ and $s_0 \xrightarrow {t_1 \cdots t_n} s_n$, then D2 yields an $s'_n$ such that $s_n \xrightarrow {t} s'_n$, after which D1 yields an $s''_0$ such that $s_0 \xrightarrow {t} s''_0 \xrightarrow {t_1 \cdots t_n} s'_n$. Because transitions are deterministic, $s''_0 = s'_0$, so De is obtained.

Assume now that Dd and De hold. Then D2 follows immediately from De. If $s_0 \xrightarrow {t_1 \cdots t_n} s_n \xrightarrow {t} s'_n$, then Dd yields an $s'_0$ such that $s_0 \xrightarrow {t} s'_0$, after which De yields an $s''_n$ such that $s'_0 \xrightarrow {t_1 \cdots t_n} s''_n$ and $s_n \xrightarrow {t} s''_n$. Because transitions are deterministic, $s''_n = s'_n$, so D1 is obtained.    $\square$

Similarly to the $\leadsto _M$-relation in Sect. 2, $\leadsto _s$-relations can be defined for Petri nets and other formalisms such that they guarantee D1 and D2. Please see e.g., [19, 24, 26] for more information. This means that the stubborn set construction algorithm in Sect. 2 can be applied to many formalisms. Indeed, its implementation in ASSET is unaware of the formalism. It only has access to the $\leadsto _s$-relation and to the enabling status of each transition.

It would not be easy to describe this algorithm without allowing disabled transitions in the aps set. Indeed, instead of this algorithm, publications on ample and persistent sets suggest straightforward algorithms that test whether some obviously $\leadsto _s$-closed set is available and if not, revert to the set of all enabled transitions. This means that they waste reduction potential. The running time is not an important issue here, because, as experiments with ASSET have demonstrated [20, 21, 26], the algorithm is very fast.

The first publications on stubborn sets (such as [15]) used formalism-specific conditions resembling PNd and PNe instead of abstract conditions such as D1 and D2.

It is now easy to show that every ample set is strongly stubborn.

Theorem 5

If transitions are deterministic, $\mathsf {ample}(s_0) \subseteq \mathsf {en}(s_0)$, and $\mathsf {ample}(s_0)$ satisfies C0 and C1, then $\mathsf {ample}(s_0)$ satisfies D0, D1, and D2.

Proof

Clearly C0 implies D0. Dd follows trivially from $\mathsf {ample}(s_0) \subseteq \mathsf {en}(s_0)$, and De follows immediately from C1. Now Theorem 4 gives the claim.    $\square$

Fig. 4.

An example where $\{t\}$ satisfies D0, D1, and D2, but not C1.

Figure 4 demonstrates that the opposite does not hold. Clearly $\{t\}$ satisfies D0 in 21. The only enabled sequences of transitions not containing t are $\varepsilon$ and $t_1$. Checking them both reveals that $\{t\}$ also satisfies D1 and D2 in 21. However, $\{t\}$ does not satisfy C1, because t is not independent of $t_1$ because of 11.

To relate strong stubborn sets to persistent sets, the following theorem is useful.

Theorem 6

Let $s_0$ be a state and $\mathsf {stubb}(s_0)$ be a set of transitions. If $\mathsf {stubb}(s_0)$ obeys D0, D1, and D2 in $s_0$, then also $\mathsf {stubb}(s_0) \cap \mathsf {en}(s_0)$ obeys them in $s_0$.

Proof

That $\mathsf {stubb}(s_0) \cap \mathsf {en}(s_0)$ obeys D0 is immediate from D0 for $\mathsf {stubb}(s_0)$.

Assume that $s_0 \xrightarrow {t_1 \cdots t_n}$, where $t_i \notin \mathsf {stubb}(s_0) \cap \mathsf {en}(s_0)$ for $1 \le i \le n$. We prove that no $t_i$ is in $\mathsf {stubb}(s_0)$. To derive a contradiction, let i be the smallest such that $t_i \in \mathsf {stubb}(s_0)$. So $t_i \in \mathsf {stubb}(s_0)$, $t_i \notin \mathsf {en}(s_0)$, $s_0 \xrightarrow {t_1 \cdots t_{i-1} t_i}$, and $t_j \notin \mathsf {stubb}(s_0)$ for $1 \le j < i$. This contradicts D1 for $\mathsf {stubb}(s_0)$.

If the if-part of D1 holds for $\mathsf {stubb}(s_0) \cap \mathsf {en}(s_0)$, then by the above, the if-part of D1 holds also for $\mathsf {stubb}(s_0)$. So the then-part for $\mathsf {stubb}(s_0)$ holds, which is the same as the then-part for $\mathsf {stubb}(s_0) \cap \mathsf {en}(s_0)$. Similar reasoning applies to D2.    $\square$

Persistent sets also assume that transitions are deterministic. They rely on independence in a state. If t and $t'$ are independent in s, then the following hold [6, Def. 3.17]:

• 1. If $s \xrightarrow {t}$ and $s \xrightarrow {t'}$, then there is $s'$ such that $s \xrightarrow {t t'} s'$ and $s \xrightarrow {t' t} s'$.

• 2. If $s \xrightarrow {t t'}$, then $s \xrightarrow {t'}$.

• 3. If $s \xrightarrow {t' t}$, then $s \xrightarrow {t}$.

A set $\mathsf {pers}(s_0)$ is persistent in $s_0$ if and only if $\mathsf {pers}(s_0) \subseteq \mathsf {en}(s_0)$ and for every $t_1$, ..., $t_n$ and $s_1$, ..., $s_n$ such that $s_0 \xrightarrow {t_1} s_1 \xrightarrow {t_2} \cdots \xrightarrow {t_n} s_n$ and $t_i \notin \mathsf {pers}(s_0)$ for $1 \le i \le n$, it holds that every element of $\mathsf {pers}(s_0)$ is independent of $t_i$ in $s_{i-1}$ [6, Definition 4.1].

It is worth noticing that the concept of persistency would not change if items 2 and 3 were removed from the definition of independence in a state. Let $t \in \mathsf {pers}(s_0)$, and let $s'_0$ be such that $s_0 \xrightarrow {t} s'_0$. Repeated application of item 1 yields $s'_1$, ..., $s'_n$ such that $s'_0 \xrightarrow {t_1} s'_1 \xrightarrow {t_2} \cdots \xrightarrow {t_n} s'_n$ and $s_i \xrightarrow {t} s'_i$ for $1 \le i \le n$. Because for $1 \le i \le n$, both t and $t_i$ are enabled in $s_{i-1}$, the then-parts of items 2 and 3 hold, and thus the items as a whole hold. That is, items 2 and 3 can be proven for the states $s_{i-1}$, so they need not be assumed. It seems plausible that items 2 and 3 were originally adopted by analogy to the independence relation in Mazurkiewicz traces [9].

The next theorem, from [27, Lemma 4.14], says that persistent sets are equivalent to strong stubborn sets restricted to deterministic transitions.

Theorem 7

Assume that transitions are deterministic. Every nonempty persistent set satisfies D0, D1, and D2. If a set satisfies D1 and D2, then its set of enabled transitions is persistent.

Proof

Persistency immediately implies De. Because $\mathsf {pers}(s_0) \subseteq \mathsf {en}(s_0)$, it also implies Dd. These yield D1 and D2 by Theorem 4. If a persistent set is not empty, then it trivially satisfies D0.

Assume that $\mathsf {stubb}(s_0)$ satisfies D1 and D2. Let $\mathsf {pers}(s_0) = \mathsf {stubb}(s_0)~\cap ~\mathsf {en}(s_0)$. By Theorems 4 and 6, $\mathsf {pers}(s_0)$ satisfies De. Let $t \in \mathsf {pers}(s_0)$, $s'_0$ be the state such that $s_0 \xrightarrow {t} s'_0$, $s_0 \xrightarrow {t_1} s_1 \xrightarrow {t_2} \cdots \xrightarrow {t_n} s_n$, and $t_i \notin \mathsf {pers}(s_0)$ for $1 \le i \le n$. De implies $s'_0 \xrightarrow {t_1 \cdots t_n}$. Let $s'_1$, ..., $s'_n$ be the states such that $s'_0 \xrightarrow {t_1} s'_1 \xrightarrow {t_2} \cdots \xrightarrow {t_n} s'_n$. Let $1 \le i \le n$. By giving De $t_1 \cdots t_i$ in the place of $t_1 \cdots t_n$ we see that De implies $s_i \xrightarrow {t} s'_i$ for $1 \le i \le n$. As a consequence, De implies for $1 \le i \le n$ that t is independent of $t_i$ in $s_{i-1}$. This means that $\mathsf {pers}(s_0)$ is persistent.    $\square$

Deadlock-preserving weak stubborn sets use D1 and the following condition D2w, that replaces both D0 and D2.

 

D2w. :

If $\mathsf {en}(s_0) \ne \emptyset$, then there is $t_\mathsf {k}\in \mathsf {stubb}(s_0)$ such that if $t_i \notin \mathsf {stubb}(s_0)$ for $1 \le i \le n$ and $s_0 \xrightarrow {t_1 \cdots t_n} s_n$, then $s_n \xrightarrow {t_\mathsf {k}}$.

 

By choosing $n=0$ we see that $s_0 \xrightarrow {t_\mathsf {k}}$. That is, instead of requiring that all enabled transitions in a stubborn set remain enabled while outside transitions occur, D2w requires that one of them exists and remains enabled. This one is called key transition and denoted above with $t_\mathsf {k}$.

Every strong stubborn set is also weak but not necessarily vice versa. Therefore, weak stubborn sets have potential for better reduction results. The first publication on stubborn sets [15] used weak stubborn sets. The added reduction potential of weak stubborn sets has only recently found its way to tools [4, 7, 8]. The proof of Theorem 3 goes through with D2w instead of D2 and D0. Indeed, weak stubborn sets preserve many, but not necessarily all of the properties that strong stubborn sets preserve.

Excluding a situation that does not occur with most verification tools, if the system has infinite executions, then all methods in this section preserve at least one. The nondeterministic case of this theorem is new or at least little known.

Theorem 8

Assume that $s_0 \in S_\mathsf {r}$ and $s_0 \xrightarrow {t_1} s_1 \xrightarrow {t_2} \ldots$. If transitions are deterministic or the reduced state space is finitely branching, then there are $t'_1$, $t'_2$, ... such that $s_0 \xrightarrow {t'_1 t'_2 \cdots }$ in the reduced state space.

Proof

If any of the $t_i$ is in $\mathsf {stubb}(s_0)$, then, for the smallest such i, by D1, there is $s'_0$ such that $s_0 \xrightarrow {t_i} s'_0 \xrightarrow {t_1 \cdots t_{i-1} t_{i+1} \cdots }$. Otherwise, by D2w, for every $j \in \mathbb {N}$ there is $s'_j$ such that $s_j \xrightarrow {t_\mathsf {k}} s'_j$. If transitions are deterministic, then D1 yields $s'_0 \xrightarrow {t_1} s'_1 \xrightarrow {t_2} \cdots$. This argument can be repeated at $s'_0$ and so on without limit, yielding the claim.

If transitions are not necessarily deterministic, then, for every $n \in \mathbb {N}$, D1 can be applied to $s_0 \xrightarrow {t_1 \cdots t_n}$ or to $s_0 \xrightarrow {t_1 \cdots t_n t_\mathsf {k}}$. This can be repeated n times, yielding an execution of length n in the reduced state space starting at $s_0$. If the reduced state space is finitely branching, then König’s Lemma type of reasoning yields the claim.    $\square$

Consider a Petri net with two transitions and no places. Any reasonable implementation of the deadlock-preserving aps set method fires initially one transition, notices that it introduced a self-loop adjacent to the initial state, and terminates without ever trying the other transition. Let t be the fired and $t'$ the other transition. In terms of Theorem 8, the infinite execution $\hat{s} \xrightarrow {t' t' t' \cdots }$ became represented by $\hat{s} \xrightarrow {t t t \cdots }$. So it is possible that $\{t_1, t_2, \ldots \} \cap \{t'_1, t'_2, \ldots \} = \emptyset$ in Theorem 8. More generally, if an original execution does not lead to a deadlock, then it is often the case that its representative in the reduced state space does not consist of precisely the same transitions. As a consequence, in the opinion of the present authors, when trying to understand aps set methods, Mazurkiewicz traces [9] and partial orders of transition occurrences are not a good starting point.

5 Visible and Invisible Transitions

Figure 5 shows a 1-safe Petri net, the directed graph that the $\leadsto _M$-relation spans in the shown marking $\{1,4,9\}$, and the similar graph for the marking $\{1,6,9\}$ that is obtained by firing $t_3$. Please ignore the grey $p_{12}$ and $t_7$ until Sect. 6. Please ignore the dashed arrows for the moment. They will be explained soon.

Fig. 5.

A Petri net with two visible transitions and its $\leadsto _{\{1,4,9\}}$- and $\leadsto _{\{1,6,9\}}$-graphs. In the latter, $p_2$ is chosen as $p_{t_2}$. The dashed arrows arise from V.

Assume that we want to check whether always at least one of $p_1$ and $p_8$ is empty. We denote this property with $\Box ((M(p_1) = 0) \vee (M(p_8) = 0))$. It does not hold, as can be seen by firing $t_3 t_4 t_5$.

According to the theory developed this far, $\{t_1\}$ is stubborn. Therefore, it suffices to fire just $t_1$ in the initial marking. After firing it, $p_1$ is permanently empty. As a consequence, no counterexample to $\Box ((M(p_1) = 0) \vee (M(p_8) = 0))$ is found. We see that the basic strong stubborn set method does not preserve the validity of this kind of properties.

This problem can be solved in two steps. The second step will be described in Sects. 6 and 7, where systems that may exhibit cyclic behaviour are discussed. The first step consists of classifying transitions as visible and invisible, and adopting an additional requirement. The atomic propositions of $\Box ((M(p_1) = 0) \vee (M(p_8) = 0))$ are $M(p_1) = 0$ and $M(p_8) = 0$. If a transition is known not to change the truth value of any atomic proposition in any reachable marking, it is classified as invisible. If the transition is known to change the truth value in at least one reachable marking or it is not known whether it can change it, then it is classified as visible. The additional requirement is the following.

 

V. :

If $\mathsf {stubb}(s_0)$ contains an enabled visible transition, then it contains all visible transitions (also disabled ones).

 

In the example, the grey transitions are visible and the rest are invisible. V adds the dashed arrows to the $\leadsto _M$-graphs in Fig. 5.

Assume V. Consider D1. Its t is enabled because $s_0 \xrightarrow {t t_1 \cdots t_n}$. Consider the sequence of visible transitions within $t t_1 \cdots t_n$, that is, the projection of $t t_1 \cdots t_n$ on visible transitions. If t is invisible, then it is obviously the same as the projection of $t_1 \cdots t_n t$. If t is visible, then V implies that $t_1$, ..., $t_n$ are invisible, because they are not in $\mathsf {stubb}(s_0)$ by the assumption in D1. So again the projections are the same. This means that when $t_1 \cdots t_n$ and $t'_1 \cdots t'_n$ are like in Theorems 2 and 3, the projection of $t_1 \cdots t_n$ is the same as the projection of $t'_1 \cdots t'_n$.

With Theorem 8, the projection of $t_1 t_2 \cdots$ is a prefix of the projection of $t'_1 t'_2 \cdots$ or vice versa. Sections 6 and 7 tell how they can be made the same.

For instance, $t_3 t_4 t_5 t_1$ leads to a deadlock in Fig. 5. In it, $t_5$ occurs before $t_1$. V guarantees that $t_5$ occurs before $t_1$ also in the permutation of $t_3 t_4 t_5 t_1$ whose existence Theorem 3 promises. By executing the permutation to a point where $t_5$ has but $t_1$ has not yet occurred, a state in the reduced state space is found that violates $\Box ((M(p_1) = 0) \vee (M(p_8) = 0))$. In this way V makes it possible to check many kinds of properties from the reduced state space.

Indeed, with the dashed arrow, the $\leadsto _M$-graph in Fig. 5 middle yields two stubborn sets: $\{t_1, \ldots , t_5\}$ and T. In both cases, $t_3$ is in the stubborn set. By firing $t_3$, the marking $\{1,6,9\}$ is obtained whose $\leadsto _M$-graph is shown in Fig. 5 right. This graph yields the stubborn sets $\{t_4, t_6\}$, $\{t_1, t_4, t_5, t_6\}$, and some others that have the same enabled transitions as one of these, such as $\{t_3, t_4, t_5, t_6\}$. All of them contain $t_4$. After firing it, each stubborn set contains $t_1$, $t_5$, and possibly some disabled transitions. So the sequence $t_3 t_4 t_5$ is fired in the reduced state space (after which $t_1$ is fired).

In the ample set theory, instead of V there is the following condition:

 

C2. :

If $\mathsf {ample}(s_0)$ contains a visible transition, then make $\mathsf {ample}(s_0) = \mathsf {en}(s_0)$.

 

This condition is stronger than V in the sense that C2 always forces at least the same enabled transitions to be taken as V, but not necessarily vice versa. In particular, although $\{t_1, \ldots , t_5\}$ obeys V in the initial marking of our example, its set of enabled transitions (that is, $\{t_1, t_3\}$) does not obey C2. Indeed, C2 commands to fire all enabled transitions in $\{1,4,9\}$, including also $t_6$. Therefore, ample sets yield worse reduction in this example than stubborn sets.

It is difficult to formulate V without talking about disabled transitions in the stubborn set. For instance, consider “if the stubborn set contains an enabled visible transition, then it contains all enabled visible transitions”. It allows to choose $\{t_1\}$ in $\{1,4,9\}$. However, we already saw that $\{t_1\}$ loses all counterexamples to the property. The ability to formulate better conditions than C2 is an example of the advantages of allowing disabled transitions in stubborn sets.

The basis of the running example of this section (but not most of the details) is from [26].

6 The Ignoring Problem, Part 1: Finite Executions

Assume that the initially marked place $p_{12}$, transition $t_7$, and arcs between them are added to the Petri net in Fig. 5. Before the addition, the state space of the net is acyclic and has the deadlocks $\{3,5,11\}$, $\{2,8,10\}$, and $\{2,6,11\}$. The addition adds number 12 and the self-loop $M \xrightarrow {t_7} M$ to each reachable marking. It adds the stubborn set $\{t_7\}$ to each reachable marking and otherwise keeps the $\sqsubseteq _M$-minimal stubborn sets the same.

If $t_7$ is investigated first in the initial marking $\{1,4,9,12\}$, then the stubborn set $\{t_7\}$ is chosen. Firing $t_7$ leads back to the initial marking. Therefore, the method only constructs the initial marking and its self-loop—that is, one marking and one edge. This is correct, because like the full state space, this reduced state space has no deadlocks but has an infinite execution. As a matter of fact, from the point of view of checking these two properties, the obtained reduction is ideal.

On the other hand, this reduced state space is clearly invalid for disproving the formula $\Box ((M(p_1) = 0) \vee (M(p_8) = 0))$. This problem is known as the ignoring problem. After finding out that $t_7$ causes a self-loop in every reachable marking, the method stopped and ignored the rest of the Petri net.

Let $s \xrightarrow {\mathrm {key}} s'$ denote that there are $s_0$, ..., $s_n$ and $t_1$, ..., $t_n$ such that $s = s_0 \xrightarrow {t_1} s_1 \xrightarrow {t_2} \cdots \xrightarrow {t_n} s_n = s'$ and $t_i$ is a key transition of $\mathsf {stubb}(s_{i-1})$ for $1 \le i \le n$. In [17, 18], the ignoring problem was solved with the following condition Sen, and in [18] also with SV:

 

Sen. :

For every $t \in \mathsf {en}(s_0)$ there is $s_t$ such that $s_0 \xrightarrow {\mathrm {key}} s_t$ and $t \in \mathsf {stubb}(s_t)$.

SV. :

For every visible t there is $s_t$ such that $s_0 \xrightarrow {\mathrm {key}} s_t$ and $t \in \mathsf {stubb}(s_t)$.

 

With deterministic transitions, D1, D2w, and Sen guarantee that if $s \in S_\mathsf {r}$ and $s \xrightarrow {t_1 \cdots t_n}$, then there are $t'_1$, ..., $t'_m$ such that $s \xrightarrow {\pi }$ in the reduced state space for some permutation $\pi$ of $t_1 \cdots t_n t'_1 \cdots t'_m$. This facilitates the verification of many properties. For instance, a transition is Petri net live (that is, from every reachable state, a state can be reached where it is enabled) if and only if it is Petri net live in the reduced state space. With deterministic transitions, D1, D2w, V, and SV guarantee that if $s \in S_\mathsf {r}$ and $s \xrightarrow {t_1 \cdots t_n}$, then there is some transition sequence $\pi$ such that $s \xrightarrow {\pi }$ in the reduced state space and the projection of $\pi$ on the visible transitions is the same as the projection of $t_1 \cdots t_n$.

With deterministic transitions and strong stubborn sets, Sen can be implemented efficiently as follows [17, 19]. Terminal strong components of the reduced state space can be recognized efficiently on-the-fly with Tarjan’s algorithm [3, 14]. (This resembles the algorithm in Sect. 2, but the directed graph in question is different.) If some transition is enabled in some state of a terminal strong component but does not occur in the component, then it is enabled in every state of the component by D2 and D1. When the algorithm is about to backtrack from the component, it checks whether there are such transitions. If there are, it expands the stubborn set of the current state (called the root of the component) so that it contains at least one such transition. The expanded set must satisfy D1 and D2. To avoid adding unnecessary enabled transitions, it is reasonable to compute it using the algorithm in Sect. 2 (without entering the transitions in the original stubborn set).

SV can be implemented similarly, except that the algorithm checks whether each visible transition is in some stubborn set used in the terminal strong component [26]. By V, this is certainly the case if any visible transition occurs in the component. Let $\mathsf {CV}(M)$ denote the $\leadsto _M$-closure of the set of visible transitions. In the negative case, the algorithm expands the stubborn set of the root of the component with some subset of $\mathsf {CV}(M)$ maintaining D1, D2, and V. This is continued until for each terminal strong component, either a visible transition occurs in it or the stubborn set of its root is a superset of $\mathsf {CV}(M)$.

In the latter case it is certain that no visible transition can occur in the future, and the analysis may be terminated even if some enabled transitions were never investigated. This reasoning is valid also in the deadlocks of the reduced state space. In particular, if $\mathsf {CV}(M)$ contains no enabled transitions, then no transitions need to be fired, even if that violates D0. As a consequence, it is correct (and good for reduction results) to only use subsets of $\mathsf {CV}(M)$ as stubborn sets.

Fig. 6.

Illustrating the nonoptimality of Sen and SV.

SV is nonoptimal in the sense that expanding the stubborn set with $\mathsf {CV}(M)$ may require the addition of enabled transitions that Sen and V together do not add. Figure 6 illustrates this. In it, the task is to find out whether $t_5$ can ever fire. It cannot, because $t_4$ is always disabled in a nontrivial way. We cannot assume that the stubborn set construction algorithm can detect that $t_4$ is always disabled, because detecting such a thing is PSPACE-hard in general. To be realistic, we instead assume that the stubborn set construction algorithm just uses PNd and PNe like in Sect. 2. In any reachable M, PNd declares either $t_4 \leadsto _M t_1$ and $t_4 \leadsto _M t_2$ or $t_4 \leadsto _M t_3$.

Assume that transitions are tried in the order of their indices as the starting points of the construction of stubborn sets. The stubborn set method first uses $\mathsf {stubb}(\hat{M}) = \{t_1\}$. So it fires $t_1$ yielding $M_1$. We have $t_1 \leadsto _{M_1} t_3 \leadsto _{M_1} t_1$, $t_3 \leadsto _{M_1} t_2 \leadsto _{M_1} t_4 \leadsto _{M_1} t_1$, and $t_4 \leadsto _{M_1} t_2$ (the last two via $p_3$). So the method uses $\mathsf {stubb}(M_1) = \{t_1, t_2, t_3, t_4\}$ and fires $t_2$ yielding $M_2$. Next it fires $t_3$ closing a cycle, using $\mathsf {stubb}(M_2) = \{t_3, t_4\}$, because $t_3 \leadsto _{M_2} t_4 \leadsto _{M_2} t_3$ (the latter via $p_2$). Because $t_5$ is visible and is not in any of these stubborn sets, the algorithm expands the root of the terminal strong component, that is, $\hat{M}$. The algorithm is cunning enough to avoid $t_6$, since $t_5 \not \leadsto _{\hat{M}}^* t_6$. On the other hand, $t_5 \leadsto _{\hat{M}} t_4 \leadsto _{\hat{M}} t_2$. So the algorithm fires $t_2$ at $\hat{M}$, making the size of the reduced state space grow.

Also Sen and V together guarantee that projections on visible transitions are preserved. Indeed, they were used in [18]. They do not add $t_2$ to $\mathsf {stubb}(\hat{M})$ in Fig. 6, because $t_2 \in \mathsf {stubb}(M_1)$. Unfortunately, they are nonoptimal in the sense that they unnecessarily solve the ignoring problem also for the invisible transitions. In Fig. 6, they add $t_6$ to $\mathsf {stubb}(\hat{M})$.

We now present and prove correct a novel condition that is free from both of these problems. We first rewrite Dd using $T'$ in the place of $\mathsf {stubb}(s_0)$.

 

Dd. :

If $t \in T'$, $\lnot (s_0 \xrightarrow {t})$, $t_i \notin T'$ for $1 \le i \le n$, and $s_0 \xrightarrow {t_1 \cdots t_n} s_n$, then $\lnot (s_n \xrightarrow {t})$.

 

Let $T_\mathsf {i}\subseteq T$ be any set of transitions. Typical examples of $T_\mathsf {i}$ are the set of visible transitions and the set of all transitions. We call its elements the interesting transitions. The following condition solves the ignoring problem.

 

S. :

There is $T' \subseteq T$ such that $T_\mathsf {i}\subseteq T'$, $T'$ satisfies Dd in $s_0$, and for every $t \in T' \cap \mathsf {en}(s_0)$ there is $s_t$ such that $s_0 \xrightarrow {\mathrm {key}} s_t$ and $t \in \mathsf {stubb}(s_t)$.

 

An often good $T'$ can be computed by first introducing a $\leadsto '_s$-relation only using PNd or its counterpart in the formalism in question, and then computing the $\leadsto '_s$-closure of $T_\mathsf {i}$. In Fig. 6 in $\hat{M}$, this yields $\{t_1, t_2, t_4, t_5\}$. For each root s of each terminal strong component, the algorithm checks that each element of $T' \cap \mathsf {en}(s)$ occurs within the component. In the negative case, the algorithm expands $\mathsf {stubb}(s)$ with the traditional $\leadsto _s$-closure (that is, the one that uses the counterparts of both PNd and PNe) of some missing element of $T' \cap \mathsf {en}(s)$. To obtain an $\sqsubseteq _M$-minimal result, Tarjan’s algorithm is used similarly to Sect. 2 also during this step. In Fig. 6 in $\hat{M}$, we have $T' \cap \mathsf {en}(\hat{M}) = \{t_1, t_2\}$. Because $t_1 \in \mathsf {stubb}(\hat{M})$ and $t_2 \in \mathsf {stubb}(M_1)$, S holds. The algorithm terminates, without expanding $\mathsf {stubb}(\hat{M})$ and without ever trying $t_6$.

By choosing $T_\mathsf {i}= T$ we get $T' = T$ and see that Sen implies S. Together with the example in Fig. 6, this shows that S is strictly better than Sen.

The comparison of S to SV is more difficult. Therefore, we only compare their implementations described above. Let $T_\mathsf {i}$ be the set of visible transitions. If no visible transition can be made enabled in the future, then the algorithm for $\mathbf SV$ ultimately expands the stubborn set $\mathsf {stubb}(s)$ of the root s of the terminal strong component with $\mathsf {CV}(s)$. The word “ultimately” refers to the fact that the algorithm may try subsets of $\mathsf {CV}(s)$ before trying $\mathsf {CV}(s)$ as a whole, and, as a consequence, new states may be generated such that the component ceases from being terminal or s ceases from being its root.

In the same situation, the algorithm for S obtains $T' \cap \mathsf {en}(s)$ by computing the $\leadsto '_s$-closure of $T_\mathsf {i}$ and picking the enabled transitions in it. If none of these transitions occurs in the component, then the S algorithm ultimately expands $\mathsf {stubb}(s)$ with them. When doing so it computes their $\leadsto _s$-closures, to satisfy D1, D2, and V. The union of the computed sets is $\mathsf {CV}(s)$. So in this case, the S algorithm makes the same expansion as the SV algorithm. On the other hand, if any of these transitions does occur in the component, then the S algorithm does not use it for expanding $\mathsf {stubb}(s)$. Then the S algorithm is better than the SV algorithm. This is what happened with $t_2$ in Fig. 6.

We now prove that S is correct.

Lemma 9

If transitions are deterministic, $s_0 \in S_\mathsf {r}$, $\mathsf {stubb}(s_0)$ obeys S, $\mathsf {stubb}(s)$ obeys D2w in every $s \in S_\mathsf {r}$, and $s_0 \xrightarrow {t_1 \cdots t_n} s_n$ where $t_n \in T_\mathsf {i}$, then there are $s'_0$, ..., $s'_m$ and $t_\mathsf {k}^1$, ..., $t_\mathsf {k}^m$ such that $s'_0 = s_0$, $s'_0 \xrightarrow {t_\mathsf {k}^1} s'_1 \xrightarrow {t_\mathsf {k}^2} \cdots \xrightarrow {t_\mathsf {k}^m} s'_m$, $t_\mathsf {k}^{i+1}$ is a key transition of $\mathsf {stubb}(s'_i)$ and $\{t_1, \ldots , t_n\} \cap \mathsf {stubb}(s'_i) = \emptyset$ for $0 \le i < m$, and $\{t_1, \ldots , t_n\} \cap \mathsf {stubb}(s'_m) \ne \emptyset$.

Proof

Because $t_n \in T_\mathsf {i}\subseteq T'$, there is $1 \le i \le n$ such that $t_i \in T'$ but $t_j \notin T'$ for $1 \le j < i$. By Dd $t_i \in \mathsf {en}(s_0)$. By S there is $s_{t_i}$ such that $t_i \in \mathsf {stubb}(s_{t_i})$ and $s_0 \xrightarrow {\mathrm {key}} s_{t_i}$. Let the states along this path be called $s'_0$, ..., $s'_h$. So $s'_0 = s_0$, $s'_h = s_{t_i}$ and $t_i \in \{t_1, \ldots , t_n\} \cap \mathsf {stubb}(s'_h)$. Thus there is the smallest m such that $\{t_1, \ldots , t_n\} \cap \mathsf {stubb}(s'_m) \ne \emptyset$, completing the proof.    $\square$

Theorem 10

Assume that transitions are deterministic and $\mathsf {stubb}(s)$ obeys D1, D2w, and S in every $s \in S_\mathsf {r}$. Let $s_0 \in S_\mathsf {r}$ and $s_0 \xrightarrow {t_1} s_1 \xrightarrow {t_2} \cdots \xrightarrow {t_n} s_n$. There are $t'_1$, ..., $t'_m$, and $s_m$ such that $s_0 \xrightarrow {t'_1 \cdots t'_m} s_m$ in the reduced state space and each $t \in T_\mathsf {i}$ occurs in $t'_1 \cdots t'_m$ at least as many times as it occurs in $t_1 \cdots t_n$. Furthermore,

• If $T_\mathsf {i}= T$, then there are $t_{n+1}$, ..., $t_m$ such that $s_n \xrightarrow {t_{n+1} \cdots t_m} s_m$ and $t'_1 \cdots t'_m$ is a permutation of $t_1 \cdots t_m$.

• If $T_\mathsf {i}$ is the set of visible transitions and $\mathsf {stubb}(s)$ obeys V in every $s \in S_\mathsf {r}$, then the projections of $t_1 \cdots t_n$ and $t'_1 \cdots t'_m$ on $T_\mathsf {i}$ are the same.

Proof

If none of $t_1$, ..., $t_n$ is in $T_\mathsf {i}$, the first claim holds vacuously with $m=0$. Otherwise let $1 \le n' \le n$ be the biggest such that $t_{n'} \in T_\mathsf {i}$. Lemma 9 yields $s'$ and $t_\mathsf {k}^1$, ..., $t_\mathsf {k}^{m'}$ such that $s_0 \xrightarrow {t_\mathsf {k}^1 \cdots t_\mathsf {k}^{m'}} s'$ and $\{t_1, \ldots , t_{n'}\} \cap \mathsf {stubb}(s') \ne \emptyset$. Applying D2w, D1, and determinism $m'$ times yields $s''$ such that $s' \xrightarrow {t_1 \cdots t_{n'}} s''$ and $s_{n'} \xrightarrow {t_\mathsf {k}^1 \cdots t_\mathsf {k}^{m'}} s''$. D1 produces from $s' \xrightarrow {t_1 \cdots t_{n'}} s''$ a transition occurrence in the reduced state space that consumes one of $t_1$, ..., $t_{n'}$. The first claim follows by induction.

If $T_\mathsf {i}= T$, then always $n' = n$. The $t_\mathsf {k}^1$, ..., $t_\mathsf {k}^{m'}$ introduced in each application of Lemma 9 are the $t_{n+1}$, ..., $t_m$.

In the case of the last claim, each key transition is invisible, because otherwise $t_{n'}$ would be in the stubborn set of the key transition by V, contradicting Lemma 9. Therefore, the applications of D2w neither add visible transitions nor change the order of the visible transitions. By V, the same holds for the applications of D1.    $\square$

In the literature, S may refer to any condition that plays the role of Sen, SV, or (from now on) the S of the present study. This is because there is usually no need to talk about more than one version of the condition in the same publication. The name S refers to “safety properties”, which is the class of properties whose counterexamples are finite (not necessarily deadlocking) executions.

In [20, 22] it was pointed out that it is often possible and perhaps even desirable to modify the model such that from every reachable state, a deadlock is reachable. Reduction with deterministic transitions, D0, D1, and D2 preserves this property. Two efficient algorithms were given for checking from the reduced state space that this property holds. Such systems trivially satisfy S. This solution to the ignoring problem is simple. As far it is known, it gives good reduction results. (Little is known on the relative performance of alternative solutions to the ignoring problem.)

7 The Ignoring Problem, Part 2: Diverging Executions

Figure 7 demonstrates that S does not always suffice to preserve a property. Consider $\Diamond \Box (M(p_2) = 0)$, that is, from some point on, $p_2$ remains empty. It fails because of $t_5 t_1 t_4 t_4 t_4 \cdots$. However, the figure shows a reduced state space that obeys D0, D1, D2, V, and S, but contains no counterexample.

Fig. 7.

Terminal strong components vs. cycles.

This problem only arises with diverging counterexamples, that is, those which end with an infinite sequence of invisible transitions. A state is called diverging if and only if there exists an infinite sequence of invisible transitions from it. When finite counterexamples apply, the methods in Sect. 6 suffice. If the reduced state spaces are finite (as they usually are with practical computer tools), they suffice also for counterexamples that contain an infinite number of visible transitions. This is because the methods preserve every finite prefix of the projection on visible transitions, from which König’s Lemma type of reasoning proves that also the infinite projection is preserved.

With stubborn sets, this problem has been solved by two conditions that together replace S:

 

I. :

If $\mathsf {en}(s_0)$ contains an invisible transition, then $\mathsf {stubb}(s_0)$ contains an invisible key transition.

L. :

For every visible transition t, every cycle in the reduced state space (which is assumed to be finite) contains a state s such that $t \in \mathsf {stubb}(s)$.

 

Let $t_1 t_2 \cdots$ be such that $s_0 \xrightarrow {t_1 t_2 \cdots }$ and only a finite number of the $t_i$ are visible. Assume that $t_1 t_2 \cdots$ contains at least one visible transition $t_v$. Similarly to the proof of Theorem 10, key transitions and D2w are used to go to a state whose stubborn set contains some $t_i$, and then D1 is used to move a transition occurrence from the sequence to the reduced state space. At most $|S_\mathsf {r}|-1$ applications of D2w and D1 may be needed before some $t_i$ such that $i \le v$ is consumed, because otherwise the reduced state space would contain a cycle without $t_v$ in any of its stubborn sets, violating L. As a consequence, each visible transition of $t_1 t_2 \cdots$ is eventually consumed.

When that has happened, I ensures that the reduced state space gets an infinite invisible suffix. Without I, it could happen that only visible transitions are fired immediately after consuming the last $t_v$, spoiling the counterexample.

A diverging execution $\xi$ is minimal if and only if there is no infinite execution whose projection on visible transitions is a proper prefix of the projection of $\xi$. Minimal diverging counterexamples are preserved even without L and S. This implies that if the reduced state space is finite, then D1, V, I, and a variant of D2w preserve [18, 23] the failures–divergences semantics in CSP theory [13]. D2w is replaced by a variant, because CSP uses nondeterministic transitions.

With deterministic transitions D1 and D2w also give an interesting result for diverging executions, one that is worth commenting here.

Theorem 11

Assume that transitions are deterministic and $\mathsf {stubb}(s)$ obeys D1 and D2w in every $s \in S_\mathsf {r}$. Assume further that $s_0 \xrightarrow {t_1} s_1 \xrightarrow {t_2} \cdots \xrightarrow {t_m} s_0$ are invisible key transitions. If $s_0 \xrightarrow {u_1 \cdots u_n} s_0'$ is a sequence in the full state space such that $\{u_1, \ldots , u_n\} \cap \bigcup _{i=0}^{m-1} (\mathsf {stubb}(s_i) \cap \mathsf {en}(s_i)) = \emptyset$, then $s_0'$ is diverging in the full state space.

Proof

Proof is by induction on m. $s_0 \xrightarrow {u_1 \cdots u_n} s_0'$ holds as the base case. Assume as inductive hypothesis that there is some $s_i'$ such that $s_i \xrightarrow {u_1 \cdots u_n} s_i'$ and $s_0' \xrightarrow {t_1 \cdots t_i} s_i'$. $u_j\notin \mathsf {stubb}(s_i) \cap \mathsf {en}(s_i)$ for each $1 \le j \le n$. Because $u_1$, if it exists, is enabled at $s_i$, it must be that $u_1 \notin \mathsf {stubb}(s_i)$, and applying D1 to $j = 2,\ldots ,n$ we get that $u_j \notin \mathsf {stubb}(s_i)$ for each $1 \le j \le n$. Because $t_{i+1}$ is a key transition, D2w guarantees $s_i' \xrightarrow {t_{i+1}} s_{i+1}'$ for some state $s_{i+1}'$ and $s_{i+1} \xrightarrow {u_1 \cdots u_n} s_{i+1}'$ is guaranteed by D1. Because $s_{m-1} \xrightarrow {t_m} s_0$, deterministic transitions guarantee that $s_m' = s_0'$.    $\square$

Note that when D2 or De is used instead of D2w, every enabled transition in any stubborn set is a key transition, so the theorem can be restated so that if a state is diverging in the reduced state space, then all states reachable by firing transitions that were ignored in the cycle are likewise diverging.

The theorem works to reinforce the intuition behind L. Consider Fig. 7. In the state in the upper right corner, $\{t_3,t_4\}$ is a stubborn set, and the state is diverging. According to the theorem, $t_1$ will lead to a diverging state, but nothing is guaranteed about the divergence in the part where $t_3$ has been fired. Theorem 11 can be used to make the reduced state space smaller, by not stipulating I when the presence of a divergence can be obtained with the theorem. More information on this is in [23].

Ample sets do not mention I, because it follows from C0, C2, and the fact that all transitions in an ample set are key transitions by C1. Instead of L, ample sets use the following condition.

 

C3. :

For every t and every cycle in the reduced state space, if t is enabled in some state of the cycle, then the cycle contains a state s such that $t \in \mathsf {ample}(s)$.

 

The relation of L to C3 resembles the relation of SV to Sen. This suggests that an improvement on C3 could be developed similarly to how S improves Sen. We leave this for future research.

The recommended implementation of C3 is called C3’ in [1]. It assumes that the reduced state space is constructed in depth-first order. It also implements L.

 

C3’. :

If $\mathsf {ample}(s) \ne \mathsf {en}(s)$, then for every $t \in \mathsf {ample}(s)$ and every $s'$ such that $s \xrightarrow {t} s'$, $s'$ is not in the depth-first stack.

 

Figure 8 illustrates that C3’ sometimes leads to the construction of unnecessarily many states. In it, all reachable states are constructed, although the processes do not interact at all. Better results are obtained if the component (either $\{t_1,t_2,t_3\}$ or $\{t_4,t_5,t_6\}$) is preferred to which the most recent transition belongs. Then the sequence $t_1 t_2 t_4 t_5 t_3 t_1$ is fired, after which both $t_2$ and $t_6$ are fired. This improved idea fails badly with the three-dimensional version of the example. In [2, Sect. 4, Fig. 4], the bad performance of C3’ was illustrated with a different example.

Fig. 8.

Transitions are tried in the order of their indices until one is found that does not close a cycle. If such a transition is not found, then all transitions are taken.

C3’ fully expands the last state of the cycle it closes. If the first state of the cycle is expanded instead and if the component is remembered, then the leftmost column and topmost row of Fig. 8 right are constructed. (Expanding the first or the last state is correct, but other states are not necessarily safe [23, Lemma 15].) This is better than with C3’, and works well also in the three-dimensional example, as well as for the example in [2]. There has been very little research on the performance of cycle conditions besides [2], although the problem is clearly important.

8 Trouble with Fairness

Fairness refers to assumptions about infinite executions that are used to root out certain nonsensical counterexamples. For example in Fig. 9, there is an infinite execution $(t_1 t_2)^\omega$ where $t_5$ is never fired, even though it is constantly enabled. Weak fairness is an assumption that if a transition is constantly enabled, it will eventually be fired. This can be understood, for example, so that in a concurrent execution of several processes, each process gets processor time, making it a reasonable assumption to discuss. Strong fairness is a stronger assumption that if a transition is enabled infinitely often (though it may be disabled infinitely often also), then it is eventually fired. That is, we say that a cycle $s_0 \xrightarrow {t_1 \cdots t_n} s_n$ such that $s_0 = s_n$ is

• weakly fair if and only if for every $t \in T$, either there is some i such that $t_i = t$ or $t \notin \mathsf {en}(s_i)$, and

• strongly fair if and only if for every $t \in T$, either there is some i such that $t_i = t$ or $t \notin \mathsf {en}(s_j)$ for every $1 \le j \le n$.

Fig. 9.

All weakly fair non-progress cycles may be lost.

In Fig. 9 we see a situation where weak fairness and stubborn sets encounter a problem. The set $\{t_1\}$ is an aps set in the initial state that satisfies all the conditions this far. In the second state $\{t_2, t_3\}$ satisfies all except C3 and C3’. In particular, it satisfies L.

The cycle in the reduced state space, indicated by the solid arrows, seems like a fair cycle in the reduced state space, but in the full state space it has a constantly enabled transition that is not fired along the cycle. A cycle that is fair in the reduced state space, but not necessarily in the full state space, is called a seemingly fair cycle. The full state space has a fair cycle, but this is not explored, only the seemingly fair cycle above it. The condition C3 is sufficiently strong in this example, as it guarantees that $t_5$ is fired in at least one state of the seemingly fair cycle. The cycle remains seemingly fair, but the corresponding fair cycle is also explored.

Fig. 10.

A seemingly weakly fair non-progress cycle may be fake.

One is tempted to explore a hypothesis that a seemingly fair cycle exists in the reduced state space if and only if a corresponding fair cycle exists in the full state space. In Fig. 10, we see that this hypothesis does not hold. The transition $t_3$ is constantly enabled, and the transition is fired in one of the states along the cycle, so that L is satisfied. The cycle itself is not fair, but it is seemingly fair. This happens even if C3 is used.

Fig. 11.

Two Petri nets illustrating yet another weak fairness problem.

Again, we are tempted to form a hypothesis that some algorithm that makes use of book-keeping regarding transitions along a cycle could be used to determine whether a weakly fair cycle was lost or not. The example in Fig. 11 leaves little hope for the development of such methods. In the leftmost example, the first cycle is unfair, but becomes seemingly fair when reduced. The second cycle, consisting of the same transitions, is not explored and the initial state does have all the enabled transitions in the aps set, so that the reduction satisfies C3. The full state space has a fair cycle and the reduced state space has a seemingly fair cycle.

In the rightmost example in the same figure, exactly the same aps sets can be used. The reduced state space is the same as in the leftmost example, and the sets of enabled transitions are the same in all the states of the reduced state space. Now the full state space does not have a fair cycle, but the reduced state space still has a seemingly fair cycle.

The first state space contains a fair cycle in the unexplored part and the second does not. Unless a method can use information about the system structure beyond that expressed by the conditions seen this far, and the part of the state space that has been explored, it cannot distinguish between the two state spaces.

Fig. 12.

Illustrating a strong fairness problem.

None of the cycles in Fig. 11 is strongly fair, but a similarly discouraging example for preserving strong fairness exists, and is shown in Fig. 12. The full state space has a strongly fair cycle that is never explored by a reduction. Again, from the point of view of aps sets and the enabled transitions in the reduced state space, the Petri net is equivalent to the ones in Fig. 11.

9 Conclusions

The goal in the development of stubborn sets has been as good reduction as possible, while ample and persistent sets have favoured straightforward easily implementable conditions and algorithms. As a consequence, where stubborn set methods differ from other aps set methods, stubborn sets tend to be more difficult to implement but yield better reduction results. Very little is known on the differences of the reduction power between different methods. Reliable information is difficult to obtain experimentally, because in addition to the issue that is being experimented, the results may depend on the optimality of the chosen $\leadsto _s$- or independence relation, on the order in which the transitions are listed in the input file (Sect. 3), and other things.

Some stubborn set ideas are difficult to implement efficiently. For instance, no very fast algorithm is known that can utilize the freedom to choose any one from among the places that disable a transition (the $p_t$ in Sect. 2). On the other hand, the likelyhood of finding good ways of exploiting some reduction potential decreases significantly, if the existence of the potential is never pointed out.

The algorithm in Sect. 2 seems intuitively very good, and experiments with the ASSET tool strongly support this view [20, 21, 26]. The present authors believe that it deserves more attention than it has received.

The biggest immediate difference between stubborn sets and other aps set methods is the possibility of disabled transitions in the set. It is difficult to think of the above-mentioned algorithm without this possibility. Furthermore, in Sect. 5 it was shown how it facilitates an improvement to the visibility condition. It is also important that stubborn sets allow nondeterministic transitions.

Perhaps the most important area where more research is needed is the ignoring problem. The example in Fig. 8 may be extreme and thus not representative of the typical situation. Unfortunately, very little is known on what happens in the typical situation with each solution.