Abstract
After our researches on the effect of a non-sharing resource in a kth order which is the concept of customization manufacturing, in this article we extend the research on the closed-form solution of control-related states to the so-called A-net which has one top non-sharing circle subnet connected to the idle place of left process in a deficient kth order system and is the fundamental model of different productions sharing the same common parts in manufacturing. The formulas just are depended on the parameter k and states’ function of top non-sharing circle subnet for a subclass of nets with k sharing resources. By combining the concept of the partial deadlock avoidance/prevention policy, the moment to launch resource (controller) allocation based on the current state, and the construction of closed-form solution for deficient kth order system, it can realize the concept of dynamic non-sharing processes’ allocation.
Introduction
Petri nets (PNs) have been used for modeling and analyzing concurrent systems such as flexible manufacturing system (FMS) or resource allocation system (RAS).1–10 The net behavior depends not only on the graphical structure but also on the initial marking of the net. Therefore, they cannot be determined by static analysis such as dependency analysis; rather, they can be obtained with reachability analysis.11–16 It has been shown that the complexity of the reachability analysis of the PNs is exponential. 15
When using the Integrated Net Analyzer (INA) 17 as reachability analysis tools, there are some potential risks in large model systems: the first is the time-consuming risk as it may take 1 month to complete the reachability analysis; the second is validating the input net structure data by a human; it may take a long time to waiting an error result while the input net structure is wrong; the third is non-significant error due to the fact that presently INA cannot detect the so-called livelock states as shown in section “Computation of CRSs of an ordinary A-net”; the information of reachability analysis will become not valuable.
The deadlock avoidance/prevention policy for PNs presently is to find critic first-met bad markings (FBMs) for maximally permissive control purpose which is the policy based on the net structure.18–23 The structural analysis based deadlock prevention has been extensively studied by researchers, in which siphon computation and control play an essential role.24–30 However, current advanced approaches such as those in Chen et al. 31 produce maximally permissive supervisors while not being able to synthesize large controllers since reachability analysis of the PN must be employed; Chen et al. 20 applied the methodology of interval inhibitor arcs to optimal supervisory control under resources containing multi-token circumstance while suffering from the exponential increment state explosion problem. One solution is to apply mathematics to solve the reachability-related problem of PN in terms of closed-form solutions. As a result, an infinitely large system can be handled with ease.
To efficiently break the ever exponential time plight of getting control states’ information into reasonable waiting time, Chao 32 applied the concept of complete reachability graph and graph theory to split the reachability graph of the control net into reachable, live, forbidden, deadlock, non-reachable, and non-reachable + empty-siphon states (below we call all different types of states as control-related states (CRSs), described in section “Methodology of closed-form solution of kth order system”). Enumerating the tokens’ distribution and applying combinatorial mathematics, Chao 32 pioneered the very first closed-form solution of the number of CRSs for kth order system (defined in Definition 1). This is the first step that allows the exponential computation time for particular and very large PNs to be reduced into intra-seconds. We have also progressed one step further to analyze the effect of non-sharing resources of kth order and k-net systems based on the token number of idle place in each process being equal to the number of resource places in the associated process33–37 and proposed the “proof by model” methodology to accelerate the construction of the closed-form formula for PNs.36,37
One of contributions of the closed-form solution of PN is that the solution can enhance the capability of dynamically modeling large real-time systems. Examples of application are the concept of moment to launch resource (MLR) (controller) allocation and the deadlock avoidance algorithm introduced below.
On the research of the deadlock prevention policy topic, Chao 18 showed that in a kth order system, it needs additional 10 controllers; Li et al. 28 showed that in a kth order–like system where k = 3 and initial marking = 4, it needs additional three controllers where the total token number in these additional controllers is 5. The derived problem is, “Should we need a deadlock prevention policy for very (infinitely) large nets?” Meanwhile in the structural analysis method, there is no indicator to show when to allocate the controllers for a partial deadlock prevention policy.
To solve this problem, based on the contributions of our closed-form solution researches listed above, we proposed a partial deadlock avoidance/prevention policy concept for a very large real-time dynamic RAS: the MLR35,38 for such policy. Presently, the moment can be calibrated by the future deadlock ratio (the number of deadlock states/the number of reachable states) of the current state, which can be derived real-time by closed-form solution, as the indicator. Letting the deadlock thread-holder (DTH) be regarded as a dummy non-sharing waiting resource that can provide one process holding this DTH and wait for the other processes’ work flow, a simple deadlock avoiding algorithm with the transitory maximum number of int(k/2)+1 DTH is proposed in Yu. 37 The decision-making of a DTH allocation is based on the maximum value of the reachable states that the DTH can be allocated at different location in a kth order system subnet, which will consume heavy computation time by applying mixed integer programming (MIP) method for a large system due to the non-deterministic polynomial-time hard (NP-hard) characteristic of the MIP problem 39 but can be derived by closed-form solution intra-seconds.
However, another symmetry system problem that we propose to solve is the effect of top non-sharing subnet connected to idle place (we call this kind of subnet as top non-sharing circle subnet below (TNCS)) in which structure the position of subnet will affect the token distribution for CRSs caused by some tokens flowing into TNCS but not going through the entire process of kth order system. In other words, with a TNCS connected to a kth order system, we have to construct the closed-form solution of CRSs of a modified kth order system, in which case the number of tokens of idle place is less than the number of places in the belonging process. Here, we call such a modified kth order system as deficient kth order system, defined in Definition 1, and an A-net as a net composed by TNCS and deficient kth order system, defined in Definition 4.
In this article, an example of A-net called a-net adopted from Liu et al. 40 will be deconstructed and analyzed, followed by the construction of the closed-form solution for the deficient kth order system to compute the number of CRSs of the a-net.
It is important to use A-net as a target net for research: first, it is most suitable and easy understanding net structure to enter the new research domain, especially the concept of states’ classification, the methodology for closed-form solution of kth order system, integration analysis of different net structures, and the generalization of both deficient kth order system and TNCS adopted in this article. Second, the information obtained from the INA tool shows that A-net has no deadlock states, as explained in section “Computation of CRSs of an ordinary A-net.” Hence, we focus on the characteristic of livelock states where the corresponding kth order system is in deadlock states, which can be analyzed by our methodology. Here, we improve the blind spot of INA tools. Third, by combining the concept of the partial deadlock avoidance/prevention policy, MLR, and the construction of closed-form solution for deficient kth order system, it can realize the concept of dynamic non-sharing processes’ allocation.
The rest of the article is organized as follows. Appendix 2 presents the preliminaries about PNs and S3PR, respectively. Section “Methodology of closed-form solution of kth order system” defines deficient kth order system and lists the relative methodology of closed-form solution of kth order system. Section “Computation of CRSs of an ordinary A-net” analyzes and deconstructs an ordinary A-net structure to compute the number of CRSs. In sections “Computation of CRSs of deficient kth order system” and “Computation of CRSs of A-net,” we construct the closed-form solution of CRSs for both deficient kth order system and A-net. Section “Conclusion” concludes the article. Appendix 3 shows how to apply our methodology to construct the closed-form solution for AR+-net which is a net structure extended from A-net and contains multi-processes on the right-hand side.
Methodology of closed-form solution of kth order system
Let N be a PN and Nr be the reverse net of N. Nr is the net that all the input arcs in N reverse to output arcs; output arcs reverse to input arcs. Chao 32 defined the kth order system (as shown in parts of Definition 1); proposed the concept of complete reachability graph (Figure 5) that lists all states and all paths that any state can be reachable from all states in a kth order system; split the reachability graph of the control net into reachable, live, forbidden, deadlock, non-reachable, and non-reachable+empty-siphon states; and called all the different types of states as CRSs. Table 1 lists all the CRSs of a third-order system. Based on the concept of complete reachability graph, the relationship of the number of different types of CRSs in a kth order system is that the number of non-reachable states is the number of total states − R (R is the number of reachable states); L = R − ϑ where L (resp., ϑ) is the number of live (resp., forbidden) states.
Control-related states of third-order system.
According to graph theory, Chao found and proved Lemma 1, Lemma 2, and Theorem 1; Lemma 3 (resp., Theorem 2) enumerated the number of live (resp., reachable) states of a kth order system; based on the relationship between each type of CRSs, Corollary 2 derived the closed-form formulas of the number of forbidden, non-reachable, and non-reachable+empty-siphon states, respectively.
Here, we first define more general form of the kth order system, called deficient kth order system below. A kth order system is just one of its special cases.
Definition 1
A deficient kth order system is a subclass of S3PR with k resource places r1, r2, …, rk shared between two processes N1 and N2: 32
For all r ∈ PR, M0(r) = 1. 32
N1 (resp., N2) uses r1 − rk (resp., rk − r1) in that order. 32
1 ≤ M0(p0) < k,
Holder places of rj in N1 and N2 are denoted as pj and
The compound circuit containing ri, ri+1, …, rj−1, rj is called (ri − rj) region. 32
There are three possibilities for the token initially at ri to sit at pi (N1),
Examples are shown in Figures 1–4. Figure 4 is an example of deficient fourth-order system with M0(p0) = 3.

First-order system.

Second-order system.

Third-order system.

Deficient fourth-order system.
Definition 2 32
s = (x1, x2, …, xk), xi = 1, 0, or −1, i = 1 to k, is a state for a kth order system N, xi is the token at ri to sit at pi (N1), ri, or
For example, (0 0 0) is the state of third-order system that only resource places r1, r2, and r3 carry tokens.
In Figures 3 and 4, reversing all the input arcs to output arcs, output arcs to input arcs, and inverting the net structures, we can find the reverse net of a (deficient) kth order system is also a (deficient) kth order system but the index of sharing resource is reversed. The reverse state of state (a b c) in third-order system N is (c b a) in its reverse net Nr. This implies that a (deficient) kth order system and its reverse net have the same number of each type of CRSs. In Table 1, the reverse state of the forbidden state (1 0 −1) in N is (−1 0 1) in Nr which is a non-reachable state as shown in Lemma 1. For the third-order system, there are three kinds of unmarked (resp., non-reachable) siphon states: (1 −1 x), (x 1 −1), and (1 0 −1) (resp., (−1 1 x), (x−1 1), and (−1 0 1)), where x = −1, 0, 1. Extending Lemmas 1 and 2, Chao et al. 36 found that the reverse state of a live state in a PN N is a live state in its reverse net Nr, and the number of live states in N is equal to the number of live states in Nr which is the main theory of the concept of proof by model.
Lemma 1 32
Any forbidden state in N is non-reachable in Nr.
Lemma 2 32
Any non-reachable state s in N is a forbidden one or a non-reachable one in Nr.
Theorem 1 32
ϑ(k) = ¥(k) − B(k), where ϑ(k), ¥(k), and B(k) are the number of forbidden, non-reachable, and non-reachable+empty-siphon states in a kth order system, respectively.
Lemma 3 32
(1) s is a live state if and only if (iff) s = {y1, …, yk)|yi = −1 or 0}, or s = {(x1, …, xk)|xi = 1 or 0}. (2) The set of live states Lk = {(x1, …, xk)|xi = 1 or 0} ∪ {(y1, …, yk)|yi = −1 or 0} = La ∪ Lb. (3) The total number of live states is 2k+1 − 1.
Theorem 2 32
The possible reachable states are s = {(x1, x2, …, xj, yj+1, …, yk)|0 ≤ j ≤ k} = {(x1, …, xj 1 yj+2, …, yk)|1 ≤ j ≤ k} ∪ {(y1, …, yk)}, where xi = 1 or 0 (i = 1 to j) and yp = 0 or −1 (p = j+2 to k) = Rc ∪ Rd.
The total number of reachable states is (k+2)2(k−1).
Corollary 2 32
(1) The number of forbidden states ϑ(k) = (k − 2)2(k−1)+1. (2) The number of non-reachable states ¥(k) = 3 k − (k+2)2(k−1). (3) The number of non-reachable+empty-siphon states B(k) = 3 k − k2 k − 1.
Theorem 3 32
In kth order system, a deadlock state has the pattern: (11 12, …, 1 m −1m+1−1m+2, …, −1 k ), 1 ≤ m < k. The total number of deadlock states D(k) = k − 1.
To sum up, shown below are the total number of each type of CRSs in a kth order system that Chao 32 proved.
The total number of states is 3 k .
The total number of live states L(k) = 2k+1 − 1.
The total number of reachable states R(k) =(k+2)2(k−1).
The number of forbidden states ϑ(k) = R(k) − L(k)= (k − 2)2(k−1)+1.
The number of non-reachable states ¥(k) = 3 k − R(k) = 3 k − (k + 2)2(k−1).
The number of non-reachable+empty-siphon states B(k) = ¥(k) − ϑ(k) = 3 k − k2 k − 1.
The total number of deadlock states D(k) = k − 1.
Based on the concept of complete reachability graph (Figure 5) and letting a livelock state be the state that has a directed path to itself state but has no path to initial state, here we extend the definition of forbidden states as the states that have no directed path to the initial state but have a directed path to a deadlock or livelock states. Due to that, the sets of live and forbidden states are two independent sets in a static complete reachability graph, and the number of forbidden states still is ϑ = R − L.

Computation of CRSs of an ordinary A-net
Compared with Figure 3, Figure 6 is a kth order–like system connecting with the TNCS on the left-side process formed by (t1, t11, p12, p11, t12, p13, t13, p14, p0), where the link point is t1.

a-net, an ordinary A-net: composed by deficient kth order system and TNCS. 40
Since there is no empty siphon in TNCS, it will have no deadlock states in this subnet. The tokens in p12 can either fire t1 or t12, which shows that TNCS and the left process can be concurrently processed. However, there are so-called livelock states where tokens can only flow in the left process TNCS when the kth order–like system contains the deadlock states’ pattern as shown in Theorem 3. When tokens flow into left process TNCS, it will affect the A-net’s state.
We follow the kth order system to compute the number of states. Since p11 and p14 are resources, and p12 is a holder of p11; p13 is a holder of p14. We can focus on tokens’ distribution of resource set of {p11, r1, r2, r3, p14} to simplify presentation and computation of CRSs, where {r1, r2, r3} is a resources’ set of a third-order system; {p11, p14} is a resources’ set of TNCS.
Let z be the token number that has flowed into TNCS. We can use (g(f(z),i)x1, x2, x3) to denote the state of an A-net, where x1, x2, x3 are r1, r2, r3 states defined in step (6) of Definition 1; f(z) is a sequence function mapping to two-dimensional vector set which is token distribution of {p11, p14}. In this case, f(0) = {(011, 014)}; f(1) = {(111, 014)), (011, 114)}; f(2) = {(111, 114)} where 011 (resp., 014) is token in p11 (resp., p14); 111 (resp., 114) is token in p12 (resp., p13). |f(0)| = 1; |f(1)| = 2; |f(2)| = 1. g(f(z), i) is a function mapping to a TNCS state according to given f(z) and i, 1 < = i < = |f(z)|, i is the sequence of the set of f(z). For example g(f(1), 1) = (111, 014); g(f(1), 2) = (011, 114); g(f(2), 1) = (111, 114).
Up to now, we have constructed the presentation of state of an a-net that not only can show the sequence of state transformation but also provide the important variable, f(z), to compute the number of CRSs.
Computation of CRSs of a-net
Let R(k) (resp., L(k) and D(k)) be the number of reachable (resp., live and deadlock) states of the kth order system; RD(k, q) (resp., LD(k, q) and DD(k, q)) be the number of reachable (resp., live and deadlock) states of deficient kth order system with the token number of left idle place being q; R′(3) (resp., L′(3) and D′(3)) be the number of reachable (resp., forbidden and livelock) states of a-net. We have the below:
The number of reachable states of a-net is R′(3) = |f(0)|R(3)+|f(1)|RD(3, 2) + |f(2)|RD(3, 1) = R(3)+2RD(3, 2) + RD(3, 1).
The number of live states of a-net is L′(3) = |f(0)|L(3)+|f(1)|LD(3, 2) + |f(2)|LD(3, 1) = L(3)+2LD(3, 2) + LD(3, 1).
The number of livelock states of a-net is D′(3) = |f(0)|D(3)+|f(1)|DD(3, 2) + |f(2)|DD(3, 1) = D(3)+2DD(3, 2) + DD(3, 1).
When the token number in TNCS is 0, the number of reachable states in the right third-order system is |f(0)|R(3) since there is only one state (011, 014); hence, the number of reachable states is R(3) for the third-order system. The case of |f(1)|RD(3, 2) is when the token number in TNCS is 1; there being two states (111, 014) and (011, 114), the number of reachable states is 2RD(3, 2), in which case the token number of the left idle place is 2. The case of |f(2)|RD(3, 1) is the token number in TNCS being 2, the token number of left idle place being 1, and the state of TNCS being (111, 114) only. The analysis of L′(3) and D′(3) is similar to that for R′(3).
By Theorem 2, R(k) = (k+2)2(k−1) => R(3) = (3+2)2(3−1) = 20.
Extending Theorem 2, RD(3, 2) = |Rc|+|Rd| = (2(3−1)+2 × 2(3−2)+2(3−1) − 1)+(23) = 19, where Rc = {(1 y2y3)} ∪ {(x1 1 y3)} ∪ {(01 02 13), (01 12 13), (11 02 13)}, where x1 = 0 or 1, y2 and y3 can be 0 or −1. Rd = {(y1, …, y3)} yp = 0 or −1, p = 1 to 3.
RD(3, 1) = |Rc|+|Rd| = (2(3−1)+2(2–1)+2(1–1))+(23) = 15, where Rc = {(1 y2y3)} ∪ {(01 1 y3)} ∪ {(01 02 13)}, where y2 and y3 can be 0 or −1. Rd = {(y1, …, y3)} yp = 0 or −1, p = 1 to 3.
Hence, R′(3) = R(3)+2RD(3, 2)+RD(3, 1) = 20+2 × 19+15 = 73.
By Lemma 3, L(k) = 2k+1 − 1 => L(3) = 23+1 − 1 = 15.
Extending Lemma 3, LD(3, 2) = |La|+|Lb| = (2(3−3)+2(3−2)+2(3−1) − 1)+(23) = 14, where La = {(11 02 03)} ∪ {(x1 12 03)} ∪ {(01 02 13), (01 12 13), (11 02 13)} where x1 = 1 or 0}, Lb = {(y1y2y3)|yi = −1 or 0, i = 1 to 3}.
LD(3, 1) = |La|+|Lb| = (2(3−3)+2(3−2) − 1+1)+(23) = 11.
Hence, L′(3) = L(3)+2LD(3, 2)+LD(3, 1) = 15 + 2 × 14+11 = 54.
By Theorem 3, D(k) = k − 1. Since the total number of deadlock states corresponds to the position m, hence D(3) = DD(3, 2) = DD(3, 1) = 2. D′(3) = D(3) + 2DD(3, 2) + DD(3, 1) = 8.
The number of forbidden states of a-net is R′(3) − L′(3) = 73 − 54 = 19.
To sum up, shown below are the total number of reachable, live, forbidden and livelock states of a-net.
The total number of reachable states R′(3) = 73.
The total number of live states L′(3) = 54.
The number of forbidden states ϑ′(3) = 19.
The total number of livelock states D′(3) = 8.
Computation of CRSs of deficient kth order system
To extend to general A-net, we have to complete the general formula of RD(k, q) and LD(k, q) of the deficient kth order system described in section “Computation of CRSs of an ordinary A-net” first.
The phenomenon of the deficient kth order system in an A-net is when the token number flowing into TNCS is greater than 1 as described in section “Computation of CRSs of an ordinary A-net.”
Construct general formula of RD(k, q) and LD(k, q)
Let kq be a deficient kth order system with q (q ≤ k) tokens in the left idle place; that is, M(p0) = q and
Definition 3
An impossible state in a deficient kth order system is a reachable state in kth order system, but not a legal state due to the token number in left process being greater than that of the left idle place p0.
For example, state s = (11 12 13 14 05) is a reachable state in fifth-order system but an impossible state in deficient 53-th order system, since the token number in left process is 4, greater than 3 which is the token number of the left idle place in deficient 53-th order system.
Theorem 4
Let R(k) be the reachable states of a kth order system and RD(k, q) be the number of reachable states of kq, a deficient kth order system, then
where C(l − 1, l − 1 − i) = (l − 1)!/[(l − 1 − i)!i!], is a binomial coefficient.
Proof
The line of thinking is RD(k, q) = R(k) − (the impossible states in kq but are all reachable states in kth order system). According to Theorem 2, comparing with RD(k, q) and R(k), the same value both in RD(k, q) and R(k) is |Rd|, where Rd = {(y1, …, yk)|yi = 0 or −1 (p = 1 to k)}, which is the token distribution on the right S2PR (Definition 7 in Appendix 2). In Rc, the same number of reachable states’ subsets both in RD(k, q) and R(k) are from subset {(11, y2, …, yk)|1 ≤ q ≤ k, yp = 0 or −1 (p = 2 to k)} till subset {(x1, …, xq−1 1
q
yq+1, …, yk)|1 ≤ q ≤ k, where xi = 1 or 0 (i = 1 to q − 1) and yp = 0 or −1 (p = q+1 to k)}. By induction, the impossibility of reachable states in subset Rq+1 = {(x1, …, xq 1q+1yq+2, …, yk)|…} of RD(k, q) is subset Iq = {(x1, …, xq 1q+1yq+2, …, yk)|where xi = 1, i = 1 to q, yp = 0 or −1 (p = q+2 to k)}, and |Iq| = C(q, q)2(k−q−1). When Rq+2 = {(x1, …, xq+1 1q+2yq+3, …, yk)|…}, the set of impossibility is Iq+1 = {(x1, …, xq+1 1q+2yq+3, …, yk)} where xi = 1, i = 1 to q+1 (the number is 2(k−q−2)C(q+1, q+1)) ∪ {(x1, …, xq+1 1q+2yq+3, …, yk)|xi = 0 or 1, i = 1 to q+1, x1+···+xq+1 = q, yp = 0 or −1 (p = q+3 to k)} (the number is 2(k−q−2)C(q+1, q)); hence |Iq+1| = [C(q+1, q+1))+C(q+1, q)]2(k−q−2), till Rk = {(x1, …, xk−1 1
k
)|…} the subset of impossibility is Ik−1 = {(x1, …, xq+1xq+2xq+3… 1
k
)|xi = 0 or 1, i = 1 to k − 1, x1+···+xk−1 ≥ q}, and |Ik−1| = [C(k − 1, k − 1))+···+C(k − 1, q)]2(k−k). We have all subsets of impossibility occurring from Rq+1 to Rk, and the number of impossibility counts from C(q, q)2(k−q−1) to [C(k − 1, k − 1)) + ···+C(k − 1, q)]2(k−k) =
Hence,
Let k = 8, q = 2, impossible states of RD(8, 2) are shown below. l is the first position of xi = 1 (Table 2).
Counts of impossible states of RD(k, q) where k = 8, q = 2.
Theorem 5
Let L(k) be the live states of a kth order system, LD(k, q) be the number of live states of kth order system with token number of left idle place being q
Proof
The proof is similar to that of RD(k, q). The difference is that by Lemma 3, s is a live state if and only if s = {(y1, …, yk)|yi = −1 or 0}, or s = {(x1, …, xk)|xi = 1 or 0}. Hence, comparing to RD(k, q), the impossibility of live states in subset Lq+1 = {(x1, …, xq 1q+1yq+2, …, yk)|…} of LD(k, q) is subset Iq = {(x1, …, xq 1q+1 0q+2… 0
k
)| where xi = 1, i = 1 to q, yp = 0 (p = q+2 to k)}, |Iq| = C(q, q). Iq+1 = {(x1, …, xq+1 1q+2 0q+3… 0
k
)} where xi = 1, i = 1 to q + 1(the number is C(q + 1, q + 1)) ∪ {(x1, …, xq+1 1q+2 0q+3… 0
k
)|xi = 0 or 1, i = 1 to q+1, x1+···+xq+1 = q} (the number is C(q+1, q)), hence |Iq+1| = C(q + 1, q+1)) + C(q + 1, q). Similar to RD(k, q), we have all the subsets of impossibility occurring from Lq+1 to Lk; the number of impossibility counts from C(q, q) to [C(k − 1, k − 1)) + ··· +C(k −1, q) =
Hence,
The forbidden states of kq is
The value of RD(k, q), LD(k, q), and LD(k, q), where k = 8, q = 1 to 7.
Computation of CRSs of A-net
According to RD(k, q) and LD(k, q) of deficient kth order system derived in section “Computation of CRSs of deficient kth order system,” and a given state function of TNCS, f(z), in this section we construct closed-form solution to compute CRSs of A-net.
Definition 4
An A-net system is a subclass of S3PR composed by a kth order system and a deadlock-free TNCS connected to idle process of left process:
The link point of kth order system and TNCS is the top-left transition of kth order system.
None of transition of TNCS is firable by the resources and places of kth order system.
Let m be the maximum token number that can flow into TNCS; the limitation of m is m < k.
Under the limitation of m < k, both kth order system and TNCS can expand its net structure independently.
There is a measurable state function of TNCS f(z), where z is the number of tokens flowing into TNCS, such that |f(z)| can map to a non-ambiguous number of different states of combination under current information of z in TNCS.
Let RD(k, k) = R(k). Hence, we have the following:
The reachable state of A-net is
The live state of A-net is
The forbidden state of A-net is
The livelock state of A-net is
The important characteristic of A-net is that m and k can be expanded independently under the condition m < k. Extending k of A-net from 4 to 8, we have the value of
The value of
These results of
Extending m of A-net from 3 to 5 with k = 8, we have the value of
The value of
Application
Based on the closed-form solution and the concept of proof by model, we can accelerate the construction of the closed-form formula of the reverse net of A-net, rev(A-net), which is the fundamental model of merging two different manufacturing processes, due to that the live states’ pattern of rev(A-net) will be the reverse states of A-net’s live states and they have the same number of live states.
In Appendix 3, we will show how to extend our methodology to derivate the closed-form solution of AR+-net which is a net structure containing a non-sharing subnet and multi-processes on the right-hand side extended from A-net.
Conclusion
Here, we not only report the very first method to compute in closed form the number of CRSs of A-net without constructing a reachability graph but also demonstrate the procedure of how to construct deficient kth order system by particular case step by step. The most important line of thinking is RD(k, q) = R(k) − (the impossible states in kq but are all reachable states in kth order system), as shown in the proof procedure of Theorem 4. According to the procedure listed above, readers can derive the closed-form solution of more complicated A-net or even of which case non-sharing circle subnet can be any position in left or right process. Besides, by our closed-form solution, we can provide live, forbidden, and livelock states’ information that INA tool cannot offer, which show non-significant reachable states’ information only, due to no deadlock states in A-net and that INA tool cannot detect livelock states. This helps estimate the percentage of livelock (deadlock) and legal state losses due to the addition of a monitor and avoid the dire situation of mid-run abortion of reachability analysis due to exhausted memory. Furthermore, here we extend the MLR concept to the variant kth order system with non-sharing subnet.
Future work should extend the analysis method in this article to A-net with one non-sharing resource (e.g. used by only one process) located in any position of the system.
Footnotes
Appendix 1
Appendix 2
Appendix 3
Academic Editor: ZhiWu Li
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 by the National Science Council (Republic of China) under Grant NSC 103-2221-E-004-001.
