I. INTRODUCTION

Petri nets^{[1,2,3,4,5,6,7,8,9,10,11]} have been widely used for modeling and control ofdiscrete event system (DES) since 1960s. As a well-known analysis tool of Petri nets, reachability trees, i.e., the tree representations of their reachability sets, are fundamental and powerful for checking various properties such as reachability, boundedness, liveness, reversibility and coverability^{[12,13,14,15,16,17,18,19]}. However, such a tree may be an infinite tree for a given initial state or marking^[7]. In past decades, many scholars focused on finding a finite representation for an infinite reachability tree.

In 1969, Karp and Miller^[4] developed a finite reachability tree (FRT) method by introducing a special symbol ω, to represent an infinite component in markings resulting from some transition firing loops. FRT is useful in determining such properties as safeness, boundedness, conservativeness, and coverability^[6,7]. However, it fails to solve deadlocks^[20,21,22], liveness^[23], and reachability problems of unbounded nets due to the information loss caused by the use of ω.

Wang^[16] proposed a modified reachability tree (MRT) method. An MRT can capture more information about the underlying net than an FRT since it adopts the expression $a+bn_{i}$ suggested by Peterson^[7] rather than ω to represent the value of some component of a marking. Later, a computer program for the automated generation of an MRT for a Petri net was developed in [24]. Jeng and Peng^[13,14] extended the capability of FRT for determining liveness, and proposed an augmented reachability tree (ART), which is applicable to one-place-unbounded nets only.

Wang et al.^[17] formalized and improved their previous results in [16] with a proof for the finiteness of an MRT and its usefulness in solving reachability, deadlock and liveness problems. Their work sets a milestone toward the solution of this long-standing problem. However, the set of markings represented by the nodes of an MRT is not necessarily equal to that of reachable markings^{[12,13,14,15]}. Wang et al. proposed an improved reachability tree (IRT) for one-place-unbounded nets in [19]. The set of markings represented by an IRT is equal to that of reachable markings.

Motivated by the aforementioned work, Wang et al.^[18] proposed a new modified reachability tree (NMRT) method for ω-independent unbounded nets, which has a larger application scope than all the existing methods. An NMRT consists of only but all reachable markings from its initial marking and can correctly check deadlocks. However, it still suffers from a problem that the number of nodes in the tree grows rapidly with respect to the net size.

In order to decrease the number of nodes in a reachability tree, this work proposes a reduced reachability tree for ω-independent nets based on NMRTs, and we call it an ωRT for short. The ωRT removes duplicate and ω-duplicate nodes in the tree such that the number of nodes decreases. The rest of this paper is organized as follows. Section II briefly reviews preliminaries used in this paper. An ωRT construction algorithm is presented in Section III. Section IV provides an example for the proposed method to illustrate its superiority. Finally, conclusions are presented in Section V.

II. PRELIMINARIES

In the remaining discussion, assume ${\bf Z}$, ${\bf N}$, and ${\bf N^{+}}$, denote the set of integers, nonnegative integers, and positive integers, respectively.

A. Basics of Petri Nets

The following basics of Petri nets (PNs) are due to [5,6,7].

A generalized PN is a 4-tuple ${N = (P, T, F, W)}$, where $P$ and $T$ are finite, non-empty, and disjoint sets. $P$ is the set of places and $T$ is the set of transitions with $P\cup T$ $\neq\emptyset$ and $P\cap T$, =, $\emptyset$. $F\subseteq(P\times T)$ $\cup, (T\times P)$ is called a flow relation of the net, represented by arcs with arrows from places to transitions or from transitions to places. $W$ is a mapping that assigns a weight to an arc: $W(x, y)>0$ if $(x, y)\in F$, and $W(x, y)=0$ otherwise, where, $x, y\in P\cup T$.

A marking $\mu$ represents a system state, which shows the number of tokens contained in each place $p\in P$. The initial marking is denoted as $\mu_{0}$. A transition $t\in T$ is enabled at $\mu$ if $\forall p\in\bullet t$, $\mu(p)\geq W(p, t)$. The fact is denoted by $\mu [t\rangle$. Firing it yields a new marking $\mu'$ such that $\forall p\in P$, $\mu'(p) =\mu(p)-W(p, t)+ W(t, p)$, as denoted by $\mu[t\rangle\mu'$. $\mu'$ is called an immediately reachable marking from $\mu$. $\mu"$ is said to be reachable from $\mu$ if there exists a sequence of transitions $\sigma=t_{0}t_{1}\ldots t_{n}$ and markings $\mu_{1}, \mu_{2}, \ldots$, and $\mu_{n}$ such that $\mu[t_{0}\rangle \mu_{1}[t_{1} , \ldots, \mu_{n}[t_{n}\rangle \mu"$ holds. The set of markings reachable from $\mu_{0}$ in N is called the reachability set of $(N, \mu_{0})$ and denoted by $R(N, \mu_{0})$.

Given a PN $(N, \mu_{0})$, $t\in T$ is live at $\mu_{0}$ if $\forall \mu\in R(N, \mu_{0})$, $\exists \mu'\in R(N, \mu)$, $\mu'[t\rangle$. $(N, \mu_{0})$ is live if $\forall t\in T$, t is live at $\mu_{0}$. $(N, \mu_{0})$ is dead at $\mu_{0}$ if$\nexists$ $t\in T$, $\mu_{0}[t\rangle$. $(N, \mu_{0})$ is deadlock-free (weakly live or live-locked) if $\forall \mu\in R(N, \mu_{0})$, $\exists t\in T$, $\mu[t\rangle$. It is bounded if $\exists$ $k$ $\in {\bf N}^{+}$, $\forall \mu\in R(N, \mu_{0})$, $\forall p\in P$, $\mu(p)\leq k$. It is said to be unbounded if it is not bounded.

B. ω-number

The definitions and notations of ω-numbers in this subsection are from [16,17,18].

1) ω-number. A subset of integers S is called an ω-number if $\exists k\in {\bf N}^{+}, n, q\in {\bf Z}$ such that $S = \{ ik + q|i \ge n, 0 \le q < k\} $. S can be expressed uniquely as $S=\omega(k, n, q)\equiv k$ ω $_n + q \equiv \{ ik + q|k \in {{\bf{N}}^ + }, n \in {\bf{Z}}, 0 \le q < k, i \ge n\} $, where $\omega(k, n, q)$ or $k\omega_{n}+q$ is called a canonical ω-number with $k$ as its base, $n$ the last bound, and $q$ the remainder.

2) Addition of ω-number and integers. Given an ω-number $\omega(k, n, q)$ and an integer $a\in {\bf Z}$, it is defined that $\omega(k, n, q)+a=\omega(k, n+s, r)$, where $q+a=sk+r$, $s\in {\bf Z}$,$0 \le r < k$.

3) Comparison of two ω-numbers. Let ${{\bf Z}_{\omega}}$ be the set of integers and ω-numbers. $\forall a, b\in {\bf Z}$, $a\leq b$ is defined as either $a, b\in {{\bf Z}_{\omega}}$ and $a\leq b$ or $a=\omega(k, m, q)$, $b=\omega(k, n, q)$, and $m\leq n$. Note that in the second case, $b$ is a subset of $a$, i.e., $a\supseteq b$, if both can be viewed as sets.

4) Comparison of two ω-vectors. A vector x, $\in$ ${\bf Z}^{n}_\omega$ is called an ω-vector if at least one of its elements is an ω-number. Note that if x has no ω-number, it is simply an $n$-dimensional integer vector, i.e., $x\in {\bf Z}^{n}$. A marking $\mu$ is called an ω-marking if it can be represented by an ω-vector. An ω-marking can be viewed as a set of ordinary markings. An ω-marking $a$ is less than or equal to $b$ (or $a$ contains $b$) if $a$ and $b$ have the same non-ω-number coordinates, and the other coordinates of $a$ are less than or equal to the ones of $b$.

C. NMRT

Following [18], we give the following definitions.

${\bf Definition 1.}$ At an ω-marking $\mu$ that is a set of ordinary markings, $t\in T$ is enabled if $t$ is enabled at each ordinary marking in $\mu$; $t$ is not enabled at $\mu$ if $t$ is not enabled at any ordinary marking in $\mu$; $t$ is conditionally enabled at $\mu$ if it is not enabled at some ordinary markings in $\mu$ but enabled at any other ordinary marking in $\mu$.

In the remaining discussion, assume that the next-state marking function $\delta(\mu, t)$ is the marking resulting from firing $t$ at $\mu$.

${\bf Definition 2.}$ Given a marking $\mu$ and $t\in T$,

1) If $\mu$ is an ordinary marking and $t$ is enabled at $\mu$, then $\delta(\mu, t)$ is computed by using the transition firing rule for ordinary markings;

2) If $\mu$ is an ω-marking and $t$ is enabled at $\mu$, then $\delta(\mu, t)$ is computed by using the transition firing rule for ordinary markings and the addition of ω-numbers and integers;

3) If $\mu$ is an ω-marking and $t$ is conditionally enabled at $\mu$, then $\delta(\mu, t)$ is computed as follows:

a) Let $\mu'$ be an ω-marking derived from $\mu$ by removing each ordinary marking of $\mu$ at which $t$ is not enabled;

b) Let $\delta (\mu, t) = \delta (\mu', t)$, where $\delta(\mu', t)$ is computed in the same way as 2).

${\bf Definition 3.}$ Let x and z be two nodes in an NMRT, where $\mu_{z}$ is the marking resulting from firing transition $t$ at the current marking $\mu_{x}$ and $\mu_{z}$$\neq $$\delta(\mu_{x}, t)$. $\mu_{z}$ is called ω-dependent if there exists a node $y$ on the path from the root node to z such that 1) $\delta(\mu_{x}, t)> \mu_{y}$ and 2) at least two components in $\delta(\mu_{x}, t)$ are larger than the corresponding ones in $\mu_{y}$.

${\bf Definition 4.}$ Given an unbounded PN $(N, \mu_{0})$ and its NMRT obtained by the algorithm in [18]. $(N, \mu_{0})$ is called ω-independent if its NMRT does not contain any ω-dependent markings. Otherwise, it is called ω-dependent.

For example, in Fig. 1(b), $\mu_{2}=(\omega_{1}, \omega_{1})$ is an ω-dependent marking since $\mu_{2}\neq \delta(\mu_{0}, t_{2})$, $\delta(\mu_{0}, t_{2})=(1, 1)>(0, 0)$ and two components in (1, 1) are larger than those respective ones in (0, 0). Similarly, $\mu_{4}$ can be verified to be an ω-dependent marking. Therefore, the net in Fig. 1(a) is ω-dependent. While, the net in Fig. 2(a) is ω-independent since its NMRT contains no ω-dependent markings.

Fig. 1

	Download: JPG larger image
Fig. 1 (a) An ω-dependent unbounded net and (b) Its NMRT.

Fig. 2

	Download: JPG larger image
Fig. 2 (a) An ω-independent unbounded net and (b) Its NMRT.

III. GENERATION OF REDUCED REACHABILITY TREES

A. Construction Algorithm for ωRT

To describe an ωRT, four types of nodes are introduced including: terminal, duplicate, ω-duplicate and common nodes pictured by the circle with oblique lines, the filled circle, the circle with vertical lines and the hollow circle, respectively. A terminal node is a node corresponding to a dead marking without any enabled transitions. The definitions of duplicate and ω-duplicate nodes are as follows.

${\bf Definition 5.}$ Let x with a marking $\mu_{x}$ be a current node of an ωRT. It is called a duplicate node if $\mu_{x}$ has been computed previously during the procedure of constructing an ωRT.

${\bf Definition 6.}$ Let x with an ω-marking $\mu_{x}$ be a current node of an ωRT. It is called an ω-duplicate node if $\mu_{x}$ can be contained by an ω-marking $\mu_{y}$ of another node that was computed previously during the procedure of constructing an ωRT.

${\bf Remark 1.}$ These concepts of "duplicate" and "ω-duplicate nodes" are first proposed in [17] and used in the algorithm proposed in [18]. As stated in [17,18], a duplicate node is a node with a marking that previously appears in the tree along the same path and an ω-duplicate node is a node with a ω-marking that is contained by another node that appears previously in the tree along the same path. Note that in this paper, pduplicateq and pω-duplicate nodesq in generating an ωRT is based on these modified definitions.

An ωRT construction algorithm for ω-independent nets based on NMRTs is stated as follows.

$\textbf{Algorithm 1. Construction algorithm for ωRT}$

$\textbf{Input:}$ An ω-independent PN (N,$\mu_{0}$).

$\textbf{Output: }An ωRT.$

1) Let $x_{0}$ be the root node of the ωRT and $\mu_{0}$ be the marking of node $x_{0}$;

2) Initialize the stack $\Lambda: =(x_{0})$ and the set $\Xi:={\mu_{0}}$;

/*$\Lambda$ is a stack consisting of common nodes and Ξ a set containing all the markings of nodes that have appeared in the tree computed by this algorithm */

3) ${\bf{while\Lambda }} \ne (){\bf{do}}$

4)$\quad x: = pop(\Lambda );$

/*Remove the last node x from the stack.*/

5) Let $\mu_{x}$ be the marking of node x;

6)$\quad \textbf{ for }$ each $t\in T\; \textbf{do}$

7)$\quad\quad \textbf{ if }$ t is enabled or conditionally enabled at $\mu_{x}\; \textbf{then}$

8)$\quad\quad\quad$ Compute the next-state function $\delta(\mu_{x}, t)$ by

$\quad\quad\quad$ Definition 2 and create a new node z;

9)$\quad\quad \textbf{if}$ there exists a node $y$ in the path from $x_{0}$ to x

$\quad\quad\quad$ with $\delta(\mu_{x}, t)> \mu_{y} \;\textbf{then}$

10)$\quad \quad \quad {\bf{for}}\;each\;p \in P\;{\bf{do}}$

11)$\quad \quad \quad \;{\bf{if}}\;\delta {({\mu _x}, t)_p} > {({\mu _y})_p}\;and\;\delta {({\mu _x}, t)_p} \in {\bf{N}}\;{\bf{then}}$

12)$\quad \quad {({\mu _z})_p}: = \omega (k, n, q), wherek = \delta {({\mu _x}, t)_p} - {({\mu _y})_p}, $

$\quad \quad \delta {({\mu _x}, t)_p} = nk + q, and\;0 \le q < k;$

13)$\quad\quad\quad \textbf{ else}$

14)$\quad\quad\quad (\mu_{z})_{p}:=\delta(\mu_{x}, t)_{p}$;

15)$\quad\quad \textbf{ end if}$

16)$\quad\quad \textbf{end for}$

17)$\quad \textbf{ else}$

18)$\quad\quad \mu_{z}:=\delta(\mu_{x}, t)$;

19)$\quad \textbf{end if}$

20)$\quad$Ξ := Ξ$\cup {\mu_{{z}}}$;

21)$\quad \textbf{if}$ z is a common node $\textbf{ then}$

22)$\quad \quad \Lambda : = push(\Lambda , z)$;

/*Push node z into stack $\Lambda$ as the last node in $\Lambda$.*/

23)$\quad \textbf{end if}$

24)$\quad \textbf{ if }$ t is enabled at $\mu_{x} \textbf{then}$

25)$\quad\quad$ Add a solid arc $t$ from x to z;

/* A solid arc indicates that $t$ is enabled at $\mu_{x}$.*/

26)$\quad \textbf{else}$

27)$\quad\quad$ Add a dotted arc $t$ from x to z;

/*A dotted arc indicates that $t$ is conditionally enabled at $\mu_{x}$.*/

28)$\quad \textbf{end if}$

29)$\quad\textbf{end if}$

30)$\quad \textbf{end for}$

31) $\textbf{end while}$

32) $\textbf{end.}$

Given an ω-independent net, its ωRT can be constructed by Algorithm 1. We briefly explain this algorithm as follows. First, let $x_{0}$ be the root node of an ωRT and $\mu_{0 }(0, 0)$ the marking of $x_{0}$, $\Xi= \{{\mu_{0}}\}, \Lambda=(x_{0})$. Second, remove the last node from a stack $\Lambda$, and then obtain the current marking $\mu_{x}$. Third, for each $t\in T$ that is enabled or conditionally enabled at $\mu_{x}$, compute the next-state $\delta(\mu_{x}, t)$ by Definition 2, and then obtain the next-state marking $\mu_{z}$ according to the rule proposed in this paper. Finally, a new node z is created and is pushed into $\Lambda$ if it is a common node. Repeat these steps until $\Lambda$ is empty and an ωRT is hence constructed.

Compared with NMRT, ωRT can decrease the number of nodes in the reachability tree by eliminating more duplicate and ω-duplicate nodes that have been computed already. An ω-independent unbounded net with two unbounded places is shown in Fig. 3(a) and (b) is its NMRT with 35 nodes. It is \noindent easy to see that more than a half of nodes are reduced by using ωRT since its ωRT shown in Fig. 3(c) has only 17 nodes. Clearly, our method successfully decreases the number of nodes in the reachability tree.

Fig. 3

	Download: JPG larger image
Fig. 3 (a) An ω-independent unbounded net with two unbounded places, (b) Its NMRT, and (c) Its ωRT.

B. Applications of ωRT

The following theorems guarantee the finiteness of ωRTs and their usefulness in determining reachability, deadlocks, and liveness of ω-independent unbounded PNs.

${\bf Theorem 1 (Finiteness).}$ The ωRT of an ω-independent unbounded Petri net is finite.

${\bf Proof. }$ It has been proved that an NMRT is finite in [18]. As shown earlier, an NMRT just removes some duplicate nodes with markings that previously appear in the path from the root node to the current node and ω-duplicate nodes with ω-markings that are contained by another node in the path from the root node to the current node. While an ωRT removes some duplicate nodes with markings that previously appear in the whole tree and ω-duplicate nodes with ω-markings that are contained by another node in the tree. Clearly, the number of nodes in an ωRT is smaller than that in an NMRT. Therefore, the conclusion holds.

$\square$

${\bf Theorem 2 (Reachability).}$ The ωRT of an ω-independent unbounded Petri net consists of only but all reachable markings from its initial marking.

${\bf Proof.}$ It has been proved in [18] that the NMRT of an ω-independent unbounded Petri net consists of all and only reachable markings from its initial marking. Hence, we only need to prove that the ωRT represents the same marking set as the NMRT for the ω-independent unbounded Petri net. Obviously, we can transform the NMRT into the ωRT by eliminating some duplicate and ω-duplicate nodes that have been computed in the NMRT. Hence, the ωRT represents the same marking set as the NMRT. Therefore, we can conclude that the ωRT of an ω-independent unbounded Petri net consists of only but all reachable markings from its initial marking.

$\square$

${\bf Theorem 3 (Deadlock-checking).}$ An ω-independent unbounded Petri net has deadlocks if and only if its ωRT contains terminal nodes or full conditional nodes.

${\bf Proof.}$ Sufficiency: By the definition of terminal nodes or full conditional nodes, we can conclude that there exists a dead marking in terminal nodes or full conditional nodes. Since the ωRT contains terminal nodes or full conditional nodes, there exists a dead marking in the ωRT. Hence, there exists a dead marking in the ω-independent unbounded Petri net by Theorem 2. Therefore, the ω-independent unbounded Petri net has deadlocks.

Necessity: By Theorem 2, there exists a dead marking in the ωRT, since the ω-independent unbounded Petri net has deadlocks. Obviously, only terminal nodes or full conditional nodes contain dead markings for all nodes in the ωRT. Hence, the ωRT contains terminal nodes or full conditional nodes.

$\square$

IV. EXAMPLE

An illustrative example is presented in this section to show the superiority of ωRT. An ω-independent unbounded net with three unbounded places is shown in Fig. 4(a) and its ωRT is shown in (b). We can see that there are only 65 nodes in its ωRT. However, there are more than 600 nodes in its NMRT. Due to the space limit, we do not present its NMRT and more details about its NMRT are in Appendix. Trivially, the number of nodes in its ωRT is much smaller than that in its NMRT. This example illustrates that our method can drastically decrease the number of nodes in a reachability tree by eliminating numerous duplicate and ω-duplicate nodes in the tree. Besides, our method can avoid spurious markings and can correctly check deadlocks for ω-independent nets. According to Theorem 3, it is easy to see that the net in Fig. 4(a) is deadlock-free.

Fig. 4

	Download: JPG larger image
Fig. 4 (a) An ω-independent unbounded net with three unbounded places and (b) Its ωRT.

V. CONCLUSION

How to establish a finite reachability tree to solve reachability problems of arbitrary unbounded nets has remained an open problem since the inception of Petri nets half a century ago^[25,26,27]. Due to its extreme difficulty, only limited progress has been made.

In this work, we propose a reduced reachability tree called ωRT for ω-independent nets based on new modified reachability trees. It can drastically decrease the number of nodes by removing some duplicate nodes and ω-duplicate nodes in the tree. Furthermore, ωRT can be used to determine some properties such as reachability, liveness and deadlocks as well.

Since the method proposed in this paper can be applicable for ω-independent nets only, future work should extend the proposed results to more general classes of Petri nets. Additional efforts to reduce such tree size should be made, e.g., by allowing the net to fire multiple transitions whenever no conflicts are involved. Computer aided design tools should be developed to facilitate the applications of the proposed finite trees to such application fields as industrial hybrid systems, Internet-based game systems, Internet of things and Internet of vehicles^[28,29,30].