Keywords

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

Petri nets (or, equivalently, vector addition systems) represent one of the most popular formalisms for specifying, modeling, and analyzing concurrent systems. In spite of their popularity, many interesting problems concerning Petri nets are either undecidable or of very high complexity. For instance, the reachability problem is known to be decidable [13] (see also [6]) and exponential-space-hard [12]. (The reader is referred to [11] for an improved upper bound.) Historically, before the work of [13], a number of attempts were made to investigate the problem for restricted classes of Petri nets, in hope of gaining more insights and developing new tools in order to conquer the general Petri net reachability problem. A common feature of those attempts is that decidability of reachability for those restricted classes of Petri nets was built upon their reachability sets being semilinear. As semilinear sets precisely correspond to the those characterized by Presburger Arithmetic (a decidable theory), decidability of the reachability problem follows immediately.

Formally speaking, a Petri net (PN, for short) is a 3-tuple \((P,T,\varphi )\), where P is a finite set of places, T is a finite set of transitions, and \(\varphi \) is a flow function \(\varphi \) : (\(P \times T\)) \(\cup \) (\(T \times P\)) \(\rightarrow \) N. A marking is a mapping \(\mu : P \rightarrow \) N, specifying a PN’s configuration. (\(\mu \) assigns tokens to each place of the PN.) A transition \(t \in T\) is enabled at a marking \(\mu \) iff \(\forall p \in P\), \(\varphi (p,t) \le \mu (p)\). If a transition t is enabled, it may fire by removing \(\varphi (p,t)\) tokens from each input place p and putting \(\varphi (t,p')\) tokens in each output place \(p'\). We then write \(\mu \mathop {\rightarrow }\limits ^{t} \mu '\), where \(\mu '(p) = \mu (p) - \varphi (p,t) + \varphi (t,p)\), \(\forall p \in P\). A sequence of transitions \(\sigma = t_{1}...t_{n}\) is a firing sequence from \(\mu _{0}\) iff \(\mu _{0} \mathop {\rightarrow }\limits ^{t_{1}} \mu _{1} \mathop {\rightarrow }\limits ^{t_{2}} \cdots \mathop {\rightarrow }\limits ^{t_{n}} \mu _{n}\) for some markings \(\mu _{1}\),...,\(\mu _{n}\). (We also write ‘\(\mu _{0} \mathop {\rightarrow }\limits ^{\sigma } \mu _{n}\)’ or ‘\(\mu _{0} \mathop {\rightarrow }\limits ^{\sigma }\)’ if \(\mu _n\) is irrelevant.) Given a PN \(\mathcal{P}=(P,T,\varphi )\), its reachability set w.r.t. the initial marking \(\mu _{0}\) is \(R(\mathcal{P}, \mu _0)\)=\(\{\mu \mid \mu _0 \mathop {\rightarrow }\limits ^{\sigma } \mu , \ \) for some \( \ \sigma \in T^{*}\}\). The reachability relation of \(\mathcal P\) is \(R(\mathcal{P})\)=\(\{(\mu _0, \mu ) \mid \mu _0 \mathop {\rightarrow }\limits ^{\sigma } \mu , \ \) for some \( \ \sigma \in T^{*}\}\).

A subset L of \(N^k\) is a linear set if there exist vectors \(v_0,v_1, \dots , v_t\) in \(N^k\) such that \(L = \{ v \mid v = v_0 + m_1v_1 + \cdots + m_tv_t, \ m_i \in N\}\). The vectors \(v_0\) (referred to as the constant vector) and \(v_1, v_2, \dots , v_t\) (referred to as the periods) are called the generators of the linear set L. A set \(SL \subseteq N^k\) is semilinear if it is a finite union of linear sets, i.e., \(SL = \bigcup _{1 \le i \le d} \mathcal{L}_{i}\), where \(\mathcal{L}_{i}\) (\(\subseteq N^k\)) is a linear set. It is worthy of noting that semilinear sets are exactly those that can be expressed by Presburger Arithmetic (i.e., first order theory over natural numbers with addition), which is a decidable theory.

A PN is said to be semilinear if has a semilinear reachability set. In addition to the trivial example of finite PNs, the following are notable classes of semilinear PNs, including PNs of dimension 5 [4], conflict-free [7], persistent [7], normal [15], sinkless [15], weakly persistent [14], cyclic [1], communication-free PNs [2, 5], and several others (see [16] for more). It is also known that checking whether a PN has a semilinear reachability set is decidable [3]. In view of the above, a natural question to ask is to identity, if at all possible, the key behind the exhibition of semilinear reachability sets for such a wide variety of restricted PN classes, while their restrictions are imposed on the PN model either structurally or behaviorally. We are able to answer the question affirmatively to a certain extent. In what follows, we give a sketch for the idea behind our unified strategy. The idea was originally reported in [17]. As we shall explain later, for each of considered PNs, any reachable marking is witnessed by somewhat of a canonical computation which will be elaborated later. Furthermore, such canonical computations can be divided into a finite number of groups, each of which has a finite number of “minimal computations” associated with a finite number of “positive loops.” As one might expect, such minimal computations and positive loops exactly correspond to the constant vectors and periods, respectively, of a semilinear set. It is worth pointing out that the implication of our approach is two-fold. First, we are able to explain in a unified way a variety of semilinearity results reported in the literature. Second, perhaps more importantly, our approach yields new results in the following aspects:

  1. (i)

    new semilinearity results for additional subclasses of PNs,

  2. (ii)

    unified complexity and decidability results for problems including reachability, model checking, etc.

Given an \(\alpha =r_1 \cdots r_{d-1} \in T^*\) and an initial marking \(\mu _0\), a computation of the form

$$\begin{aligned} \pi : \ \mu _0 \mathop {\rightarrow }\limits ^{\sigma _0} \mu _1 \mathop {\rightarrow }\limits ^{r_1} \bar{\mu }_1 \mathop {\rightarrow }\limits ^{\sigma _1} \mu _2 \mathop {\rightarrow }\limits ^{r_2} \cdots \mathop {\rightarrow }\limits ^{r_{d-1}} \bar{\mu }_{d-1} \mathop {\rightarrow }\limits ^{\sigma _{d-1}} \mu _{d}, \end{aligned}$$

where \(\mu _i, \bar{\mu _j} \in N^k\), and \(\sigma _r \in T^*\) (\(0 \le i \le d, 1 \le j \le d-1, 0 \le r \le d\)), is called an \(\alpha \)-computation. We write \(cv(\pi )=(\mu _1, ..., \mu _d)\). Suppose \(\delta _i \in T^{*}, 1 \le i \le d\), are transition sequences such that \(\varDelta (\delta _i) \ge 0\) and \((\mu _i + \sum ^{i-1}_{j=1}\varDelta (\delta _j)) \mathop {\rightarrow }\limits ^{\delta _i}\), then following the monotonicity property of PNs,

$$\begin{aligned} \pi ': \mu _0 \mathop {\rightarrow }\limits ^{\sigma _0\delta _1} \mu '_1 \mathop {\rightarrow }\limits ^{r_1} \bar{\mu }'_1 \mathop {\rightarrow }\limits ^{\sigma _1\delta _2} \mu '_2 \mathop {\rightarrow }\limits ^{r_2} \cdots \mathop {\rightarrow }\limits ^{r_{d-1}} \bar{\mu }'_{d-1} \mathop {\rightarrow }\limits ^{\sigma _{d-1}\delta _d} \mu '_d \end{aligned}$$

remains a valid PN computation. In fact, we have \(\mu _0 \mathop {\rightarrow }\limits ^{\sigma _0(\delta _1)^+ r_1 \sigma _1(\delta _2)^+ r_2 \cdots r_{d-1}\sigma _{d-1}(\delta _d)^+}\), meaning that \(\delta _1, ..., \delta _{d}\) constitute “pumpable loops”. In view of the above and if we write \(cv(\pi ) \mathop {\Rightarrow }\limits ^{(\delta _1, \cdots , \delta _d)} cv(\pi ')\), clearly “\(\Rightarrow \)” is transitive as \(v \mathop {\Rightarrow }\limits ^{(\alpha _1, \cdots , \alpha _d)} v'\) and \(v' \mathop {\Rightarrow }\limits ^{(\delta _1, \cdots , \delta _d)} v''\) imply \(v \mathop {\Rightarrow }\limits ^{(\alpha _1\delta _1, \cdots , \alpha _d\delta _d)} v''\), where \(v, v', v'' \in (N^k)^d\), \(k=|P|\).

It turns out that the following properties are satisfied by several interesting subclasses of PNs all of which have semilinear reachability sets. With respect to an \(\alpha \in T^d\),

  1. (1)

    there is a finite set of transition sequences \(F \subseteq {T^{*}}\) with nonnegative displacements (i.e., \(\forall \gamma \in F\), \(\varDelta (\gamma ) \ge 0\)) such that if \((\mu _1, \cdots , \mu _d) \mathop {\Rightarrow }\limits ^{(\delta _1, \cdots , \delta _d)} (\mu '_1, \cdots , \mu '_d)\) in some \(\alpha \)-computations, then \(\delta _i = \gamma ^i_1 \cdots \gamma ^i_{h_i}\), for some \(h_i\) where \(\gamma ^i_j \in F\) (i.e., \(\delta _i\) can be decomposed into \(\gamma ^i_1 \cdots \gamma ^i_{h_i}\)), and

  2. (2)

    the number of “minimal” \(\alpha \)-computations is finite.

Intuitively, (2) ensures the availability of a finite set of constant vectors of a semilinear set, while (1) allows us to construct a finite set of periods based on those \(\varDelta (\gamma ), \gamma \in F\).

A PN \(\mathcal{P}=(P, T, \varphi )\) with initial marking \(\mu _0\) is said to be computationally decomposable (or simply decomposable) if every reachable marking \(\mu \in R(\mathcal{P}, \mu _0)\) is witnessed by an \(\alpha \)-computation (\(\alpha \in T^*\)) which meets Conditions (1) and (2) above. \(\mathcal{P}\) is called globally decomposable if \(\mathcal{P}\) is decomposable for every initial marking \(\mu _0 \in N^k\). Let \(RR_{\alpha }(\mathcal{P}, \mu _0) = \{ cv(\pi ) \mid \pi \) is an \( \ \alpha \)-computation from \( \ \mu _0 \) for some \( \alpha \in T^* \}\), and \(RR_{\alpha }(\mathcal{P}) = \{ (\mu _0, cv(\pi )) \mid \pi \) is an \( \ \alpha \)-computation from \( \ \mu _0\) for some \( \alpha \in T^*\}\). We are able to show that if a PN is decomposable (resp., globally decomposable) then \(RR_{\alpha }(\mathcal{P}, \mu _0)\) (resp., \(RR_{\alpha }(\mathcal{P})\)) is semilinear.

Among various subclasses of PNs, conflict-free, persistent, normal, sinkless, weakly persistent, cyclic, and communication-free PNs can be shown to be decomposable. Furthermore, each of the above classes of PNs also enjoys a nice property that

  1. (3)

    there exists a finite set \(\{\alpha _1, ..., \alpha _r\} \subseteq T^*\) (for some r) such that every reachable marking of the PN is witnessed by an \(\alpha _i\)-computation, for some \(1 \le i \le r\).

As a result, our unified strategy shows \(R(\mathcal{P}, \mu _0)\) of a PN \(\mathcal{P}\) with initial marking \(\mu _0\) for each of the above subclasses to be semilinear. Furthermore, a stronger result shows that conflict-free and normal PNs are globally decomposable; hence, their reachability relations \(R(\mathcal{P})\) are always semilinear.

For semilinear PNs, a deeper question to ask is: What is the size of its semilinear representation? An answer to the above question is key to the complexity analysis of various problems concerning such semilinear PNs. To this end, we are able to incorporate another ingredient into our unified strategy, yielding size bounds for the semilinear representations of the reachability sets. Consider a computation \(\mu \mathop {\rightarrow }\limits ^{\sigma } \mu '\). Suppose \(T=\{t_1, ..., t_h\}\). For a transition sequence \(\sigma \in T^*\), let \(PK(\sigma )=(\#_{\sigma }(t_1), ..., \#_{\sigma }(t_h))\) be an h-dimensional vector of nonnegative integers, representing the so-called Parikh map of \(\sigma \). The i-th coordinate denotes the number of occurrences of \(t_i\) in \(\sigma \). In addition to Conditions (1)-(3) above, if the following is also known for a PN:

  1. (4)

    a function \(f(\mu )\) which bounds the size of each of the minimal elements of \(ER(\mu )=\{(PK(\sigma ), \mu ') \mid \mu \mathop {\rightarrow }\limits ^{\sigma } \mu '\}\) (i.e., the so-called extended reachability set),

then we are able to come up with a bound for the size of the semilinear representation of a PN’s reachability set.

Semilinearity for PNs is also related to the concept of the so-called flatness. A PN is said to be flat if there exist some words \(\sigma _1, ..., \sigma _r \in T^*\) such that every reachable marking \(\mu \) is witnessed by a computation \(\mu _0 \mathop {\rightarrow }\limits ^{\sigma } \mu \) with \(\sigma \in \sigma ^*_1 \cdots \sigma ^*_r\), i.e., it has a witnessing sequence of transitions belonging to a bounded language. It is not hard to see the reachability set of a flat PN to be semilinear, and as shown in [10], a variety of known PN classes are indeed flat. In a recent article [9], flatness is shown to be not only sufficient but also necessary for a PN to be semilinear. We shall compare flat PNs with the aforementioned decomposable PNs.

Finally, we also briefly touch upon recent advances for the general PN reachability problem in which the notion of (almost) semilinearity is essential in yielding a simpler decidability proof [8] in comparison with that of [6, 13].