Structural Liveness of Conservative Petri Nets

Petri nets are a well-known model of a class of distributed systems; we can refer, e.g., to the monographs [25] or [3] for an introduction. The reachability problem, asking if a given target configuration is reachable from a given initial configuration, is a basic problem of system analysis; in the case of Petri nets this problem is famous for its computational complexity: its Ackermann-completeness has been only recently established (see [6, 18] for the lower bound, and [19] for the upper bound). The boundedness problem, asking if the reachability set for a given initial configuration is finite, and the liveness problem, asking if no action can become dead, are among other standard analysis problems. While boundedness is known to be EXPSPACE-complete [5, 24], liveness is tightly related to reachability [10], and is thus now known to be Ackermann-complete.

There are also natural structural versions of boundedness and liveness. The structural boundedness problem asks, given a Petri net, if the net is bounded for each possible initial configuration; the structural liveness problem asks, given a Petri net, if there is an initial configuration for which the net is live.

While structural boundedness is easily shown to be in PTIME (and is thus substantially easier than boundedness), structural liveness is only known to be EXPSPACE-hard and decidable [14]. In fact, the decidability result can be strengthened by the recent result on the home-space problem [12, 13] that easily implies an Ackermannian upper bound for structural liveness as well, but the huge complexity gap still calls for a clarification.

Our contribution. As a step towards clarifying the complexity of structural liveness for general Petri nets, we show the EXPSPACE-completeness in the case of conservative nets, which do not change a weighted sum of the tokens during their executions. We recall that the problem if a given net is conservative is also in PTIME, similarly as structural boundedness (see, e.g., [22]). A crucial notion in our proof is structural reversibility, called just reversibility in this paper; a net is reversible if there is a sequence of actions that contains each action at least once and whose effect is zero (it does not change the configuration when executed). Reversibility is also in PTIME, and it can be easily shown to be a necessary condition for structural liveness in the case of structurally bounded nets. Moreover, it is trivial that each conservative net is structurally bounded, and a straightforward application of Farkas’ lemma shows that each reversible structurally bounded net is conservative. Hence our EXPSPACE-completeness result can be equivalently presented as the result for structurally bounded nets. A first natural step of our future research plan is to deal with a few subtle points that would allow us to extend the result to the whole class of reversible nets.

The lower bound, the EXPSPACE-hardness, is achieved by adapting the construction of [14] that shows a reduction from the EXPSPACE-complete word problem for commutative semigroups which can be also phrased as a coverability problem for reversible Petri nets [5, 20, 21]. We recall that coverability is a weaker form of reachability: it asks whether there is a reachable configuration that is component-wise at least as large as the target. Our adaptation, described in detail in the arxiv version of this paper, shows that we get the EXPSPACE-hardness of structural liveness even in the case of nets where each transition has precisely two input places and two output places (i.e., for the nets that naturally correspond to population protocols [1]).

Our main result is the EXPSPACE upper bound. The crucial step proves that for every structurally live conservative net there is a live configuration with an at most 2-exp (double exponential) number of tokens, which in principle matches the lower bound. We achieve this by showing that for any structurally live conservative net there is a quantifier-free Presburger formula which has a “small” (i.e. 2-exp) solution and for which all solutions are live configurations. More precisely, a solution of this formula presents a collection of at most exponentially many configurations that are mutually reachable and are chosen so that they witness that they are all live.

For showing the existence of the mentioned Presburger formula we suggest a way to present a witness for which reachability is safely replaced with conceptually much simpler virtual reachability, which allows us to have also negative numbers of tokens in (virtual) configurations. For expressing virtual reachability of reversible nets we use linear systems, i.e. boolean combinations of linear (in)equations and divisibility constraints. As a proof ingredient with a potential of wider applicability, we present exponential bounds on the least solutions of linear systems, which is an extension of the known results like those in [23] (which are also referred to in the survey [9]).

We try to perform our analysis of 2-exp functions at a level that allows us to derive the results with sufficient rigour but without technical details that we find unnecessary. To this aim we also introduce the notion of RB-functions (“Rackoff-bounded” functions, inspired by [24]) that constitute a special case of 2-exp functions with two variables. The class of RB-functions is closed under various operations including iteration, which gives us a lucid method to build the needed new RB-functions from already established ones.

Related research. This paper can be viewed as a continuation of the research line initiated by the paper [4] which explicitly indicated that even the decidability question for structural liveness of Petri nets had been still open. As already mentioned, now the decidability and the EXPSPACE-hardness are known [14], and the decidability can be strengthened by [12, 13] that implies an Ackermannian upper bound. Another result of this research line shows the PSPACE-completeness of structural liveness for IO-nets (Immediate Observation Petri Nets) that were introduced in [8], inspired by a subclass of population protocols in [2]. The paper [8] does not consider structural liveness explicitly, but a PSPACE upper bound follows from its results on liveness immediately; an explicit self-contained proof of the PSPACE-completeness is given in [15].

There is a long list of papers that studied liveness for various subclasses of Petri nets, often exploring related structural properties (we can refer to the monographs [3, 7, 25] for examples). We can also name [11] as an example of a paper in which structural liveness is among the explicitly studied problems for a subclass of Petri nets. We will also use the known results on liveness for conservative nets, for which we can refer, e.g., to [22].

Organization of the paper. Section 2 gives basic notions and notation, introduces linear systems and RB-functions, and the main results. Section 3 proves the above mentioned 2-exp upper bound, also using the results that are proved separately in Sections 4 and 5. Section 6 discusses the EXPSPACE lower bound. A longer version of this paper can be found at arxiv.org.

By \(\mathbb {N}\), \(\mathbb {N}_+\), and \(\mathbb {Z}\) we denote the sets of nonnegative integers, positive integers, and integers, respectively. For \(i,j\in \mathbb {Z}\) we put \([i,j]=\{i,i{+}1,\dots ,j\}\). The unary operation |.| denotes the absolute value for numbers, the cardinality for sets, and the length for sequences. For a vector \(x\in \mathbb {Z}^d\) (\(d\in \mathbb {N}\)), by x(i) we denote the value of its component \(i\in [1,d]\), hence \(x=(x(1),x(2),\ldots ,x(d))\). We use the component-wise (partial) order \(\le \) on \(\mathbb {Z}^d\).

It will be clear from the context when a vector is understood as a column vector; e.g., if B is an \(m\times n\) matrix, then in \(Bx=b\) the vectors x, b are viewed as column vectors \(n\times 1\) and \(m\times 1\), respectively. By \(\textbf{0}\) we denote the zero vector whose type is clear from the context. Sometimes we consider vectors as elements of \(\mathbb {Z}^J\) where J is a finite subset of \(\mathbb {N}_+\); e.g., \(\mathbb {N}^d\) is viewed as equal to \(\mathbb {N}^{[1,d]}\). For \(x\in \mathbb {Z}^d\) and \(J\subseteq [1,d]\), by \(x_{|{J}}\) we denote the (restricted) vector from \(\mathbb {Z}^J\) satisfying \(x{_{| J}}(i)=x(i)\) for each \(i\in J\); for \(X\subseteq \mathbb {Z}^d\) we put \(X_{|{J}}=\{x_{|{J}}\mid x\in X\}\).

We use “\(\cdot \)” for the standard multiplication, but \((x \cdot y)\) for \(x,y\in \mathbb {Z}^d\) denotes the dot product \(\sum _{i=1}^d x(i)\cdot y(i)\). The rank of an \(m\times n\) matrix B is denoted by \(\operatorname {rank}(B)\); hence \(\operatorname {rank}(B)\le \min \{m,n\}\).

We use the norms of \(x\in \mathbb {Z}^J\) and finite sets \(X\subseteq \mathbb {Z}^J\) (where \(\mathbb {Z}^J\) can be \(\mathbb {Z}^d\)):hence \(0\le ||x||\le \Vert x \Vert _{1}\le |J|\cdot ||x||\), and \(0\le ||X||\le \Vert X \Vert _{1}\le |J|\cdot ||X||\). We define \(||B||\) and \(\Vert B \Vert _{1}\) also for matrices over \(\mathbb {Z}\), viewing them as the sets of their rows: for an \(m\times n\) matrix B, \(\Vert B \Vert =\max _{i,j}|B_{ij}|\) and \(\Vert B \Vert _{1}=\max _{i\in [1,m]}\sum _{j=1}^n|B_{ij}|\).

For \(X\subseteq \mathbb {Z}^d\), by \(X^*\) we denote the submonoid of \((\mathbb {Z}^d,+)\) generated by X, i.e. the set of finite sums of elements of X.

Petri Nets. A Petri net A of dimension \(d\in \mathbb {N}\), a d-dim net A for short, is a finite set of pairs \(a=(a_-,a_+) \in \mathbb {N}^d \times \mathbb {N}^d\) which are called actions (or transitions); we put \(||A||=\max _{a\in A}||a||\) where \(||a||=||\{a_+,a_-\}||\).

A configuration (or a marking) of A is a vector \(x\in \mathbb {N}^d\), attaching the values x(i) (the number of tokens) to the components (or places) \(i\in [1,d]\). Each action \(a=(a_-,a_+)\) has the associated displacement, namely \(\varDelta (a)=(a_+-a_-)\in \mathbb {Z}^d\). A d-dim net A is conservative if there is \(w\in (\mathbb {N}_+)^d\) such that \((\varDelta (a) \cdot w)=0\) for all \(a\in A\); if \(w(i)=1\) for all \(i\in [1,d]\), then A is 1-conservative.

Example. Figure 1(left) shows a conservative 5-dim net \(A_1\) with 4 actions (and with \(w=(1,1,1,2,1)\)); e.g., \(a_1= \left( (a_1)_-,(a_1)_+\right) = \left( (1,0,1,0,1),(0,1,2,0,0)\right) \), \(\varDelta (a_1)=({-}1,1,1,0,{-}1)\), \(\varDelta (a_3)=(0,0,{-}2,1,0)\), ...

If \({x}=c+{a_-}\) and \({y}=c+{a_+}\) for some \(c\in \mathbb {N}^d\), then we have \({x}\xrightarrow {a}{y}\); this defines the relation \(\xrightarrow {a}\) on \(\mathbb {N}^d\). (For \(A_1\) in Figure 1 we have \((0,2,0,1,0)\xrightarrow {a_2}(1,1,0,1,0)\) but not \((0,2,0,0,0)\xrightarrow {a_2}(1,1,0,0,0)\).) For an action sequence \(\sigma =a_1a_2\ldots a_k\), the relation \(\xrightarrow {\sigma }\,\subseteq \mathbb {N}^d\times \mathbb {N}^d\) is the composition \(\xrightarrow {a_1}\circ \xrightarrow {a_2}\cdots \circ \xrightarrow {a_k}\), with the displacement \(\varDelta (\sigma )=\sum _{j=1}^k \varDelta (a_j)\). Hence \(x\xrightarrow {\sigma }y\) implies \(y=x+\varDelta (\sigma )\) but not necessarily vice versa. To \(x\xrightarrow {\sigma }y\) we also refer as to an execution of A. The reachability relation of A is \({\mathop {\rightarrow }\limits ^{*}}\,\subseteq \mathbb {N}^d\times \mathbb {N}^d\) where \(x\xrightarrow {*}y\) if \(x\xrightarrow {\sigma }y\) for some \(\sigma \).

For a d-dim net A, the virtual reachability relation of A is the relation on \(\mathbb {Z}^d\) for which if \(y-x=\varDelta (\sigma )\) for some action sequence \(\sigma \); in this case we speak on a virtual execution of A. We define \(A _{\delta }=\{\varDelta (a)\mid a\in A\}\), and note that iff \((y-x)\in (A _{\delta })^*\); we further write \(A _{\delta }^*\) instead of \((A _{\delta })^*\). A net A is structurally reversible, called just reversible in this paper, if the monoid \(A _{\delta }^*\) is a subgroup of \((\mathbb {Z}^d,+)\), i.e., if for every \(a\in A\) we have \(-\varDelta (a)\in A _{\delta }^*\); in this case the virtual reachability is symmetric: iff .

For a d-dim net A and \(I\subseteq [1,d]\), the |I|-dim net \(A_{|{I}}\) arises by the restriction of A to the components in I. We also refer to executions \(x\xrightarrow {\sigma }y\) (or virtual executions ) of \(A_{|{I}}\), implicitly assuming that \(x,y\in \mathbb {N}^I\) (or \(x,y\in \mathbb {Z}^I\)) and that the actions in \(\sigma \) are restricted to I (\(a\in A\) is in \(A_{|{I}}\) viewed as \(((a_-)_{|{I}},(a_+)_{|{I}})\)). We note that reversibility of A implies reversibility of \(A_{|{I}}\); this implication does not hold for conservativeness. (In Figure 1, \(A_2=(A_1)_{|{[1,4]}}\) is not conservative since \(\varDelta (a_1a_2)=(0,0,1,0)\).)

A configuration \(x\in \mathbb {N}^d\) of a net A is live if for all \(a\in A\) and \(x'\) such that \(x{\mathop {\rightarrow }\limits ^{*}}x'\) there is y such that \(x'{\mathop {\rightarrow }\limits ^{*}}y\) and \(y\ge a_-\) (hence \(y\xrightarrow {a}y+\varDelta (a)\)). A net A is structurally live if it has a live configuration. (\(A_1\) in Figure 1 is an example.)

Linear Systems. Let \(\textbf{x}\) be a variable ranging over \(\mathbb {Z}^d\), a d-dim variable for short. A constraint of the form \((\alpha \cdot \textbf{x})\sim c\) where \(\alpha \in \mathbb {Z}^d\), \(c\in \mathbb {Z}\), and \(\sim \mathop {\in }\,\{=,\ge \}\) is an equality constraint if \(\sim \) is \(=\), and an inequality constraint if \(\sim \) is \(\ge \); it is a homogeneous constraint if \(c=0\). For \(m\in \mathbb {N}_+\), a constraint \((\alpha \cdot \textbf{x})\equiv c\,(\bmod \, m)\), where \(\alpha \in [0,m{-}1]^d\) and \(c\in [0,m{-}1]\), is called a divisibility constraint. A d-dim linear system S is a propositional formula in which atomic propositions are equality, inequality, and divisibility constraints, for a fixed d-dim variable. The set \([[S]]\) of solutions of S consists of the vectors \(x\in \mathbb {Z}^d\) satisfying S; if \([[S]]\ne \emptyset \), then S is satisfiable. By \(||S||\) we mean the least \(s\in \mathbb {N}\) such that \(\max \{||\alpha ||,|c|\}\le s\) for all equality and inequality constraints \((\alpha \cdot \textbf{x})\sim c\) in S; moreover, \(\operatorname {lcm}(S)\) is the least common multiple of all m occurring in \((\bmod \, m)\) in divisibility constraints in S, stipulating \(\operatorname {lcm}(S)=1\) if there are no such constraints.

Given a set \(M\subseteq \mathbb {N}^d\), by \(\min _\le (M)\) we denote the set of minimal vectors in M w.r.t. the (component-wise) order \(\le \). Since \(\le \) is a well quasi order on \(\mathbb {N}^d\), the set \(\min _\le (M)\) is finite. In [23], Pottier provided several bounds for minimal nonnegative solutions of a conjunction of homogeneous equality constraints. We now recall a bound that is particularly useful for us.

We note that the “rank” bound r in Lemma 1 satisfies \(r\le \min \{m,n\}\). There is also a bound on the solutions of a conjunction of inequality constraints, \(Bx\ge b\), in [23], but with the exponent m; this is not convenient for us when m, the number of constraints, is much larger than \(n=d\), the dimension related to our problem. Therefore in Section 4 we provide a proof of the following theorem:

Remark. Given a structurally live conservative d-dim net A, we will later (in the proof of Theorem 5) use a \(d'\)-dim linear system S where \(d'=d+d\cdot 2^d\); it is crucial for us that Theorem 2 then yields a solution that is at most 2-exp in d. By [16, Theorem 3.12] we could derive that for S, even in the case of no divisibility constraints, the size of the minimal automaton encoding \([[S]]\) in binary is bounded by \((2+2\cdot ||S||)^{|S|}\) where |S| is the number of constraints in S; in our case \(|S|\ge 2^d\). The bounds on the values of minimal solutions of S that can be derived from the shortest accepting paths of that automaton are thus not smaller than \(2^{(2+2\cdot ||S||)^{|S|}}\), which is 3-exp in d.

Linear Systems for Subgroups of \(\mathbb {Z}^d\). In the sequel, by a group we mean a subgroup of \((\mathbb {Z}^d,+)\), which is also called a lattice in this context. The group spanned by a set \(X\subseteq \mathbb {Z}^d\) is the monoid \((X\cup -X)^*\), i.e., the set of finite sums of elements of \(X\cup -X\) . In Section 5 we prove the following theorem that provides a way to encode any group by a linear system, with a bound on its size.

We thus get a corollary characterizing virtual reachability of reversible nets:

RB-functions. We call a function \(f:\mathbb {N}^2\rightarrow \mathbb {N}\) an RB-function (from “Rackoff bounded”) if there are \(c\in \mathbb {N}\) and a polynomial \(p:\mathbb {N}\rightarrow \mathbb {N}\) so thatfor all \(m,d\in \mathbb {N}\). Using this notion, we state our main theorem:

Convention on RB-functions. It is straightforward to derive that the set of RB-functions (defined by (1)) is closed under the standard operations of sum, product, and composition, when the composition is defined by \(f\circ g\,(m,d)=f(g(m,d),d)\). Moreover, if f(m, d) is an RB-function, then \(f'(m,d)=f^{(d)}(m,d)\) is an RB-function as well, when \(f^{(i)}\) denotes \(f\circ f\cdots \circ f\) where f occurs i times. We use these facts implicitly when deriving the existence of RB-functions. For convenience, we also assume that each RB-function f that we consider satisfies \(m\le f(m,d)\), and is nondecreasing, i.e. \((m\le m'\wedge d\le d')\Rightarrow f(m,d)\le f(m',d')\).

Convention on using “small” and “large”. In the following proof, if we consider a d-dim net A and say that a value \(k\in \mathbb {N}\) is small, then we mean that \(k\le f(||A||,d)\) for an RB-function f (independent of A) whose existence is clear from the context or will be clarified later, while its concrete form might be left implicit. When we say that a value \(k\in \mathbb {N}\) is (sufficiently) large, then we analogously mean that \(k\ge f(||A||,d)\) for a suitable RB-function f. We use the same convention for Petri nets with states (PNSs) that are introduced later; in such cases the size \(||A||\) in \(f(||A||,d)\) is replaced with \(||G||\) for the respective PNS G.

Overview of the proof. In Section 3.1 we show that structurally live conservative nets are reversible, and that for any in a reversible net there is a virtual execution from x to y that consists of small segments that stepwise approach the target y from the start x. Section 3.2 introduces Petri nets with states (PNSs) that handle the case when some components in live configurations are necessarily small, in which case their values can be viewed as “control states”. In Section 3.3 we show how to extract a suitable PNS G with a small set of control states when given a structurally live conservative net A. Section 3.4 then shows how to reduce virtual reachability in the extracted PNS G to virtual reachability in a small net \(A_{\textsc {sc}}^G\) whose actions correspond to simple cycles in the control unit of G. Sections 3.5 and 3.6 give a characterization of large nonlive configurations of G in terms of virtual reachability in \(A_{\textsc {sc}}^G\). Finally, Section 3.7 uses this characterization to prove Theorem 5 by defining a related linear system and applying Corollary 4 and Theorem 2. We remark that we use the name lemma for a few important ingredients of the main proof; the proofs of lemmas use facts captured by propositions.

We first extend Lemma 1 to equality constraints that are not homogeneous:

The following lemma handles a conjunction of inequality constraints.

We strengthen Theorem 2 for linear systems without divisibility constraints:

Proof of Theorem 2. We consider a satisfiable linear system S. We introduce \(\ell =\operatorname {lcm}(S)\). Euclidean divisor by \(\ell \) shows that \(\mathbb {Z}^d\) is the disjoint union of sets \(a+\ell \mathbb {Z}^d\) where a ranges in the finite set of vectors \([0,\ell -1]^d\). In particular \([[S]]\) is the disjoint union of the sets \([[S]]\cap (a+\ell \mathbb {Z}^d)\) where \(a\in [0,\ell -1]^d\). Since \([[S]]\) is non-empty, there exists a vector \(a\in [0,\ell -1]^d\) such that the set \([[S]]\cap (a+\ell \mathbb {Z}^d)\) is non empty. This last set can be denoted by a linear system \(S_a\) obtained from S by replacing:

Now, just observe that \([[S]]\cap (a+\ell \mathbb {Z}^d)=a+\ell [[S_a]]\) and in particular \(S_a\) is satisfiable. Notice that if \((\alpha \cdot \textbf{x})\sim c\) is a constraint of S where \(\sim \) is the equality or the inequality, then \(|(\alpha \cdot a)|\le d(\ell -1)||S||\) and \(|c|\le ||S||\). We deduce that \(|c-(\alpha \cdot a)|\le d\ell ||S||\). We have proved the inequality \(||S_a||\le d||S||\). As \(S_a\) does not contain any divisibility constraint, Lemma 22 shows that there exists a solution y of \(S_a\) such that \(\Vert y \Vert _{1}\le (2+d+d||S_a||)^{2d+1}\). Observe that \(x=a+\ell y\) is a solution of S. Moreover \(\Vert x \Vert _{1}\le d(\ell -1) +\ell (2+d+d^2||S||)^{2d+1}\le (d+1)\ell (2+d+d^2||S||)^{2d+1}\).    \(\square \)

In this section, we introduce a linear system denoting a group spanned by a finite set of vectors. More precisely, we prove Theorem 3, all other results of this section are only used for proving that theorem.

We define the rank of a set \(X\subseteq \mathbb {Z}^d\) as the maximal \(r\in [0,d]\) such that there exists a finite sequence \(x_1,\ldots ,x_k\in X\) such that r is the rank of the \(d\times k\) matrix \([x_1|\cdots |x_k]\). This rank is denoted as \(\operatorname {rank}(X)\). We recall some classical results from the book [26, Chapter 4]. In that book, groups L are assumed to be full-rank, i.e. \(\operatorname {rank}(L)=d\). In order to overcome this limitation, we introduce the notion of maximal ranking set. A set \(K\subseteq \{1,\ldots ,d\}\) is called a maximal ranking set for a set \(X\subseteq \mathbb {Q}^d\) if \(\operatorname {rank}(X{_{| K}})=|K|=\operatorname {rank}(X)\), where \(X{_{| K}}=\{x{_{| K}}\mid x\in X\}\). Classical linear algebra results shows that any set admits a maximal ranking set.

Example. The maximal ranking sets of \(\{(1,1)\}\) are \(\{1\}\) and \(\{2\}\), for \(\{(1,0)\}\) and \(\{(1,0),(0,1)\}\) the unique maximal ranking sets are \(\{1\}\) and \(\{1,2\}\) respectively.

A Hermite decomposition of (K, L) where K is a maximal ranking set of a group L is a sequence \((v_i)_{i\in K}\) of vectors in \(\mathbb {N}^d\) that span the group L and such that for every \(i,j\in K\), we have \(v_j(i)<v_i(i)\) if \(j<i\), \(v_j(i)>0\) if \(j=i\), and \(v_j(i)=0\) if \(j>i\). Recall that there exists a unique Hermite decomposition of (K, L). We denote by \(\det _K(L)\) the product \(\prod _{i\in K}v_i(i)\). This product corresponds to the determinant of the triangular matrix \((v_i(j))_{i,j\in K}\).

Given a vector \(x\in \mathbb {Z}^d\) and a positive integer \(\ell \ge 1\), let us introduce that \([x]_{\ell }\) the unique vector in \([0,\ell -1]^d\) such that \(x\in [x]_{\ell }+\ell \mathbb {Z}^d\).

We are now ready for proving Theorem 3. Let L be a group spanned by a finite set \(X\subseteq [-m,m]^d\) for some \(m\in \mathbb {N}\). We introduce a maximal ranking set K for L, let \(r=|K|\), and \(\ell =\det _K(L)\). Lemma 23 shows that \(\ell \le (d!)m^d\). Let \(B=[L{_{| K}}]_{\ell }\). Lemma 24 shows that there exists a linear system \(S_0\) given as a conjunction of \(d-r\) homogeneous equality constraints such that \(\Vert S_0 \Vert \le d(d!)m^d\) and such that L is the set of solutions x of \(S_0\) satisfying \([x{_{| K}}]_{\ell }\in B\). It follows that the following linear system S satisfies \(L=[[S]]\).

\([\bigvee _{b\in B}(\bigwedge _{i=1}^d x(i)\in b(i)+\ell \mathbb {Z})]\wedge S_0\)

Notice that \(\Vert S \Vert =\Vert S_0 \Vert \) and \(\operatorname {lcm}(S)=\ell \).

We recall the EXPSPACE-complete uniform word problem for commutative semigroups [21]: an instance consists of a finite alphabet \(\Sigma \), a finite set of equations \(u\equiv v\) for \(u,v\in \Sigma ^*\) and \(u_0,v_0\in \Sigma ^*\), and we ask whether \(u_0\equiv v_0\). The crux of the high complexity is the fact that the commutative semigroup defined by \(a\equiv b^{2^{2^n}}\) (which can be written in space \(O(2^n)\) when using binary notation for exponents) can be embedded in a commutative semigroup of size O(n) (even when using unary notation for exponents). In fact, by [21] even the (weaker) coverability version in which \(u_0,v_0\in \Sigma \) and we ask whether \(u_0\equiv v_0w\) for some \(w\in \Sigma ^*\) is EXPSPACE-complete.

The mentioned problems can be naturally presented by reversible Petri nets, and [14] shows how a given instance of the coverability problem for reversible Petri nets can be transformed into a net A that is structurally live iff the instance is positive. In the arxiv version we show that we can transform such a net A so that it becomes 1-conservative, and even such that in each vector in the actions \((a_-,a_+)\in A\) two components have the value one while the other are zero. This reduction, together with the above mentioned fact on the equation \(a\equiv b^{2^{2^n}}\), witnesses that structural liveness of conservative nets is EXPSPACE-hard and also that the 2-exp upper bound in Theorem 5 cannot be essentially improved.