METHOD FOR ANALYZING REACHABILITY OF PETRI NET
20220398364 · 2022-12-15
Inventors
Cpc classification
G06N5/01
PHYSICS
International classification
Abstract
A method for analyzing reachability of a Petri net and deriving the control-related state of the PN extended from the kth variant closed-form formula (CFF) system for numbers, comprising by proving that the first system Gen-Right(k, gen) and the second system Gen_Left(k, k−gen) are topological inverse networks of Gen-Left(k, gen), the first system and the second system An invertible one-to-one mapping between; wherein the first series Gen-Right(k, gen) and Gen-Left(k, k−gen) have the same closed-form formula, and by putting Gen-Left(k, gen) in the verified closed-form formula The parameter gen can be obtained by replacing it with k−gen, and its corresponding reachability state can be directly obtained through a reversible one-to-one mapping.
Claims
1. A method for analyzing reachability of a Petri net (PN) and deriving the control-related state of the PN extended from the kth variant closed-form formula (CFF) system for numbers, the method comprising: by proving that the first system Gen-Right(k, gen) and the second system Gen_Left(k, k−gen) are topological inverse networks of Gen-Left(k, gen), the first system and the second system An invertible one-to-one mapping between; wherein the first series Gen-Right(k, gen) and Gen-Left(k, k−gen) have the same closed-form formula, and by putting Gen-Left(k, gen) in the verified closed-form formula The parameter gen can be obtained by replacing it with k−gen, and its corresponding reachability state can be directly obtained through a reversible one-to-one mapping.
2. The method for analyzing reachability of a Petri net as claim 1, wherein the method is based on knowledge-based use of the verified network accessibility and closure solution information to change parameter values such as itineraries, non-shared resources and multi-scepter shared resource locations, and directly obtain the new network, the network architecture has a reversible one-to-one mapping of the reachability and closure solution information of the new network architecture, the method is referred to here as Topological Reverse Mirroring (TRM).
3. The method for analyzing reachability of a Petri net as claim 2, wherein the topological inverse mirror system is used to analyze reachability and derive a closed-form formula to control the number of control-related states.
4. The method for analyzing reachability of a Petri net as claim 3, wherein the control-related states are reachable, active, prohibited, deadlocked, livelocked, and unreachable.
5. The method for analyzing reachability of a Petri net as claim 1, wherein the method further includes providing the CFF of the number of CRSs of the double-deficient k-order system of non-shared resources.
6. The method for analyzing reachability of a Petri net as claim 5, wherein the method further includes using embedded filter coefficients (EFC) in front of the CFF as a necessary condition for each of the α and β of the CRS.
7. The method for analyzing reachability of a Petri net as claim 5, wherein the necessary conditions for the EFC of the reachable state are α≥0 and β≥0; where min(max(min(α, β, 0)+1, 0), 1)) is used as the embedded filter coefficient (EFC) to exclude possibilities (α<0 or β<0).
8. The method for analyzing reachability of a Petri net as claim 5, wherein the necessary conditions for the EFC of the active state are α≥0 and β≥0, but excluding the conditions of α=0 and β=0; where, using (min(max(min(α, β, 0)+1, 0), 1)) (min(max(max(α, 0), max(β, 0)), 1)) as EFC.
9. The method for analyzing reachability of a Petri net as claim 5, wherein the basic condition of the EFC of the dead state is (α=β=0) union (α>0 and β>0); where, use 1−(min(max(max(α, 0), max(β, 0)), 1)); max(min(α, β, 1), 0) as (α>0 and β>0) EFC of CFF under condition.
10. The method for analyzing reachability of a Petri net as claim 1, wherein the CFF of the number of CRSs of the non-shared resource double-deficient k-order system is used as the basic model for deriving the CFF of more complex PNs by applying the TRM, and provides decision-making based on the current state of the real-time reachability information system control application.
Description
BRIEF DESCRIPTION OF THE DRAWINGS
[0026] One or more embodiments are illustrated by way of example, and not by limitation, in the figures of the accompanying drawings, wherein elements are having the same reference numeral designations represent like elements throughout. The drawings are not to scale, unless otherwise disclosed.
[0027]
[0028]
[0029]
[0030]
[0031]
[0032]
[0033]
[0034]
DETAILED DESCRIPTION
[0035] Unless defined otherwise, all technical and scientific terms used herein have the same meanings as commonly understood by one of skill in the art to which this disclosure belongs. It will be further understood that terms; such as those defined in commonly used dictionaries, should be interpreted as having a meaning that is consistent with their meaning in the context of the relevant art and the present disclosure, and will not be interpreted in an idealized or overly formal sense unless expressly so defined herein.
[0036] Reference throughout this specification to “one embodiment” or “an embodiment” means that a particular feature, structure, or characteristic described in connection with the embodiment is included in at least one embodiment. Thus, the appearances of the phrases “in one embodiment” or “in an embodiment” in various places throughout this specification are not necessarily all referring to the same embodiment. Furthermore, the particular features, structures, or characteristics may be combined in any suitable manner in one or more embodiments.
[0037] To solve the problems listed above, the present invention reports Topological Reverse Mirroring (TRM), a knowledge-based methodology, to accelerate reachability analysis and the construction of CFF for more complicated PNs without whole net structure analysis; and provides the CFF of the number of CRSs for Double Deficient k-th order system with one non-sharing resource as the basic model for applying TRM to derive CFF for more complicated PNs to providing real-time reachability information based on current state for the decision-making of system control applications.
[0038] Comparing to presently analyzing whole net structure method, topological reverse mirroring’ (TRM) is a new knowledge-based methodology for more efficiently analyzing reachability and deriving the closed-form formulas (CFF) of the number of Control-Related states for PNs extended from variant k-th order systems.
[0039] According to variant k-th order systems, TRM is constructed by proving that both Gen-Right(k, gen) and Gen_Left(k, k−gen) are the topological reverse nets of Gen-Left(k, gen) such that there is a reversible one-to-one mapping (Mirroring) between these two systems. Thus, CFF for Gen-Right(k, gen) and Gen-Left(k, k−gen) have same CFF, which can be immediately derived by replacing the parameter ‘gen’ by ‘k−gen’ in validated CFF for Gen-Left(k, gen). The CFF for variant double deficient k-th order system is reported as the basic system to extend analyzing reachability and deriving the CFF for more topological reverse mirroring. Also, the present invention provides real-time reachability information based on current state. The shown applications of TRM include the reachability analyzing for systems with non-sharing sub-net; double deficient tokens; multi-non-sharing/multi-tokens resources; and multi-processes extended from k-th order system. The present invention reports the core methodology to accelerate furthering emerging system-control applications for more complicated PNs based on the real-time information derived by their CFF.
[0040] A Petri net is a 4-tuple N=(P, T, F, W), where P is the set of places, T is the set of transitions, F.Math.(P×T)∪(T×P) is called flow relation of the net, represented by arcs with arrows from places to transitions or vice versa, and W: F.fwdarw.Z (the set of non-negative integers) is a mapping that assigns a weight to an arc. M.sub.0: P.fwdarw.Z is the initial marking assigned to each place p∈P, M.sub.0(p) token, and (N, M.sub.0) is called a marked net or a net system. The set of input (resp. output) transitions of a place p is denoted by .sup.•p (resp. p.sup.•).
[0041] Similarly, the set of input (resp. output) places of a transition t is denoted by .sup.•t (resp. t.sup.•). It is called a Marked Graph (MG) if ∀p∈.sup.⋅P, |p.sup.⋅|=|.sup.⋅p|=1. An elementary directed path Γ in N is a graphical object containing a sequence of nodes such that there is an arc between each two successive nodes in the sequence with the notation: Γ=[n.sub.1 n.sub.2 . . . n.sub.k], k≥1, such that n.sub.i≠n.sub.j for i≠j is the reverse net of N obtained by reversing the direction of all arcs in N with the initial marking unchanged. A is the incidence matrix of a net with m places and n transitions: A=[a.sub.ij]; a matrix of integers and its typical entry is given by a.sub.ij=a.sub.ij.sup.+−a.sub.ij.sup.− where a.sub.ij.sup.−=W(i, j) is the weight of the arc from transition i to its output place j, and a.sub.ij.sup.+=W(j, i) is the weight of the arc to transition i from its input place j. A.sup.r=−A where A.sup.r is the incidence matrix of the reverse net N.sup.r of N. Given a marking M, a transition t is enabled if ∀p∈.sup.⋅t, M(p)≥W(p, t), and this is denoted by M[t>. Firing an enabled transition t results in a new marking M.sub.1, which is obtained by removing W(p, t) tokens from each place p∈.sup.⋅t and placing W(t, p′) tokens in each place p′∈t.sup.⋅, moving the system state from M.sub.0 to M.sub.1.
[0042] Repeating the foregoing process, it reaches M′ by firing a sequence σ=t.sub.1t.sub.2 . . . t.sub.k of transitions. M′ is said to be reachable from M0; i.e., M.sub.0[σ>M′. R(N, M.sub.0) is the set of markings reachable from M.sub.0. A forbidden (resp. live) marking or state is one that is (resp. is not) a—or necessarily evolves into—a deadlock marking. For a Petri net (N, M.sub.0), a non-empty subset S (resp. τ) of places is called a siphon (resp. trap) if .sup.•S.Math.S.sup.•(resp. τ.sup.•.Math..sup.•τ), i.e., every transition having an output (resp. input) place in S has an input (resp. output) place in S (resp. τ). A siphon is a set of places where tokens can continuously flow out so that M.sub.0(S)=Σ.sub.p∈SM.sub.0 (p)=0, S is called an empty siphon or unmarked siphon at M.sub.0; all output transitions of S are permanently dead.
[0043] Several definitions are introduced in the following paragraphs.
[0044] Definition 1
[0045] (J. Ezpeleta et al. 1995): A simple sequential process (S.sup.2P) is a net N=(P∪{p.sup.0}, T, F) where: P≠Ø, p.sup.0.Math.P (p.sup.0 is called the process idle or initial or final operation place); 2) N is strongly connected state machine and 3) every circuit of N contains the place p.sup.0.
[0046] Transitions in p.sup.0⋅ and .sup.⋅p.sup.0 are called source and sink transitions respectively.
[0047] Definition 2
[0048] (J. Ezpeleta et al. 1995): A simple sequential process with resources (S.sup.2PR), also called a working process (WP), is a net N=(P∪{p.sup.0}∪P.sub.R, T, F) so that 1) the subnet generated by X=P∪{p.sup.0}∪T is an S.sup.2P; 2) P.sub.R≠Ø and P∪{p.sup.0}∩P.sub.R=Ø; 3)∀p∈P, ∀t∈.sup.⋅p, ∀t′Ep.sup.⋅, ∃r.sub.p∈P.sub.R, t∩P.sub.R=t′.sup.•ωP.sub.R={r.sub.p}; 4) The two following statements are verified: ∀r∈P.sub.R, a) .sup.⋅⋅r∩P=r.sup.⋅⋅∩P≠Ø; b) .sup.⋅r∩r.sup.⋅=Ø. 5) .sup.⋅⋅(p.sup.0)∩P.sub.R=(p0).sup.⋅⋅∩P.sub.R=Ø. ∀p∈P, p is called an operation place. ∀r∈P.sub.R, r is called a resource place. H(r)=.sup.⋅⋅r∩P denotes the set of holders of r (operation places that use r). Any resource r is associated with a minimal P-invariant whose support is denoted by ρ(r)={r}∪H(r).
[0049] Definition 3
[0050] (J. Ezpeleta et al. 1995): A system of S.sup.2PR (S.sup.3PR) is defined recursively as follows: 1) An S.sup.2PR is defined as an S.sup.3PR; 2) Let Ni=(P.sub.i∪P.sub.i.sup.0∪P.sub.Ri, T.sub.i, i∈{1,2} be two S.sup.3PR so that)) (P.sub.1∪P.sub.1.sup.0)∩(P.sub.2∪P.sub.2.sup.0)=Ø. PR.sub.1∩PR.sub.2=P.sub.C(≠Ø) and T.sub.1∩T.sub.2=Ø. The net N=(P∪P.sup.0∪P.sub.R, T, F) resulting from the composition of N.sub.1 and N.sub.2 via P.sub.C (denoted by N.sub.1 o N.sub.2) defined as follows: 1) P=P.sub.1∪P.sub.2; 2) P.sup.0=P.sub.1.sup.0∪P.sub.2.sup.0; 3) P.sub.R=P.sub.R1∪P.sub.R2; 4) T=T.sub.1∪T.sub.2 and 5) Γ=F.sub.1∪F.sub.2 is also an S.sup.3PR.
[0051] Definition 4
[0052] A variant k-th order system is a subclass of S.sup.3PR with k resource places r.sub.1, r.sub.2, . . . , r.sub.k shared between two processes N.sub.1 and N.sub.2 and one non-sharing resource place r′.sub.gen (=r*) used by an operation place p* in N.sub.1 or N.sub.2. [0053] 1. M.sub.0(r′.sub.gen)=1 and ∀r∈P.sub.R, M.sub.0(r)=1. [0054] 2. N.sub.1 (resp. N.sub.2) uses r.sub.1, r.sub.2, . . . , r.sub.k (resp. r.sub.k, r.sub.k−1, . . . r.sub.2, r.sub.1) in that order. [0055] 3. When p* in N.sub.1 (resp. N.sub.2) M.sub.0(p.sub.0)=k+1, M.sub.0(p′.sub.0)=k (resp. M.sub.0(p.sub.0)=k, M.sub.0(p′.sub.0)=k+1), where p.sub.0 and p′.sub.0 are the idle places in processes N.sub.1 and N.sub.2, respectively. [0056] 4. Holder places of r.sub.j in N.sub.1 and N.sub.2 are denoted as p.sub.j and p′.sub.j respectively. [0057] 5. The compound circuit containing r.sub.i, r.sub.i+1, . . . r.sub.j−1, rj is called the (r.sub.i-r.sub.j)-region. [0058] 6. The position of r′.sub.gen is located between r.sub.gen and r.sub.gen+1. If r′.sub.gen does not exist, then it is called a k-th order system; when M.sub.0(p.sub.0)<k, then it is called a Deficient k-th order system; when both M.sub.0(p.sub.0)<k and M.sub.0(p′.sub.0)<k, then it is called a Double Deficient k-th order system. [0059] 7. There are 3 possibilities for the token initially at r.sub.i to sit at: p.sub.i(N.sub.1), p′.sub.i(N.sub.2), and r.sub.i. The corresponding token or r.sub.i state is denoted by 1, −1 and 0, respectively. [0060] 8. x[y] means r.sub.gen is at x state (x=1, 0, −1) and r′.sub.gen is at y state (y=1, 0, −1), where gen is the location of non-sharing resource being used by an operation place p*, 1≤gen≤k−1. The system is denoted as a Gen-Left(k, gen) system when p* in N.sub.1; a Gen-Right(k, gen) system when p* in N.sub.2. Unless otherwise listed parameters, Gen-Left is the abbreviation of Gen-Left(k, gen); Gen-Right is the abbreviation of Gen-Right(k, gen). [0061] 9. The union of Gen-Left and Gen-Right is denoted as a Gen-One system.
[0062] Definition 5
[0063] A generalized k-th order system (k-net) (Chao, 2016; Chao & Yu, 2014; 2016) is a subclass of S.sup.3PR with k resource places r.sub.1, r.sub.2, . . . , r.sub.k shared between α+ processes N.sub.1.sup.+, N.sub.2.sup.+, . . . , Nα.sup.+ and β.sup.− processes, N.sub.1.sup.−, N.sub.2.sup.−, . . . , N.sub.β.sup.− (denoted as k G th-order system). M(r)=M(r)= . . . =M (r)=1. N.sub.i.sup.+(respectively N.sub.j.sup.−) uses r.sub.1, r.sub.2, . . . , r.sub.k (resp. r.sub.k, r.sub.k−1, . . . r.sub.2, r.sub.1) in that order, i=1, 2, . . . , α(resp. j=1, 2, . . . , β). Each of N.sub.i.sup.+ and N.sub.j.sup.− is an elementary circuit. When there is exactly one+ process and one− process, a generalized k-th order system becomes a k-th one (a k G-th order system is a k-th order system). P.sup.+ (respectively P.sup.−) is the set of operation places in + processes (respectively− processes). H(r).sup.+ (respectively H(r).sup.−) is the set of holder places of r that are in P.sup.+ (respectively P.sup.−). Let a generalized k-th order system with a non-sharing resource in gen location of N.sub.i process be denoted as a kαβ(i, gen)-th order system.
[0064] Definition 6
[0065] The equivalent N.sup.e=(P.sup.e∪P.sup.e.sub.R, F.sup.e) of a net N=(P∪P.sub.R∪P.sub.NR, T, F) (P.sub.NR is the set of non-sharing places) is defined as [0066] 1. P.sup.e.sub.R=P.sub.R\P.sub.NR; [0067] 2. P.sup.e=P\∪.sub.r∈PNRH(r); [0068] 3. T.sup.e=T\∪.sub.r∈PNRr.sup.⋅; [0069] 4. F.sup.e=(F∪.sub.r∈PNR(.sup.⋅r,r.sup.⋅⋅)∪(.sup.⋅(r.sup.⋅),.sup.⋅r)\∪.sub.r∈PNR [(H(r), H(r).sup.⋅)∪(.sup.⋅H(r), H(r))∪(.sup.⋅r,r)∪(r,r.sup.⋅) ∪(r.sup.⋅,r.sup.⋅⋅)∪(.sup.⋅(r.sup.⋅),r.sup.⋅)].
[0070] Definition 7
[0071] (Chao, 2014): s=(x.sub.1 x.sub.2 . . . x.sub.k), x.sub.i=1, 0 or −1, i=1 to k, is a state for a k-th order system N, x.sub.i is the token at r.sub.i to sit at: p.sub.i(N.sub.1), r.sub.i or p′.sub.i(N.sub.2) respectively. (x.sub.i x.sub.i+1 . . . x.sub.q), k≥i≥1, k≥q≥i≥1 (embedded in s) is a sub-state of s.
[0072] Theoretical Framework for Constructing CFS for PNs
[0073] According to Definition 4, examples of the subset of Gen-One k-th order system are shown in
[0074] Let rev(N) be the reverse net of a PN N (e.g.,
[0075] According to Definitions 4 and 7, the present invention presents the notation of state and sub-state by the viewpoint of the distribution of tokens between “resources” instead of by the viewpoint of the “places” applied by INA tools. For example, when p.sub.1, p.sub.2 and p′.sub.3 contain one token in
[0076] In addition, Chao (2014) showed that (−1 0 1), (−1 1 x) and (x −1 1) [resp. (1 0 −1), (1 −1 x) and (x 1 −1)] where x=−1, 0 or 1 are three basic kinds of non-reachable (resp. unmarked siphon) states in k-th order system where k=3. Extending to a large system, a non-reachable state contains the sub-states pattern (−1 x x x 1) where x=1, 0, −1; a sub-state of (1 x x x −1) (x=1, 0, −1) corresponds to a forbidden or a non-reachable state; and a forbidden state finally reaches to a deadlock state that has the state pattern: (1.sub.1 1.sub.2 . . . 1.sub.m −1.sub.m+1 −1.sub.m+2 . . . −1.sub.k), 1≤m<k.
[0077] Further, Chao (2014) proved that any forbidden state in an N is non-reachable in rev(N); any non-reachable states in a N is a forbidden one or a non-reachable one in rev(N). Chao et al. (2016) enhanced this theoretical framework by proving that a reverse state of a live state in a N is also a live state in the rev(N) such that both of N and rev(N) have same number of live states.
[0078] The Effects of a Non-Sharing Resource in Variant k-th Order System
[0079] By the definition of the equivalent (Definition 6), k-th order system (e.g.
[0080] Let N be Gen-One k-th order system (e.g. Gen-Left or Gen-Right), Ne be the corresponding k-th order system, y=1 in Gen-Left, y=−1 in Gen-Right, the generalized forbidden and non-reachable state pattern in Gen-one are shown as following: [0081] 1. The patterns of forbidden states including the non-sharing resource in N are the states that contain or will contain sub-state (1 0[y] −1) and (1[y] −1); the non-reachable states part contains or will contain sub-state (−1[y] 1) and (−1 0[y] 1). [0082] 2. A sub-state of (−1 x . . . x[y] x . . . 1) (x=1, 0, −1) is a non-reachable state in N. [0083] 3. A sub-state of (1 x . . . x[y] x . . . −1) (x=1, 0, −1) is a forbidden or a non-reachable state in N.
[0084] The followings list the effects of increasing a non-sharing resource in k-th order system based on the viewpoint of Gen-Left (Chao and Yu, 2016) and then extending the viewpoint to Gen-one. [0085] 1. Let M.sup.e be reachable (resp. live) in N.sup.e, since both M*=M.sup.e+r* and M′=M.sup.e+p* are reachable (resp. live) in N, and the number of reachable (resp. live) states is greater than 2R(k) (resp. 2L(k)). [0086] 2. The phenomenon of increasing “the additional restricted reachable (resp. live) states derived from non-reachable (resp. non-live, including non-reachable and forbidden) states of the equivalent caused by a non-sharing resource”, ARRS, (resp. ARLS) occurs when one process waits for the work flow of the other process in the holder of the one existing non-sharing resource. In this situation the current state is a non-reachable (resp. non-live) marking of N.sup.e but a reachable (resp. maybe live) marking of Gen-one. The states pattern of ARRS in Gen-Left is s=(x.sub.1 . . . −1.sub.ix.sub.i+1 . . . x.sub.gen . . . x.sub.j+1 x.sub.j+2 . . . x.sub.k) where x.sub.m=0 or −1, i+1≤m≤gen and j+1≤m≤k; x.sub.m=0, gen+1≤m≤j−1; (x.sub.1 . . . x.sub.i−1) is a reachable states pattern of (i−1)-th order system, because the process can wait in only one existing non-sharing resource for the other process work flow.
[0087] 1. Topological Reverse Mirroring (TRM), a Knowledge-Based Methodology:
[0088] Based on variant k-th order system, Topological Reverse Mirroring (TRM) methodology is constructed by proving Theorem 1.1, Lemma 1.1 and Corollary 1.1 as shown below:
[0089] Theorem 1.1: Gen-Right(k, gen), rev(Gen-Left(k, gen)), and Gen-Left(k, k−gen) have the same topological net structure.
[0090]
[0091] Let mapX.sub.IP be the mapping function corresponding to idle places where X=1 to 3; mapX.sub.PT corresponding to places and transitions; mapX.sub.R corresponding to sharing resources; mapX.sub.HN corresponding to the holder of the non-sharing resource; mapX.sub.NR corresponding to the non-sharing resource, the example shown in
[0097] Let the states pattern of Gen-Left(k, gen), Gen-Left(k, k−gen), rev(Gen-Left(k, gen)) and the inverted and left and right rotation net of Gen-Right(k, gen) be headed with s.sub.L, s.sub.L.sup.k−g, s.sub.L.sup.rev and s.sub.R, respectively, as shown in
[0098] Lemma 1.1: Let s.sub.1, . . . , s.sub.k−gen, [y], s.sub.k be the token distribution of resources r.sub.1, . . . , r.sub.k−gen, r* . . . , r.sub.k in Gen-Left(k, k−gen), then s.sub.L.sup.k−g(s.sub.1, . . . , s.sub.k−gen[y], . . . , s.sub.k), s.sub.L.sup.rev(s.sub.k, . . . , [y]s.sub.gen, . . . s.sub.1) and s.sub.R(−s.sub.k, . . . , [−y](−s).sub.gen . . . −s.sub.1) are the functional equivalence states and they have the same type of CRSs. Let k=3, gen=2, for a Gen-Left(3, 3−2) as shown in
[0099] Corollary 1.1: Gen-Left(k, k−gen), rev(Gen-Left(k, gen)) and Gen-Right(k, gen) all have same closed-form solution (CFS).
[0100] Theorem 1.1 shows that Gen-Left(k, k−gen) is a “topological reverse” net of Gen-Left(k, gen). Gen-Left(k, k−gen) can be called a relay reverse net because its CFS can be directly derived from the validated parts of Gen-Left(k, gen) by replacing “gen” with “k−gen”. Applying functional equivalence mapping of Gen-Left(k, k−gen) and Gen-Right, the mirroring, CFS for the Gen-Right can be derived without detailed siphon net structure analysis. Lemma 1 provide the state transformation rule among Gen-Left(k, k−gen), rev(Gen-Left(k, gen)) and Gen-Right(k, gen). The present invention calls this analyzing methodology topological reverse mirroring (TRM).
[0101] 2. The CFF for Variant Double Deficient k-Th Order System with One Non-Sharing Resource
[0102] Let DDk(k, α, β) be Double Deficient k-th order system, where k is the number of sharing resources places M.sub.0(p.sub.0)=α, M.sub.0(p′.sub.0)=β; DDGen-Left(k, α, β, gen) be Gen-Left(k, gen), where M.sub.0(p.sub.0)=α, M.sub.0(p′.sub.0)=β; DDGen-Right(k, α, β, gen) be Gen-right(k, gen), where M.sub.0(p.sub.0)=α, M.sub.0(p′.sub.0)=β, the CFF for Variant Double Deficient k-th order system are shown as followings.
[0103] The present invention will use an embedded filtering coefficient (EFC) in front of the CFF as the essential condition for α and β for each type of CRSs as shown in table 1.
[0104] 1. The EFC for reachable states: the essential condition is (α≥0 and β≥0). One can use min(max(min(α, β, 0)+1, 0), 1)) as embedded filtering coefficient (EFC) to exclude the possibility (α<0 or β<0). For example, (α<0 or β<0)=>max(min(α, β, 0)+1, 0)=0=>min(max(min(α, β, 0)+1, 0), 1))=0, in which case will force the value of whole formula being 0; (α≥0 or β≥0)=>max(min(α, β, 0)+1, 0)≥1=>min(max(min(α, β, 0)+1, 0), 1))=1, in which case the value of CFF is depending on the successive formula.
[0105] 2. The EFC for live states: the essential condition is (α≥0 and β≥0) but excluding the condition of (α=0 and β=0), under which condition the state is a deadlock state. One can use (min(max(min(α, β, 0)+1, 0), 1)) (min(max(max(α, 0), max(β, 0)), 1)) as the EFC. For example (α=β=0)=>the value of (min(max(max(α, 0), max(β, 0)), 1)) is 0.
[0106] 3. The EFC for live states: according to the formula Ļ.=Ŗ−F̧, it is embedded in the formula of reachable and live states.
[0107] 4. The EFC for deadlock states: the essential condition is (α=β=0)∪(α>0 and β>0). One can use 1−(min(max(max(α, 0), max(β, 0)), 1)) for the special condition of (α=β=0); max(min(α, β, 1), 0) as the EFC for the CFF under the condition of (α>0 and β>0).
[0108] 5. The EFC for ARRS and ARLS: the essential condition is (α≥1 and β≥1). One can use max(min(α, β, 1), 0) as the EFC. For example, (α≤0 or β≤0)=>min(α, β, 1)≤0=>max(min(α, β, 1), 0)=0; otherwise (α≥1 and β≥1)=>min(α, β, 1)=1=>max(min(α, β, 1), 0)=1, in which case the value of CFF is depending on the successive formula.
TABLE-US-00001 TABLE 1 The essential conditions and EFC for α and β of each type of CRSs Types of essential states condition(s) EFC Reachable (α ≥ 0 and β ≥ 0) min(max(min state (α, β, 0) + 1, 0), 1) Live state (α ≥ 0 and β ≥ 0)/ (min(max(min (α = 0 (α, β, 0) + 1, 0), 1)) × and β = 0) (min(max(max (α, 0), max(β, 0)), 1)) Forbidden (α ≥ 0 and β ≥ 0) embedded in the formula of Ŗ − F Deadlock 1.(α > 0 and β > 0) 1. Dependent on the 2.the special deadlock states pattern. condition of (α 2. 1 − (min(max(max = 0 and β = 0) (α, 0), max(β, 0)), 1)) ARRS and (α > 0 and β > 0) max(min(α, β, 1), 0) ARLS
[0109] Theorem 2.1: The total number of live states of a DDk(k, α, β) is ĻGC(k, α, β)=(min(max(min(α, β, 0)+1, 0), 1))(min(max(max(α, 0), max(β, 0)), 1)) (Σ.sub.I=0 to min(k, α)C(k, i)+Σ.sub.i=0 to min(k, β)C(k, j)−1).
[0110] Theorem 2.2: The total number of reachable states of a DDk(k, α, β) is ŖGC(k, α, β)=min(max(min(α, β, 0)+1, 0), 1)(Σ.sub.j=0 to k((Σ.sub.i=0 to min(j, α-1)C(j, i))(Σ.sub.i=0 to min(k−j−1, β)C(k−j−1, i)))+(Σ.sub.i=0 to min(k, β)C(k, i))). Corollary 1: 1) The number of forbidden states in a DDk(k, α, β) is FGC(k, α, β)=min(max(min(α, β, 0)+1, 0), 1)(Σ.sub.j=0 to k((Σ.sub.j=0 to min(j, α-1)C(j, i))(Σ.sub.i=0 to min(k−j−1, β)C(k−j−1, i)))+(Σ.sub.i=0 to min(k, β)C(k, i)))−(min(max(min(α, β, 0)+1, 0), 1)) (min(max(max(α, 0), max(β, 0)), 1)) (Σ.sub.i=0 to min(k, α)C(k, i)+Σ.sub.j=0 to min(k, β)C(k, j)−1).
[0111] Theorem 2.3: The total number of deadlock states of a DDk(k, α, β) is ĎGC(k, α, β)=1−(min(max(max(α, 0), max(β, 0)), 1))+(min(α, β, 1))(k−1).
[0112] Theorem 2.4: The total number of reachable states in a DDGen-Left is ŖGOL(k, α, β, gen)=ŖGC(k, α, β)+ŖGC(k, α−1, β)+(min(α, β, 1))(Σ.sub.l=1 to gen(Σ.sub.u=gen+1 to k(Σ.sub.j=0 to min(k-u, β−1)(ŖGC(l−1, α−1, β−j−1)C(k−u, j))))).
[0113] Theorem 2.5: The total number of live states in a DDGen-Left is ĻGOL(k, α, β, gen)=ĻGC(k, α, β)+ĻGC(k, α−1, β)+(min(α, β, 1))(Σ.sub.l=1 to gen(Σ.sub.u=gen+1 to k((Σ.sub.i=0 to min(β−1, u−1)C(u−1, i))))+Σ.sub.l=1 to gen(Σ.sub.u=gen+1 to k(((Σ.sub.i=0 to min(β−1, k−u)C(k−u, i)))).
[0114] Theorem 2.6: The total number of deadlock states in a DDGen-Left is ĎGOL(k, α, β, gen)=1−(min(max(max(α, 0), max(β, 0)), 1))+(max(min(α, β, 1), 0))(gen−1)+min(max(α, 0), 1))*min(max(β, 0), 1))(Σ.sub.i=gen+1 to k−1(min(max(i−gen−α+1, 0), 1))+.sub.Σi=1 to gen(min(max(α−1, 0), 1)*min(max(β−gen+i, 0), 1)+Σ.sub.i=gen+1 to k−1(min(max(α+gen−i, 0), 1)*min(max(β, 0), 1))+(min(max(α−1, 0), 1)*min(max(β−1, 0), 1)*(Σ.sub.i=1 to gen−1(Σ.sub.j=gen+1 to k−1(Σ.sub.q=1 to min(β−1, gen−i) min(max(β−q, 0), 1)))).
[0115] The formulas are consistent with the reachability analysis using the INA (Integrated Net Analyzer) tool (1992). Extending TRM to DDGen-Left(k, α, β, gen), one can find rev(DDGen-Left(k, α, β, k−gen)=DDGen-Left(k, α, β, gen)), and there is a 1−1 and convertible mapping between the DDGen-Left(k, α, β, k−gen) and the DDGen-Right(k, β, α, gen) such that one can directly derived the CFS for a DDGen-Right by replacing the parameter list (k, α, β, gen) of a DDGen-Left by (k, β, α, k−gen).
[0116] Hence, the CFS for a DDGen-Right is shown below: [0117] ŖGOR(k, α, β, gen)=ŖGOL(k, β, α, k−gen); [0118] ĻGOR(k, α, β, gen)=ĻGOL(k, β, α, k−gen); [0119] FGOR(k, α, β, gen)=FGOL(k, β, α, k−gen); [0120] ḐGOR(k, α, β, gen)=ĎGOL(k, β, α, k−gen).
[0121] As such, the present invention completes the CFS for a Gen-One with parameters k, α, β, gen and process, where process contains Left and Right two value only.
TABLE-US-00002 If process = Left then GO(k, α, β, gen, process) = ŖGOL(k, α, β, gen);
GO(k, α, β, gen, process) =
GOL(k, α, β, gen); FGO(k, α, β, gen, process) = FGOL(k, α, β, gen); {hacek over (D)}GO(k, α, β, gen, process) = {hacek over (D)}GOL(k, α, β, gen). Else
GO(k, α, β, gen, process) = ŖGOL(k, β, α ,k-gen);
GO(k, α, β, gen, process) =
GOL(k, β, α, k-gen); FGO(k, α, β, gen, process) = FGOL(k, β, α, k-gen); {hacek over (D)}GO(k, α, β, gen, process) = {hacek over (D)}GOL(k, β, α, k-gen). End if
[0122] The application for carrying out the present invention will be described in the following paragraphs.
[0123] 1. The reachability analyzing for systems with non-sharing sub-net; Double Deficient tokens; multi-non-sharing/multi-tokens resources; and multi-processes extended from variant k-th order system without whole net structure analysis.
[0124] 1.1 Applying to the Construction of CFS for NNS System
[0125] The deficient k-th order system is the essential element of a k-th order system with a non-sharing sub-net (NNS) (as shown in
[0126] The total number of reachable states in deficient k-th order system (Def (k, q)) (Chao & Yu, 2017) is RD (k, q)=R(k)−Σ.sub.l=q+1 to k(Σ.sub.i=0 to l−q−1C(1 −1, 1 −1−i))(2.sup.k−1), where q is the number of tokens in the idle place of the left-hand-side process.
[0127] The total number of reachable states in Deficient Gen-Left k-th order system (Def-Gen-Left(k, q, gen)) (Yu, 2016 b) is RDG (k, q, gen)=RD(k, q)+RD(k, q−1)+Σ.sub.i=1 to gen(Σ.sub.j=gen+1 to kRD(i−1, q−1) (2.sup.k−j)), where gen is the location of a non-sharing resource in the Def-Gen-Left(k, q, gen).
[0128] Based on the formulas listed above, one can derive CFF of the number of reachable state for k-th order system with a NNS and a non-sharing resource in left-hand-side process, NNS-Gen-Left k-th order system (NNS-Left(k, m, gen)), as shown below.
[0129] RNNS−Gen (k, m, gen)=Σ.sub.l=0 to m((|f(l)|)RDG (k, k−1, gen)), where m is the maximum token number that can flow into NNS and the limitation of m is m<k; f(l) is a measurable state function of NNS and l is the number of tokens flowing into NNS, such that |f(l)| can map to a non-ambiguous number of different states combination under the current information of l in NNS.
[0130] According to TRM one can easily derive CFS for the rev(NNS-Left(k, m, gen)) which is the fundamental model of merging two different manufacturing processes. The topological reverse net of Def-Gen-Left(k, q, gen) is Def-Gen-Left(k, q, k−gen) and the mirroring is the net of Def-Gen-Left(k, q, k−gen) itself which is a reversible one-to-one function. Hence, one can derive CFF of reachable states for rev(NNS-Left(k, m, gen)) being
[0131] Rrev(NNS−Gen)(k, m, k−gen)=Σ.sub.l=0 to m((|f(l)|)RDG(k, k−1, k−gen)) without whole net structure analysis.
[0132] 1.2 Reachability Analysis for Double Deficient k-th Order System with One Non-Sharing Resource
[0133]
[0134] Let ŖGC(k, α, β)=min(max(min(α, β, 0)+1, 0), 1)(Σ.sub.j=0 to k((Σ.sub.i=0 to min(j, α−1)C(j, i))(Σ.sub.i=0 to min(k−j−1, β)C(k−j−1, i)))+(Σ.sub.i=0 to min(k, β)C(k, i))) be the number of reachable states of Double Deficient k-th order system with α tokens in p.sub.0; β tokens in p′.sub.0, the number of reachable states of Double Deficient k-th order system with a non-sharing resource at lon location of the left process is ŖGOL(k, α, β, lon)=ŖGC(k, α, β)+ŖGC(k, α−1, β)+(min(α, β, 1))(Σ.sub.l=1 to lon(Σ.sub.u=lon+1 to k(Σ.sub.j=0 to min(k−u, β−1)(ŖGC(l−1, α−1, β−j−1)C(k−u, j))))).
[0135] Applying TRM, one can easily derive the number of reachable states of double deficient k-th order system with a non-sharing resource at lon location of the right process is ŖGOL(k, β, α, k−lon).
[0136] 1.3 Reachability Analysis for Multi-Non-Sharing Resources Systems
[0137] For a subnet containing two non-sharing resource systems, s=(x.sub.1 . . . x.sub.i[y] . . . xj[z] . . . x.sub.k), where x.sub.m=1, 0, −1; y=0, 1; z=0, −1, with a left side non-sharing resource after i location, x.sub.i[y], and a right side one after j location, x.sub.j[z]. According to the “additional restricted reachable (resp. live) States derived from non-reachable (non-live) states of the equivalent (defined in Definition 6) caused by the non-sharing resource” (ARRS)(resp. ARLS) information of Gen-Right and Gen-Left, one can intuitively exclude the states patterns that do not belong to the ARRS pattern of s:(x.sub.1 . . . −1 x.sub.i[y] . . . 1 1 . . . x.sub.j[z] . . . x.sub.k) and (x.sub.1 . . . x.sub.i[y] . . . −1 −1 . . . x.sub.j[z] . . . 1 x.sub.k), since (−1 x.sub.i[y] . . . 1 1) is not a reachable sub-state of the Gen-Left, nor is (−1 −1 . . . x.sub.j[z] . . . 1 x.sub.k) for Gen-Right. Hence the ARRS information of Gen-One can be used for analyzing the reachability and constructing the CFF for k-th order system with multi-non-sharing resources. The effort required for the construction of CFF can be reduced by the TRM. When one construct CFF, fs(k, Li, Rj) for s, one can also derive CFF fs(k, R(k−i), L(k−j)) for a right side non-sharing resource x.sub.i[y] and a left side one x.sub.j[z] (y=0, 1; z=0 −1) just according to the TRM.
[0138] 1.4 Reachability Analysis for Multi-Tokens Resources Systems
[0139] In variant k-th order system with sharing resources containing multi-tokens, there is a similar ARRS states pattern because under the condition of multi-tokens in a sharing resource the left or right process can wait in this sharing resource rm for the other process's work flow. To construct CFS for such a net structure, after deriving CFF f(k, om, gen) of CRSs with the tokens number om of rm resource being in the left process pgen, one can immediately derive the part of the same number of tokens in the right process p′gen, f(k, om, k−gen−1) according to the TRM methodology.
[0140] 1.5 Reachability Analysis for Multi-Processes Systems
[0141]
[0142] 2. Directly Deriving the CFF for PNs Extended from Variant k-Th Order System without Whole Net Structure Analysis.
[0143] With validated CFF for k.sub.ij(j.sup.+, gen), the CFF for k.sub.ji(j.sup.−, gen) can be derived according to the mapping relationship map2(map1(k.sub.ij(j.sup.+, k−gen)))=map2(rev(k.sub.ij(j.sup.+, gen)))=k.sub.ji(j.sup.−, gen) as shown in Theorem 1.1,
[0144] 3. Realize the DTH Deadlock Avoiding Function
[0145] A simple deadlock avoiding function algorithm EnableState((x.sub.C, x.sub.N)) (Yu, 2016) is shown below, where x.sub.C is the single token distribution of the current state to be changed to the single token distribution x.sub.N of the next state.
[0146] Let Nk be a k-th order system that is the equivalent of a Variant k-th order system N, sub-state.sub.t(m, n) be a t-th reachable sub-state (x.sub.m . . . x.sub.n) so that the current state of N can be composed by (sub-state.sub.1 . . . sub-state.sub.t . . . sub-state.sub.e), where 1≤e≤int(k/2)+1, URt be or will be the only one unmarked siphon (r.sub.i-r.sub.j)-region of Nk in sub-state.sub.t where it contains a zero or null sub-state (0.sub.i+1 . . . 0.sub.j−1), and s.sub.t be the possible unmarked minimal siphon (denoted as UMS) region derived from URt (the exception condition is that the sub-state.sub.t is live or sub-state.sub.t contains an ARRS due to NSR).
[0147] The function Search(x.sub.1) returns the sub-state.sub.t containing the single state x1; [0148] MinProcess(sub-state.sub.t) returns the process with the minmal number of operation places containing a token; [0149] Deallocate(sub-state.sub.t, DTH) will deallocate all of DTH in sub-state.sub.t; [0150] Split(sub-state.sub.t) will Deallocate(sub-state.sub.t, DTH) and split the sub-state.sub.t into sub-state.sub.t− and sub-state.sub.t+ at s.sub.t while s.sub.t is a non-reachable marking in Nk; [0151] Merge(sub-state.sub.t(m.sub.t, n.sub.t) sub-state.sub.t+1(m.sub.t+1, n.sub.t+1)) generates the new sub-state′.sub.t(m.sub.t, n.sub.t+1); [0152] AllocateDTH(sub-state.sub.t, P.sub.i) will allocate a DTH according to max(DDGen-Left(k, α, β, gen) or DDGen-Right(k, α, β, gen)) of URt in process Pi where gen is the possible location of DTH; [0153] Protect(s.sub.t) (resp. Unprotect(s.sub.t)) protects (resp. unprotects) s.sub.t from the traps holding the token due to the work flow of other siphons; [0154] Place(x.sub.C) returns the place containing the token in a single state x.sub.C; isProtected(s.sub.t) returns the Boolean value as true when s.sub.t is protected; and [0155] ProcessOf(Place(x.sub.C)) will return the process P.sub.i of Place(x.sub.C).
TABLE-US-00003 EnableState((x.sub.C, x.sub.N)) { 1 sub-state.sub.t=Search(x.sub.C); sub-state't=Search(x.sub.N); 2 if (sub-state.sub.t≠sub-state'.sub.t) then {Merge(sub-state.sub.t, sub-state'.sub.t); } 3 if (x.sub.C is not in UR.sub.t) then {return SUCC;} 4 if (UR.sub.t contains no NSR or DTH) then {AllocateDTH(sub-state.sub.t, MinProcess(sub-state.sub.t));} 5 if (isProtected(s.sub.t) and Place(x.sub.C) in trap of s.sub.t) {return SUCC} 6 if (isProtected(s.sub.t) and Place(x.sub.C) in H(DTH) and reachable to x.sub.C) { if (no other H(DTH) contains token in UR.sub.t) then { Unprotected(s.sub.t); Split(sub-state.sub.t); Merge(sub-state.sub.t−1, sub-state.sub.t); Merge(sub-state.sub.t+,sub-state.sub.t+1); } return SUCC; } 7 if (Place(x.sub.N) in H(DTH) and UR.sub.t is UMS and not isProtected(s.sub.t) ) {Protect(s.sub.t); return WAITING; } 8 if (Place(x.sub.N) not in H(DTH) and UR.sub.t is UMS and not isProtected(s.sub.t)) { Protect(s.sub.t); Deallocate(s.sub.t, DTH); Allocate_DTH(s.sub.t, ProcessOf(x.sub.C)); return WAITING; } 9 if (Place(x.sub.C) not in s.sub.t and isProtected(s.sub.t)) {return HOLDING; } } When the return value is SUCC then the state can progress to x.sub.N from xC; WAITING, waiting in DTH of xC ; and HOLDING waiting in xC until Unprotected(st).
[0156] The additional advantage of DTH deadlock avoiding function is that one can dynamically encapsulate such sub-state as an independent module of whole system because no extra allocated sharing resource is needed for deadlock policy.
[0157] Conclusively, CFF for Petri nets realize the possibility of providing real-time reachability information from EXPSPACE-hard problem. Some concepts of large system control applications based on current state are proposed. However the traditional whole-net structure analyzing method limits presently the CFF only the variant k-th order systems be derived such that limits new applications proposed and the applications be applied to more complicated modeling Petri nets. To solve the problem, the present invention reports a new efficient knowledge-based methodology “topological reverse mirroring” (TRM) to enhance the theoretical framework for constructing CFS for PNs without complicated whole-net siphon analysis, and the CFF for Variant Double Deficient k-th order system as the basic system to extend analyzing reachability and deriving the CFF for more complicated Petri Nets.
[0158] An embodiment is given in the following to better understand the present invention.
[0159] Suppose a flexible manufacturing sub-system containing two manufacturing processes (N.sub.1 and N.sub.2 in
[0160] In case of no additional sharing resource allowed due to limited space and only the temporary storage of each place (p.sub.i and p′.sub.i) of both processes can avoid deadlock, one can apply deadlock ratio of current state as the indicator to launch a deadlock avoidance policy. Yu (2016a) proposed a deadlock thread-holder (DTH, a dummy non-sharing waiting resource) avoidance deadlock policy based on which location DTH allocated will increase maximum reachability. Here, DTH is the temporary storage of a place for waiting the other working process. Furthermore one can encapsulate such sub-system as an independent module of whole system because no extra allocated sharing resource is needed for deadlock policy.
[0161] Extending the sub-system containing two sub-nets in both processes as shown
[0162] When k is very large, based on CFF for PN, such as ŖGOL(k, α, β, lon) formula, the values of deadlock ratio, the location of DTH and the DRO of current state can be easily estimated real-time to realize the total solution for manufacturing mentioned above. However, due to NP-complete problem, presently the values cannot be derived real-time based on traditional reachability analysis method.
[0163] CFF for Petri nets realizes the possibility of providing real-time reachability information from EXPSPACE-hard problem. Some concepts of large system control applications based on current state are proposed. However the traditional whole-net structure analyzing method limits presently the CFF only the variant k-th order systems be derived such that limits new applications proposed and the applications be applied to more complicated modeling Petri nets.
[0164] To solve the problem, the present invention reports a new efficient knowledge-based methodology “topological reverse mirroring” (TRM) to enhance the theoretical framework for constructing CFS for PNs without complicated whole-net siphon analysis, and the CFF for Variant Double Deficient k-th order system as the basic system to extend analyzing reachability and deriving the CFF for more complicated Petri Nets.
[0165] Unless otherwise defined, all terms (including technical and scientific terms) used herein have the same meaning as commonly understood by one of ordinary skill in the art to which this disclosure belongs. It will be further understood that terms; such as those defined in commonly used dictionaries, should be interpreted as having a meaning that is consistent with their meaning in the context of the relevant art and the present disclosure, and will not be interpreted in an idealized or overly formal sense unless expressly so defined herein.