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.

Keywords

Petri net reachability graph combinatorics resource circuit initial state

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 $ω$ , to represent an infinite component in states. However, there exists the problem of reachability information loss caused by the usage of $ω$ . 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 $Ω$ , is a mapping $Ω : A \to ℕ$ , which is represented as a formal sum $\sum_{a \in A} Ω (a) \cdot a$ , where A is a non-empty set and $ℕ = {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) \cdot 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) \geq 1$ and denoted as $M [t 〉$ . Firing it yields a new state $M'$ such that $\forall p \in^{•} t$ , $M' (p) = M (p) - 1$ , $\forall p \in t^{•}$ , $M' (p) = M (p) + 1$ , $\forall p \in {p \in P | p \notin^{•} t \cup t^{•}}$ , $M' (p) = M (p)$ , as denoted by $M [t 〉 M'$ . $M'$ is called an immediately reachable state from M and M is called a closely previous reachable state of $M'$ . A state $M^{″}$ is said to be reachable from M if there exist a sequence of transitions $σ = t_{0} t_{1} \dots t_{n}$ and states $M_{1}, M_{2}, \dots$ , and $M_{n}$ such that $M [t_{0} 〉 M_{1} [t_{1} 〉 M_{2} \dots 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 Z$ indexed by P and a T-vector is a column vector $J : T \to 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 \neq 0$ and $I^{T} [N] = 0^{T}$ and $∥ I ∥ = {p | I (p) \neq 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 (∥ I ∥, M_{0}^{∥ I ∥})$ denotes the set of reachable states of the support of P-semiflow I at the initial state $M_{0}^{∥ I ∥}$ . The number of reachable states in $R (∥ I ∥, M_{0}^{∥ I ∥})$ is denoted as $| R (∥ I ∥, M_{0}^{∥ I ∥}) |$ . In this work, we use $\sum_{p \in ∥ I ∥} I (p) \cdot 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} \neq \emptyset$ 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

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

$P_{R} \neq \emptyset$ and $(P_{A} \cup {p^{0}}) \cap P_{R} = \emptyset$ , where $P_{R}$ is called the set of resource places.

$\forall p \in P_{A}$ , $\forall t \in^{•} p$ , $\forall t' \in p^{•}$ , $\exists r_{p} \in P_{R}$ , ${}^{•}t \cap P_{R} = {t'}^{•} \cap P_{R} = {r_{p}}$ .

(a) $\forall r \in P_{R}$ , ${}^{• •}r \cap P_{A} = r^{• •} \cap P_{A} \neq \emptyset$ and (b) $\forall r \in P_{R}$ , ${}^{•}r \cap r^{•} = \emptyset$ .

${}^{• •}{(p^{0})} \cap P_{R} = (p^{0})^{• •} \cap P_{R} = \emptyset$ .

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:¹⁵

An S²PR is an S³PR.

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}}) = \emptyset$ , $P_{R_{1}} \cap P_{R_{2}} = P_{C} \neq \emptyset$ , and $T_{1} \cap T_{2} = \emptyset$ . 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.

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 $∥ I_{r} ∥ = {r} \cup H (r)$ . Suppose that there are m places and k tokens in $∥ I_{r} ∥$ at the initial state $M_{0}^{∥ I_{r} ∥}$ , then the maximal number of possible reachable states of $∥ I_{r} ∥$ is $| R (∥ I_{r} ∥, M_{0}^{∥ I_{r} ∥}) | = 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 $∥ I_{r} ∥$ and the number of tokens in it is a constant. Similar to Theorem 1, suppose that there are k tokens and m places in $∥ I_{r} ∥$ , the maximal number of possible reachable states of $∥ I_{r} ∥$ 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 $∥ I_{p_{19}} ∥$ 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}}{Π} | R (∥ I_{r} ∥, M_{0}^{∥ I_{r} ∥}) |$ .

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, M_{0}) | = | R (∥ I_{p_{14}} ∥, M_{0}^{∥ I_{p_{14}} ∥}) | \\ \times | R (∥ I_{p_{15}} ∥, M_{0}^{∥ I_{p_{15}} ∥}) | \times | R (∥ I_{p_{16}} ∥, M_{0}^{∥ I_{p_{16}} ∥}) | \\ \times | R (∥ I_{p_{17}} ∥, M_{0}^{∥ I_{p_{17}} ∥}) | \times | R (∥ I_{p_{18}} ∥, M_{0}^{∥ I_{p_{18}} ∥}) | \\ \times | R (∥ I_{p_{19}} ∥, M_{0}^{∥ I_{p_{19}} ∥}) | = 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 \geq 2)$ be a set of resources in an S³PR $N = (P_{0} \cup P_{A} \cup P_{R}, T, F)$ . A simple circuit $RC = (r_{1}, t_{1}, r_{2}, t_{2}, \dots, r_{m}, t_{m})$ is called a resource circuit if (1) $\forall i \in ℕ_{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 $RC = (r_{1}, t_{1}, r_{2}, t_{2}, \dots, r_{m}, t_{m})$ , respectively. $P_{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}) \land 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 $RC = (r_{1}, t_{1}, r_{2}, t_{2}, \dots, r_{m}, t_{m})$ such that $R C_{R} = P_{SR}$ , $P_{S} = H (P_{SR})$ , $T_{S} = P_{S}^{•}$ , where $P_{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 (∥ I_{r_{i}} ∥) = M_{0} (r_{i})$ .

Theorem 2

Let $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}) \cdot p_{i}$ is an unreachable state of $(N_{S}, M_{0}^{N_{S}})$ derived by RC if $p_{i} \in P_{op} \land^{•} p_{i} \subseteq R C_{T}$ , where $r_{i} \in P_{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_{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 $∥ I_{r_{j}} ∥ \subset P_{S}$ and $M_{u}^{N_{S}} (∥ I_{r_{j}} ∥) = M_{0} (r_{j})$ . At this moment, it is easy to find that $M_{p} (∥ I_{r_{j}} ∥) = 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 $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_{op} = {p_{6}, p_{7}, p_{10}, p_{11}}$ . $\forall p \in P_{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_{oc}^{m} \cap P_{oc}^{n}$ , ${}^{•}p \subseteq {RC}_{T}^{m} \cup {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}) \cdot p_{i}$ , $p_{i} \in P_{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}} ⊈ {RC}_{T}^{d}$ and ${}^{•}{p_{5}} ⊈ {RC}_{T}^{e}$ . However, ${}^{•}{p_{5}} \subseteq {RC}_{T}^{d} \cup {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 \geq 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} \ 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} \neq 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:

If ${RC}_{R}^{m} = {RC}_{R}^{n}$ , then $R_{u}^{N_{S}^{m}} (N, M_{0}) \neq 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}) |$ .

If ${RC}_{R}^{m} \subset {RC}_{R}^{n}$ , then $R_{u}^{N_{S}^{n}} (N, M_{0}) \subset R_{u}^{N_{S}^{m}} (N, M_{0})$ .

If ${RC}_{R}^{m} \cap {RC}_{R}^{n} \neq \emptyset$ , ${RC}_{R}^{n} ⊈ {RC}_{R}^{m}$ , and ${RC}_{R}^{m} ⊈ {RC}_{R}^{n}$ , then $R_{u}^{N_{S}^{m}} (N, M_{0}) \cap R_{u}^{N_{S}^{n}} (N, M_{0}) = \emptyset$ .

If ${RC}_{R}^{m} \cap {RC}_{R}^{n} = \emptyset$ , then $R_{u}^{N_{S}^{m}} (N, M_{0}) \cap R_{u}^{N_{S}^{n}} (N, M_{0}) \neq \emptyset$ . 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

Since $R C^{m} \neq 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, ${RC}_{R}^{m} = {RC}_{R}^{n}$ indicates $| R_{u}^{N_{S}^{m}} (N, M_{0}) | = | R_{u}^{N_{S}^{n}} (N, M_{0}) |$ .

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.

It is proved by contradictions. Supposing that $M_{u}^{N_{S}^{m}} = M_{0} (r_{m_{1}}) \cdot p_{m_{1}} + \dots + M_{0} (r_{m_{k}}) \cdot p_{m_{k}} + \dots + M_{0} (r_{m_{k}}) \cdot p_{m_{i}}$ and $M_{u}^{N_{S}^{n}} = M_{0} (r_{n_{1}}) \cdot p_{n_{1}} + \dots + M_{0} (r_{n_{l}}) \cdot p_{n_{l}} + \dots + M_{0} (r_{n_{j}}) \cdot p_{n_{j}}$ . ${RC}_{R}^{m} \cap {RC}_{R}^{n} \neq \emptyset$ , ${RC}_{R}^{n} ⊈ {RC}_{R}^{m}$ , and ${RC}_{R}^{m} ⊈ {RC}_{R}^{n}$ indicate that $| {RC}_{R}^{m} \cap {RC}_{R}^{n} | \geq 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}) \neq \emptyset$ , it is easy to conclude that $p_{m_{k}} \neq 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 (∥ I_{r} ∥) = 2 M_{0} (r)$ contradicts the fact that $I_{r}$ is a P-invariant and the number of tokens in $∥ I_{r} ∥$ is a constant $M_{0} (r)$ . Consequently, $R_{u}^{N_{S}^{m}} (N, M_{0}) \cap R_{u}^{N_{S}^{n}} (N, M_{0}) = \emptyset$ is proved.

$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' \in R_{u}^{N_{S}^{m + n}} (N, M_{0})$ , $M' \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 S³PR

(N, M_{0})

Output:

| R_{e} (N, M_{0}) |

1. begin

\forall r_{i} \in P_{R}

i \in {1, \dots, n}

, calculate

| R (∥ I_{r_{i}} ∥, M_{0}^{∥ I_{r_{i}} ∥}) |

by Corollary 1.

3. Find

| R_{b} (N, M_{0}) | = Π_{i = 1}^{n} | R (∥ I_{r_{i}} ∥, M_{0}^{∥ I_{r_{i}} ∥}) |

by Property 1.

4. Find the set of resource circuits with

Π = {R C^{1}, \dots, R C^{n}}

in N by Definition 4.

\forall R C^{i} \in Π

if there exists a resource circuit

R C^{j}

such that

{RC}_{R}^{j} \subset {RC}_{R}^{i}

Π : = Π \ {R C^{i}}

\forall R C^{i} \in Π

such that

p^{i} \in P_{op} \land^{•} p^{i} ⊈ {RC}_{T}^{i}

6.1

\forall R C^{j} \in Π

such that

p^{j} \in P_{op} \land^{•} p^{j} ⊈ {RC}_{T}^{j}

satisfies that

\forall p \in P_{op}^{i} \cap P_{op}^{j},^{•} p \subseteq {RC}_{T}^{i} \cup {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

Π : = Π \cup {R C^{i + j}}

6.2

Π : = Π \ {R C^{i}}

| R_{u} (N, M_{0}) | : = 0

\forall R C^{i} \in Π

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

Π \neq \emptyset

9.1. Choose a resource circuit

R C^{i}

from

Π

;

Π : = Π \ {R C^{i}}

9.2. if there exists a resource circuit

R C^{j}

Π

such that

{RC}_{R}^{i} \cap {RC}_{R}^{j} \neq \emptyset

{RC}_{R}^{j} ⊈ {RC}_{R}^{i}

, and

{RC}_{R}^{i} ⊈ {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}^{2 a}} (N, M_{0}) | = | R_{u}^{N_{S}^{2 b}} (N, M_{0}) | = 24$ since $N_{S}^{2 a} = N_{S}^{2 b}$ , $| R_{u}^{N_{S}^{2 f}} (N, M_{0}) | = 6$ , and $| R_{u}^{N_{S}^{4 a}} (N, M_{0}) | = | R_{u}^{N_{S}^{4 b}} (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}^{2 a}} (N, M_{0}) | + | R_{u}^{N_{S}^{2 b}} (N, M_{0}) | + | R_{u}^{N_{S}^{2 f}} (N, M_{0}) | + | R_{u}^{N_{S}^{4 a}} (N, M_{0}) | + | R_{u}^{N_{S}^{4 b}} (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 (∥ I_{r_{i}} ∥, M_{0}^{∥ I_{r_{i}} ∥}) |$ , $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}}{Π} | R (∥ I_{r_{i}} ∥, M_{0}^{∥ I_{r_{i}} ∥}) | = 34, 992$ . Hence, 34,992 is the least upper bound of reachable states of $(N, M_{0})$ .

Table 1.

Calculations of $| R (∥ I_{r_{i}} ∥, M_{0}^{∥ I_{r_{i}} ∥}) |$ .

$I_{r_{i}}$	Calculation
$I_{p_{20}}$	$\| R (∥ I_{p_{20}} ∥, M_{0}^{∥ I_{p_{20}} ∥}) \| = C (3 + 1 - 1, 1) = 3$
$I_{p_{21}}$	$\| R (∥ I_{p_{21}} ∥, M_{0}^{∥ I_{p_{21}} ∥}) \| = C (6 + 1 - 1, 1) = 6$
$I_{p_{22}}$	$\| R (∥ I_{p_{22}} ∥, M_{0}^{∥ I_{p_{22}} ∥}) \| = C (3 + 1 - 1, 1) = 3$
$I_{p_{23}}$	$\| R (∥ I_{p_{23}} ∥, M_{0}^{∥ I_{p_{23}} ∥}) \| = C (2 + 2 - 1, 2) = 3$
$I_{p_{24}}$	$\| R (∥ I_{p_{24}} ∥, M_{0}^{∥ I_{p_{24}} ∥}) \| = C (3 + 2 - 1, 2) = 6$
$I_{p_{25}}$	$\| R (∥ I_{p_{25}} ∥, M_{0}^{∥ I_{p_{25}} ∥}) \| = C (3 + 2 - 1, 2) = 6$
$I_{p_{26}}$	$\| R (∥ I_{p_{26}} ∥, M_{0}^{∥ I_{p_{26}} ∥}) \| = 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}} ⊈ {RC}_{T}^{d}$ , and ${}^{•}{p_{10}} ⊈ {RC}_{T}^{h}$ . However, it is found that ${}^{•}{p_{10}} \subseteq {RC}_{T}^{d} \cup {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 $Π = {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{matrix} | R_{u}^{N_{S}^{a}} (N, M_{0}) | = | R (∥ I_{p_{21}} ∥, M_{0}^{∥ I_{p_{21}} ∥}) | \times | R (∥ I_{p_{22}} ∥, M_{0}^{∥ I_{p_{22}} ∥}) | \times | R (∥ I_{p_{23}} ∥, M_{0}^{∥ I_{p_{23}} ∥}) | \times \\ | R (∥ I_{p_{24}} ∥, M_{0}^{∥ I_{p_{24}} ∥}) | \times | R (∥ I_{p_{26}} ∥, M_{0}^{∥ I_{p_{26}} ∥}) | = 6 \times 3 \times 3 \times 6 \times 6 = 1944 \end{matrix}$

$\begin{matrix} | R_{u}^{N_{S}^{b}} (N, M_{0}) | = | R (∥ I_{p_{20}} ∥, M_{0}^{∥ I_{p_{20}} ∥}) | \times | R (∥ I_{p_{22}} ∥, M_{0}^{∥ I_{p_{22}} ∥}) | \times | R (∥ I_{p_{23}} ∥, M_{0}^{∥ I_{p_{23}} ∥}) | \times \\ | R (∥ I_{p_{24}} ∥, M_{0}^{∥ I_{p_{24}} ∥}) | \times | R (∥ I_{p_{26}} ∥, M_{0}^{∥ I_{p_{26}} ∥}) | = 3 \times 3 \times 3 \times 6 \times 6 = 972 \end{matrix}$

$\begin{matrix} | R_{u}^{N_{S}^{c}} (N, M_{0}) | = | R (∥ I_{p_{20}} ∥, M_{0}^{∥ I_{p_{20}} ∥}) | \times | R (∥ I_{p_{22}} ∥, M_{0}^{∥ I_{p_{22}} ∥}) | \times | R (∥ I_{p_{23}} ∥, M_{0}^{∥ I_{p_{23}} ∥}) | \times \\ | R (∥ I_{p_{24}} ∥, M_{0}^{∥ I_{p_{24}} ∥}) | \times | R (∥ I_{p_{25}} ∥, M_{0}^{∥ I_{p_{25}} ∥}) | = 3 \times 3 \times 3 \times 6 \times 6 = 972 \end{matrix}$

$\begin{matrix} | R_{u}^{N_{S}^{e}} (N, M_{0}) | = | R (∥ I_{p_{20}} ∥, M_{0}^{∥ I_{p_{20}} ∥}) | \times | R (∥ I_{p_{22}} ∥, M_{0}^{∥ I_{p_{22}} ∥}) | \times | R (∥ I_{p_{23}} ∥, M_{0}^{∥ I_{p_{23}} ∥}) | \times \\ | R (∥ I_{p_{25}} ∥, M_{0}^{∥ I_{p_{25}} ∥}) | \times | R (∥ I_{p_{26}} ∥, M_{0}^{∥ I_{p_{26}} ∥}) | = 3 \times 3 \times 3 \times 6 \times 6 = 972 \end{matrix}$

$\begin{matrix} | R_{u}^{N_{S}^{f}} (N, M_{0}) | = | R (∥ I_{p_{20}} ∥, M_{0}^{∥ I_{p_{20}} ∥}) | \times | R (∥ I_{p_{22}} ∥, M_{0}^{∥ I_{p_{22}} ∥}) | \times | R (∥ I_{p_{23}} ∥, M_{0}^{∥ I_{p_{23}} ∥}) | \times \\ | R (∥ I_{p_{25}} ∥, M_{0}^{∥ I_{p_{25}} ∥}) | \times | R (∥ I_{p_{26}} ∥, M_{0}^{∥ I_{p_{26}} ∥}) | = 3 \times 3 \times 3 \times 6 \times 6 = 972 \end{matrix}$

$\begin{matrix} | R_{u}^{N_{S}^{g}} (N, M_{0}) | = | R (∥ I_{p_{22}} ∥, M_{0}^{∥ I_{p_{22}} ∥}) | \times | R (∥ I_{p_{24}} ∥, M_{0}^{∥ I_{p_{24}} ∥}) | \times | R (∥ I_{p_{26}} ∥, M_{0}^{∥ I_{p_{26}} ∥}) | \\ = 3 \times 6 \times 6 = 108 \end{matrix}$

$\begin{matrix} | R_{u}^{N_{S}^{i}} (N, M_{0}) | = | R (∥ I_{p_{20}} ∥, M_{0}^{∥ I_{p_{20}} ∥}) | \times | R (∥ I_{p_{23}} ∥, M_{0}^{∥ I_{p_{23}} ∥}) | \times | R (∥ I_{p_{25}} ∥, M_{0}^{∥ I_{p_{25}} ∥}) | \\ = 3 \times 3 \times 6 = 54 \end{matrix}$

It is found that ${RC}_{R}^{a} \cap {RC}_{R}^{c} = \emptyset$ , ${RC}_{R}^{a} \cap {RC}_{R}^{e} = \emptyset$ , ${RC}_{R}^{a} \cap {RC}_{R}^{f} = \emptyset$ , and ${RC}_{R}^{a} \cap {RC}_{R}^{i} = \emptyset$ . 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{matrix} | 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}) | - \\ | 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}) | + \\ | 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 \end{matrix}$ .

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 marked net	Initial state of resources	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.

Footnotes

Academic Editor: Jiacun Wang

Declaration of conflicting interests

The author(s) declared no potential conflicts of interest with respect to the research, authorship, and/or publication of this article.

Funding

The author(s) disclosed receipt of the following financial support for the research, authorship, and/or publication of this article: This work was supported, in part, by the National Natural Science Foundation of China under Grant No. 61301276, the Natural Science Basic Research Plan in Shaanxi Province of China under Grant No. 2015JQ6258, the Scientific Research Program Funded by Shaanxi Provincial Education Department under Grant No. 15JK1297, and the Discipline Construction Funds of Xi’an Polytechnic University under Grant No. 107090811.

References

Esparza

Reachability in live and safe free choice Petri nets is NP-complete. Theor Comput Sci 1998; 198: 211–224.

Ichikawa

Yokoyama

Kurogi

Control of event-driven systems: reachability and control of conflict-free Petri nets. Trans Soc Instrum Control Eng 1985; 21: 324–330.

Uzam

Gelen

. Comments on “supervisor design to enforce production ratio and absence of deadlock in automated manufacturing systems.”IEEE T Syst Man Cy A 2014; 44: 1455–1456.

Wang

Zhou

Controllability conditions of resultant siphons in a class of Petri nets. IEEE T Syst Man Cy A 2012; 42: 1206–1215.

Patel

Joshi

AY.

Modeling and analysis of a manufacturing system with deadlocks to generate the reachability tree using Petri net system. Proced Eng 2013; 64: 775–784 (also published in International conference on design and manufacturing).

Wang

Zhou

Gan

. New reachability trees for unbounded Petri nets. In: Proceedings of the 2015 IEEE international conference on robotics and automation, Seattle, WA, 26–30 May 2015, vol. 2, pp.3862–3867. New York: IEEE.

Wang

Gan

Zhou

. A reduced reachability tree for a class of unbounded Petri nets. IEEE/CAA J Automat Sin 2015; 2: 345–352.

Zhou

MC.

Deadlock control of automated manufacturing systems based on Petri nets: a literature review. IEEE T Syst Man Cy C 2012; 42: 437–462.

Zhou

Jeng

MD.

A maximally permissive deadlock prevention policy for FMS based on Petri net siphon control and the theory of regions. IEEE T Autom Sci Eng 2008; 5: 182–188.

10.

Giua

Design of optimal Petri net controllers for disjunctive generalized mutual exclusion constraints. IEEE T Automat Contr, 2015, http://dx.doi.org/10.1109/TAC.2015.2389313

11.

Xing

Tian

. Optimal polynomial complexity deadlock avoidance policies for manufacturing systems with flexible routings. In: Proceedings of the IEEE international conference on automation science and engineering, Shanghai, China, 8–10 October 2006, pp.448–453. New York: IEEE.

12.

Ghaffari

Rezg

Xie

XL.

Design of a live and maximally permissive Petri net controller using the theory of regions. IEEE T Robotic Autom 2003; 19: 137–142.

13.

Uzam

Zhou

MC.

An improved iterative synthesis method for liveness enforcing supervisors of flexible manufacturing systems. Int J Prod Res 2006; 44: 1987–2030.

14.

Uzam

Zhou

MC.

An iterative synthesis approach to Petri net-based deadlock prevention policy for flexible manufacturing systems. IEEE T Syst Man Cy A 2007; 37: 362–371.

15.

Ezpeleta

Colom

Martinez

A Petri net based deadlock prevention policy for flexible manufacturing systems. IEEE T Robotic Autom 1995; 11: 173–184.

16.

Zhao

Hou

. A divide-and-conquer method for the synthesis of non-blocking supervisors for flexible manufacturing systems. In: Proceedings of the IEEE international conference on automation science and engineering, Taipei, Taiwan, 18–22 August 2014, pp.455–460. New York: IEEE.

17.

Chen

Khalgui

. Design of a maximally permissive liveness-enforcing Petri net supervisor for flexible manufacturing systems. IEEE T Autom Sci Eng 2011; 8: 374–393.

18.

Chen

Liu

. Computation of resource circuits of Petri nets by using binary decision diagrams. In: Proceedings of the 5th international conference on modeling, simulation and applied optimization, Hammamet, Tunisia, 28–30 April 2013, pp.1–6. New York: IEEE.

19.

Lipton

RJ.

The reachability problem requires exponential space. Research report 62, 1976. New Haven, CT: Department of Computer Science, Yale University.

20.

Starke

PH.

Integrated net analyzer (INA). Handbuch, 1992.

21.

Hong

Chao

DY.

Enumeration of reachable states for arbitrary marked graphs. IET Control Theory A 2012; 6: 1536–1543.

22.

Chao

. Closed form formula construction to enumerate control related states of K-th order S³PR system (with a top left side non-sharing resource place) of Petri nets. In: Proceedings of the 2014 IEEE 11th international conference on networking, sensing and control, Miami, FL, 7–9 April 2014, pp.132–137. New York: IEEE.

23.

Roberts

Tesman

Applied combinatorics. Oxford: Taylor & Francis, 2009.

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

Abstract

Keywords

Introduction

Preliminaries

Multisets

Definition 1

Basics of Petri nets

S3PR nets

Definition 2

Definition 3

Estimate approach

Upper bound estimation of reachable states

Theorem 1

Corollary 1

Property 1

Unreachable states exclusion

Definition 4

Definition 5

Definition 6

Theorem 2

Proof 1

Corollary 2

Proof 2

Property 2

Definition 7

Property 3

Theorem 3

Proof 3

State estimate algorithm

Example and discussion

Conclusion and future work

Footnotes

Declaration of conflicting interests

Funding

References

S³PR nets