ABSTRACT
Logic Petri nets (LPN) can describe and analyze batch processing function and passing value indeterminacy in cooperative systems and its practical applications are shown with some nontrivial examples. This study focuses on the analysis of the modeling power of LPNs and the equivalency between LPNs and Petri nets with inhibitor arcs (IPN). The equivalency is proved formally and a constructing algorithm of equivalent IPNs from LPNs is proposed based on the disjunctive normal forms of logic input/output expressions. Moreover, the size of an LPN model is smaller than that of the equivalent IPN model.
PDF Abstract XML References Citation
How to cite this article
DOI: 10.3923/itj.2009.95.100
URL: https://scialert.net/abstract/?doi=itj.2009.95.100
INTRODUCTION
Petri nets (PNs) (Murata, 1989) are a well-founded procedure modeling technique and have been used to model and analyze all kinds of procedures with applications ranging from protocols, hardware and embedded systems to flexible manufacturing systems and business processes. PNs are a graphical language. As a result, PNs are intuitive and easy to learn. Also, the semantics of PNs and several enhancements (color, time, hierarchy) have been defined formally (Wang et al., 2000).
PNs provide a solid framework for modeling and analyzing workflow processes (Vander Aalst, 2000; Derks et al., 2001). Workflow management is becoming a mature technology that can be applied within organizations and across organizational boundaries. It is very important to use an established framework for modeling and analyzing workflow processes (Vander Aalst, 1998), since processes are a main factor in workflow management systems. However, the existing Petri-net-based approaches are mainly used to investigate functional and secure properties of workflows. With rapid increase in the number of workflow processes where multiple organizations are involved, a batch processing function is urgently needed in cooperative systems, i.e., a batch data of the same type from different organizations need to be processed before a deadline. Also, the arrival times of these data are indeterminable, i.e., some data arrive before a given deadline, but others may not arrive. One usually requires that, to enhance the efficiency of workflows, all arrived data be processed at a same time slice, while late received data after the deadline be processed in the next workflow cycle. This situation is called passing value indeterminacy (Yuyue and Changium, 2002; Du et al., 2007). Therefore, a good formalism of cooperative systems should be able to model and analyze both the batch processing function and the passing value indeterminacy.
However, it is very difficult to apply Petri nets to the description of the batch processing function and the indeterminacy (Hao and Wang, 2003). Because the processing transition doesnt been fired until all its input places contain tokens strictly. However, in that situation the transition needs a flexible trigger condition, i.e., some of its input places containing tokens are also able to fire the transition. Petri nets with weights of flow arcs may offer the batch processing function, but cannot easily represent the data arrival indeterminacy as the weights are not less than 1. Petri nets with inhibitor arcs (IPN) have the modeling power of a Turing machine (Suzuki and Lu, 1989). Although IPNs may model the batch processing function and the data arrival indeterminacy, the models of systems with these properties are very complex. To tackle the above problems, therefore, a new formal method- Logic Petri Net (LPN), an extend Petri net with logic transitions, is proposed and applied efficiently to the modeling and analysis of stock trading systems and electronic commerce systems (Yuyue and Changium, 2002, 2003; Du et al., 2007). It is illustrated sufficiently that LPNs can model explicitly and represent compactly the batch processing function and the data arrival indeterminacy and mitigate the state explosion problem to some extent.
LPNs sort the indeterminacy from interactive across organizational boundaries into the input and output indeterminacy and describe them respectively by logic input and output transitions. Firing them is subject to the constraints from logic expressions. In fact, the indeterminacy is implied by the logic expressions attached to logic transitions. Doubtless this will enhance the expression ability of PNs and cater to more application needs. Moreover, LPNs are able to reduce the size of system models. The objective of this study is to investigate the equivalence between LPNs and IPNs and to propose a constructing algorithm of an equivalent IPN from an LPN.
LOGIC PETRI NETS
To apply LPNs to the description of cooperative systems with the batch processing function and the passing value indeterminacy, two types of places in LPNs, control and data places are introduced. Control places are used to store control tokens within an organization, while data places to store data tokens forwarded from other organizations. Thereby, data places are also called interface places. Also, there are two kinds of logic transitions in LPNs, logic input and output transitions. Logic transitions are restricted by logic expressions that can efficiently describe the batch processing function and the passing value indeterminacy, such as the indeterminacy of arrival orders or actual trading quantities in electronic commerce. The transitions cannot be usually expressed in high-level PNs (Atluri and Huang, 2000), since the type of the data passed or generated is explicitly fixed by the variable symbol sums.
Assume that this research is based on the elementary net system, i.e., the capacity of each place is limited to 1. A brief introduction to PNs and IPNs is reviewed as follows.
Definition 1: PN = (P, T, F, M0) is a PN if and only if
• | P is a finite nonempty set of places; |
• | T is a finite nonempty set of transitions; |
• | P∩T = ø; |
• | F⊆(TxP) ∪ (PxT) is a set of arcs, i.e. flow relations; |
• | M0: P→{0, 1} is the initial marking. |
In the graphic representation, places are drawn as circles or ellipses, transitions as bars. The flow relations between the nodes (i.e., places and transitions) are represented as directed arcs and the tokens of the marking as dots inside places. This study uses the following symbols for the pre-set and post-set of a node xεP∪T: •x = {y|(y, x)εF}, x• = {y|(x, y)εF}, respectively. R(M0) represents a set of all markings reachable from M0. A transition t is enabled if each pεCt contains one token at the current marking Mε R(M0). If t is enabled, it can fire and a new marking M is generated from the current marking M, represented by M[t>M, where when pεCt-t•, M(p) = M(p)-1; when pεt•-•t, M(p) = M(p)+1; otherwise, M(p) = M(p).
Definition 2: IPN = (P, T, F, I, M0) is a PN with inhibitor arcs if and only if
• | P is the set of places; |
• | T is the set of transitions; |
• | F⊆(PxT)∪(TxP) is a set of the edges (flow relations); |
• | I⊂PxT is the inhibitor arc set, I∩F = φ and (p, t)εI is represented as a non-directed arc with a small circle at t side; |
• | M0: P→ {0,1} is the initial marking of IPN; |
• | Transition firing rules: ∀tεT, t is enabled if ∀pεP: (p, t)εF •t and (p, t)εF: M(p) = M(p)-1; •: M(p) = M(p)+1; otherwise: M(p) = M(p). |
In the following, LPNs are first defined formally. Then an example is given to show expressive ability of logic transitions.
Definition 3: LPN = (P, T, F, I, O, M0) is a logic PN if and only if
• | (P, T, F, M0) is a PN; |
• | T includes three subsets of transitions, i.e., T = TG∪TI∪TO, ∀tεTI∪TO: •t∩t• = φ where |
• | TG denotes a set of traditional transitions; |
• | TI denotes a set of logic input transitions; |
• | TO denotes a set of logic output transitions; |
• | I is a mapping from a logic input transition to a logic input expression, i.e., I, I(t) = fI(t); |
• | O is a mapping from a logic output transition to a logic output expression, i.e., O, O(t) = fO(t); |
• | Transition firing rules: |
• | ∀tεTG, the firing rules of t are the same as in PNs; |
• | ∀tεTI, t is enabled only if fI(t)|M = •T•. M [t> M,∀pε•t, if M(p) = 1, then M(p) = M(p)-1; •: M(p) = M(p)+1; ∀p∉•t∪t•: M(p) = M(p). |
• | ∀tεTO,, t is enabled only if ∀pεCt: M(p) = 1. Firing t will generate a new marking M, notation M[t>M and ∃S⊆t•, S must satisfy fO(t)|M = •T•; ∀pεS: M(p) = M(p)+1;∀pε•t: M(p) = M(p)-1; ∀p∉t•∪•t or ∀pεt•-S: M(p) = M(p). |
Fig.1: | Representation of logic input\output transitions in LPNs, (a) in put and (b) out put |
Usually such S is not unique, but only one case is selected and the selection is random. The randomness of S can describe the output indeterminacy of cooperative systems.
In Fig. 1, t1/t2 is a logic input/output transition and it is restrained by a logic input/output expression fI (t1)/fO (t2). p1 is the control place; p2 and p3 are the data places. According to logic input expression fI(t1) = p1Λ (p2ν p3), in Fig. 1a t1 is enabled if place p1 has one token and one or each of places p2 and p3 includes one token. In Fig. 1b, p3 is the control place; p1 and p2 are the data places. t2 is enabled once p includes one token and firing t2 will generate one token in place p3 and one or each of places p1 and p2 respectively based on logic output expression fO (t2) = (p1ν p2)Λp3.
In the application situation, when the control place in Fig. 1a contains a token, starting the business processing (transition t1) requires at least one of the data places whose tokens come from other organizations contains tokens, instead of each of the data places must contain tokens rigidly in general Petri nets. The situation in Fig. 1b is similar to that in Fig. 1a. So, LPNs can describe clearly the batch processing function and the indeterminacy of data arrival with the corresponding logic expressions. In fact, the logic expressions can enhance the representation ability of LPNs. With respect to LPN expressivity, this study will prove that there is the equivalence between LPNs and IPNs.
EQUIVALENCE OF LPNS AND IPNS
In order to prove the equivalence between LPNs and IPNs, their isomorphism and equivalent definitions are introduced first.
Definition 4 (Isomorphism): Let Σ1 = (P, T, F, I, O, M0) be an LPN and Σ2 = (P, T, F, I, M0) an IPN. RG (Σi) is the reachable marking graph of Σi and Ri is the vertex set of RG (Σi), i = 1, 2. If there exists a bijective function f : R1→R2, such that ∀M1, M2ε R1 , tεT, M1[t> M2, → ∃t0T, f(M1)[ t >f(M2). Then RG(Σ1) and RG(Σ2) are isomorphic.
Definition 5 (Equivalence): Let Σ1 = (P, T, F, I, O, M0) be an LPN and Σ2 = (P, T, F, I, M0) an IPN. Σ1 and Σ2 are equivalent if and only if RG(Σ1) and RG (Σ2) are isomorphic.
Theorem 1: For any LPN, there exists an equivalent IPN.
Proof: Given an LPN Σ1 = (P, T, F, I, O, M0) and IPN Σ2 = (P, T, F, I, M0) is equivalent to Σ1.
For ∀tεT, we transform each transition of Σ1 into a corresponding transition or a subnet of Σ2 on the basis of the following three cases.
tεTG=T-TI ∪TO: Let tεT; ∀pεP, if (p, t) εF, then (p, t) ε F; and if (t, p)εF, then (t, p)ε F.
tεTI : Let •t = {pi1, pi2, , pik}, fI(t) is its logic input expression. t is enabled once the value of fI(t) is true on the basis of the token change of places pi1-pik. In fact, there may be several situations of places pi1-pik where fI(t) is true. However, fI(t) can be transformed into a disjunctive normal form and the disjunctive normal form is unique, i.e., each disjunctive clause in the disjunct is a conjunct which consists of all positive or negative places pi1-pik and each conjunct corresponds to a situation of places pi1-pik where fI(t) is true.
Thus, the disjunctive normal form of fI(t) can be represented as follows:
where, τlj = pij or ¬ pij. fI(t) is true if and only if one of m disjunctive clauses is satisfied. Any two disjunctive clauses are mutually exclusive. In the following, m transitions in Σ2 corresponding to m kinds of the true value states are constructed in the disjunctive normal form respectively. That is, a logic input transition t with logic expression fI(t) in Σ1 can be represented equivalently by a subnet including m transitions in Σ2 and m transitions correspond to m disjunctive clauses in the disjunctive normal form of fI(t) respectively. The subnet is constructed in detail as follows:
For any disjunctive clause lε{1, 2, , m}
Assume that the disjunctive clause corresponds to a transition tl in Σ2, i.e., tl0T. Then the arc set of this subnet is defined. , then (pij, tl)εF; if τlj = ¬ pij, then (pij, tl)εI.
If ∀pεt•, then (tl, p)εF. Therefore, firing a logic input transition of Σ1 corresponds to firing a transition of Σ2, i.e., if a logic input transition is enabled in Σ1, then there must be an enabled transition in the corresponding subnet of Σ2 and it is unique.
tεTO: Let t• = {pi1, pi2, , pik}, fO(t) is its logic output expression. t is enabled once its input place p includes a token. Firing t will generate a token in all or some output places and must assure that fO(t) is true at the next state of places pi1-pik..
Similarly, fO(t) can be transformed into a unique disjunctive normal form. Without loss of generality, assume that the disjunctive normal form consists of r disjunctive clauses. Thus,
where τlj = pij or ¬ pij. fO(t) decides all possible states of places pi1-pik and each disjunctive clause corresponds to a possible state in which fO(t) is true. Thus r transitions in Σ2 corresponding to r kinds of the possible states are constructed in the disjunctive normal form respectively. That is, a logic output transition t with logic expression fO(t) in Σ1 can be represented equivalently by a subnet including r transitions in Σ2 and r transitions correspond to r disjunctive clauses in the disjunctive normal form of fO(t) respectively. The subnet is built as follows.
For any disjunctive clause,
lε{1, 2, , r}. Assume that the disjunctive clause corresponds to a transition tl in Σ2, i.e., tl0T. Then the arc set of this subnet is defined., then (tl, pij)εF; if τlj = ¬ pij, then (tl, pij)∉F. ∀pε •t, then (p, tl)εF. Therefore, firing a logic output transition of Σ1 corresponds to the occurrence of a transition in Σ2, i.e., firing a logic output transition t is functionally equivalent to the occurrence of one of transitions t1- tr.
Therefore, the place set P in Σ1 is the same as that in Σ2. But T≠ T, F≠ F and |T|#*T*, |F|#*F*, where |T |denotes the size of set T. Since Σ1 and Σ2 have the same initial marking M0, the equivalence between Σ1 and Σ2 are now proved based on the reachable marking graph.
In Σ1, for ∀M1, M2εR(Σ1), tεT and M1[t> M2. Then there is a mapping function f: R(Σ1)→R(Σ2) based on the construction of Σ2, such that f(M1) = M1 and f(M2) = M2 and in Σ2, if tεTG, then ∃t0T: t = t and f(M1) [t >f(M2); if tεTI ∪TO, then ∃tl0T: tl = t and f(M1) [tl>f(M2). Accordingly, f is an identity mapping and satisfies injective and surjection requirements at MεR(M0). That means that Σ1 and Σ2 have the same behavior characteristics. Moreover, the structure of Σ2 is unique since the disjunctive normal form is only one. So f is a bijective function and RG(Σ1) and RG(Σ2) are isomorphic.
Consequently, Σ1 and Σ2 are equivalent based on definition 5. The conclusion holds.
From Theorem 1 and the construction of Σ2, the following constructing algorithm of an equivalent IPN from an LPN can be obtained.
Algorithm 1 (Constructing Algorithm): Transforming an LPN into an equivalent IPN
Input: an LPN Σ1 = (P, T, F, I, O, M0)
Output: an equivalent IPN Σ2=(P, T, F, I, M0)
(1) | IPN.P = LPN.P; |
(2) | For each transition t in LPN.TG |
(3) | IPN.T = IPN.T ∪{t}; |
(4) | For each p in •t |
(5) | IPN.F = IPN.F ∪{(p, t)}; |
(6) | End for |
(7) | For each p in t• |
(8) | IPN.F = IPN.F ∪{(t, p)}; |
(9) | End for |
(10) | End for |
(11) | For each t in LPN.TI |
(12) | For each disjunctive clause of fI(t) |
(13) | IPN.T = IPN.T ∪{ tl}; |
(14) | For each pij in •t |
(15) | If τlj = pij then IPN.F = IPN.F ∪{( pij, tl)}; |
(16) | else IPN.I = IPN.I ∪{( pij, tl)}; |
(17) | End for |
(18) | For each p in t• |
(19) | IPN.F = IPN.F ∪{( tl, p)}; |
(20) | End for |
(21) | End for |
(22) | End for |
(23) | For each t in LPN.TO |
(24) | For each disjunctive clause of fO(t) |
(25) | IPN.T = IPN.T ∪{ tl}; |
(26) | For each pij in t• |
(27) | If τlj = pij then IPN.F = IPN.F ∪{( tl, pij)}; |
(28) | End for |
(29) | For each p in •t |
(30) | IPN.F = IPN.F ∪{(p, tl)}; |
(31) | End for |
(32) | End for |
(33) | End for |
Fig. 2: | Equivalent IPN subnet of a logical input transition, (a) logical Input transition and (b) equivalent IPN subnet |
Fig. 3: | Equivalent IPN subnet of a logical output transition (a) logical output transition and (b) equivalent IPN subnet |
For any LPN, therefore, its equivalent IPN can be easily built based on theorem 1 and algorithm 1. In the following, the transformation processes from a logic transition in LPN to an equivalent subnet in IPN are illustrated with two examples (Fig. 2, 3).
Example 1: Transforming a logic input transition in LPNs to an equivalent subnet in IPNs. In Fig. 2a, t1 is a logic input transition in an LPN and fI(t1) = p1Λ(p2νp3) is its logic input expression. t1• = {p} and •t1 = {p1, p2, p3}. fI(t1) is transformed into a disjunctive normal form as follows.
fI(t1) | = | p1Λ(p2νp3) |
 | = | (p1Λp2)ν(p1Λp3) |
 | = | ((p1Λp2)Λ(p3ν5p3))ν((p1Λp3)Λ(p2ν5p2)) |
 | = | (p1Λp2Λ5p3)ν(p1Λ5p2Λp3)ν(p1Λp2Λp3) |
By means of the proof process of theorem 1 and algorithm 1, logic input transition t1 can be transformed equivalently into the subnet of an IPN in Fig. 2b. From the proof process of theorem 1, three disjunctive clauses of fI(t1) correspond with three transitions in the IPN subnet, i.e., (p1Λp2Λ5p3)→t11, (p1Λ5p2Λp3) →t12 and (p1Λp2Λp3) →t13. That is, the disjunctive normal form of fI(t1) decides fully the structure of the corresponding IPN subnet. (p3, t11) and (p2, t12) are two inhibitor arcs. The place sets in Fig. 2a and Fig. 2b are the same, i.e., •t1∪t1• = •t11∪t11•∪ •t12∪ t12• ∪ •t13∪t13• = {p1, p2, p3, p}.
Example 2: Transforming a logic output transition in LPNs to an equivalent subnet in IPNs. In Fig. 3a, t2 is a logic output transition in an LPN and fO(t2) = (p1νp2)Λp3 is its logic output expression. t2• = {p1, p2, p3} and •t2 = {p}. The disjunctive normal form of fO(t2) is deduced as follows.
fO(t2) | = | (p1νp2)Λp3 |
 | = | (p1Λp3)ν(p2Λp3) |
 | = | ((p1Λp3) Λ(p2ν5p2))ν((p2Λp3)Λ(p1ν5p1)) |
 | = | (p1Λ5p2Λp3)ν(¬ p1Λp2Λp3)ν(p1Λp2Λp3) |
Similarly, Fig. 3b shows the equivalent IPN subnet of t2. By the constructing method of IPNs, three disjunctive clauses of fO(t2) correspond with three transitions in the IPN subnet. Therefore, the disjunctive normal form of fO(t2) decides fully the structure of the corresponding IPN subnet.
From the examples, it is a fact that the size of an IPN model can be reduced in its equivalent LPN model, since many transitions are capsulized into an equivalent logic transition. Their modeling power and behaviors are same, because IPNs and LPNs have the same reachable marking graph in essence and IPNs and LPNs are isomorphic.
CONCLUSION
With the rapid progress of cooperative and network extent of interorganizational workflows, batch processing function and passing value indeterminacy of workflow processes need often to be considered in the design of workflow systems. Moreover, formal modeling and analysis technologies should have the modeling ability of these functions. To deal with the problems, a new extension of PNs, i.e., LPNs, is proposed in (Yuyue and Changium, 2002; Du et al., 2007) and its practical application is illustrated with some nontrivial examples. This study focuses on the analysis of the modeling power of LPNs and the equivalency between LPNs and IPNs. The equivalency is proved formally and a constructing algorithm of equivalent IPNs from LPNs is proposed based on the disjunctive normal forms of logic input/output expressions. Moreover, the size of LPN models is smaller than that of the equivalent IPN models.
Further study will be the investigation of fundamental properties of LPNs, such as liveness, state equivalency and reachability. Moreover, the analysis technologies of LPNs will be studied and its developmental tool is considered and designed.
ACKNOWLEDGMENTS
This study was supported in part by the National Natural Science Foundation of China under Grant 60773034 the Taishan Scholar Construction
Project of Shandong Province, China; the National Basic Research Program of China (973 Program) under Grants 2007CB316502 and 2004CB318001-03; and the Open Project of the State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences under Grant SYSKF0804.
REFERENCES
- Van der Aalst, W.M.P., 1998. The application of Petri nets to workflow management. J. Circ. Syst. Comput., 8: 21-66.
CrossRefDirect Link - Van der Aalst, W.M.P., 2000. Loosely coupled interorganizational workflows: Modeling and analyzing workflows crossing organizational boundaries. Inform. Manage., 37: 67-75.
CrossRefDirect Link - Du, Y.Y., C.J. Jiang and M.C. Zhou, 2007. Modeling and analysis of real-time cooperative systems using petri nets. IEEE Trans. Syst. Man Cybern. Part A: Part A: Syst. Hum., 37: 643-654.
CrossRefDirect Link - Du, Y.Y. and C.J. Jiang, 2003. Towards a workflow model of real-time cooperative systems. Proceedings of the 5th International Conference on Formal Engineering Methods, November 5-7, 2003, Singapore, pp: 452-470.
Direct Link - Murata, T., 1989. Petri nets: Properties, analysis and applications. Proc. IEEE., 77: 541-580.
CrossRefDirect Link - Wang, J.C., Y. Deng and G. Xu, 2000. Reachability analysis of real-time systems using time Petri nets. IEEE Trans. Syst. Man Cybernet B Cybernet, 30: 725-736.
CrossRefDirect Link - Du, Y.Y. and C.J. Jiang, 2002. Formal representation and analysis of batch stock trading systems by logical Petri net workflows. Proceedings of the 4th International Conference on Formal Engineering Methods, October 21-25, 2002, Shanghai, China, pp: 221-225.
CrossRef