Fair Testing and Stubborn Sets
 10 Citations
 465 Downloads
Abstract
Partialorder methods alleviate state explosion by considering only a subset of transitions in each constructed state. The choice of the subset depends on the properties that the method promises to preserve. Many methods have been developed ranging from deadlockpreserving to CTL\(^*\) and divergencesensitive branching bisimilarity preserving. The less the method preserves, the smaller state spaces it constructs. Fair testing equivalence unifies deadlocks with livelocks that cannot be exited, and ignores the other livelocks. It is the weakest congruence that preserves whether the ability to make progress can be lost. We prove that a method that was designed for trace equivalence also preserves fair testing equivalence. We describe a fast algorithm for computing highquality subsets of transitions for the method, and demonstrate its effectiveness on a protocol with a connection and data transfer phase. This is the first practical partialorder method that deals with a practical fairness assumption.
Keywords
Partialorder methods Fairness Progress Fair testing equivalence1 Introduction
State spaces of systems that consist of many parallel components are often huge. Usually many states arise from executing concurrent transitions in different orders. Socalled partialorder methods [2, 3, 5, 6, 7, 10, 11, 14, 16, 17, 18, 20] try to reduce the number of states by, roughly speaking, studying only some orders that represent all of them. This is achieved by only investigating a subset of transitions in each state. This subset is usually called ample, persistent, or stubborn. In this study we call it aps, when the differences between the three do not matter.
This intuition works well only with executions that lead to a deadlock. However, traces and divergence traces, for instance, arise from not necessarily deadlocking executions. With them, to obtain good reduction results, a constructed execution must often lack transitions and contain additional transitions compared to the executions that it represents. With branchingtime properties, thinking in terms of executions is insufficient to start with.
As a consequence, a wide range of aps set methods has been developed. The simplest only preserve the deadlocks (that is, the reduced state space has precisely the same deadlocks as the full state space) [14], while at the other end the CTL\(^*\) logic (excluding the next state operator) and divergencesensitive branching bisimilarity are preserved [5, 11, 16]. The more a method preserves, the worse are the reduction results that it yields. The preservation of the promised properties is guaranteed by stating conditions that the aps sets must satisfy. Various algorithms for computing sets that satisfy the conditions have been proposed. In an attempt to improve reduction results, more and more complicated conditions and algorithms have been developed. There is a tradeoff between reduction results on the one hand, and simplicity and the time that it takes to compute an aps set on the other hand.
Consider a cycle where the system does not make progress, but there is a path from it to a progress action. As such, traditional methods for proving liveness treat the cycle as a violation against liveness. However, this is not always the intention. Therefore, socalled fairness assumptions are often formulated, stating that the execution eventually leaves the cycle. Unfortunately, how to take them into account while retaining good reduction results has always been a problem for aps set methods. For instance, fairness is not mentioned in the partial order reduction chapter of [2]. Furthermore, as pointed out in [3], the most widely used condition for guaranteeing lineartime liveness (see, e.g., [2, p. 155]) often works in a way that is detrimental to reduction results.
Fair testing equivalence [12] always treats this kind of cycles as progress. If there is no path from a cycle to a progress action, then both fair testing equivalence and the traditional methods treat it as nonprogress. This makes fair testing equivalence suitable for catching many nonprogress errors, without the need to formulate fairness assumptions; for an application, see Sect. 7.
Fair testing equivalence implies trace equivalence. So it cannot have better reduction methods than trace equivalence. Fair testing equivalence is a branching time notion. Therefore, one might have guessed that any method that preserves it would rely on strong conditions, resulting in bad reduction results. Suprisingly, it turned out that a 20 years old tracepreserving stubborn set method [16] also preserves fair testing equivalence. This is the main result of the present paper. It means that no reduction power is lost compared to trace equivalence.
Background concepts are introduced in Sect. 2. Sections 3 and 4 present the tracepreserving method and discuss how it can be implemented. This material makes this publication selfcontained, but it also contains some improvements over earlier publications. Section 5 discusses further why it is good to avoid strong conditions. The proof that the method also applies to fair testing equivalence is in Sect. 6. Some performance measurements are presented in Sect. 7.
2 Labelled Transition Systems and Equivalences
In this section we first define labelled transition systems and some operators for composing systems from them. We also define some useful notation. Then we define the wellknown trace equivalence and the fair testing equivalence of [12]. We also define tree failure equivalence, because it is a strictly stronger equivalence with a related but much simpler definition.
The symbol \(\tau \) denotes the invisible action. A labelled transition system or LTS is a tuple \(L = (S, \varSigma , \varDelta , \hat{s})\) such that \(\tau \notin \varSigma \), \(\varDelta \subseteq S \times (\varSigma \cup \{\tau \}) \times S\) and \(\hat{s} \in S\). The elements of S, \(\varSigma \), and \(\varDelta \) are called states, visible actions, and transitions, respectively. The state \(\hat{s}\) is the initial state. An action is a visible action or \(\tau \).
We adopt the convention that, unless otherwise stated, \(L' = (S', \varSigma ', \varDelta ', \hat{s}')\), \(L_i = (S_i, \varSigma _i, \varDelta _i, \hat{s}_i)\), and so on.
The empty string is denoted with \(\varepsilon \). We have \(\varepsilon \ne \tau \) and \(\varepsilon \notin \varSigma \).
Let \(n \ge 0\), s and \(s'\) be states, and \(a_1, \ldots , a_n\) be actions. The notation \(s \mathrel {{}\,a_1 \cdots a_n{\rightarrow }} s'\) denotes that there are states \(s_0, \ldots , s_n\) such that \(s = s_0\), \(s_n = s'\), and \((s_{i1}, a_i, s_i) \in \varDelta \) for \(1 \le i \le n\). The notation \(s \mathrel {{}\,a_1 \cdots a_n{\rightarrow }}\) denotes that there is \(s'\) such that \(s \mathrel {{}\,a_1 \cdots a_n{\rightarrow }} s'\). The set of enabled actions of s is defined as \(\mathsf {en}(s) = \{ a \in \varSigma \cup \{\tau \} \mid s \mathrel {{}\,a{\rightarrow }} \}\).

\(S' \ =\ \{ s \in S \mid \exists \sigma \in (\varSigma \cup \{\tau \})^*: \hat{s} \mathrel {{}\,\sigma {\rightarrow }} s \}\) and

\(\varDelta ' \ =\ \{ (s,a,s') \in \varDelta \mid s \in S' \}\).

\((s_1,a,s'_1) \in \varDelta _1\), \(s'_2 = s_2 \in S_2\), and \(a \notin \varSigma _2\),

\((s_2,a,s'_2) \in \varDelta _2\), \(s'_1 = s_1 \in S_1\), and \(a \notin \varSigma _1\), or

\((s_1,a,s'_1) \in \varDelta _1\), \((s_2,a,s'_2) \in \varDelta _2\), and \(a \in \varSigma _1 \cap \varSigma _2\).
That is, if a belongs to the alphabets of both components, then an atransition of the parallel composition consists of simultaneous atransitions of both components. If a belongs to the alphabet of one but not the other component, then that component may make an atransition while the other component stays in its current state. Also each \(\tau \)transition of the parallel composition consists of one component making a \(\tau \)transition without the other participating. The result of the parallel composition is pruned by only taking the reachable part.
It is easy to check that \((L_1 \,\,L_2) \,\,L_3\) is isomorphic to \(L_1 \,\,(L_2 \,\,L_3)\). This means that \(\,\,\) can be considered associative, and that \(L_1 \,\,\cdots \,\,L_n\) is welldefined for any positive integer n.
The hiding of an action set A in L is denoted with \(L{\setminus }A\). It is \(L{\setminus }A = (S, \varSigma ', \varDelta ', \hat{s})\), where \(\varSigma ' = \varSigma {\setminus }A\) and \(\varDelta ' = \{ (s,a,s') \in \varDelta \mid a \notin A \}\cup \{ (s,\tau ,s') \mid \exists a \in A: (s,a,s') \in \varDelta \}\). That is, labels of transitions that are in A are replaced by \(\tau \) and removed from the alphabet. Other labels of transitions are not affected.
Let L be an LTS, \(K \subseteq \varSigma ^+\), and \(s \in S\). The state s refuses K if and only if for every \(\sigma \in K\) we have \(\lnot (s \mathrel {{=}\,\sigma {\Rightarrow }})\). For example, \(\hat{s}\) refuses K if and only if \(K \cap \mathsf {Tr}(L) = \emptyset \). Because \(s \mathrel {{=}\,\varepsilon {\Rightarrow }}\) holds vacuously for every state s, this definition is equivalent to what would be obtained with \(K \subseteq \varSigma ^*\). The pair \((\sigma , K) \in \varSigma ^* \times 2^{\varSigma ^+}\) is a tree failure of L, if and only if there is \(s \in S\) such that \(\hat{s} \mathrel {{=}\,\sigma {\Rightarrow }} s\) and s refuses K. The set of tree failures of L is denoted with \(\mathsf {Tf}(L)\). The LTSs \(L_1\) and \(L_2\) are tree failure equivalent if and only if \(\varSigma _1 = \varSigma _2\) and \(\mathsf {Tf}(L_1) = \mathsf {Tf}(L_2)\).
To define the main equivalence of this publication, we also need the following notation: For \(\rho \in \varSigma ^*\) and \(K \subseteq \varSigma ^*\), we write \(\rho ^{1}K\) for \(\{ \pi \mid \rho \pi \in K \}\) and call \(\rho \) a prefix of K if \(\rho ^{1}K\ne \emptyset \).
Definition 1
 1.
\(\varSigma _1 = \varSigma _2\),
 2.
if \((\sigma , K) \in \mathsf {Tf}(L_1)\), then either \((\sigma , K) \in \mathsf {Tf}(L_2)\) or there is a prefix \(\rho \) of K such that \((\sigma \rho , \rho ^{1}K) \in \mathsf {Tf}(L_2)\), and
 3.
Part 2 holds with the roles of \(L_1\) and \(L_2\) swapped.
If \(K \ne \emptyset \), then the first option “\((\sigma , K) \in \mathsf {Tf}(L_2)\)” implies the other by letting \(\rho = \varepsilon \). Therefore, the “either”part could equivalently be written as “\(K = \emptyset \) and \((\sigma , \emptyset ) \in \mathsf {Tf}(L_2)\)”. The way it has been written makes it easy to see that tree failure equivalence implies fair testing equivalence.
If \(L_1\) and \(L_2\) are fair testing equivalent, then \(\sigma \in \mathsf {Tr}(L_1)\) implies by the definitions that \((\sigma , \emptyset ) \in \mathsf {Tf}(L_1)\), \((\sigma , \emptyset ) \in \mathsf {Tf}(L_2)\), and \(\sigma \in \mathsf {Tr}(L_2)\). So fair testing equivalence implies trace equivalence and cannot have better reduction methods.
3 The TracePreserving Strong Stubborn Set Method

\(\bar{\varSigma }_i \ =\ \varSigma _i \cup \{\tau _i\}\) and

\(\bar{\varDelta }_i \ =\ \{ (s,a,s') \mid a \in \varSigma _i \wedge (s,a,s') \in \varDelta _i \} \cup \{ (s, \tau _i ,s') \mid (s, \tau ,s') \in \varDelta _i \}\).

\(\bar{L} \ =\ \bar{L}_1 \,\,\cdots \,\,\bar{L}_m\),

\(V \ =\ \varSigma {\setminus }A\) (the set of visible actions), and

\(I \ =\ (\varSigma \cap A) \cup \{\tau _1, \ldots , \tau _m\}\) (the set of invisible actions).
Now we can write \(L' \ =\ (\bar{L}_1 \,\,\cdots \,\,\bar{L}_m){\setminus }I \ =\ \bar{L}{\setminus }I\).
It is obvious from the definitions that \(L'\) is the same LTS as L. The only difference between \(\bar{L}\) and \(L_1 \,\,\cdots \,\,L_m\) is that the \(\tau \)transitions of the latter are \(\tau _i\)transitions of the former, where i reveals the \(L_i\) from which the transition originates. The hiding of I makes them \(\tau \)transitions again. We have \(V \cap I = \emptyset \), \(V \cup I = \bar{\varSigma }= \varSigma \cup \{\tau _1, \ldots , \tau _m\}\), and \(\bar{L}\) has no \(\tau \)transitions at all (although it may have \(\tau _i\)transitions). Therefore, when discussing the tracepreserving strong stubborn set method, the elements of V and I are called visible and invisible, respectively.
The method is based on a function \(\mathcal {T}\) that assigns to each \(s \in S\) a subset of \(\bar{\varSigma }\), called stubborn set. Before discussing the definition of \(\mathcal {T}\), let us see how it is used. The stubborn set method computes a subset of S called \(S_\mathsf {r}\) and a subset of \(\varDelta \) called \(\varDelta _\mathsf {r}\). It starts by letting \(S_\mathsf {r} = \{\hat{s}\}\) and \(\varDelta _\mathsf {r} = \emptyset \). For each s that it has put to \(S_\mathsf {r}\) and for each \(a \in \mathcal {T}(s)\), it puts to \(S_\mathsf {r}\) every \(s'\) that satisfies \((s,a,s') \in \bar{\varDelta }\) (unless \(s'\) is already in \(S_\mathsf {r}\)). Furthermore, it puts \((s,a',s')\) to \(\varDelta _\mathsf {r}\) (even if \(s'\) is already in \(S_\mathsf {r}\)), where \(a' = \tau \) if \(a \in I\) and \(a' = a\) otherwise. The only difference to the computation of \(L'\) is that in the latter, every \(a \in \bar{\varSigma }\) is used instead of every \(a \in \mathcal {T}(s)\).
The LTS \(L_\mathsf {r} = (S_\mathsf {r}, \varSigma , \varDelta _\mathsf {r}, \hat{s})\) is the reduced LTS, while \(L = L' = (S, \varSigma , \varDelta , \hat{s})\) is the full LTS. We will refer to concepts in \(L_\mathsf {r}\) with the prefix “r”, and to L with “f”. For instance, if \(s \in S_\mathsf {r}\) and \(\lnot (s \mathrel {{=}\,\sigma {\Rightarrow }})\) holds in \(L_\mathsf {r}\) for all \(\sigma \in K\), then s is an rstate and s rrefuses K. Because \(S_\mathsf {r} \subseteq S\) and \(\varDelta _\mathsf {r} \subseteq \varDelta \), every rstate is also an fstate and every rtrace is an ftrace. We will soon state conditions on \(\mathcal {T}\) that guarantee that also the opposite holds, that is, every ftrace is an rtrace.
Typically many different functions could be used as \(\mathcal {T}\), and the choice between them involves tradeoffs. For example, a function may be easy and fast to compute, but it may also tend to give worse reduction results (that is, bigger \(S_\mathsf {r}\) and \(\varDelta _\mathsf {r}\)) than another more complex function. Therefore, we will not specify a unique function \(\mathcal {T}\). Instead, in the remainder of this section we will only give four conditions that it must satisfy, and in the next section we will discuss how a reasonably good \(\mathcal {T}\) is computed quickly.

D1 If \(a \in \mathcal {T}(s)\), \(a_1, \ldots , a_n\) are not in \(\mathcal {T}(s)\), and \(s \mathrel {{}\,a_1 \cdots a_n a{\rightarrow }} s'_n\), then \(s \mathrel {{}\,a a_1 \cdots a_n{\rightarrow }} s'_n\).

D2 If \(a \in \mathcal {T}(s)\), \(a_1, \ldots , a_n\) are not in \(\mathcal {T}(s)\), \(s \mathrel {{}\,a{\rightarrow }} s'\), and \(s \mathrel {{}\,a_1 \cdots a_n{\rightarrow }} s_n\), then there is \(s'_n\) such that \(s' \mathrel {{}\,a_1 \cdots a_n{\rightarrow }} s'_n\) and \(s_n \mathrel {{}\,a{\rightarrow }} s'_n\).

V If \(\mathcal {T}(s) \cap V \cap \mathsf {en}(s) \ne \emptyset \), then \(V \subseteq \mathcal {T}(s)\).

S For each \(a \in V\) there is an rstate \(s_a\) and an rpath from s to \(s_a\) such that \(a \in \mathcal {T}(s_a)\).
Intuitively, D1 says two things. First, it says that a sequence of actions that are not in the current stubborn set (\(a_1 \cdots a_n\) in the definition) cannot enable an action that is in the current stubborn set (a in the definition). That is, disabled actions in a stubborn set remain disabled while actions outside the set occur. Second, together with D2 it says that the enabled actions inside the current stubborn set are in a certain kind of a commutativity relation with enabled sequences of outside actions. In theories where actions are deterministic (that is, for every s, \(s_1\), \(s_2\), and a, \(s \mathrel {{}\,a{\rightarrow }} s_1\) and \(s \mathrel {{}\,a{\rightarrow }} s_2\) imply \(s_1 = s_2\)), the thenpart of D2 is usually written simply as \(s_n \mathrel {{}\,a{\rightarrow }}\). It, D1, and determinism imply our current version of D2. However, we do not assume that actions are deterministic.
Certain partialorder semantic models of concurrency use a socalled independence relation [9]. Unlike in the present study, actions are assumed to be deterministic. If \(a_1\) and \(a_2\) are independent, then (1) if \(s \mathrel {{}\,a_1{\rightarrow }} s_1\) and \(s \mathrel {{}\,a_2{\rightarrow }} s_2\), then there is an \(s'\) such that \(s_1 \mathrel {{}\,a_2{\rightarrow }} s'\) and \(s_2 \mathrel {{}\,a_1{\rightarrow }} s'\); (2) if \(s \mathrel {{}\,a_1 a_2{\rightarrow }}\) then \(s \mathrel {{}\,a_2{\rightarrow }}\); and (3) if \(s \mathrel {{}\,a_2 a_1{\rightarrow }}\) then \(s \mathrel {{}\,a_1{\rightarrow }}\). It is often claimed that ample, persistent, and stubborn set methods rely on an independence relation. This is why they are classified as “partialorder methods”. In reality, they rely on various strictly weaker relations. For instance, even if determinism is assumed, D1 and D2 do not imply independence of \(a_1\) from a, because they fail to yield (3).

D0 If \(\mathsf {en}(s) \ne \emptyset \), then \(\mathcal {T}(s) \cap \mathsf {en}(s) \ne \emptyset \).
That is, if s is not a deadlock, then \(\mathcal {T}(s)\) contains an enabled action. We skip the (actually simple) proof that D0, D1, and D2 guarantee that deadlocks are preserved, see [16].
The condition V says that if the stubborn set contains an enabled visible action, then it contains all visible actions (also disabled ones). It guarantees that the reduction preserves the ordering of visible actions, in a sense that will become clear in the proof of Lemma 3.
The function \(\mathcal {T}_\emptyset \) that always returns the empty set satisfies D1, D2, and V. Its use as \(\mathcal {T}\) would result in a reduced LTS that has one state and no transitions. It is thus obvious that D1, D2, and V alone do not guarantee that the reduced LTS has the same traces as the full LTS.
The condition S forces the method to investigate, intuitively speaking, everything that is relevant for the preservation of the traces. It does that by guaranteeing that every visible action is taken into account, not necessarily in the current state but necessarily in a state that is rreachable from the current state. Taking always all visible actions into account in the current state would make the reduction results much worse. The name is S because, historically, a similar condition was first used to guarantee the preservation of what is called safety properties in the linear temporal logic framework. Again, the details of how S does its job will become clear in the proof of Lemma 3.
If \(V = \emptyset \), then \(\mathcal {T}_\emptyset \) satisfies also S. Indeed, then \(\mathsf {Tr}(L) = \{\varepsilon \} = \mathsf {Tr}(L_\mathsf {r})\) even if \(L_\mathsf {r}\) is the onestate LTS that has no transitions. That is, if \(V = \emptyset \), then \(\mathcal {T}_\emptyset \) satisfies the definition and yields ideal reduction results.
No matter what V is, the function \(\mathcal {T}(s) = \bar{\varSigma }\) always satisfies D1, D2, V, and S. However, it does not yield any reduction. The problem of computing sets that satisfy D1, D2, V, and S and do yield reduction will be discussed in Sect. 4. In Sect. 6 we prove that D1, D2, V, and S guarantee that the reduced LTS is fair testing equivalent (and thus also trace equivalent) to the full LTS.
4 On Computing TracePreserving Stubborn Sets
To make the abstract theory in the remainder of this publication more concrete, we present in this section one new good way of computing sets that satisfy D1, D2, V, and S. It is based on earlier ideas but has been finetuned for the present situation. We emphasize that it is not the only good way. Other possibilities have been discussed in [17, 20], among others.
Because the expression under analysis is of the form \((\bar{L}_1 \,\,\cdots \,\,\bar{L}_m){\setminus }I\), its states are of the form \((s_1, \ldots , s_m)\), where \(s_i \in L_i\) for each \(1 \le i \le m\). We employ the notation \(\mathsf {en}_i(s_i) = \{ a \mid \exists s'_i: (s_i,a,s'_i) \in \varDelta _i\}\), that is, the set of actions that are enabled in \(s_i\) in \(L_i\). We have \(\tau \notin \mathsf {en}_i(s_i) \subseteq \bar{\varSigma }_i = \varSigma _i \cup \{\tau _i\}\). Furthermore, if \(a \notin \mathsf {en}(s)\), then there is at least one i such that \(a \in \bar{\varSigma }_i\) and \(a \notin \mathsf {en}_i(s_i)\). Let \(\mathsf {dis}(s,a)\) denote the smallest such i.
We start by presenting a sufficient condition for D1 and D2 that does not refer to other states than the current.
Theorem 2
 1.
If \(a \notin \mathsf {en}(s)\), then there is i such that \(a \in \bar{\varSigma }_i\) and \(a \notin \mathsf {en}_i(s_i) \subseteq \mathcal {T}(s)\).
 2.
If \(a \in \mathsf {en}(s)\), then for every i such that \(a \in \bar{\varSigma }_i\) we have \(\mathsf {en}_i(s_i) \subseteq \mathcal {T}(s)\).
Then \(\mathcal {T}(s)\) satisfies D1 and D2.
Proof
Let \(a_1 \notin \mathcal {T}(s)\), ..., \(a_n \notin \mathcal {T}(s)\).
Let first \(a \notin \mathsf {en}(s)\). Obviously \(s \mathrel {{}\,a{\rightarrow }}\) does not hold, so D2 is vacuously true. We prove now that D1 is as well. By assumption 1, there is i such that \(L_i\) disables a and \(\mathsf {en}_i(s_i) \subseteq \mathcal {T}(s)\). To enable a, it is necessary that \(L_i\) changes its state, which requires that some action in \(\mathsf {en}_i(s_i)\) occurs. These are all in \(\mathcal {T}(s)\) and thus distinct from \(a_1\), ..., \(a_n\). So \(s \mathrel {{}\,a_1 \cdots a_n a{\rightarrow }}\) cannot hold.
Let now \(a \in \mathsf {en}(s)\). Our next goal is to show that there are no \(1 \le k \le n\) and \(1 \le j \le m\) such that both \(a \in \bar{\varSigma }_j\) and \(a_k \in \bar{\varSigma }_j\). To derive a contradiction, consider a counterexample where k has the smallest possible value. So none of \(a_1, \ldots , a_{k1}\) is in \(\bar{\varSigma }_j\). If \(s \mathrel {{}\,a_1 \cdots a_n{\rightarrow }}\), then there is \(s'\) such that \(s \mathrel {{}\,a_1 \cdots a_{k1}{\rightarrow }} s' \mathrel {{}\,a_k{\rightarrow }}\). Obviously \(a_k \in \mathsf {en}_j(s'_j)\). This implies \(a_k \in \mathsf {en}_j(s_j)\), because \(L_j\) does not move between s and \(s'\) since none of \(a_1, \ldots , a_{k1}\) is in \(\bar{\varSigma }_j\). By assumption 2, \(\mathsf {en}_j(s_j) \subseteq \mathcal {T}(s)\). This contradicts \(a_k \notin \mathcal {T}(s)\).
This means that the \(L_j\) that participate in a are disjoint from the \(L_j\) that participate in \(a_1 \cdots a_n\). From this D1 and D2 follow by wellknown properties of the parallel composition operator. \(\square \)
Theorem 2 makes it easy to represent a sufficient condition for D1 and D2 as a directed graph that depends on the current state s. The set of the vertices of the graph is \(\bar{\varSigma }\). There is an edge from \(a \in \bar{\varSigma }\) to \(b \in \bar{\varSigma }\), denoted with \(a \leadsto b\), if and only if either \(a \notin \mathsf {en}(s)\) and \(b \in \mathsf {en}_i(s_i)\) where \(i = \mathsf {dis}(s,a)\), or \(a \in \mathsf {en}(s)\) and there is i such that \(a \in \bar{\varSigma }_i\) and \(b \in \mathsf {en}_i(s_i)\). By the construction, if \(\mathcal {T}(s)\) is closed under the graph (that is, for every a and b, if \(a \in \mathcal {T}(s)\) and \(a \leadsto b\), then \(b \in \mathcal {T}(s)\)), then \(\mathcal {T}(s)\) satisfies D1 and D2.
It is not necessary for correctness to use the smallest i, when more than one \(L_i\) disables a. The choice to use the smallest i was made to obtain a fast algorithm. An alternative algorithm (called deletion algorithm in [17]) is known that exploits the freedom to choose any i that disables a. It has the potential to yield smaller reduced LTSs than the algorithm described in this section. On the other hand, it consumes more time per constructed state.
Furthermore, the condition in Theorem 2 is not the weakest possible, as shown by the following useful observation: Assume a writes to a finitecapacity fifo \(L_f\), \(\bar{a}\) reads from it, and they have no other \(L_i\) in common; although \(\bar{\varSigma }_f\) links them, we need not declare \(a \leadsto \bar{a}\) when a is enabled, and we need not declare \(\bar{a} \leadsto a\) when \(\bar{a}\) is enabled, since they commute if both are enabled. Trying to make the condition as weak as possible would have made it very hard to read.
It is trivial to also take the condition V into account in the graph representation of the stubborn set computation problem. It suffices to add the edge \(a \leadsto b\) from each \(a \in V \cap \mathsf {en}(s)\) to each \(b \in V\).
Let “\(\leadsto ^*\)” denote the reflexive transitive closure of “\(\leadsto \)”. By the definitions, if \(a \in \bar{\varSigma }\), then \(\{ b \mid a \leadsto ^* b \}\) satisfies D1, D2, and V. We denote it with \(\mathsf {clsr}(a)\). It can be computed quickly with wellknown elementary graph search algorithms.
However, we can do better. The better algorithm is denoted with \(\mathsf {esc}(a)\), for “enabled strong component”. Applied at some state s, it uses a as the starting point of a depthfirst search in (\(\bar{\varSigma }\), “\(\leadsto \)”). During the search, the strong components (i.e., the maximal strongly connected subgraphs) of (\(\bar{\varSigma }\), “\(\leadsto \)”) are recognized using Tarjan’s algorithm [4, 13]. It recognizes each strong component at the time of backtracking from it. When \(\mathsf {esc}(a)\) finds a strong component C that contains an action enabled at s, it stops and returns C as the result; note that a might not be in C. In principle, the result should also contain actions that are reachable from C but are not in C. However, they are all disabled, so leaving them out does not change \(L_\mathsf {r}\), which we are really interested in. If \(\mathsf {esc}(a)\) does not find such a strong component, it returns \(\emptyset \).
Obviously \(\mathsf {esc}(a) \subseteq \mathsf {clsr}(a)\). So \(\mathsf {esc}(a)\) has potential for better reduction results. Tarjan’s algorithm adds very little overhead to depthfirst search. Therefore, \(\mathsf {esc}(a)\) is never much slower than \(\mathsf {clsr}(a)\). On the other hand, it may happen that \(\mathsf {esc}(a)\) finds a suitable strong component early on, in which case it is much faster than \(\mathsf {clsr}(a)\).
To discuss the implementation of S, let \(V = \{a_1, \ldots , a_{V}\}\). Let S(s, i) denote that there is an \(s_i\) and an rpath from s to \(s_i\) such that \(a_i \in \mathcal {T}(s_i)\). Our algorithm constructs \(L_\mathsf {r}\) in depthfirst order. The root of a strong component C of \(L_\mathsf {r}\) is the state in C that was found first. Our algorithm recognizes the roots with Tarjan’s algorithm. In each root \(s_C\), it enforces S\((s_C,i)\) for each \(1 \le i \le n\) in a manner which is discussed below. This suffices, because if S(s, i) holds for one state in a strong component, then it clearly holds for every state in the component.
Each state s has an attribute \(\nu \) such that if \(\nu > V\), then S(s, i) is known to hold for \(a_1, \ldots , a_{\nu V}\). When a state is processed for the first time, its \(\nu \) value is set to 1 and \(\mathsf {esc}(a_1)\) is used as its stubborn set. When the algorithm is about to backtrack from a root \(s_C\), it checks its \(\nu \) value. The algorithm actually backtracks from a root only when \(\nu = 2V\). Otherwise it increments \(\nu \) by one. Then it extends \(\mathcal {T}(s_C)\) by \(\mathsf {esc}(a_{\nu })\) if \(\nu \le V\), and by \(\mathsf {clsr}(a_{\nu V})\) if \(V < \nu \le 2V\). The extension may introduce new outgoing transitions for \(s_C\), and \(s_C\) may cease from being a root. If \(s_C\) remains a root, then its \(\nu \) eventually grows to 2V and S holds for \(s_C\). The purpose of making \(\mathcal {T}(s_C)\) grow in steps with \(\mathsf {esc}\)sets first is to obtain as small a stubborn set as possible, if \(s_C\) ceases from being a root.
During the depthfirst search, information on \(\nu \)values is backward propagated and the maximum is kept. This way, if \(s_C\) ceases from being a root, the new root benefits from the work done at \(s_C\). Furthermore, nonterminal strong components automatically get \(\nu = 2V\). To exploit situations where \(V \subseteq \mathcal {T}(s)\) by condition V, if a visible action is in \(\mathsf {en}(s) \cap \mathcal {T}(s)\), then the algorithm makes the \(\nu \) value of s be 2V.
 1.
Try to make the system always mayterminating.
 2.
Construct \(L'_\mathsf {r}\) obeying D0, D1, D2, and V.
 3.
If \(L'_\mathsf {r}\) is always mayterminating, then extract a reduced LTS for the original system from \(L'_\mathsf {r}\) as will be described in Sect. 7. Otherwise, go back to 1.
Stubborn sets obeying D0, D1, D2, and V can be computed by, in each state that is not a deadlock, choosing an enabled a and computing \(\mathsf {esc}(a)\).
5 On the Performance of Various Conditions
The goal of aps set methods is to alleviate the state explosion problem. Therefore, reducing the size of the state space is a main issue. However, if the reduction introduces too much additional work per preserved state, then time is not saved. So the cost of computing the aps set is important. Also the software engineering issue plays a role. Little is known on the practical performance of ideas that have the biggest theoretical reduction potential, because they are complicated to implement, so few experiments have been made. For instance, first big experiments on weak stubborn sets [17] and the deletion algorithm [17] appeared in [8].
Often a state has more than one aps set. Let \(T_1\) and \(T_2\) be two of them and let \(\mathcal {E}(T_1)\) and \(\mathcal {E}(T_2)\) be the sets of enabled transitions in \(T_1\) and \(T_2\). It is obvious that if the goal is to preserve deadlocks and if \(\mathcal {E}(T_1) \subseteq \mathcal {E}(T_2)\), then \(T_1\) can lead to better but cannot lead to worse reduction results than \(T_2\). We are not aware of any significant result on the question which should be chosen, \(T_1\) or \(T_2\), if both are aps, \(\mathcal {E}(T_1) \not \subseteq \mathcal {E}(T_2)\), and \(\mathcal {E}(T_2) \not \subseteq \mathcal {E}(T_1)\). Let us call it the nonsubset choice problem. Already [15] gave an example where always choosing the set with the smallest number of enabled transitions does not yield the best reduction result.
We now demonstrate that the order in which the components of a system are given to a tool can have a tremendous effect on the running time and the size of the reduced state space. Assume that \(L_1 \,\,\cdots \,\,L_m\) has deadlocks. Consider \(L_1 \,\,\cdots \,\,L_m \,\,L_{m+1}\), where \(L_{m+1} =\) Open image in new window . This extended system has no deadlocks. If the deadlockpreserving stubborn set method always investigates \(L_{m+1}\) last, then it finds the deadlocks of the original system in the original fashion, finds that \(L_{m+1}\) is enabled in them, and eventually concludes that the system has no deadlocks. So it does approximately the same amount of work as it does with \(L_1 \,\,\cdots \,\,L_m\). If, in the initial state \(\hat{s}\), the method happens to investigate \(L_{m+1}\) first, it finds a \(\tau \)loop \(\hat{s} \mathrel {{}\,\tau {\rightarrow }} \hat{s}\). D0, D1, and D2 do not tell it to investigate anything else. So it stops extremely quickly, after constructing only one state.
For this and other reasons, measurements are not as reliable for comparing different methods as we would like them to be.
Technically, optimal sets could be defined as those (not necessarily aps) sets of enabled transitions that yield the smallest reduced state space that preserves the deadlocks. Unfortunately, it was shown in [20] that finding subsets of transitions of a 1safe Petri net that are optimal in this sense is at least as hard as testing whether the net has a deadlock. Another similar result was proven in [2, p. 154]. Therefore, without additional assumptions, optimal sets are too hard to find.
The situation is much more complicated when preserving other properties than deadlocks. We only discuss one difficulty. Instead of S, [2, p. 155] assumes that the reduced state space is constructed in depthfirst order and tells to choose an aps set that does not close a cycle if possible, and otherwise use all enabled transitions. Figure 2 shows an example where this condition leads to the construction of all reachable states, although the processes do not interact at all. The condition S is less vulnerable to but not totally free from this kind of difficulties. Far too little is known on this problem area.
The approach in Sects. 4 and 7 that does not use S is entirely free of this difficulty. This is one reason why it seems very promising.
In general, it is reasonable to try to find as weak conditions as possible in place of D1, V, S, and so on, because the weaker a condition is, the more potential it has for good reduction results. Because of the nonsubset choice problem and other similar problems, it is not certain that the potential can be exploited in practice. However, if the best set is ruled out already by the choice of the condition, then it is certain that it cannot be exploited.
For instance, instead of V, [2, p. 149] requires that if \(\mathcal {T}(s) \cap V \cap \mathsf {en}(s) \ne \emptyset \), then \(\mathcal {T}(s)\) must contain all enabled transitions. This condition is strictly stronger than V and thus has less potential for reduction. Furthermore, the algorithm in Sect. 4 can exploit the additional potential of V at least to some extent.
This also illustrates why stubborn sets are defined such that they may contain disabled transitions. The part \(V \subseteq \mathcal {T}(s)\) in the definition of condition V could not be formulated easily, or perhaps not at all, if \(\mathcal {T}(s)\) cannot contain disabled transitions. The following example reveals both that \(V \cap \mathsf {en}(s) \subseteq \mathcal {T}(s)\) fails (it loses the trace b) and that V yields better reduction than the condition in [2] (\(\{a,b,u,\tau _2\}\) is stubborn, satisfies V, but \(\tau _3 \in \mathsf {en}(s) \not \subseteq \{a,b,u,\tau _2\}\)):
6 The Fair Testing Equivalence Preservation Theorem
Lemma 3
Assume that \(n \in \mathbb {N}\), \(s_n \in S_\mathsf {r}\), \(s'_n \in S\), \(\varepsilon \ne \sigma _n \in V^*\), and there is an fpath of length n from \(s_n\) to \(s'_n\) such that its trace is \(\sigma _n\). There are \(s_{n1} \in S_\mathsf {r}\), \(s'_{n1} \in S\), \(\lambda _{n1} \in V \cup \{\varepsilon \}\), and \(\sigma _{n1} \in V^*\) such that \(\lambda _{n1} \sigma _{n1} = \sigma _n\), \(s_n \mathrel {{=}\,\lambda _{n1}{\Rightarrow }} s_{n1}\) in \(L_\mathsf {r}\), \(s'_n \mathrel {{=}\,\varepsilon {\Rightarrow }} s'_{n1}\) in L, and there is an fpath of length \(n1\) from \(s_{n1}\) to \(s'_{n1}\) such that its trace is \(\sigma _{n1}\).
Proof
Let \(s_{0,0} = s_n\) and \(s_{0,n} = s'_n\). Let the fpath of length n be \(s_{0,0} \mathrel {{}\,a_1 \cdots a_n{\rightarrow }}\) \(s_{0,n}\). Because \(\sigma _n \ne \varepsilon \), there is a smallest v such that \(1 \le v \le n\) and \(a_v \in V\). By S, there are \(k \in \mathbb {N}\), \(s_{1,0}, \ldots , s_{k,0}\), and \(b_1, \ldots , b_k\) such that \(a_v \in \mathcal {T}(s_{k,0})\) and \(s_{0,0} \mathrel {{}\,b_1{\rightarrow }} s_{1,0} \mathrel {{}\,b_2{\rightarrow }} \ldots \mathrel {{}\,b_k{\rightarrow }} s_{k,0}\) in \(L_\mathsf {r}\). Let h be the smallest natural number such that \(\{a_1, \ldots , a_n\} \cap \mathcal {T}(s_{h,0}) \ne \emptyset \). Because \(a_v \in \mathcal {T}(s_{k,0})\), we have \(0 \le h \le k\). By h applications of D2 at \(s_{0,0}, \ldots , s_{h1,0}\), there are \(s_{1,n}, \ldots , s_{h,n}\) such that \(s_{i,0} \mathrel {{}\,a_1 \cdots a_n{\rightarrow }} s_{i,n}\) in L for \(1 \le i \le h\) and \(s_{0,n} \mathrel {{}\,b_1{\rightarrow }} s_{1,n} \mathrel {{}\,b_2{\rightarrow }} \ldots \mathrel {{}\,b_h{\rightarrow }} s_{h,n}\) in L. If \(b_i \in V\) for some \(1 \le i \le h\), then \(V \subseteq \mathcal {T}(s_{i1,0})\) by V. It yields \(a_v \in \mathcal {T}(s_{i1,0})\), which contradicts the choice of h. As a consequence, \(s_{0,0} \mathrel {{=}\,\varepsilon {\Rightarrow }} s_{h,0}\) in \(L_\mathsf {r}\) and \(s_{0,n} \mathrel {{=}\,\varepsilon {\Rightarrow }} s_{h,n}\) in L.
Because \(\{a_1, \ldots , a_n\} \cap \mathcal {T}(s_{h,0}) \ne \emptyset \), there is a smallest i such that \(1 \le i \le n\) and \(a_i \in \mathcal {T}(s_{h,0})\). By D1 at \(s_{h,0}\), there is \(s_{n1}\) such that \(s_{h,0} \mathrel {{}\,a_i{\rightarrow }} s_{n1}\) in \(L_\mathsf {r}\) and \(s_{n1} \mathrel {{}\,a_1 \cdots a_{i1} a_{i+1} \cdots a_n{\rightarrow }} s_{h,n}\) in L. We choose \(s'_{n1} = s_{h,n}\) and let \(\sigma _{n1}\) be the trace of \(a_1 \cdots a_{i1} a_{i+1} \cdots a_n\). If \(a_i \notin V\), then we choose \(\lambda _{n1} = \varepsilon \), yielding \(\lambda _{n1} \sigma _{n1} = \sigma _n\). If \(a_i \in V\), then \(V \subseteq \mathcal {T}(s_{h,0})\) by V, so none of \(a_1, \ldots , a_{i1}\) is in V, and by choosing \(\lambda _{n1} = a_i\) we obtain \(\lambda _{n1} \sigma _{n1} = \sigma _n\). That \(s_n \mathrel {{=}\,\lambda _{n1}{\Rightarrow }} s_{n1}\) in \(L_\mathsf {r}\) follows from \(s_{0,0} \mathrel {{=}\,\varepsilon {\Rightarrow }} s_{h,0} \mathrel {{}\,a_i{\rightarrow }} s_{n1}\) in \(L_\mathsf {r}\). The rest of the claim is obtained by replacing \(s'_n\) for \(s_{0,n}\) and \(s'_{n1}\) for \(s_{h,n}\) in already proven facts. \(\square \)
Lemma 4
Let \(n \in \mathbb {N}\). Assume that \(s \in S_\mathsf {r}\), \(s' \in S\), \(\sigma \in V^*\), and \(s \mathrel {{=}\,\sigma {\Rightarrow }} s'\) in L due to an fpath of length n. Then there are \(z \in S_\mathsf {r}\) and \(z' \in S\) such that \(s \mathrel {{=}\,\sigma {\Rightarrow }} z\) in \(L_\mathsf {r}\), \(z \mathrel {{=}\,\varepsilon {\Rightarrow }} z'\) in L, and \(s' \mathrel {{=}\,\varepsilon {\Rightarrow }} z'\) in L.
Proof
The proof is by induction on n. We start with the observation that, in case \(\sigma = \varepsilon \), the claim holds with choosing \(z=s\) and \(z'=s'\). This settles the base case \(n=0\) and a subcase of the induction step, and it leaves us with the case \(n>0\) and \(\sigma \ne \varepsilon \).
We apply Lemma 3 and get \(s_1 \in S_\mathsf {r}\), \(s_1' \in S\), \(\sigma _1 \in V^*\), and \(\lambda _{1} \in V \cup \{\varepsilon \}\) such that \(\lambda _{1}\sigma _{1} = \sigma \), \(s \mathrel {{=}\,\lambda _{1}{\Rightarrow }} s_{1}\) in \(L_\mathsf {r}\), and \(s' \mathrel {{=}\,\varepsilon {\Rightarrow }} s'_{1}\) in L. Furthermore, \(s_1 \mathrel {{=}\,\sigma _1{\Rightarrow }} s_1'\) in L due to an fpath of length \(n1\), for which the lemma holds; hence, there are \(z \in S_\mathsf {r}\) and \(z' \in S\) such that \(s_1 \mathrel {{=}\,\sigma _1{\Rightarrow }} z\) in \(L_\mathsf {r}\), \(z \mathrel {{=}\,\varepsilon {\Rightarrow }} z'\) in L, and \(s_1' \mathrel {{=}\,\varepsilon {\Rightarrow }} z'\) in L. Together, these also give \(s \mathrel {{=}\,\lambda _{1}{\Rightarrow }} s_{1} \mathrel {{=}\,\sigma _1{\Rightarrow }} z\) in \(L_\mathsf {r}\) and \(s' \mathrel {{=}\,\varepsilon {\Rightarrow }} s'_{1} \mathrel {{=}\,\varepsilon {\Rightarrow }} z'\) in L, so we are done. \(\square \)
Lemma 5
Assume that \(n \in \mathbb {N}\), \(s_n \in S_\mathsf {r}\), \(s'_n \in S\), \(\sigma _n \in V^*\), \(s_n \mathrel {{=}\,\sigma _n{\Rightarrow }}\) in \(L_\mathsf {r}\), and there is an fpath of length n from \(s_n\) to \(s'_n\) such that its trace is \(\varepsilon \). Either \(s'_n \mathrel {{=}\,\sigma _n{\Rightarrow }}\) in L or there are \(s_{n1} \in S_\mathsf {r}\), \(s'_{n1} \in S\), and \(\rho _{n1}\) such that \(\rho _{n1}\) is a prefix of \(\sigma _n\), \(s_n \mathrel {{=}\,\rho _{n1}{\Rightarrow }} s_{n1}\) in \(L_\mathsf {r}\), \(s'_n \mathrel {{=}\,\rho _{n1}{\Rightarrow }} s'_{n1}\) in L, and there is an fpath of length \(n1\) from \(s_{n1}\) to \(s'_{n1}\) such that its trace is \(\varepsilon \).
Proof
Let \(s_{0,0} = s_n\) and \(s_{0,n} = s'_n\). Let the fpath of length n be \(s_{0,0} \mathrel {{}\,a_1 \cdots a_n{\rightarrow }}\) \(s_{0,n}\); obviously, the \(a_i\) are invisible. By the assumption, there is a path \(s_{0,0} \mathrel {{}\,b_1{\rightarrow }}\) \(s_{1,0} \mathrel {{}\,b_2{\rightarrow }} \ldots \mathrel {{}\,b_k{\rightarrow }} s_{k,0}\) in \(L_\mathsf {r}\) such that its trace is \(\sigma _n\).
If \(\{a_1, \ldots , a_n\} \cap \mathcal {T}(s_{i,0}) = \emptyset \) for \(0 \le i < k\), then k applications of D2 yield \(s_{1,n}, \ldots , s_{k,n}\) such that \(s_{0,n} \mathrel {{}\,b_1{\rightarrow }} s_{1,n} \mathrel {{}\,b_2{\rightarrow }} \ldots \mathrel {{}\,b_k{\rightarrow }} s_{k,n}\) in L. This implies \(s'_n \mathrel {{=}\,\sigma _n{\Rightarrow }}\) in L.
Otherwise, there is a smallest h such that \(0 \le h < k\) and \(\{a_1, \ldots , a_n\} \cap \mathcal {T}(s_{h,0}) \ne \emptyset \). There also is a smallest i such that \(1 \le i \le n\) and \(a_i \in \mathcal {T}(s_{h,0})\). Applying D2 h times yields \(s_{1,n}, \ldots , s_{h,n}\) such that \(s_{0,n} \mathrel {{}\,b_1{\rightarrow }} \ldots \mathrel {{}\,b_h{\rightarrow }} s_{h,n}\) in L and \(s_{h,0} \mathrel {{}\,a_1 \cdots a_n{\rightarrow }} s_{h,n}\) in L. By D1 there is \(s_{n1}\) such that \(s_{h,0} \mathrel {{}\,a_i{\rightarrow }} s_{n1}\) in \(L_\mathsf {r}\) and \(s_{n1} \mathrel {{}\,a_1 \cdots a_{i1} a_{i+1} \cdots a_n{\rightarrow }} s_{h,n}\) in L. The claim follows by choosing \(s'_{n1} = s_{h,n}\) and letting \(\rho _{n1}\) be the trace of \(s_{0,0} \mathrel {{}\,b_1 \cdots b_h{\rightarrow }} s_{h,0}\). \(\square \)
Lemma 6
Let \(n \in \mathbb {N}\). Assume \(K\subseteq V^*\), \(\rho \in K\), \(z \in S_\mathsf {r}\), \(z' \in S\), and \(z \mathrel {{=}\,\varepsilon {\Rightarrow }} z'\) due to an fpath of length n; assume further that \(z'\) frefuses K and \(z \mathrel {{=}\,\rho {\Rightarrow }}\) in \(L_\mathsf {r}\). Then there exist \(s \in S_\mathsf {r}\) and a prefix \(\pi \) of K such that \(z \mathrel {{=}\,\pi {\Rightarrow }} s\) in \(L_\mathsf {r}\) and s rrefuses \(\pi ^{1} K\).
Proof
The proof is by induction on n. The case \(n=0\) holds vacuously, since it would imply \(z' \mathrel {{=}\,\rho {\Rightarrow }}\), contradicting \(\rho \in K\).
So we assume the lemma to hold for \(n1\), and also the assumptions in the lemma for n. We apply Lemma 5 to z, \(z'\), and \(\rho \). In the first case, we would again have the impossible \(z' \mathrel {{=}\,\rho {\Rightarrow }}\). So according to the second case, we have a \(z_1\), \(z'_1\), and prefix \(\rho '\) of \(\rho \) and thus of K with \(z \mathrel {{=}\,\rho '{\Rightarrow }} z_1\) in \(L_\mathsf {r}\), \(z' \mathrel {{=}\,\rho '{\Rightarrow }} z'_1\) in L, and \(z_1 \mathrel {{=}\,\varepsilon {\Rightarrow }} z'_1\) due to an fpath of length \(n1\).
Since \(z'\) frefuses K, \(z'_1\) must frefuse \(\rho '^{1} K\). If \(z_1\) rrefuses \(\rho '^{1} K\), we are done. Otherwise, we can apply the induction hypothesis to \(z_1 \mathrel {{=}\,\varepsilon {\Rightarrow }} z'_1\) and \(\rho '^{1} K\). This results in an \(s \in S_\mathsf {r}\) and a prefix \(\pi '\) of \(\rho '^{1} K\) such that \(z_1 \mathrel {{=}\,\pi '{\Rightarrow }} s\) in \(L_\mathsf {r}\) and s rrefuses \(\pi '^{1} \rho '^{1} K = (\rho '\pi ')^{1} K\). We also have that \(\rho '\pi '\) is a prefix of K and \(z \mathrel {{=}\,\rho '\pi '{\Rightarrow }} s\) in \(L_\mathsf {r}\), so we are done. \(\square \)
Theorem 7
The LTS \(L_\mathsf {r}\) is fair testing equivalent to L.
Proof
Part 1 of Definition 1 is immediate from the construction.
Let \((\sigma , K)\) be a tree failure of \(L_\mathsf {r}\). That is, there is \(s \in S_\mathsf {r}\) such that \(\hat{s} \mathrel {{=}\,\sigma {\Rightarrow }} s\) in \(L_\mathsf {r}\) and s rrefuses K. Consider any \(\rho \in V^*\) such that \(s \mathrel {{=}\,\rho {\Rightarrow }}\) in L. By Lemma 4, \(s \mathrel {{=}\,\rho {\Rightarrow }}\) also in \(L_\mathsf {r}\). This implies that s refuses K in L and that \((\sigma , K)\) is a tree failure of L. In conclusion, Part 2 of Definition 1 holds.
Let \((\sigma , K)\) be a tree failure of L. That is, there is \(s' \in S\) such that \(\hat{s} \mathrel {{=}\,\sigma {\Rightarrow }} s'\) in L and \(s'\) frefuses K. By Lemma 4 there are \(z \in S_\mathsf {r}\) and \(z' \in S\) such that \(\hat{s} \mathrel {{=}\,\sigma {\Rightarrow }} z\) in \(L_\mathsf {r}\), \(s' \mathrel {{=}\,\varepsilon {\Rightarrow }} z'\) in L, and \(z \mathrel {{=}\,\varepsilon {\Rightarrow }} z'\) in L. Since \(s'\) frefuses K, also \(z'\) frefuses K.
Either z rrefuses K and we are done, or we apply Lemma 6, giving us an \(s \in S_\mathsf {r}\) and a prefix \(\pi \) of K such that \(z \mathrel {{=}\,\pi {\Rightarrow }} s\) in \(L_\mathsf {r}\) and s rrefuses \(\pi ^{1} K\). Hence, \((\sigma \pi ,\pi ^{1} K) \in \mathsf {Tf}(L_\mathsf {r})\) and Part 3 of Definition 1 also holds. \(\square \)
Consider \((L_1 \,\,L_2){\setminus }\{u\}\), where \(L_1\) and \(L_2\) are shown in Fig. 5 left and middle. Initially two sets are stubborn: \(\{a\}\) and \(\{a, u, \tau _2\}\). If \(\{a\}\) is chosen, then the LTS is obtained that is shown with solid arrows on the right in Fig. 5. The full LTS also contains the dashed arrows. The full LTS has the tree failure \((\varepsilon , \{aa\})\) that the reduced LTS lacks.
7 Example
Because messages may be lost in the data channel, the alternating bit protocol has a timeout mechanism. For each message that it receives, the receiver sends back an acknowledgement message. After sending any message, the sender waits for the acknowledgement for a while. If it does not arrive in time, then the sender resends the message. To prevent the sender and receiver from being fooled by outdated messages, the messages carry a number that is 0 or 1.
The alternating bit protocol is impractical in that if either channel is totally broken, then the sender sends without limit in vain, so the protocol diverges. The variant in Fig. 6 avoids this problem. For each sen action, Sender tries sending at most a fixed number of times, which we denote with \(\ell \). (In the figure, \(\ell = 1\) for simplicity.) The protocol is expected to behave as follows. For each sen, it eventually replies with ok or err. If it replies with ok, it has delivered the data item with rec. If it replies with err, delivery is possible but not guaranteed, and it may occur before or after the err. There are no unsolicited or double deliveries. If the channels are not totally broken, the protocol cannot lose the ability to reply with ok.
After err, Sender does not know whether any data message got through and therefore it does not know which bit value Receiver expects next. For this reason, initially and after each err, the protocol performs a connection phase before attempting to deliver data items. It consists of sending a flush message and expecting an acknowledgement with the same bit value. When the acknowledgement comes, it is certain that there are no remnant messages with the opposite bit value in the system, so the use of that value for the next data message is safe. This is true despite the fact that the acknowledgement with the expected bit value may itself be a remnant message.
Assume that neither channel can lose infinitely many messages in a row. This is a typical fairness assumption. It guarantees that if there are infinitely many senactions, then infinitely many flush actions go through and infinitely many acknowledgements come back. However, it does not guarantee that any data message ever gets through. To guarantee that, it is necessary to further assume that if the acknowledgement channel delivers infinitely many messages, then eventually the data channel delivers at least one of the next \(\ell \) messages that have been sent via it after the acknowledgement channel delivered a message. This assumption is very unnatural, because it says that the channels must somehow coordinate the losses of messages.
As a consequence, the traditional approach of proving liveness that is based on fairness assumptions is not appropriate for this protocol. On the other hand, fair testing equivalence can be used to prove a weaker but nevertheless useful property: the protocol cannot lose the ability to deliver data items and reply ok. This is why the protocol was chosen for the experiments in this section.
Each channel consists of c separate cells. Times are in seconds
c  Full LTS  Full, with ttransitions  Stubborn sets  

States  Edges  Time  States  Edges  Time  States  Edges  Time  
1  380  1068  0.0  440  1254  0.1  372  700  0.0 
2  1880  6212  0.0  2224  7360  0.1  1234  1992  0.0 
3  9200  34934  0.1  10976  41560  0.1  2986  4382  0.0 
4  44000  188710  0.2  52672  224928  0.3  6104  8360  0.1 
5  205760  983614  0.5  246656  1173536  0.6  11140  14494  0.1 
6  944000  4977246  2.3  1132288  5941760  2.7  18726  23432  0.2 
7  4263680  24582270  11.4  5115392  29357952  13.8  29578  35906  0.2 
8  19013120  119011454  63.4  22813696  142177792  77.2  44496  52732  0.3 
10  90150  103124  0.4  
20  946520  1005784  3.6  
30  4083190  4238144  18.8  
40  11854160  12170204  68.2 
Each channel is a single reduced LTS
c  Full LTS  Full, with ttransitions  Stubborn sets  

States  Edges  Time  States  Edges  Time  States  Edges  Time  
10  42680  183912  0.3  51128  216300  0.4  16818  29756  0.2 
20  287280  1278742  2.1  344568  1502900  2.4  84928  144116  0.7 
30  913880  4112572  9.0  1096408  4831900  10.7  236438  391276  2.0 
40  2102480  9513402  25.9  2522648  11175300  30.6  503348  819236  4.6 
50  4033080  18309232  60.4  4839288  21505100  71.9  917658  1475996  9.3 
60  1511368  2409556  17.7  
70  2316478  3667916  29.1  
80  3364988  5299076  45.9  
90  4688898  7351036  70.3  
100  6320208  9871796  102.8 
Table 1 shows analysis results obtained with the ASSET tool [18, 19]. ASSET does not input parallel compositions of LTSs, but it allows to mimic their behaviour with C++ code. It also allows to express the “\(\leadsto \)” relation in C++ and computes stubborn sets with the esc algorithm. Thus it can be used to compute Step 2 of Sect. 4. ASSET verified that each LTS with the ttransitions is indeed always mayterminating. To gain confidence that the modelling with C++ is correct, additional runs were conducted where the ASSET model contained machinery that verified most of the correctness properties listed above, including that the protocol cannot lose the ability to execute ok (except by executing t).
Table 1 shows spectacular reduction results, but one may argue that the model of the channels in Fig. 6 is unduly favourable to stubborn sets. The messages travel through the channels step by step. Without stubborn sets, any combination of empty and full channel slots may be reached, creating an exponential number of states. If a message is ready to move from a cell to the next one, then the corresponding action constitutes a singleton stubborn set. Therefore, the stubborn set method has the tendency to quickly move messages to the front of the channel, dramatically reducing the number of constructed states.
To not give stubborn sets unfair advantage, another series of experiments was made where the messages are always immediately moved as close to the front of the channel as possible during construction of the full LTS. The fact about fifo queues and the “\(\leadsto \)” relation that was mentioned in Sect. 4 is also exploited. The results are shown in Table 2. Although they are less spectacular, they, too, show great benefit by the stubborn set method.
Notes
Acknowledgements
We thank the anonymous reviewers for their comments. Unfortunately, space constraints prevented us from implementing some of these.
References
 1.Bartlett, K.A., Scantlebury, R.A., Wilkinson, P.T.: A note on reliable fullduplex transmission over halfduplex links. Commun. ACM 12(5), 260–261 (1969)CrossRefGoogle Scholar
 2.Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking, p. 314. MIT Press, Cambridge (1999)Google Scholar
 3.Evangelista, S., Pajault, C.: Solving the ignoring problem for partial order reduction. Softw. Tools Technol. Transf. 12(2), 155–170 (2010)CrossRefGoogle Scholar
 4.Eve, J., KurkiSuonio, R.: On computing the transitive closure of a relation. Acta Inform. 8(4), 303–314 (1977)MathSciNetCrossRefzbMATHGoogle Scholar
 5.Gerth, R., Kuiper, R., Peled, D., Penczek, W.: A partial order approach to branching time logic model checking. In: Proceedings of Third Israel Symposium on the Theory of Computing and Systems, pp. 130–139. IEEE (1995)Google Scholar
 6.Godefroid, P.: Using partial orders to improve automatic verification methods. In: Proceedings of CAV 1990, AMSACM DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 3, pp. 321–340 (1991)Google Scholar
 7.Godefroid, P. (ed.): PartialOrder Methods for the Verification of Concurrent Systems: An Approach to the StateExplosion Problem. LNCS, vol. 1032. Springer, Heidelberg (1996)zbMATHGoogle Scholar
 8.Laarman, A., Pater, E., van de Pol, J., Hansen, H.: Guardbased partialorder reduction. Softw. Tools Technol. Transf. 1–22 (2014)Google Scholar
 9.Mazurkiewicz, A.: Trace theory. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) Petri Nets 1986. LNCS, vol. 255, pp. 279–324. Springer, Heidelberg (1987)Google Scholar
 10.Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993)CrossRefGoogle Scholar
 11.Peled, D.: Partial order reduction: linear and branching temporal logics and process algebras. In: Proceedings of POMIV 1996, Workshop on Partial Order Methods in Verification, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 29, pp. 233–257. American Mathematical Society (1997)Google Scholar
 12.Rensink, A., Vogler, W.: Fair testing. Inf. Comput. 205(2), 125–198 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
 13.Tarjan, R.E.: Depthfirst search and linear graph algorithms. SIAM J. Comput. 1(2), 146–160 (1972)MathSciNetCrossRefzbMATHGoogle Scholar
 14.Valmari, A.: Error Detection by reduced reachability graph generation. In: Proceedings of the 9th European Workshop on Application and Theory of Petri Nets, pp. 95–122 (1988)Google Scholar
 15.Valmari, A.: State space generation: efficiency and practicality. Dr. Techn. thesis, Tampere University of Technology Publications 55, Tampere (1988)Google Scholar
 16.Valmari, A.: Stubborn set methods for process algebras. Peled, D.A., Pratt, V.R., Holzmann, G.J. (eds.) Partial Order Methods in Verification: DIMACS Workshop, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 29, pp. 213–231. American Mathematical Society (1997)Google Scholar
 17.Valmari, A.: The state explosion problem. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 429–528. Springer, Heidelberg (1998)CrossRefGoogle Scholar
 18.Valmari, A.: Stop it, and be stubborn! In: Haar, S., Meyer, R. (eds.) 15th International Conference on Application of Concurrency to System Design, pp. 10–19. IEEE Computer Society (2015). doi: 10.1109/ACSD.2015.14
 19.Valmari, A.: A state space tool for concurrent system models expressed in C++. In: Nummenmaa, J., SieviKorte, O., Mäkinen, E. (eds.) SPLST 2015 Symposium on Programming Languages and Software Tools, vol. 1525, pp. 91–105. CEUR Workshop Proceedings (2015)Google Scholar
 20.Valmari, A., Hansen, H.: Can stubborn sets be optimal? Fundamenta Informaticae 113(3–4), 377–397 (2011)MathSciNetzbMATHGoogle Scholar