Combinatorics and resource circuit–based enumeration of reachable states for S 3 PR

Abstract

Reachability graphs can accurately reflect the state information of bounded Petri nets. However, the complexity of reachability graphs generation is exponential, which makes time waste and sometimes the computation may stop midway after a long time due to exhausted memory. Hence, this work presents combinatorics and resource circuit–based method to estimate the number of reachable states for a class of Petri nets–S³PR. First, by combinatorics, an upper bound of reachable states of an S³PR can be calculated. The upper bound is the sum of reachable states and unreachable states. Hence, the next step is to obtain the number of unreachable states. By analysis, it is found that there exists a close relationship between resource circuits and the unreachable states. Therefore, the number of unreachable states of an S³PR can be found by extracting all the resource circuits. Finally, the resulting number of subtracting the number of unreachable states from the upper bound is the expected result. In addition, example calculation and analysis are given to show the effectiveness of the proposed method.

Introduction

Behavioral permissiveness is a very important criterion to evaluate the performance of a liveness-enforcing supervisor.^1–4 Reachability trees (RT) and reachability graphs (RG) are powerful analysis tools to systematically investigate many characteristics of Petri nets, such as boundedness, liveness, and reversibility. For unbounded Petri nets, there exist infinite reachable states. RT^5–7 can represent an unbounded Petri net by introducing a special symbol $\omega$ , to represent an infinite component in states. However, there exists the problem of reachability information loss caused by the usage of $\omega$ . RG cannot describe the complete behavior of an unbounded Petri net in a finite structure. However, it can provide complete reachability information for bounded Petri nets. This work mainly refers to S³PR, a class of bounded Petri nets. In an RG, there exist four zones: ⁸ live zone, dangerous zone, bad zone, and deadlock zone. Among them, the state in the live zone is called a good state, which can always reach initial state. The states in the deadlock zone are all deadlocks. Without control, the states in the dangerous zone may reach bad even deadlock states. The states in the bad zone are called bad states, which will inevitably reach deadlock states. A liveness-enforcing supervisor with all good states is what we long for and called optimal supervisor.^9–11 The RG of a Petri net is a graph that contains all states of the Petri net and shows the relationship between the states via enabled transitions.

By an RG, a suboptimal or optimal supervisor can always be obtained. The theory of regions is an effective approach, which depends on a complete enumeration of reachable states. It can definitely find an optimal liveness-enforcing supervisor if it exists. ¹² Uzam and Zhou^13,14 use region analysis to an S³PR ¹⁵ (System of Simple Sequential Processes with Resources) to obtain a nearly maximally permissive control policy. In Zhao and Hou, ¹⁶ RG is used to synthesize non-blocking supervisor for G-systems by a divide-and-conquer method. It in general can lead to an optimal or a suboptimal liveness-enforcing supervisor. Binary decision diagrams (BDD) can represent large sets of reachable states with small shared data structures and implement the efficient manipulation on those sets. BDD is used by Chen et al.^17,18 to represent the state space in order to overcome the state explosion problem.

The above RG-based methods can provide a suboptimal or optimal supervisor. However, the generation of RG is based on transition fire relationship and it contains the process of excluding repetitive states, which implies that it is a calculation with high computational complexity ¹⁹ and reachability analysis is impossible by using the popular integrated net analyzer (INA) ²⁰ to analyze large Petri net models. It usually takes a very long time to complete the reachability analysis. In the worst case, it may stop midway due to insufficient memory.

Consequently, it is necessary to find an approach, with a low computational complexity and independent of generating RG via transition fire relationship, to enumerate the reachable states. The computational complexity of RG-based methods will reduce as the reduction of computational complexity of generating RG. Moreover, in order to avoid the fruitless calculation, it is necessary to predict the outcome before one conducts the state analysis. If the result shows that the state analysis will stop in vain, one would not conduct it. Combinatorics can realize the enumeration in a low computational complexity. By combinatorics, the upper bound of the reachable states and unreachable states of a Petri net can be found, which give us an opportunity to enumerate the reachable states in a low computational complexity. Furthermore, by combinatorics, the number of reserved legal states after adding monitors can be obtained, which is useful for checking the performance of a liveness-enforcing supervisor.

In the work by Hong and Chao, ²¹ a method is proposed to enumerate the reachable states of marked graphs. As a model of flexible manufacturing systems (FMS), an S³PR is more general than a marked graph, and Chao et al. ²² propose a method to enumerate reachable states for an S³PR. They obtain the reachable states by analyzing local states and integrating the local states to global states. However, the method only applies to the Kth order S³PR (with a top left side non-sharing resource place) although it can calculate the number of reachable states rapidly.

In our previous work, a method to calculate the reachable states of an S³PR is proposed, where an upper bound of reachable states is obtained by combinatorics and the number of unreachable states is excluded via siphons. The difference between them is the result to be desired. As an extended research, resource circuits are applied in this work instead of siphons to calculate the unreachable states. The calculated number of reachable states in the work is still an estimate value, which is equal or greater than the actual number. However, the calculated number is very close to the actual number of reachable states.

The rest of this article is organized as follows. Section “Preliminaries” presents the preliminaries used in this study. The three stages of the calculation of reachable states are introduced and the method is shaped to an algorithm in section “Estimate approach.” A well-known S³PR is used as an example to show the detailed calculation of the number of reachable states and a discussion is made in section “Example and discussion.” Finally, section “Conclusions and future work” concludes the article.

Preliminaries

Multisets

Definition 1

A multiset $\mathrm{\Omega }$ , is a mapping $\mathrm{\Omega }:A\to \mathrm{\mathbb{N}}$ , which is represented as a formal sum $\sum _{a\in A}\mathrm{\Omega }(a)·a$ , where A is a non-empty set and $\mathrm{\mathbb{N}}=\{0,1,2,\dots \}$ .

Basics of Petri nets

An ordinary Petri net is a 3-tuple $N=(P,T,F)$ where P and T are finite and non-empty sets. P and T represent the sets of places and transitions, respectively. $F\subseteq (P\times T)\cup (T\times P)$ is called a flow relation, denoted by directed arcs from places to transitions or from transitions to places.

A marking (also called a state) M is a mapping from P to ℕ. The number of tokens in place p is denoted by $M(p)$ . A place p is marked at a marking M if $M(p)>0$ . $M(S)$ denotes the sum of tokens of all places in S, that is, $M(S)=\sum _{p\in S}M(p)$ , where $S\subseteq P$ . S is marked at M if $M(S)>0$ . S is unmarked at M if $M(S)=0$ . $(N,M_0)$ is called a net system or marked net and $M_0$ is called an initial marking of N. A state of a subset $S\subseteq P$ is denoted as $M^S=\sum _{p\in S}{M}^S(p)·p$ , where $M^S(p)$ denotes the number of tokens in place p of S. The sum of tokens of all places in S is denoted by $M(S)$ , that is, $M(S)=\sum _{p\in S}M(p)$ . $M_0^S$ is called an initial state of S such that $\forall p\in S$ , $M_0^S(p)=M_0(p)$ .

Let $x\in P\cup T$ be a node of $N=(P,T,F)$ . ${}^{•}x=\{y\in P\cup T|(y,x)\in F\}$ is called the preset of x and $x^{•}=\{y\in P\cup T|(x,y)\in F\}$ is called the postset of x. Similar notation extended to a set of nodes: given $X\subseteq P\cup T$ , ${}^{•}X={{\cup }_{x\in X}}^{•}x$ , $X^{•}={\cup }_{x\in X}{x}^{•}$ , ${}^{•}X={{\cup }_{x\in X}}^{••}x$ , and $X^{••}={\cup }_{x\in X}{x}^{••}$ .

A transition $t\in T$ is enabled at a marking M if $\forall p{\in }^{•}t$ , $M(p)\ge 1$ and denoted as $M[t〉$ . Firing it yields a new state $M\prime$ such that $\forall p{\in }^{•}t$ , $M\prime (p)=M(p)-1$ , $\forall p\in t^{•}$ , $M\prime (p)=M(p)+1$ , $\forall p\in \{p\in P|p{\notin }^{•}t\cup t^{•}\}$ , $M\prime (p)=M(p)$ , as denoted by $M[t〉M\prime$ . $M\prime$ is called an immediately reachable state from M and M is called a closely previous reachable state of $M\prime$ . A state $M^{″}$ is said to be reachable from M if there exist a sequence of transitions $\sigma =t_0{t}_1\cdots t_n$ and states $M_1,M_2,\dots$ , and $M_n$ such that $M[t_0〉M_1[t_1〉M_2\cdots M_n[t_n〉M^{″}$ holds. The set of states reachable from M in N is called the set of reachable states of Petri net $(N,M)$ and denoted as $R(N,M)$ . $|R(N,M)|$ denotes the number of reachable states in $R(N,M)$ .

A P-vector is a column vector $I:P\to \mathbb{Z}$ indexed by P and a T-vector is a column vector $J:T\to \mathbb{Z}$ indexed by T, where ℤ is the set of integers. The column vectors where every entry equals 0(1) are denoted by 0(1). $[N]$ is a $|P|\times |T|$ integer matrix with $[N](p,t)=W(t,p)-W(p,t)$ . $I^T$ is the transposed versions of vector I. P-vector I is called a P-invariant if $I\ne 0$ and $I^T[N]=0^T$ and $\parallel I\parallel =\{p|I(p)\ne 0\}$ is the support of I. I is minimal if its support is not contained in the support of any other and its components are mutually prime. P-invariant I is a P-semiflow if its every element is non-negative. In this study, a P-semiflow that contains resources is denoted as a P_r-semiflow. $R(\parallel I\parallel ,M_0^{\parallel I\parallel })$ denotes the set of reachable states of the support of P-semiflow I at the initial state $M_0^{\parallel I\parallel }$ . The number of reachable states in $R(\parallel I\parallel ,M_0^{\parallel I\parallel })$ is denoted as $|R(\parallel I\parallel ,M_0^{\parallel I\parallel })|$ . In this work, we use $\sum _{p\in \parallel I\parallel }I(p)·p$ to denote vector I.

S³PR nets

A class of Petri nets called S³PR and first defined by Ezpeleta et al., ¹⁵ which stands for Systems of Simple Sequential Processes with Resources, is introduced via the following definitions.

Definition 2

A simple sequential process (S²P) is a Petri net $N=(\{p^0\}\cup P_A,T,F)$ where $P_A\ne \varnothing$ is the set of operation places, $p^0$ is the idle process place, N is a strongly connected state machine, and every circuit of N contains $p^0$ . ¹⁵ An S²P with resources is a Petri net $N=(\{p^0\}\cup P_A\cup P_R,T,F)$ such that

1. The subnet generated by $X=P_A\cup \{p^0\}\cup T$ is an S²P.

2. $P_R\ne \varnothing$ and $(P_A\cup \{p^0\})\cap P_R=\varnothing$ , where $P_R$ is called the set of resource places.

3. $\forall p\in P_A$ , $\forall t{\in }^{•}p$ , $\forall t\prime \in p^{•}$ , $\exists r_p\in P_R$ , ${}^{•}t\cap P_R={t\prime }^{•}\cap P_R=\{r_p\}$ .

4. (a) $\forall r\in P_R$ , ${}^{••}r\cap P_A=r^{••}\cap P_A\ne \varnothing$ and (b) $\forall r\in P_R$ , ${}^{•}r\cap r^{•}=\varnothing$ .

5. ${}^{••}\left(p^0\right)\cap P_R=(p^0{)}^{••}\cap P_R=\varnothing$ .

In this work, we call a resource place a resource for short.

Definition 3

A system of S²PR, called S³PR for short, is defined as follows: ¹⁵

1. An S²PR is an S³PR.

2. Let $N_i=(\{p_i^0\}\cup P_{A_i}\cup P_{R_i},T_i,F_i)$ , $i\in \{1,2\}$ , be two S³PR such that $(P_{A_1}\cup \{p_1^0\})\cap (P_{A_2}\cup \{p_2^0\})=\varnothing$ , $P_{R_1}\cap P_{R_2}=P_C\ne \varnothing$ , and $T_1\cap T_2=\varnothing$ . Then, the net $N=(P^0\cup P_A\cup P_R,T,F)$ resulting from the composition of $N_1$ and $N_2$ via $P_C$ defined as follows: (1) $P_A=P_{A_1}\cup P_{A_2}$ , (2) $P^0=\{p_1^0\}\cup \{p_2^0\}$ , (3) $P_R=P_{R_1}\cup P_{R_2}$ , (4) $T=T_1\cup T_2$ , and (5) $F=F_1\cup F_2$ is also an S³PR.

3. For $r\in P_R$ , $H(r){=}^{••}r\cap P_A$ is called the set of holders of r.

Estimate approach

The method contains three stages: upper bound calculation, unreachable states determination, and exclusion. For the first stage, combinatorics is applied to calculate the upper bound of reachable states in a very low computational complexity. At the second stage, resource circuit is used to determine unreachable states. At last, the final result is obtained by deducting the number of unreachable states from the upper bound.

Upper bound estimation of reachable states

Theorem 1

The number of combinations to place k elements to m distinguishable containers is $C(m+k-1,k)=(m+k-1)!/[k!(m-1)!]$ . ²³

Corollary 1

Let r be a resource and $I_r$ be a minimal P_r-semiflow with $\parallel I_r\parallel =\{r\}\cup H(r)$ . Suppose that there are m places and k tokens in $\parallel I_r\parallel$ at the initial state $M_0^{\parallel I_r\parallel }$ , then the maximal number of possible reachable states of $\parallel I_r\parallel$ is $|R(\parallel I_r\parallel ,M_0^{\parallel I_r\parallel })|=C(m+k-1,k)$ .

In an S³PR, a resource r and its holders make up the support of a minimal P_r-semiflow. The support is denoted as $\parallel I_r\parallel$ and the number of tokens in it is a constant. Similar to Theorem 1, suppose that there are k tokens and m places in $\parallel I_r\parallel$ , the maximal number of possible reachable states of $\parallel I_r\parallel$ is $C(m+k-1,k)$ . For the net shown in Figure 1, $p_7$ , $p_9$ , and $p_{19}$ make up the support of minimal P_r-semiflow $I_{p_{19}}=p_7+p_9+p_{19}$ , where $p_{19}$ is a resource place. The number of tokens in it is constant 1. $p_{19}$ has two holders $p_7$ and $p_9$ . We can find that the maximal number of possible reachable states of $\parallel I_{p_{19}}\parallel$ is $C(3+1-1,1)=(3+1-1)!/[1!(3-1)!]=3$ .

Figure 1.

(a) An S³PR and (b) its subnet derived by a resource circuit.

Property 1

Based on the multiplication rule of combinatorics, the least upper bound (supremum) of the reachable states of an S³PR $(N,M_0)$ is the product of the maximal number of the possible reachable states of the support of each minimal P_r-semiflow $I_r$ contained in the S³PR, denoted as $|R_b(N,M_0)|=\underset{r\in P_R}{\Pi }|R(\parallel I_r\parallel ,M_0^{\parallel I_r\parallel })|$ .

The places of an S³PR are made up of one or several supports of minimal P_r-semiflows. We suppose that the token distributions of the support of each P_r-semiflow are not affected by each other. And the numbers of tokens in idle places depend on the distributions of tokens in the supports of minimal P_r-semiflows. In this extreme case, according to the multiplication rule of combinatorics, we can find the least upper bound of reachable states of the S³PR.

There are five minimal P_r-semiflows in the S³PR $(N,M_0)$ shown in Figure 1(a). The maximal number of the possible reachable states of the support of each P_r-semiflow can be calculated through Corollary 1. By Property 1, we have

$$\begin{array}{l}|R_b(N\mathrm{,}{M}_0)|=|R(\parallel I_{p_{14}}\parallel \mathrm{,}{M}_0^{\parallel I_{p_{14}}\parallel })|\\ \times |R(\parallel I_{p_{15}}\parallel \mathrm{,}{M}_0^{\parallel I_{p_{15}}\parallel })|\times |R(\parallel I_{p_{16}}\parallel \mathrm{,}{M}_0^{\parallel I_{p_{16}}\parallel })|\\ \times |R(\parallel I_{p_{17}}\parallel \mathrm{,}{M}_0^{\parallel I_{p_{17}}\parallel })|\times |R(\parallel I_{p_{18}}\parallel \mathrm{,}{M}_0^{\parallel I_{p_{18}}\parallel })|\\ \times |R(\parallel I_{p_{19}}\parallel \mathrm{,}{M}_0^{\parallel I_{p_{19}}\parallel })|=3\times 3\times 3\times 2\times 2=360\end{array}$$

Obviously, not all the states in the upper bound are reachable due to the resource competition. In the next stage, we will present an approach to calculate the unreachable states.

Unreachable states exclusion

By experimental analysis, it is found that the unreachable states in the upper bound are related to resource circuits. The following definitions and theorems are proposed to determine the number of unreachable states of an S³PR.

Definition 4

Let $\{r_1,r_2,\dots ,r_m\}\subseteq P_R$ $(m\ge 2)$ be a set of resources in an S³PR $N=(P_0\cup P_A\cup P_R,T,F)$ . A simple circuit $\mathrm{RC}=(r_1,t_1,r_2,t_2,\dots ,r_m,t_m)$ is called a resource circuit if (1) $\forall i\in {\mathrm{\mathbb{N}}}_m=\{1,2,\dots ,m\}$ , $r_i{\in }^{•}{t}_i$ ; (2) $\forall i\in \{2,\dots ,m\}$ , $r_i\in t_{i-1}^{•}$ ; and (3) $r_1\in t_m^{•}$ . $R{C}_R=\{r_i|i\in (1,2,\dots ,m)\}$ and $R{C}_T=\{t_i|i\in (1,2,\dots ,m)\}$ are called the resource support and transition support of $\mathrm{RC}=(r_1,t_1,r_2,t_2,\dots ,r_m,t_m)$ , respectively. $P_{\mathrm{op}}=\{p\in t^{•}\cap P_A|t\in R{C}_R\}$ is called the set of output transitions of RC.

In Figure 1(a), there are six resource circuits, exhibited in Figure 2 and listed as follows: $R{C}^a=(p_{18},t_{13},p_{15},t_{12})$ and $R{C}^b=(p_{18},t_{13},p_{15},t_2)$ , $R{C}^c=(p_{18},t_5,p_{15},t_{12})$ , $R{C}^d=(p_{18},t_5,p_{15},t_2)$ , $R{C}^e=(p_{18},t_4,p_{14},t_3)$ , and $R{C}^f=(p_{18},t_{11},p_{17},t_{10},p_{19},t_7,p_{16},t_6)$ .

Figure 2.

Resource circuits of the net in Figure 1 (a): (a) RC^a, (b) RC^b, (c) RC^c, (d) RC^d, (e) RC^e, and (f) RC^f.

For an S³PR $(N,M_0)$ , there may exist unreachable states in $R_b(N,M_0)$ . Consequently, we propose a method to exclude most or even all of the unreachable states.

Definition 5

Let $R_b(N,M_0)$ and $R(N,M_0)$ denote the sets of reachable states computed by Property 1 and actual reachable states of an S³PR $(N,M_0)$ , respectively. An unreachable state is a state that belongs to $R_b(N,M_0)$ but not to $R(N,M_0)$ . The set of unreachable states is denoted as $R_u(N,M_0)=\{M|M\in R_b(N,M_0)\wedge M\notin R(N,M_0)\}$ .

Definition 6

Let $N=(P,T,F)$ be an S³PR with $P_S\subseteq P$ and $T_S\subseteq T$ . $N_S=(P_S,T_S,F_S)$ is called a subnet generated by $P_S\cup T_S$ if $F_S=F\cap [(P_S\times T_S)\cup (T_S\times P_S)]$ . $N_S$ is called a subnet derived by resource circuit RC, denoted as ${}^{*}{N}_S$ if there exists a resource circuit $\mathrm{RC}=(r_1,t_1,r_2,t_2,\dots ,r_m,t_m)$ such that $R{C}_R=P_{\mathrm{SR}}$ , $P_S=H(P_{\mathrm{SR}})$ , $T_S=P_S^{•}$ , where $P_{\mathrm{SR}}$ denotes the set of resource places in $P_S$ .

By Definition 6, the subnet derived by the resource circuit $R{C}^f=(p_{18},t_{11},p_{17},t_{10},p_{19},t_7,p_{16},t_6)$ in Figure 2(f) is shown in Figure 1(b).

In this article, we suppose that the tokens in the support of any minimal P_r-semiflow of an S³PR stay in the resource originally. That is to say, $\forall r_i\in P_R,M(\parallel I_{r_i}\parallel )=M_0(r_i)$ .

Theorem 2

Let $\mathrm{RC}=(r_1,t_1,r_2,t_2,\dots ,r_m,t_m)$ be a resource circuit of an S³PR $(N,M_0)$ and $N_S=(P_S,T_S,F_S)$ be the subnet derived from RC. $M_u^{N_S}=\sum _{i=1}^m{M}_0(r_i)·p_i$ is an unreachable state of $(N_S,M_0^{N_S})$ derived by RC if $p_i\in P_{\mathrm{op}}{\wedge }^{•}{p}_i\subseteq R{C}_T$ , where $r_i\in P_{\mathrm{SR}}$ .

Proof 1

We prove it by contradiction. Supposing that $M_u^{N_S}$ is reachable, there must exist $M_P=\{M_p|M_p=M_u^{N_S}-p_i+r_i+p_j,p_j{\in }^{••}{p}_i\cap P_A\}$ being the set of closely previous states of $M_u^{N_S}$ in $R(N_S,M_0^{N_S})$ , where $p_i,p_j\in P_{\mathrm{op}}$ and $r_i\in R{C}_R$ . $p_j{\in }^{••}{p}_i\cap P_A$ and ${}^{•}{p}_i\subseteq R{C}_T$ indicates that $\parallel I_{r_j}\parallel \subset P_S$ and $M_u^{N_S}(\parallel I_{r_j}\parallel )=M_0(r_j)$ . At this moment, it is easy to find that $M_p(\parallel I_{r_j}\parallel )=M_0(r_j)+1$ , which contradicts the fact that $I_{r_{j_i}}$ is a P_r-semiflow and the number of tokens in its support is always a constant $M_0(r_j)$ .

Hence, $M_u^{N_S}$ is an unreachable state of $(N_S,M_0^{N_S})$ .□

The net $(N_S,M_0^{N_S})$ shown in Figure 1(b) is a subnet of the S³PR in Figure 1(a), derived by resource circuit $\mathrm{RC}=(p_{18},t_{11},p_{17},t_{10},p_{19},t_7,p_{16},t_6)$ . $R{C}_T=\{t_6,t_7,t_{10},t_{11}\}$ and $P_{\mathrm{op}}=\{p_6,p_7,p_{10},p_{11}\}$ . $\forall p\in P_{\mathrm{op}}$ , ${}^{•}p\subseteq R{C}_T$ indicates that $M_u^{N_S}=p_6+p_7+p_{10}+p_{11}$ is an unreachable state of $(N_S,M_0^{N_S})$ .

Corollary 2

Let $R{C}^m$ and $R{C}^n$ be two resource circuits of an S³PR such that $\forall p\in P_{\mathrm{oc}}^m\cap P_{\mathrm{oc}}^n$ , ${}^{•}p\subseteq {\mathrm{RC}}_T^m\cup {\mathrm{RC}}_T^n$ . $N_S^m$ and $N_S^n$ be the subnets derived by $R{C}^m$ and $R{C}^n$ , respectively. Supposing that there exist no unreachable state in $N_S^m$ derived by $R{C}^m$ or in $N_S^n$ derived by $R{C}^n$ . Then, $R{C}^{m+n}$ is the resource circuit composed by $R{C}^m$ and $R{C}^n$ , $N_S^{m+n}$ is the subnet derived by $R{C}^{m+n}$ and also composed by $N_S^m$ and $N_S^n$ . $M_u^{N_S^{m+n}}=\sum _{i=1}^{m+n}{M}_0(r_i)·p_i$ , $p_i\in P_{\mathrm{op}}^{m+n}$ is an unreachable state of $(N_S^{m+n},M_0^{N_S^{m+n}})$ derived by $R{C}^{m+n}$ .

Proof 2

It is easy to conclude by Theorem 2.□

By Theorem 2, there exists no unreachable state of the subnet derived by the resource circuit either in Figure 2(d) or Figure 2(e) since ${}^{•}{p}_5=\{t_4,t_5\}⊈{\mathrm{RC}}_T^d$ and ${}^{•}{p}_5⊈{\mathrm{RC}}_T^e$ . However, ${}^{•}{p}_5\subseteq {\mathrm{RC}}_T^d\cup {\mathrm{RC}}_T^e$ . Hence, we can construct a resource circuit $R{C}^{d+e}$ , as shown in Figure 3(a) composed by $R{C}^d$ and $R{C}^e$ , and construct a subnet $N_S^{d+e}$ derived by $R{C}^{d+e}$ . $M_u^{N_S^{d+e}}=p_3+p_4+p_5$ is an unreachable state of $(N_S^{d+e},M_0^{N_S^{d+e}})$ . Similarly, the resource circuit in Figure 3(b) is composed by $R{C}^c$ and $R{C}^e$ and its corresponding unreachable state is $M_u^{N_S^{c+e}}=p_4+p_5+p_{12}$ .

Figure 3.

The composed resource circuits: (a) RC^{d +e} and (b) RC^{c +e}.

Property 2

Let $(N_S,M_0^{N_S})$ be a subnet of an S³PR $(N,M_0)$ , $M^{N_S}$ and M be the states of $(N_S,M_0^{N_S})$ and $(N,M_0)$ , respectively, such that $\forall p\in N_S,M^{N_S}(p)=M(p)$ . Then, M is an unreachable state of $(N,M_0)$ if $M^{N_S}$ is an unreachable state of $(N_S,M_0^{N_S})$ .

Definition 7

Let $(N_S,M_0^{N_S})$ be a subnet of an S³PR $(N,M_0)$ and $M_u^{N_S}$ be an unreachable state of $(N_S,M_0^{N_S})$ . $R_u^{N_S}(N,M_0)=\{M_u|M_u(p)=M_u^{N_S}(p),\forall p\in P_S\}$ is called the set of unreachable states of $(N,M_0)$ derived from $(N_S,M_0^{N_S})$ .

Property 3

Let $(N,M_0)$ be an S³PR with n $(n\ge 3)$ resources and $N=(P^0\cup P_A\cup P_R,T,F)$ and $(N_S^i,M_0^{N_S^i})=(P_S^i,T_S^i,F_S^i)$ be a subnet of $(N,M_0)$ derived by a resource circuit RC. $(N_S^j,M_0^{N_S^j})=(P_S^j,T_S^i,F_S^j)$ , where $P_S^j=P_{S{R}_j}\cap H(P_{S{R}_j})$ , $S{R}_j=P_R\backslash P_{S{R}_i}$ , $T_S^j=P_S^{j•}$ , and $F_S^j=F\cap [(P_S^j\times T_S^i)\cup (T_S^j\times P_S^i)]$ . Let $|R_b(N_S^j,M_0^{N_S^j})|$ be the least upper bound of reachable states of $(N_S^j,M_0^{N_S^j})$ , we have $|R_u^{N_S^i}(N,M_0)|=|R_b(N_S^j,M_0^{N_S^j})|$ .

Theorem 3

Let $R{C}^m$ and $R{C}^n$ be two resource circuits in an S³PR $(N,M_0)$ . $R{C}^m\ne R{C}^n$ , $N_S^m$ and $N_S^n$ be the subnets derived by $R{C}^m$ and $R{C}^n$ , respectively. $M_u^{N_S^m}$ and $M_u^{N_S^n}$ be two unreachable states in $N_S^m$ and $N_S^n$ obtained by $R{C}^m$ and $R{C}^n$ , respectively:

1. If ${\mathrm{RC}}_R^m={\mathrm{RC}}_R^n$ , then $R_u^{N_S^m}(N,M_0)\ne R_u^{N_S^n}(N,M_0)$ and $|R_u^{N_S^m}(N,M_0)|=|R_u^{N_S^n}(N,M_0)|$ .

2. If ${\mathrm{RC}}_R^m\subset {\mathrm{RC}}_R^n$ , then $R_u^{N_S^n}(N,M_0)\subset R_u^{N_S^m}(N,M_0)$ .

3. If ${\mathrm{RC}}_R^m\cap {\mathrm{RC}}_R^n\ne \varnothing$ , ${\mathrm{RC}}_R^n⊈{\mathrm{RC}}_R^m$ , and ${\mathrm{RC}}_R^m⊈{\mathrm{RC}}_R^n$ , then $R_u^{N_S^m}(N,M_0)\cap R_u^{N_S^n}(N,M_0)=\varnothing$ .

4. If ${\mathrm{RC}}_R^m\cap {\mathrm{RC}}_R^n=\varnothing$ , then $R_u^{N_S^m}(N,M_0)\cap R_u^{N_S^n}(N,M_0)\ne \varnothing$ . Let $R_s=R_u^{N_S^m}(N,M_0)\cap R_u^{N_S^n}(N,M_0)$ and $N_S^{m+n}$ be the subnet composed by $N_S^m$ and $N_S^n$ , that is, $P_S^{m+n}=P_S^m\cup P_S^n$ , $T_S^{m+n}=T_S^m\cup T_S^n$ , $F_S^{m+n}=F_S^m\cup F_S^n$ , and $M_u^{N_S^{m+n}}=M_u^{N_S^m}+M_u^{N_S^n}$ , we have $|R_s|=|R_u^{N_S^{m+n}}(N,M_0)|$ .

Proof 3

1. Since $R{C}^m\ne R{C}^n$ , by Theorem 2, it is easy to find that $R_u^{N_S^n}(N,M_0)\subseteq R_u^{N_S^m}(N,M_0)$ . By Property 3, ${\mathrm{RC}}_R^m={\mathrm{RC}}_R^n$ indicates $|R_u^{N_S^m}(N,M_0)|=|R_u^{N_S^n}(N,M_0)|$ .

2. Similarly, since $R{C}^m\subset R{C}^n$ , it is easy to obtain that $|R_u^{N_S^m}(N,M_0)|=|R_u^{N_S^n}(N,M_0)|$ by Property 3.

3. It is proved by contradictions. Supposing that $M_u^{N_S^m}=M_0(r_{m_1})·p_{m_1}+\cdots +M_0(r_{m_k})·p_{m_k}+\cdots +M_0(r_{m_k})·p_{m_i}$ and $M_u^{N_S^n}=M_0(r_{n_1})·p_{n_1}+\cdots +M_0(r_{n_l})·p_{n_l}+\cdots +M_0(r_{n_j})·p_{n_j}$ . ${\mathrm{RC}}_R^m\cap {\mathrm{RC}}_R^n\ne \varnothing$ , ${\mathrm{RC}}_R^n⊈{\mathrm{RC}}_R^m$ , and ${\mathrm{RC}}_R^m⊈{\mathrm{RC}}_R^n$ indicate that $|{\mathrm{RC}}_R^m\cap {\mathrm{RC}}_R^n|\ge 1$ . Hence, there must exists a resource r such that $r_{m_k}=r_{n_l}=r$ and $p_{m_k},p_{n_l}\in H(r)$ . If $R_u^{N_S^m}(N,M_0)\cap R_u^{N_S^n}(N,M_0)\ne \varnothing$ , it is easy to conclude that $p_{m_k}\ne p_{n_l}$ , which implies that there exists an marking $M\in R_u^{N_S^m}(N,M_0)\cap R_u^{N_S^n}(N,M_0)$ such that $M(p_{m_k})=M(p_{n_l})=M_0(r)$ . At this moment, $M(\parallel I_r\parallel )=2M_0(r)$ contradicts the fact that $I_r$ is a P-invariant and the number of tokens in $\parallel I_r\parallel$ is a constant $M_0(r)$ . Consequently, $R_u^{N_S^m}(N,M_0)\cap R_u^{N_S^n}(N,M_0)=\varnothing$ is proved.

4. $R_s$ is used to denote $R_u^{N_S^m}(N,M_0)\cap R_u^{N_S^n}(N,M_0)$ for economy of space. For any $M\in R_s$ , $M\in R_u^{N_S^m}(N,M_0)$ indicates that $\forall p\in P_S^i,M(p)=M_u^{N_S^m}(p)$ and $M\in R_u^{N_S^n}(N,M_0)$ indicates that $\forall p\in P_S^j,M(p)=M_u^{N_S^n}(p)$ . $P_S^{m+n}=P_S^m\cup P_S^n$ , $T_S^{m+n}=T_S^m\cup T_S^n$ , $F_S^{m+n}=F_S^m\cup F_S^n$ , and $M_u^{N_S^{m+n}}=M_u^{N_S^m}+M_u^{N_S^n}$ leads to $M\in R_u^{N_S^{m+n}}(N,M_0)$ . Hence, we have $R_s\subset R_u^{N_S^{m+n}}(N,M_0)$ . Similarly, for any $M\prime \in R_u^{N_S^{m+n}}(N,M_0)$ , $M\prime \in R_s$ implies that $R_u^{N_S^{m+n}}(N,M_0)\subset R_s$ . Consequently, we have $R_s=R_u^{N_S^{m+n}}(N,M_0)$ and $|R_s|=|R_u^{N_S^{m+n}}(N,M_0)|$ .□

Theorem 3.1 indicates that if two different resource circuits have same resources, then the circuits have different unreachable states. Moreover, a subnet can be derived by the different resource circuits with same resources. Certainly, $N_S^m=N_S^n$ leads to $|R_u^{N_S^m}(N,M_0)|=|R_u^{N_S^n}(N,M_0)|$ .

Theorem 3.3 tells us that if two different resource circuits don’t belong to each other but have at least one shared resource, then the unreachable states derived by their subnets have no intersection.

Theorem 3.4 implies that if two resource circuits have no shared resource, then the unreachable states derived by their subnets have intersections, that is, same unreachable states can be found in calculating the number of unreachable states derived from the two circuits corresponding subnets. Hence, we should minus the intersections.

In this study, the number of reachable states of an S³PR $(N,M_0)$ is obtained by eliminating the unreachable ones from the least upper bound $R_b(N,M_0)$ . Supposing that there are n resource circuits and composed resource circuits such that the subnets derived by them have unreachable states. In addition, there exist m couples resource circuits that share no resources. Then, $|R_b(N,M_0)|-\sum _{i=1}^n|R_u^{N_S^i}(N,M_0)|+\sum _{j=1}^m|R_u^{N_S^j}(N,M_0)|$ leads to the desired result.

State estimate algorithm

The upper bound of reachable states and the unreachable states of an S³PR can be found via sections “Upper bound estimation of reachable states” and “Unreachable states exclusion,” respectively. The resulting number of subtracting the number of unreachable states from the upper bound is the number of reachable states obtained by the proposed method. In this subsection, the detailed method is shaped to an algorithm. In the following algorithm, the set of estimated reachable states of an S³PR $(N,M_0)$ by the proposed method is defined as $R_e(N,M_0)$ and the number of elements in it is denoted as $|R_e(N,M_0)|$ .

Algorithm 1.

Estimation of reachable states for an S³PR.

Input: An S3PR $(N,M_0)$ .

Output: $|R_e(N,M_0)|$ .

1. begin

2. $\forall r_i\in P_R$ , $i\in \{1,\dots ,n\}$ , calculate $|R(\parallel I_{r_i}\parallel ,M_0^{\parallel I_{r_i}\parallel })|$ by Corollary 1.

3. Find $|R_b(N,M_0)|=\underset{i=1}{\overset{n}{\Pi }}|R(\parallel I_{r_i}\parallel ,M_0^{\parallel I_{r_i}\parallel })|$ by Property 1.

4. Find the set of resource circuits with $\Pi =\{R{C}^1,\dots ,R{C}^n\}$ in N by Definition 4.

5. $\forall R{C}^i\in \Pi$ ,

if there exists a resource circuit $R{C}^j$ such that ${\mathrm{RC}}_R^j\subset {\mathrm{RC}}_R^i$ , $\Pi :=\Pi \backslash \{R{C}^i\}$ .

6. $\forall R{C}^i\in \Pi$ such that $p^i\in P_{\mathrm{op}}{\wedge }^{•}{p}^i⊈{\mathrm{RC}}_T^i$ ,

6.1 $\forall R{C}^j\in \Pi$ such that $p^j\in P_{\mathrm{op}}{\wedge }^{•}{p}^j⊈{\mathrm{RC}}_T^j$ satisfies that $\forall p\in P_{\mathrm{op}}^i\cap P_{\mathrm{op}}^j{,}^{•}p\subseteq {\mathrm{RC}}_T^i\cup {\mathrm{RC}}_T^j$ ,

6.1.1 Construct a resource circuit $R{C}^{i+j}$ composed by $R{C}^i$ and $R{C}^j$ ,

6.1.2 $\Pi :=\Pi \cup \{R{C}^{i+j}\}$ ,

6.2 $\Pi :=\Pi \backslash \{R{C}^i\}$ .

7. $|R_u(N,M_0)|:=0$ .

8. $\forall R{C}^i\in \Pi$ ,

8.1 Construct a subnet $N_S^i$ derived by $R{C}^i$ ,

8.2 Calculate $|R_u^{N_S^i}(N,M_0)|$ ; $|R_u(N,M_0)|:=|R_u(N,M_0)|+|R_u^{N_S^i}(N,M_0)|$ .

9. while $\Pi \ne \varnothing$ ,

9.1. Choose a resource circuit $R{C}^i$ from $\Pi$ ; $\Pi :=\Pi \backslash \{R{C}^i\}$ ,

9.2. if there exists a resource circuit $R{C}^j$ in $\Pi$ such that ${\mathrm{RC}}_R^i\cap {\mathrm{RC}}_R^j\ne \varnothing$ , ${\mathrm{RC}}_R^j⊈{\mathrm{RC}}_R^i$ , and ${\mathrm{RC}}_R^i⊈{\mathrm{RC}}_R^j$ ,

9.2.1 Construct a subnet $N_S^{i+j}$ composed by $N_S^i$ and $N_S^j$ ,

9.2.2 Calculate $|R_u^{N_S^{i+j}}(N,M_0)|$ ,

9.2.3 $|R_u(N,M_0)|:=|R_u(N,M_0)|-|R_u^{N_S^{i+j}}(N,M_0)|$ .

10. $|R_e(N,M_0)|:=|R_b(N,M_0)|-|R_u(N,M_0)|$ .

11. Output $|R_e(N,M_0)|$ .

12. end

Here, we take the S³PR $(N,M_0)$ in Figure 1(a) as a simple example. Based on section “Upper bound estimation of reachable states,” we have $|R_b(N,M_0)|=360$ . By Definition 4, six resource circuits can be found and shown in Figure 2. Accordingly, six subnets can be derived by the circuits. By Theorem 2, it is found that there exist unreachable states in the subnets derived by the resource circuits in Figure 2(a), (b), and (f). By Corollary 2, it is found that there exist unreachable states in the subnets derived by the resource circuits in Figure 3(a) and (b). By Property 3, it is found that $|R_u^{N_S^{2a}}(N,M_0)|=|R_u^{N_S^{2b}}(N,M_0)|=24$ since $N_S^{2a}=N_S^{2b}$ , $|R_u^{N_S^{2f}}(N,M_0)|=6$ , and $|R_u^{N_S^{4a}}(N,M_0)|=|R_u^{N_S^{4b}}(N,M_0)|=12$ . It is found that there exists at least a shared resource for any two resource circuits. Hence, by Theorem 3, we can conclude that there exists no intersection of unreachable states. Hence, we can obtain that $|R_u(N,M_0)|=|R_u^{N_S^{2a}}(N,M_0)|+|R_u^{N_S^{2b}}(N,M_0)|+|R_u^{N_S^{2f}}(N,M_0)|+|R_u^{N_S^{4a}}(N,M_0)|+|R_u^{N_S^{4b}}(N,M_0)|=78$ . Consequently, $|R_e(N,M_0)|=|R_b(N,M_0)|-|R_u(N,M_0)|=282$ . In fact, the actual number of reachable states is 282. That is to say, for this example, the calculated number by the proposed method is equal to the actual value.

Example and discussion

The net shown in Figure 4 is a well-known model for an FMS, ¹⁵ where $P^0=\{p_1,p_5,p_{14}\}$ , $P_A=P_1\cup P_2\cup P_3=\{p_2,p_3,p_4\}\cup \{p_6,p_7,p_8,p_9,p_{10},p_{11},p_{12},p_{13}\}\cup \{p_{15},p_{16},p_{17},p_{18},p_{19}\}$ , and $P_R=\{p_{20},p_{21},p_{22},p_{23},p_{24},p_{25},p_{26}\}$ .

Figure 4.

The Petri net model of an FMS.

There are seven resources in $(N,M_0)$ and $|R(\parallel I_{r_i}\parallel ,M_0^{\parallel I_{r_i}\parallel })|$ , $r_i\in P_R=\{p_{20},p_{21},p_{22},p_{23},p_{24},p_{25},p_{26}\}$ , obtained by Corollary 1, are shown in Table 1. By Property 1, we have $|R_b(N,M_0)|=\underset{r_i\in P_R}{\Pi }|R(\parallel I_{r_i}\parallel ,M_0^{\parallel I_{r_i}\parallel })|=34,992$ . Hence, 34,992 is the least upper bound of reachable states of $(N,M_0)$ .

Table 1.

Calculations of $|R(\parallel I_{r_i}\parallel ,M_0^{\parallel I_{r_i}\parallel })|$ .

$I_{r_i}$	Calculation
$I_{p_{20}}$	$|R(\parallel I_{p_{20}}\parallel ,M_0^{\parallel I_{p_{20}}\parallel })|=C(3+1-1,1)=3$
$I_{p_{21}}$	$|R(\parallel I_{p_{21}}\parallel ,M_0^{\parallel I_{p_{21}}\parallel })|=C(6+1-1,1)=6$
$I_{p_{22}}$	$|R(\parallel I_{p_{22}}\parallel ,M_0^{\parallel I_{p_{22}}\parallel })|=C(3+1-1,1)=3$
$I_{p_{23}}$	$|R(\parallel I_{p_{23}}\parallel ,M_0^{\parallel I_{p_{23}}\parallel })|=C(2+2-1,2)=3$
$I_{p_{24}}$	$|R(\parallel I_{p_{24}}\parallel ,M_0^{\parallel I_{p_{24}}\parallel })|=C(3+2-1,2)=6$
$I_{p_{25}}$	$|R(\parallel I_{p_{25}}\parallel ,M_0^{\parallel I_{p_{25}}\parallel })|=C(3+2-1,2)=6$
$I_{p_{26}}$	$|R(\parallel I_{p_{26}}\parallel ,M_0^{\parallel I_{p_{26}}\parallel })|=C(3+2-1,2)=6$

The next stage is to calculate the number of unreachable states of $(N,M_0)$ . There exist eight resource circuits in $(N,M_0)$ , shown in Figure 5 and listed as below:

• $R{C}^a=(p_{20},t_{19},p_{25},t_7)$

• $R{C}^b=(p_{25},t_{18},p_{21},t_8)$

• $R{C}^c=(p_{21},t_{16},p_{26},t_{10})$

• $R{C}^d=(p_{26},t_{16},p_{22},t_{10})$

• $R{C}^e=(p_{21},t_{13},p_{24},t_4)$

• $R{C}^f=(p_{21},t_{13},p_{24},t_{12})$

• $R{C}^g=(p_{21},t_3,p_{23},t_2,p_{20},t_{19},p_{25},t_{18})$

• $R{C}^h=(p_{21},t_{17},p_{26},t_{16},p_{22},t_5,p_{24},t_4)$

By Theorem 2, there exist unreachable states in the subnets derived by $R{C}^a$ , $R{C}^b$ , $R{C}^c$ , $R{C}^e$ , $R{C}^f$ , and $R{C}^g$ , but not $R{C}^d$ and $R{C}^h$ since ${}^{•}{p}_{10}=\{t_5,t_{10}\}$ , ${}^{•}{p}_{10}⊈{\mathrm{RC}}_T^d$ , and ${}^{•}{p}_{10}⊈{\mathrm{RC}}_T^h$ . However, it is found that ${}^{•}{p}_{10}\subseteq {\mathrm{RC}}_T^d\cup {\mathrm{RC}}_T^h$ . Hence, by Corollary 2, the subnet derived by $R{C}^i$ , composed by $R{C}^d$ and $R{C}^h$ , have unreachable states. Consequently, we have $\Pi =\{R{C}^a,R{C}^b,R{C}^c,R{C}^e,R{C}^f,R{C}^i\}$ .

Figure 5.

The resource circuits of (N, M₀): (a) RC^a, (b) RC^b, (c) RC^c, (d) RC^d, (e) RC^e, (f) RC^f, (g) RC^g, and (h) RC^h.

By Property 3, the number of unreachable states derived by the resource circuit corresponding subnets is displayed as follows:

• $\begin{array}{c}|R_u^{N_S^a}(N,M_0)|=|R(\parallel I_{p_{21}}\parallel ,M_0^{\parallel I_{p_{21}}\parallel })|\times |R(\parallel I_{p_{22}}\parallel ,M_0^{\parallel I_{p_{22}}\parallel })|\times |R(\parallel I_{p_{23}}\parallel ,M_0^{\parallel I_{p_{23}}\parallel })|\times \hfill \\ |R(\parallel I_{p_{24}}\parallel ,M_0^{\parallel I_{p_{24}}\parallel })|\times |R(\parallel I_{p_{26}}\parallel ,M_0^{\parallel I_{p_{26}}\parallel })|=6\times 3\times 3\times 6\times 6=1944\hfill \end{array}$

• $\begin{array}{c}|R_u^{N_S^b}(N,M_0)|=|R(\parallel I_{p_{20}}\parallel ,M_0^{\parallel I_{p_{20}}\parallel })|\times |R(\parallel I_{p_{22}}\parallel ,M_0^{\parallel I_{p_{22}}\parallel })|\times |R(\parallel I_{p_{23}}\parallel ,M_0^{\parallel I_{p_{23}}\parallel })|\times \hfill \\ |R(\parallel I_{p_{24}}\parallel ,M_0^{\parallel I_{p_{24}}\parallel })|\times |R(\parallel I_{p_{26}}\parallel ,M_0^{\parallel I_{p_{26}}\parallel })|=3\times 3\times 3\times 6\times 6=972\hfill \end{array}$

• $\begin{array}{c}|R_u^{N_S^c}(N,M_0)|=|R(\parallel I_{p_{20}}\parallel ,M_0^{\parallel I_{p_{20}}\parallel })|\times |R(\parallel I_{p_{22}}\parallel ,M_0^{\parallel I_{p_{22}}\parallel })|\times |R(\parallel I_{p_{23}}\parallel ,M_0^{\parallel I_{p_{23}}\parallel })|\times \hfill \\ |R(\parallel I_{p_{24}}\parallel ,M_0^{\parallel I_{p_{24}}\parallel })|\times |R(\parallel I_{p_{25}}\parallel ,M_0^{\parallel I_{p_{25}}\parallel })|=3\times 3\times 3\times 6\times 6=972\hfill \end{array}$

• $\begin{array}{c}|R_u^{N_S^e}(N,M_0)|=|R(\parallel I_{p_{20}}\parallel ,M_0^{\parallel I_{p_{20}}\parallel })|\times |R(\parallel I_{p_{22}}\parallel ,M_0^{\parallel I_{p_{22}}\parallel })|\times |R(\parallel I_{p_{23}}\parallel ,M_0^{\parallel I_{p_{23}}\parallel })|\times \hfill \\ |R(\parallel I_{p_{25}}\parallel ,M_0^{\parallel I_{p_{25}}\parallel })|\times |R(\parallel I_{p_{26}}\parallel ,M_0^{\parallel I_{p_{26}}\parallel })|=3\times 3\times 3\times 6\times 6=972\hfill \end{array}$

• $\begin{array}{c}|R_u^{N_S^f}(N,M_0)|=|R(\parallel I_{p_{20}}\parallel ,M_0^{\parallel I_{p_{20}}\parallel })|\times |R(\parallel I_{p_{22}}\parallel ,M_0^{\parallel I_{p_{22}}\parallel })|\times |R(\parallel I_{p_{23}}\parallel ,M_0^{\parallel I_{p_{23}}\parallel })|\times \hfill \\ |R(\parallel I_{p_{25}}\parallel ,M_0^{\parallel I_{p_{25}}\parallel })|\times |R(\parallel I_{p_{26}}\parallel ,M_0^{\parallel I_{p_{26}}\parallel })|=3\times 3\times 3\times 6\times 6=972\hfill \end{array}$

• $\begin{array}{c}|R_u^{N_S^g}(N,M_0)|=|R(\parallel I_{p_{22}}\parallel ,M_0^{\parallel I_{p_{22}}\parallel })|\times |R(\parallel I_{p_{24}}\parallel ,M_0^{\parallel I_{p_{24}}\parallel })|\times |R(\parallel I_{p_{26}}\parallel ,M_0^{\parallel I_{p_{26}}\parallel })|\hfill \\ =3\times 6\times 6=108\hfill \end{array}$

• $\begin{array}{c}|R_u^{N_S^i}(N,M_0)|=|R(\parallel I_{p_{20}}\parallel ,M_0^{\parallel I_{p_{20}}\parallel })|\times |R(\parallel I_{p_{23}}\parallel ,M_0^{\parallel I_{p_{23}}\parallel })|\times |R(\parallel I_{p_{25}}\parallel ,M_0^{\parallel I_{p_{25}}\parallel })|\hfill \\ =3\times 3\times 6=54\hfill \end{array}$

It is found that ${\mathrm{RC}}_R^a\cap {\mathrm{RC}}_R^c=\varnothing$ , ${\mathrm{RC}}_R^a\cap {\mathrm{RC}}_R^e=\varnothing$ , ${\mathrm{RC}}_R^a\cap {\mathrm{RC}}_R^f=\varnothing$ , and ${\mathrm{RC}}_R^a\cap {\mathrm{RC}}_R^i=\varnothing$ . By Theorem 3.4, we have $|R_u^{N_S^{a+c}}(N,M_0)|=54$ , $|R_u^{N_S^{a+e}}(N,M_0)|=54$ , $|R_u^{N_S^{a+f}}(N,M_0)|=3$ , and $|R_u^{N_S^{a+i}}(N,M_0)|=3$ .

Consequently, we have $\begin{array}{c}|R(N,M_0)|=|R_b(N,M_0)|-|R_u^{N_S^a}(N,M_0)|-|R_u^{N_S^b}(N,M_0)|-|R_u^{N_S^c}(N,M_0)|-\hfill \\ |R_u^{N_S^f}(N,M_0)|-|R_u^{N_S^g}(N,M_0)|-|R_u^{N_S^i}(N,M_0)|+|R_u^{N_S^{a+c}}(N,M_0)|+\hfill \\ |R_u^{N_S^{a+e}}(N,M_0)|+|R_u^{N_S^{a+f}}(N,M_0)|+|R_u^{N_S^{a+i}}(N,M_0)|=29,112\hfill \end{array}$ .

Compared with the existing method, the proposed one can calculate an upper bound of the number of reachable states of an S³PR in a short time, especially for a net system with a large initial state (in number of tokens). INA is a widely used tool, which can provide behavioral and structural information of Petri nets. Its abilities are far beyond to provide the number of reachable states of a Petri net. In this work, INA is used to compare with the proposed method only from the point of calculating the number of reachable states. Here, INA and the proposed method are applied to compute the number of reachable states of the S³PR in Figure 4 with different initial states. The proposed method is conducted via a software package developed by our group. The calculations are carried out on a computer in Windows XP operating system with Pentium(R) Dual-Core CPU 3.0 GHz and 4 GB memory and the result is shown in Table 2. The first and the second columns show the numbers and the initial states of the marked nets, respectively. The actual numbers of the reachable states obtained by INA and the elapsed time are listed in the third and fourth, respectively. Similarly, the fifth and sixth present the estimate numbers obtained by the proposed method and theirs elapsed time. Besides, “–” in the last line indicates that the computer runs out of memory.

Table 2.

Efficiency comparison between INA and the proposed method.

No. of marked net	Initial state of resources	INA		Proposed
		No. of states	Time	No. of states	Time (s)
1	{1, 1, 1, 2, 2, 2, 2}	26,750	5.30 s	29112	0.063
2	{1, 1, 2, 2, 2, 2, 2}	53,822	10.82 s	58278	0.062
3	{1, 2, 2, 2, 2, 2, 2}	216,906	1 min 03 s	223518	0.063
4	{2, 2, 2, 2, 2, 2, 2}	449,160	4 min 18 s	460632	0.063
5	{3, 2, 2, 2, 2, 2, 2}	758,832	11 min 34 s	776852	0.064
6	{3, 3, 2, 2, 2, 2, 2}	2,085,882	6 h 25 min	2176776	0.063
7	{3, 3, 3, 2, 2, 2, 2}	3,479,022	22 h 43 min	3516568	0.063
8	{3, 4, 3, 3, 3, 3, 3}	–	–	99630520	0.063

INA: integrated net analyzer.

It is found in Table 2 that the elapsed time of the calculation by INA increases as the net initial state increases. It will cost a very long time when using INA to deal with a large marked net system and in the worst case, reachability analysis may stop midway due to exhausted memory. Instead, the elapsed time for obtaining the number of reachable states by the proposed method is very short. Meanwhile, the elapsed time is a constant; in other words, it does not increase as the initial state increases since the calculation mainly refers to algebraic operations, such as multiplication, addition, and subtraction. Hence, we can conclude that the proposed method is not sensitive to the initial state and then can be applied for handling large marked net systems.

Conclusion and future work

This study presents a theory to enumerate the reachable states for an S³PR including three stages: upper bound calculation, unreachable states determination, and exclusion. In order to reduce the computational complexity, based on the fact that an S³PR is composed by several supports of P-invariants, combinatorics is applied to calculate the number of states, including upper bound and unreachable states. Besides, resource circuits are used to determine the unreachable states in the upper bound. The theory is fairly effective that most even all unreachable states can be derived.

The theory can be used to predict the scale of reachable states of a net system to avoid wasting time on the calculation without results. Moreover, the number of reserved legal states after adding monitors for plant models can be obtained by the theory, which is useful for checking the performance of a liveness-enforcing supervisor. Furthermore, the future work will focus on calculating accurate number of reachable states. Once the accurate number of reachable states can be calculated by combinatorics, all reachable states can be enumerated accordingly. Hence, it will be an important basis of generating RG by combinatorics in a low computational complexity. Besides, note that the proposed method cannot be applied to more complex classes of Petri nets. Hence, further work is to improve the theory to realize accurate calculation and generalization.