Structural liveness of Petri nets is ExpSpace-hard and decidable

Abstract

Place/transition Petri nets are a standard model for a class of distributed systems whose reachability spaces might be infinite. One of well-studied topics is verification of safety and liveness properties in this model; despite an extensive research effort, some basic problems remain open, which is exemplified by the complexity status of the reachability problem that is still not fully clarified. The liveness problems are known to be closely related to the reachability problem, and various structural properties of nets that are related to liveness have been studied. Somewhat surprisingly, the decidability status of the problem of determining whether a net is structurally live, i.e. whether there is an initial marking for which it is live, remained open for some time; e.g. Best and Esparza (Inf Process Lett 116(6):423–427, 2016. https://doi.org/10.1016/j.ipl.2016.01.011) emphasize this open question. Here we show that the structural liveness problem for Petri nets is ExpSpace-hard and decidable. In particular, given a net N and a semilinear set S, it is decidable whether there is an initial marking of N for which the reachability set is included in S; this is based on results by Leroux (28th annual ACM/IEEE symposium on logic in computer science, LICS 2013, New Orleans, LA, USA, June 25–28, 2013, IEEE Computer Society, pp 23–32, 2013. https://doi.org/10.1109/LICS.2013.7).

1 Introduction

Petri nets (exemplified by Fig. 1) are a standard tool for modelling and analysing a class of distributed systems; see e.g., [24] for an introduction. A natural liveness property of concern is deadlock-freedom; in more detail we can ask if a concrete action, a transition in a Petri net, can become dead, i.e., lose the potential to be performed in the future. We say that a Petri net with an initial state, with an initial marking in Petri net terminology, is live if none of its transitions can become dead.

Fig. 1

Example of a net $N=(P,T,W)$, with marking $M=(3,1,0)$

There is a close relationship of the liveness problem (is a given Petri net with an initial marking live?) and the reachability problem (is one marking reachable from another in a given Petri net?), which has been clear since the early works by Hack [13, 14]. The complexity of the reachability problem is a tough research problem. The problem is known to be decidable [20], with a non-primitive recursive upper bound [19]; for long time the best known lower bound had been the ExpSpace-hardness by Lipton (see, e.g., [8]), but recently a non-elementary lower bound has been announced in [6].

Here we study the structural liveness problem that asks whether there is an initial marking for which a given Petri net is live. The semidecidability of the problem is clear by the decidability of the liveness problem (which is due to the decidability of reachability), but the decidability of structural liveness had been open, as recalled e.g. in [3]. We answer this decidability question positively; this part is based on and extends the conference paper [15], where the semidecidability of the complementary problem was shown by using the results on effectively constructible semilinear reachability sets of Petri nets [18]. We also establish a lower bound, namely the ExpSpace-hardness of structural liveness, by a reduction from the coverability problem for reversible Petri nets. We note that it remains unclear if the structural liveness problem is reducible to/from the reachability problem.

It might be worth noting that our proof also highlights the decidability of structural semilinear safety properties, i.e. whether there exists a marking of a given net for which its reachability set is included in a given semilinear set.

Section 2 provides the formal background, Sect. 3 shows the ExpSpace-hardness result, and Sect. 4 shows the decidability result. In Sect. 5 a few comments are added, in particular an example of a net is given where the set of live markings is not semilinear.

2 Basic definitions

By $\mathbb {N}$ we denote the set $\{0,1,2,\dots \}$. For a set A, by $A^*$ we denote the set of finite sequences of elements of A, and $\varepsilon$ denotes the empty sequence.

2.1 Nets

A Petri net, or just a net for short, is a tuple $N=(P,T,W)$ where P and T are two disjoint finite sets of places and transitions, respectively, and $W{:}\,(P\times T)\cup (T\times P)\rightarrow \mathbb {N}$ is the weighted flow function. A markingM of N is an element of $\mathbb {N}^P$, a mapping from P to $\mathbb {N}$, often also viewed as a vector with |P| components (i.e., an element of $\mathbb {N}^{|P|}$).

Figure 1 presents a net $N=(\{p_1,p_2,p_3\},\{t_1,t_2,t_3\},W)$ where $W(p_1,t_1)=2$, $W(p_1,t_2)=1$, $W(p_1,t_3)=0$, etc.; we do not draw an arc from x to y when $W(x,y)=0$, and we assume $W(x,y)=1$ for the arcs (x, y) with no depicted numbers. Figure 1 also depicts a marking M by using black tokens, namely $M=(3,1,0)$, assuming the ordering $(p_1,p_2,p_3)$ of places.

2.2 Reachability

Assuming a net $N=(P,T,W)$, for each $t\in T$ we define the following relation ${\mathop {\longrightarrow }\limits ^{t}}$ on $\mathbb {N}^P$:

$$\begin{aligned} M{\mathop {\longrightarrow }\limits ^{t}}M'\ \Leftrightarrow _{\text {df}}\ \forall p\in P{:}\,M(p)\ge W(p,t) \wedge M'(p)=M(p)-W(p,t)+W(t,p). \end{aligned}$$

By $M{\mathop {\longrightarrow }\limits ^{t}}$ we denote that t is enabled inM, i.e., that there is $M'$ such that $M{\mathop {\longrightarrow }\limits ^{t}}M'$; an enabled transition in M can be performed, yielding $M'$ (where $M{\mathop {\longrightarrow }\limits ^{t}}M'$). The relations ${\mathop {\longrightarrow }\limits ^{t}}$ are inductively extended to ${\mathop {\longrightarrow }\limits ^{u}}$ for all $u\in T^*$: $M{\mathop {\longrightarrow }\limits ^{\varepsilon }}M$; if $M{\mathop {\longrightarrow }\limits ^{t}}M'$ and $M'{\mathop {\longrightarrow }\limits ^{u}}M''$, then $M{\mathop {\longrightarrow }\limits ^{tu}}M''$. The reachability set for a markingM is the set

$$\begin{aligned}{}[{M}\rangle =\left\{ M'\mid M{\mathop {\longrightarrow }\limits ^{u}}M'\ \hbox {for some}\ u\in T^*\right\} . \end{aligned}$$

For the net of Fig. 1 we have, e.g., $(3,1,0){\mathop {\longrightarrow }\limits ^{t_2}}(4,0,1){\mathop {\longrightarrow }\limits ^{t_1}}(2,0,1) {\mathop {\longrightarrow }\limits ^{t_1}}(0,0,1){\mathop {\longrightarrow }\limits ^{t_3}}(1,1,0)$; we can check that the reachability set for (3, 1, 0) is

$$\begin{aligned} \{\,(x,1,0)\mid x \text { is odd }\}\cup \{\,(y,0,1)\mid y \text { is even }\}. \end{aligned}$$

(1)

We also note the monotonicity property: if $M_1{\mathop {\longrightarrow }\limits ^{u}}M'_1$ and $M_2\ge M_1$ (i.e., $M_2(p)\ge M_1(p)$ for all $p\in P$), then $M_2{\mathop {\longrightarrow }\limits ^{u}}M'_2$ where $M'_2=M'_1+(M_2-M_1)$.

2.3 Reversible nets

We use the following strong notion of reversibility: a net$N = (P,T,W)$ is reversible if for each transition $t \in T$ there is a (“reversed”) transition $t' \in T$ such that $W(p,t')=W(t,p)$ and $W(t',p)=W(p,t)$ for all $p\in P$. This obviously entails that $M' \in [{M}\rangle$ implies $M \in [{M'}\rangle$.

2.4 Coverability, in particular in reversible nets

A marking C is coverable from a marking M in a net N if there exists a marking $C' \ge C$ such that $C' \in [{M}\rangle$. By monotonicity, if $M'\ge M$ and C is coverable from M, then C is coverable from $M'$ as well.

The reversible coverability problem, denoted ReversCover, asks, given a reversible net N, an initial marking I and a target marking C, if C is coverable from I in N.

2.5 Liveness

For a net $N=(P,T,W)$, a transitiont is dead in a markingM if there is no $M'\in [{M}\rangle$ such that $M'{\mathop {\longrightarrow }\limits ^{t}}$. (Such t can be never performed in N when we start from M.)

A transitiont is live in$M_0$ if there is no $M\in [{M_0}\rangle$ such that t is dead in M. (Hence for each $M\in [{M_0}\rangle$ there is $M'\in [{M}\rangle$ such that $M'{\mathop {\longrightarrow }\limits ^{t}}$.) A set$T'\subseteq T$of transitions is live in$M_0$ if each $t\in T'$ is live in $M_0$. (Another natural definition of liveness of a set $T'$ is discussed in Sect. 5.)

A transitiont in N is structurally live if there is $M_0$ in which t is live. A set$T'\subseteq T$of transitions in N is structurally live if there is $M_0$ in which each $t\in T'$ is live.

A marked net is a pair $(N,M_0)$ where $N=(P,T,W)$ is a net and $M_0$ is a marking, called the initial marking. A marked net$(N,M_0)$ is live if each transition (in other words, the set T) is live in $M_0$ (in the net N). A netN is structurally live if there is $M_0$ such that $(N,M_0)$ is live.

E.g., the net in Fig. 1 is structurally live since it is live for the marking (3, 1, 0), as can be easily checked by inspecting the transitions enabled in the elements of the reachability set (1). We can also note that the net is not live for (4, 1, 0); we even have that no transition is live in (4, 1, 0), since $(4,1,0){\mathop {\longrightarrow }\limits ^{t_1t_1}}(0,1,0)$ where all transitions are dead.

2.6 Liveness decision problems

• The partial liveness problem, denoted $\textsc {PLP}$, asks, given a marked net $(N,M_0)$ and a set $T'$ of its transitions, if $T'$ is live in $M_0$.

• The liveness problem, denoted $\textsc {LP}$, is a special case of $\textsc {PLP}$: it asks, given a marked net $(N,M_0)$, if $(N,M_0)$ is live (i.e., if all its transitions are live in $M_0$).

• The partial structural liveness problem, denoted $\textsc {PSLP}$, asks, given a net N and a set $T'$ of its transitions, if $T'$ is structurally live.

• The structural liveness problem, denoted $\textsc {SLP}$, is a special case of $\textsc {PSLP}$: it asks, given a net N, if N is structurally live.

3 Problems $\textsc {SLP}$ and $\textsc {PSLP}$ are $\textsc {ExpSpace}$-hard

We show that (partial) structural liveness is $\textsc {ExpSpace}$-hard, by a reduction from the problem ReversCover (coverability for reversible nets).

3.1 ReversCover is $\textsc {ExpSpace}$-hard

The coverability problem for Petri nets is well known to be ExpSpace-hard due to Lipton. The result was strengthened to yield ExpSpace-hardness of the problem ReversCover (coverability for reversible nets) in the conference paper [4], with full proofs in the journal paper [22]; the problem, expressed in the framework of commutative semigroups, is also discussed in [21]. The respective construction reduces the acceptance problem for exponential-space bounded Turing machines to the equivalence/derivability problem for finitely presented commutative semigroups; in fact, here it does not matter whether equivalence (i.e. reachability) or coverability is used. Such finitely presented commutative semigroups are equivalent to reversible Petri nets [12, 22], entailing that ReversCover is indeed ExpSpace-hard (in fact, ExpSpace-complete).

Remark

We stress that the mentioned ExpSpace lower and upper bounds are independent of (unary or binary) encoding of numbers; in particular, the coverability in reversible nets is ExpSpace-hard even when the numbers (in the flow function and the initial marking) are given in unary [21].

3.2 Reducing ReversCover to SLP and PSLP

We assume a given instance of ReversCover, i.e., $N = (P, T, W), I , C$; hence N is a reversible net (each transition has its “reverse-transition”). Let $P = \{p_1, \dots , p_n \}$. We define a net $N' = (P', T', W')$, partially sketched in Fig. 2, as follows:

• $P' = P \cup \{ Z\}$ ($Z\not \in P$ is an additional place);

• $T' = T \cup \{t_{R_1} \ldots t_{R_n}, t_{R_Z}, t_C, t_I \}$ (hence $n{+}3$ new transitions are added);

• $W'(p, t) = W(p,t)$ and $W'(t, p) = W(t,p)$ for all $p\in P$ and $t\in T$ (which is not depicted in Fig. 2);

• $W'(p_i, t_C) = C(p_i)$ and $W'(t_C, p_i) = C(p_i) + 1$ (for $i=1,2,\ldots ,n$);

• $W'(t_C, Z) = 2$;

• $W'(p_i, t_{R_i}) = W'(Z, t_{R_i})= W'( t_{R_i}, Z) = 1$ (for $i=1,2,\ldots ,n$);

• $W'(Z, t_{R_Z}) = 2$ and $W'( t_{R_Z}, Z) = 1$;

• $W'(Z, t_I) = 1$ and $W'(t_I, p_i) = I(p_i)$ (for $i=1,2,\ldots ,n$).

For completeness we add that $W'(x,y)=0$ for the pairs $(x,y)\in (P'\times T')\cup (T'\times P')$ not mentioned in the above points.

Fig. 2

Net $N'$ constructed for a reversible net N (the transitions of N are not depicted)

Proposition 1

• 1. If C is not coverable from I in N, then $t_C$ is not structurally live in $N'$ (and thus $N'$ is not structurally live).

• 2. If C is coverable from I in N, then $N'$ is structurally live.

Proof

For convenience, when we write a marking of $N'=(P',T',W')$ in the form (M, z), then M is a marking of N and z is the number of tokens at place Z. By $\mathbf 0$ we denote the zero marking of N (hence $\mathbf 0 (p_i)=0$ for all $i\in \{1,2,\dots ,n\}$).

• 1. We assume that C is not coverable from I in N, and we aim to show that $t_C$ is not structurally live in $N'$. We thus fix an arbitrary initial marking (M, z) of $N'$, and we aim to show that transition $t_C$ is not live in (M, z).

If $z\ge 1$, then we can perform $t_{R_i}\ M(p_i)$-times, for $i=1,2,\dots ,n$; from (M, z) we thus reach $(\mathbf 0 ,z)$. Then by performing $t_{R_Z}\ (z{-}1)$-times we reach $(\mathbf 0 ,1)$, and we have $(\mathbf 0 ,1){\mathop {\longrightarrow }\limits ^{t_I}}(I,0)$. In (I, 0), transition $t_C$ is dead (as well as $t_{R_Z}$ and all $t_{R_i}$) since C is not coverable from I in N (and from (I, 0) net $N'$ can thus only mimic the behaviour of N).

If we fixed (M, 0) as the initial marking, and $t_C$ is not dead in (M, 0), then there is $(M',0)\in [{(M,0)}\rangle$ such that $(M',0){\mathop {\longrightarrow }\limits ^{t_C}}(M'',2)$; by the above reasoning $t_C$ is not live in $(M'',2)$, and thus $t_C$ is not live in (M, 0) either.

• 2. We assume that C is coverable from I in N, and we will show that (I, 0) is live for $N'$. We first show that (I, 0) is a “home marking” for $N'$, i.e.,

  $$\begin{aligned} \hbox {for each}\ (M,z) \in [{(I,0)}\rangle \ \hbox {we have} \ (I,0) \in [{(M,z)}\rangle . \end{aligned}$$

Let us consider $(M,z)\in [{(I,0)}\rangle$. If $z\ge 1$, then $(I,0)\in [{(M,z)}\rangle$, as was already shown above. If $z=0$, then on a fixed path

$$\begin{aligned} (I,0)=(M_0,z_0){\mathop {\longrightarrow }\limits ^{t'_1}}(M_1,z_1){\mathop {\longrightarrow }\limits ^{t'_2}}(M_2,z_2) \cdots {\mathop {\longrightarrow }\limits ^{t'_k}}(M_k,z_k)=(M,0) \end{aligned}$$

demonstrating that $(M,0)\in [{(I,0)}\rangle$ let $(M_j,z_j){\mathop {\longrightarrow }\limits ^{t'_{j+1}}}(M_{j+1},z_{j+1})\cdots {\mathop {\longrightarrow }\limits ^{t'_k}}(M_k,z_k)$ be the longest suffix with $z_j=z_{j+1}=\cdots =z_k=0$. It is clear that either $M_j=I$, or $t'_{j-1}=t_I$ (since $t_I$ is the only transition that can make Z empty), and thus $M_j\ge I$. Since the transitions $t'_{j+1},\dots ,t'_k$ are necessarily from T in $N=(P,T,W)$ and N is reversible, we have $M_j\in [{M}\rangle$ in N, and thus $(M_j,0)\in [{(M,0)}\rangle$ in $N'$. Since C is coverable from I in N, and $M_j\ge I$, we have that (C, 0) is coverable from $(M_j,0)$, and thus from (M, 0), in $N'$. When (C, 0) is covered, $t_C$ can be performed, after which $(M',2)$ is reached, and $(I,0)\in [{(M',2)}\rangle$ as noted above. Thus (I, 0) is indeed a home marking in $N'$.

Now it suffices to show that no transition is dead in (I, 0). Indeed, from (I, 0) we can cover (C, 0) and then fire $t_C$ (increasing the number of tokens in all places) sufficiently many times so that all transitions become enabled. $\square$

The proposition and the $\textsc {ExpSpace}$-hardness of $\textsc {ReversCover}$ entail the following theorem; as already discussed, the hardness result holds even when the numbers are presented in unary.

Theorem 1

The problems $\textsc {SLP}$ (structural liveness) and $\textsc {PSLP}$ (partial structural liveness) are $\textsc {ExpSpace}$-hard.

4 Problems $\textsc {SLP}$ and $\textsc {PSLP}$ are decidable

In this section we prove the following theorem.

Theorem 2

The partial structural liveness problem $(\textsc {PSLP})$ is decidable;  this also entails the decidability of the structural liveness problem $(\textsc {SLP})$.

In Sect. 4.1 we briefly recall the semidecidability of the problems. Section 4.2 then shows the semidecidability of the complementary problems.

4.1 Semidecidability of the positive case

We first explicitly recall the famous decidability result for reachability. The reachability problem, denoted $\textsc {RP}$, asks if $M\in [{M_0}\rangle$ when given $N,M_0,M$.

Theorem 3

[20] The reachability problem $(\textsc {RP})$ is decidable.

Lemma 1

Problem $\textsc {PSLP}$ is semidecidable.

Proof

It is straightforward to reduce $\textsc {PLP}$ (the partial liveness problem) to the reachability problem [13, 14]. This induces semidecidability of $\textsc {PSLP}$ (the partial structural liveness problem): given N and $T'$, we can systematically generate all markings M of N, always deciding if $T'$ is live in the currently generated M (and halt when the answer is positive). $\square$

4.2 Semidecidability of the negative case

Given a net $N=(P,T,W)$ and a set $T'\subseteq T$, we need to verify that $T'$ is not structurally live, i.e. $T'$ is non-live in all markings M, if it is the case. We first sketch the idea, which is then realized in detail.

First a (downward closed) set $\mathcal {D}_{T'}$ of markings of N is constructed in which at least one transition $t\in T'$ is dead; for this a standard backward-coverability algorithm can be used. Then we create a marked net $(N',M'_0)$ (partly sketched in Fig. 3) that works in two phases, controlled by places added to N: in the first phase, an arbitrary marking M from the set $\mathcal {D}_{T'}$ is generated, and then N is simulated in the reverse mode from M. If $T'$ is not structurally live, then the projection of the reachability set of $(N',M'_0)$ onto the set P of places of N is the whole set $\mathbb {N}^P$; if $T'$ is structurally live, then there is $M\in \mathbb {N}^P$ such that the projection of any marking reachable from $M'_0$ differs from M.

In the first case (with the whole set $\mathbb {N}^P$) the reachability set of $(N',M'_0)$ is semilinear, i.e. Presburger definable. Due to a result by Leroux [18], there is an algorithm that finishes with a Presburger description of the reachability set of $(N',M'_0)$ when this set is semilinear (while it runs forever when not). This yields the announced semidecidability.

Now we show the details, assuming a fixed net $N=(P,T,W)$ if not said otherwise.

4.2.1 Sets of “dead” markings are downward closed

We explore the set

$$\begin{aligned} \mathcal {D}_{T'}=\left\{ M\in \mathbb {N}^P\mid \ \hbox {some}\ t\in T' \ \hbox {is dead in}\ M\right\} \end{aligned}$$

for $T'\subseteq T$. We note that the definition entails $\mathcal {D}_{T'}=\bigcup _{t\in T'}\mathcal {D}_{\{t\}}$. E.g., in the net of Fig. 1 we have $\mathcal {D}_{\{t_1\}}= \{(x,0,0)\mid x\le 1\}\cup \{(0,x,0)\mid x\in \mathbb {N}\}$, $\mathcal {D}_{\{t_2,t_3\}}=\{(0,x,0)\mid x\in \mathbb {N}\}\cup \{(x,0,0)\mid x\in \mathbb {N}\}$, and

$$\begin{aligned} \mathcal {D}_T=\{(0,x,0)\mid x\in \mathbb {N}\}\cup \{(x,0,0)\mid x\in \mathbb {N}\}. \end{aligned}$$

(2)

Due to the monotonicity property ($M_1{\mathop {\longrightarrow }\limits ^{u}}M'_1$ and $M_2\ge M_1$ implies $M_2{\mathop {\longrightarrow }\limits ^{u}}M'_1+(M_2-M_1)$), each $\mathcal {D}_{T'}$ is downward closed; we say that $\mathcal {D}\subseteq \mathbb {N}^P$ is downward closed if $M\in \mathcal {D}$ implies $M'\in \mathcal {D}$ for all $M'\le M$. It is standard to characterize any downward closed subset $\mathcal {D}$ of $\mathbb {N}^P$ by the set of its maximal elements, using the extension $\mathbb {N}_\omega =\mathbb {N}\cup \{\omega \}$ where $\omega$ stands for an “arbitrarily large number” satisfying $\omega > n$ for all $n\in \mathbb {N}$. Formally we extend a downward closed set $\mathcal {D}\subseteq \mathbb {N}^P$ to the set

$$\begin{aligned} \widehat{\mathcal {D}}=\left\{ M\in (\mathbb {N}_\omega )^P\mid \forall M'\in \mathbb {N}^P{:}\,M'\le M\Rightarrow M'\in \mathcal {D}\right\} . \end{aligned}$$

We thus have

$$\begin{aligned} \mathcal {D}=\left\{ M'\in \mathbb {N}^P\mid M'\le M\ \hbox {for some} \ M\in \textsc {Max}(\widehat{\mathcal {D}})\right\} \end{aligned}$$

where $\textsc {Max}(\widehat{\mathcal {D}})$ is the set of maximal elements of $\widehat{\mathcal {D}}$. (We can refer, e.g., to [9] where such completions by “adding the limits” are handled in a general framework.) By (the standard extension of) Dickson’s Lemma, the set $\textsc {Max}(\widehat{D})$ is finite.

E.g., for the set $\mathcal {D}_T$ in (2) we have $\textsc {Max}(\widehat{\mathcal {D}_T})=\{(0,\omega ,0), (\omega ,0,0)\}$.

Proposition 2

Given $N=(P,T,W)$ and $T'\subseteq T$, the set $\mathcal {D}_{T'}$ is downward closed and the finite set $\textsc {Max}(\widehat{\mathcal {D}_{T'}})$ is effectively constructible.

Proof

We consider a net $N=(P,T,W)$ and a set $T'\subseteq T$. As discussed above, the set $\mathcal {D}_{T'}$ is downward closed.

Instead of a direct construction of the finite set $\textsc {Max}(\widehat{\mathcal {D}_{T'}})$, we first show that the set $\mathcal {S}_{T'}=\textsc {Min}(\mathbb {N}^P{\smallsetminus } \mathcal {D}_{T'})$, i.e. the set of minimal elements of the (upward closed) complement of $\mathcal {D}_{T'}$, is effectively constructible.

For each $t\in T'$, we first compute $\mathcal {S}_t=\textsc {Min}(\mathbb {N}^P{\smallsetminus } \mathcal {D}_{\{t\}})$, i.e. the set of minimal markings in which t is not dead. One standard possibility for computing $\mathcal {S}_t$ is to use the following backward algorithm, where

$$\begin{aligned} \textsc {MinPre}(t',M)\ \hbox {is the unique marking in} \ \textsc {Min}(\{M'\mid \exists M''\ge M{:}\,M'{\mathop {\longrightarrow }\limits ^{t'}}M''\}). \end{aligned}$$

(For each $p\in P$, $\textsc {MinPre}(t',M)(p)=W(p,t') +\max \{M(p){-}W(t',p),0\}$.)

An algorithm for computing $\mathcal {S}_t$:

• 1. Initialize the variable $\mathcal {S}$, containing a finite set of markings, with the value

  $$\begin{aligned} \mathcal {S}^0=\{\textsc {MinPre}(t,\mathbf {0})\} \end{aligned}$$

  (where $\mathbf {0}$ is the zero marking).

• 2. Perform the following step repeatedly, as long as possible:

  if the current value of $\mathcal {S}$ is $\mathcal {S}^i$, and for some $t'\in T$ and $M\in \mathcal {S}^i$ the marking $M'=\textsc {MinPre}(t',M)$ is not in the upward closure of $\mathcal {S}^i$ (hence $M'\not \ge M''$ for each $M''\in \mathcal {S}^i$), then put in $\mathcal {S}$ the value

  $$\begin{aligned} \mathcal {S}^{i+1}=\mathcal {S}^i\cup \{M'\}{\smallsetminus } \{M''\in \mathcal {S}^i\mid M'\le M''\}. \end{aligned}$$

Termination is clear by Dickson’s Lemma, and the final value of $\mathcal {S}$ is obviously the set $\mathcal {S}_t$ (of all minimal markings from which t can get enabled). We can remark that related studies in more general frameworks can be found, e.g., in [1, 10].

Having computed the sets $\mathcal {S}_t=\textsc {Min}(\mathbb {N}^P{\smallsetminus } \mathcal {D}_{\{t\}})$ for all $t\in T'$, we can surely compute the set $\mathcal {S}_{T'}=\textsc {Min}(\mathbb {N}^P{\smallsetminus } \mathcal {D}_{T'})$ since

$$\begin{aligned} \mathcal {S}_{T'}=\textsc {Min}\left( {\left\{ M\in \mathbb {N}^P\mid (\forall t\in T')(\exists M'\in \mathcal {S}_{t}){:}\, M\ge M'\right\} }\right) . \end{aligned}$$

This also entails that the maximum $B\in \mathbb {N}$ of values M(p) where $M\in \mathcal {S}_{T'}$ (and $p\in P$) is bounded by the maximum value M(p) where $M\in \mathcal {S}_{t}$ for some $t\in T'$. Since the finite (i.e., non-$\omega$) numbers M(p) in the elements M of $\textsc {Max}(\widehat{\mathcal {D}_{T'}})$ are obviously less than B, the set $\textsc {Max}(\widehat{\mathcal {D}_{T'}})$ can be constructed when given $\mathcal {S}_{T'}$. $\square$

Remark

Generally we must count with at least exponential-space algorithms for constructing $\textsc {Max}(\widehat{\mathcal {D}_{T'}})$ (or $\textsc {Min}(\mathbb {N}^P{\smallsetminus } \mathcal {D}_{T'})$), due to Lipton’s $\textsc {ExpSpace}$-hardness construction that also applies to the coverability (besides the reachability). On the other hand, by Rackoff’s results [23] the maximum B mentioned in the proof is at most doubly-exponential w.r.t. the input size, and thus fits in exponential space. (We can recall that Rackoff’s doubly-exponential bound on the length of a shortest covering run only depends on the target marking, not on the initial one.) Nevertheless, the precise complexity of computing $\textsc {Max}(\widehat{\mathcal {D}_{T'}})$ is not important in our context.

4.2.2 Sets of “live” markings are more complicated

Assuming $N=(P,T,W)$, for $T'\subseteq T$ we define

$$\begin{aligned} \mathcal {L}_{T'}=\left\{ M\in \mathbb {N}^P \mid T'\ \hbox {is live in}\ M\right\} . \end{aligned}$$

The set $\mathcal {L}_{T'}$ is not the complement of $\mathcal {D}_{T'}$ in general, but our definitions readily yield the following equivalence:

Proposition 3

$M\in \mathcal {L}_{T'}$ iff $[{M}\rangle \cap \mathcal {D}_{T'}=\emptyset$.

We note that $\mathcal {L}_{T'}$ is not upward closed in general. We have already observed this on the net in Fig. 1, where $\mathcal {D}_T=\{(0,x,0)\mid x\in \mathbb {N}\}\cup \{(x,0,0)\mid x\in \mathbb {N}\}$ (i.e., $\textsc {Max}(\widehat{\mathcal {D}_T})=\{(0,\omega ,0), (\omega ,0,0)\}$). It is not difficult to verify that in this net we have

$$\begin{aligned} \mathcal {L}_{T}=\left\{ M\in \mathbb {N}^{\{p_1,p_2,p_3\}} \mid M(p_2){+}M(p_3)\ge 1\text { and } M(p_1){+}M(p_3) \text { is odd}\right\} . \end{aligned}$$

(3)

Proposition 3 has the following simple corollary:

Proposition 4

The answer to an instance $N=(P,T,W)$, $T'$ of $\textsc {PSLP}$ (the partial structural liveness problem) is

• 1. YES if $\mathcal {L}_{T'}\ne \emptyset$, i.e., if $\{M\in \mathbb {N}^P; [{M}\rangle \cap \mathcal {D}_{T'}\ne \emptyset \}\ne \mathbb {N}^P$.

• 2. NO if $\mathcal {L}_{T'}=\emptyset$, i.e., if $\{M\in \mathbb {N}^P; [{M}\rangle \cap \mathcal {D}_{T'}\ne \emptyset \}=\mathbb {N}^P$.

It turns out important for us that in the case 2 (NO) the set $\{M\in \mathbb {N}^P; [{M}\rangle \cap \mathcal {D}_{T'}\ne \emptyset \}$ is semilinear. We now recall the relevant notions and facts, and then we give a proof of Theorem 2.

4.2.3 Semilinear sets

For a fixed (dimension) $d\in \mathbb {N}$, a set$\mathscr {L}\subseteq \mathbb {N}^d$ is linear if there is a (base) vector $\rho \in \mathbb {N}^d$ and (period) vectors $\pi _1,\pi _2,\dots ,\pi _k\in \mathbb {N}^d$ (for some $k\in \mathbb {N}$) such that

$$\begin{aligned} \mathscr {L}=\left\{ \rho +x_1\pi _1+x_2\pi _2+\cdots +x_k\pi _k \mid x_1,x_2,\ldots ,x_k\in \mathbb {N}\right\} . \end{aligned}$$

Such vectors $\rho , \pi _1,\pi _2,\dots ,\pi _k$ constitute a description of the set $\mathscr {L}$.

A set$\mathscr {S}\subseteq \mathbb {N}^d$ is semilinear if it is the union of finitely many linear sets; a description of $\mathscr {S}$ is a collection of descriptions of $\mathscr {L}_i$, $i=1,2,\dots ,m$ (for some $m\in \mathbb {N}$), where $\mathscr {S}=\mathscr {L}_1\cup \mathscr {L}_2\cup \cdots \cup \mathscr {L}_m$ and $\mathscr {L}_i$ are linear.

It is well known that an equivalent formalism for describing semilinear sets are Presburger formulas [11], the arithmetic formulas that can use addition but no multiplication (of variables); we also recall that the truth of (closed) Presburger formulas is decidable. E.g., all downward (or upward) closed sets $\mathcal {D}\subseteq \mathbb {N}^P$ are semilinear, and also the above sets (1) and (3) are examples of semilinear sets. Moreover, given the set $\textsc {Max}(\widehat{\mathcal {D}})$ for a downward closed set $\mathcal {D}$, constructing a description of $\mathcal {D}$ as of a semilinear set is straightforward.

It is also well known that the reachability sets $[{M}\rangle$ are not semilinear in general; similarly the sets $\mathcal {L}_{T'}$ (of live markings) are not semilinear in general. (We give an example in Sect. 5.) But we have the following result by Leroux:

Theorem 4

[18] There is an algorithm that, given a marked net $(N,M_0)$, halts iff the reachability set $[{M_0}\rangle$ is semilinear, in which case it produces a description of this set.

Roughly speaking, the algorithm guaranteed by Theorem 4 generates the reachability graph for $M_0$ while performing certain “accelerations” when possible (which captures repeatings of some transition sequences by simple formulas); this process is creating a sequence of descriptions of increasing semilinear subsets of the reachability set $[{M_0}\rangle$ until the subset is closed under all steps ${\mathop {\longrightarrow }\limits ^{t}}$ (which can be effectively checked); in this case the subset (called an inductive invariant in [18]) is equal to $[{M_0}\rangle$, and the process is guaranteed to reach such a case when $[{M_0}\rangle$ is semilinear. (A consequence highlighted in [18] is that in such a case all reachable markings can be reached by sequences of transitions from a bounded language.)

4.2.4 Proof of Theorem 2 (decidability of $\textsc {PSLP}$)

Given $N=(P,T,W)$ and $T'\subseteq T$, we will construct a marked net $(N',M'_0)$ where $N'=(P\cup P_\textit{new},T\cup T_\textit{new}, W')$ so that we will have:

• (a) if $\mathcal {L}_{T'}=\emptyset$ in N (i.e., $T'$ is non-live in each marking of N) then $[{M'_0}\rangle$ is semilinear and the projection of $[{M'_0}\rangle$ onto P is equal to $\mathbb {N}^P$;

• (b) if $\mathcal {L}_{T'}\ne \emptyset$, then the projection of $[{M'_0}\rangle$ onto P is not equal to $\mathbb {N}^P$ (and might be non-semilinear).

This construction of $(N',M'_0)$ yields the required decidability proof, since we can consider two algorithms running in parallel:

• One is the algorithm of Theorem 4 applied to $(N',M'_0)$; if it finishes with a semilinear description of $[{M'_0}\rangle$, which surely happens in the case a), then we can effectively check if the projection of $[{M'_0}\rangle$ onto P is $\mathbb {N}^P$, i.e. if $\mathcal {L}_{T'}=\emptyset$. (A projection of a semilinear set is effectively semilinear, the set-difference of two semilinear set is also effectively semilinear [11], and checking emptiness of a semilinear set is trivial.)

• The other algorithm generates all $M\in \mathbb {N}^P$ and for each of them checks if there is $M'\in [{M'_0}\rangle$ such that $M'_{\upharpoonright P}$ (i.e., $M'$ projected to P) is equal to M. It thus finds some M with the negative answer if, and only if, $\mathcal {L}_{T'}\ne \emptyset$ [(the case b)]. The existence of the algorithm checking the mentioned property for M follows from a standard extension of the decidability of reachability (Theorem 3); for our concrete construction below this extension is not needed, and just the claim of Theorem 3 will suffice.

The construction of $(N',M'_0)$ is illustrated in Fig. 3; we create a marked net that first generates an element of $\mathcal {D}_{T'}$ on the places P, and then simulates N in the reverse mode. More concretely, we assume the ordering $(p_1,p_2,\dots ,p_n)$ of the set P of places in N, and compute a description of the semilinear set $\mathcal {D}_{T'}\subseteq \mathbb {N}^{P}$ (by first constructing the set $\textsc {Max}(\widehat{\mathcal {D}_{T'}})$; recall Proposition 2). We thus get

$$\begin{aligned} \mathcal {D}_{T'}=\mathscr {L}_1\cup \mathscr {L}_2\cup \cdots \cup \mathscr {L}_m, \end{aligned}$$

given by descriptions $\rho _i,\pi _{i1},\pi _{i2},\dots ,\pi _{ik_i}$ of the linear sets $\mathscr {L}_i$, for $i=1,2,\dots ,m$.

Fig. 3

Construction of $(N',M'_0)$ for deciding the (partial) structural liveness ($\textsc {PSLP}$)

Remark

We choose this description of $\mathcal {D}_{T'}$ to make clear that the construction can be applied to any semilinear set, not only to a downward closed one.

The construction of $(N',M'_0)$, where $N'=(P\cup P_\textit{new},T\cup T_\textit{new}, W')$, is now described in detail:

• 1. Given $N=(P,T,W)$, create the “reversed” net $N_\textit{rev}=(P,T,W_\textit{rev})$, where

  $$\begin{aligned} W_\textit{rev}(p,t)=W(t,p)\ \hbox {and}\ W_\textit{rev}(t,p)=W(p,t) \ \hbox {for all}\ p\in P\ \hbox {and}\ t\in T. \end{aligned}$$

  (By induction on the length of u it is easy to verify that $M{\mathop {\longrightarrow }\limits ^{u}}M'$ in N iff $M'{\mathop {\longrightarrow }\limits ^{u_\textit{rev}}}M$ in $N_\textit{rev}$, where $u_\textit{rev}$ is defined inductively as follows: $\varepsilon _\textit{rev}=\varepsilon$ and $(tu)_\textit{rev}=u_\textit{rev}t$.)

• 2. To get $N'$, extend $N_\textit{rev}$ as described below; we will have

  $$\begin{aligned} W'(p,t)=W_\textit{rev}(p,t)\ \hbox {and}\ W'(t,p) =W_\textit{rev}(t,p)\ \hbox {for all}\ p\in P\ \hbox {and}\ t\in T. \end{aligned}$$

• 3. Create the set $P_\textit{new}$ of additional places

  $$\begin{aligned} P_\textit{new}=\left\{ \textsc {start}, \textsc {lin}_1, \textsc {lin}_2, \dots , \textsc {lin}_m, \textsc {rev}_N\right\} \end{aligned}$$

  and the set $T_\textit{new}$ of additional transitions

  $$\begin{aligned} T_\textit{new}=\bigcup _{i\in \{1,2,\dots ,m\}}\left\{ t_{\rho _i}, f_i,t_{\pi _{i1}}, t_{\pi _{i2}}, \dots , t_{\pi _{ik_i}}\right\} \end{aligned}$$

  (as partly depicted in Fig. 3.)

• 4. Put $M'_0(\textsc {start})=1$ and $M'_0(p)=0$ for all other places $p\in P\cup P_\textit{new}$.

• 5. For each $i\in \{1,2,\dots ,m\}$, put

  $$\begin{aligned} W'(\textsc {start},t_{\rho _i}) = W'(t_{\rho _i},\textsc {lin}_i)=1,\ \hbox {and} \ W'(t_{\rho _i},p_j)=(\rho _i)_j \end{aligned}$$

  for all $j\in \{1,2,\dots ,n\}$, where $(\rho _i)_j$ is the jth component of the vector $\rho _i\in \mathbb {N}^n$. (We tacitly assume that the value of $W'$ is 0 for the pairs (p, t) and (t, p) that are not mentioned.)

• 6. For each $t_{\pi _{i\ell }}$ ($i\in \{1,2,\dots ,m\}$, $\ell \in \{1,2,\dots ,k_i\}$) put

  $$\begin{aligned} W'(\textsc {lin}_i,t_{\pi _{i\ell }}) =W'(t_{\pi _{i\ell }},\textsc {lin}_i)=1, \ \hbox {and}\ W'(t_{\pi _{i\ell }},p_j)=(\pi _{i\ell })_j \end{aligned}$$

  for all $j\in \{1,2,\dots ,n\}$.

• 7. For each $f_i$ put $W'(\textsc {lin}_i,f_i)=W'(f_i,\textsc {rev}_N)=1$.

• 8. For each transition $t\in T$ in $N_\textit{rev}$ put $W'(\textsc {rev}_N,t)=W'(t,\textsc {rev}_N)=1$.

In the resulting $(N',M'_0)$ we have only one token moving on $P_\textit{new}$; more precisely, the set $[{M'_0}\rangle$ can be expressed as the union

$$\begin{aligned}{}[{M'_0}\rangle =\mathcal {S}_{\textsc {start}} \cup \mathcal {S}_{\textsc {lin}_1} \cup \cdots \cup \mathcal {S}_{\textsc {lin}_m}\cup \mathcal {S}_{\textsc {rev}_N} \end{aligned}$$

of the disjoint sets

$$\begin{aligned} \mathcal {S}_p=\left\{ M\mid M\in [{M'_0}\rangle \ \hbox {and}\ M(p)=1\right\} ,\ \hbox {for} \ p\in \left\{ \textsc {start},\textsc {lin}_1,\dots ,\textsc {lin}_m, \textsc {rev}_N\right\} . \end{aligned}$$

It is clear that each of the sets $\mathcal {S}_{\textsc {start}}$, $\mathcal {S}_{\textsc {lin}_1}$, $\dots$, $\mathcal {S}_{\textsc {lin}_m}$ is linear, and that the projection of $\mathcal {S}_{\textsc {rev}_N}$ onto $P=\{p_1,p_2,\dots ,p_n\}$ is the set $\{M\in \mathbb {N}^P; [{M}\rangle \cap \mathcal {D}_{T'}\ne \emptyset \}$ where $[{M}\rangle$ refers to the net N.

The constructed $(N',M'_0)$ clearly satisfies the above conditions (a) and (b). In the algorithm verifying (b), it suffices to generate the markings M of $N'$ that satisfy $M(\textsc {rev}_N)=1$, $M(\textsc {start})=M(\textsc {lin}_1)=\cdots =M(\textsc {lin}_m)=0$, and to check the (non)reachability from $M'_0$ for each of them (recall Theorem 3).

We have thus finished a proof of Theorem 2.

Remark

We also have another option (than Theorem 3) for establishing the non-reachability of M from $M'_0$, due to another result by Leroux (see, e.g., [17]): namely to find a description of a semilinear set that contains $M'_0$, does not contain M, and is closed w.r.t. all steps ${\mathop {\longrightarrow }\limits ^{t}}$ (being thus an inductive invariant in the terminology of [17]).

5 Additional remarks

5.1 Checking structural semilinear safety properties

We recall that our decision procedure for structural liveness of a net N first constructs the set S of markings in which no transition is dead and then decides if there is an initial marking (in S) for which its reachability set is included in S. The mentioned set S is upward closed but our procedure yields the following more general theorem.

Theorem 5

Given a net $N=(P,T,W)$ and a semilinear set $S\subseteq \mathbb {N}^P$, it is decidable whether there exists an initial marking $M \in S$ such that $[{M}\rangle \subseteq S$.

This problem can be interpreted as structural satisfiability of a safety property. However, one must be careful, since such condition may be trivial in concrete cases, e.g. when $\mathbf 0 \in S$.

5.2 Sets of live markings can be non-semilinear

In Petri net theory, there are many results that relate liveness to specific structural properties of nets. We can name [2] as an example of a cited paper from this area. Nevertheless, the general structural liveness problem is still not fully understood; one reason might be the fact that the set of live markings of a given net is not semilinear in general.

As an example, we give a net $N=(P,T,W)$ in Fig. 4. If the set $\mathcal {L}_{T}$ of live markings was semilinear, then its intersection with the set $\{(x_1,0,1,0,1,x_6)\mid x_1,x_6\in \mathbb {N}\}$ would also be semilinear (i.e., definable by a Presburger formula). But we will verify that the markings in this set are live if, and only if, $x_6> 2^{x_1}$, which makes the set clearly non-semilinear.

Fig. 4

Sets of live markings can be non-semilinear

We first observe that each marking M with $M(p_4)=M(p_6)=0$ is not live (in this case we have $M'(p_4)=M'(p_6)=0$ for each $M'\in [{M}\rangle$). In each marking M where $p_4$ is marked, i.e. $M(p_4)\ge 1$, no transition is dead; moreover, if $p_4$ is marked, then it stays marked forever. Hence each marking M with $M(p_4)\ge 1$ is live. Now we fix a marking $M=(x_1,0,1,0,1,x_6)$, depicted in Fig. 4 (where $M(p_4)=0$). It is straightforward to check that if $M'\in [{M}\rangle$ and $M'(p_4)=0$, then $M'(p_5)\le 2^{x_1}$; moreover, there is $M'\in [{M}\rangle$ where $M'(p_4)=0$ and $M'(p_5)= 2^{x_1}$. Hence if $x_6\le 2^{x_1}$, then there is $M'\in [{M}\rangle$ where $M'(p_4)=M'(p_6)=0$ (using the transition left of $p_6$); in this case M is not live. If $x_6>2^{x_1}$, then the transition right of $p_6$ remains enabled unless it is performed and marks $p_4$; hence in this case M is live.

5.3 Another version of liveness of a set of transitions

Given $N=(P,T,W)$, we defined that a set $T'$ of transitions is live in a marking M if each $t\in T'$ is live in M. Another option is to view $T'$ as live in M if in each $M'\in [{M}\rangle$ at least one $t\in T'$ is not dead. But the problem of determining whether $T'$ is live in M in this sense can be easily reduced to the problem of determining whether a specific transition is live. (We can add a place $\bar{p}$ and a transition $\bar{t}$, putting $W(\bar{p},\bar{t})=1$. For each $t\in T'$ we then add $t'$ and put $W(t',\bar{p})=1$ and $W(p,t')=W(t',p)=W(p,t)$ for each $p\in P$. Then $T'$ is live in M in the new sense iff $\bar{t}$ is live in M.) The above nuances in definitions thus make no substantial difference.

5.4 Structural liveness is trivial for reversible and other restricted nets

We have defined reversibility in a strong sense: every transition has its reverse transition. Nevertheless the reduction in Sect. 3 also works when we only require that $M' \in [{M}\rangle$ implies $M \in [{M'}\rangle$; hence the effect of each transition can be undone by some series of transitions (possibly different for different markings).

We note that the net $N'$ in Fig. 2 arises from a reversible net N but $N'$ itself is not reversible (in a strong or weak sense). This is necessary, since every reversible net is structurally live. Indeed, in a reversible net each marking $M_0$ is a home marking ($M\in [{M_0}\rangle$ entails $M_0\in [{M}\rangle$), and thus all transitions are live in a marking $M_0$ that enables all transitions.

We can also recall marked graphs as an example of a class in which each net is structurally live. A marked graph is a Petri net $N=(P,T,W)$ where $\sum _{t\in T} W(t,p) = \sum _{t\in T} W(p,t) = 1$ for each $p \in P$ (there is exactly one edge into and one edge out of each place). We note that such graphs are equivalent to directed graphs where vertices represent transitions and edges represent places; a marking thus associates a number of tokens with each edge [16]. By [5] a marked graph is live if the token count on each directed cycle is positive. It is therefore clear that such nets are structurally live, as each such net is live for the marking where each place has one token.

We note that marked graphs constitute a special case of free-choice nets, where Commoner’s theorem (see e.g., [7]) clarifies the liveness problem, and also the structural liveness problem. A detailed study of structural liveness in various Petri net subclasses can be a natural topic of a future research.

5.5 Everywhere liveness

A net N is viewed as structurally live if there is $M_0$ such that $(N,M_0)$ is live. We note that the question if $(N,M_0)$ is live for all $M_0$ is almost trivial. Indeed, $(N,M_0)$ is live for all $M_0$ iff $(N,\mathbf 0 )$ is live. (If there is no dead transition in the zero marking, then there is no dead transition in any marking.) A net $N=(P,T,W)$ with $P=\emptyset$ is trivially live for $\mathbf 0$. If $P\ne \emptyset$ and each $t\in T$ has an input place, i.e. $p\in P$ such that $W(p,t)\ge 1$, then $(N,\mathbf 0 )$ is not live. In the remaining case, $(N,\mathbf 0 )$ is live iff $(N',\mathbf 0 )$ is live where $N'$ arises from N by removing all input-free transitions together with their output places.

5.6 Open complexity status

We have not fully clarified the complexity of the (partial) structural liveness problem ($\textsc {PSLP}$, $\textsc {SLP}$). The complexity of the (partial) liveness problem ($\textsc {PLP}$, $\textsc {LP}$) is “close” to the complexity of the reachability problem $\textsc {RP}$ (as follows already by the constructions in [13]), but it seems natural to expect that the structural liveness problem might be easier. (E.g., the boundedness problem, asking if $[{M_0}\rangle$ is finite when given $(N,M_0)$, is $\textsc {ExpSpace}$-complete, by the results of Lipton and Rackoff, but the structural boundedness problem is polynomial; here we ask, given N, if $(N,M_0)$ is bounded for all $M_0$, or in the complementary way, if $(N,M_0)$ is unbounded for some $M_0$.)

The recently announced nonelementary bound for reachability [6] also yields nonelementary complexity of liveness. Structural liveness might be indeed easier; it remains “only” $\textsc {ExpSpace}$-hard since the existence of a reduction from reachability is not clear in this case. On the other hand, it has been so far not excluded that structural liveness is even harder than reachability (and thus harder than liveness), since we have no reduction to the reachability problem either.