Subscribe Now Subscribe Today
Abstract
Fulltext PDF
References
Research Article
 

Transition Firing Rules of Logic Petri Nets



Yu Yue Du, Jing Wang and Yong Feng Zhang
 
ABSTRACT

Logical Petri nets (LPNs) can well describe and analyze batch processing functions and passing value indeterminacy in cooperative systems. A new definition of the LPNs is proposed based on our initial work in this study. The standard form of logic expressions can be obtained and the logic input/output enabling vector set is defined. How to determine the corresponding relationships between logic input and output expressions is solved. In order to analyze their properties, a vector matching method is given and a therom has been proved. Finally, the feasibility of the proposed method is illustrated by an example.

Services
Related Articles in ASCI
Similar Articles in this Journal
Search in Google Scholar
View Citation
Report Citation

 
  How to cite this article:

Yu Yue Du, Jing Wang and Yong Feng Zhang, 2014. Transition Firing Rules of Logic Petri Nets. Journal of Software Engineering, 8: 23-31.

DOI: 10.3923/jse.2014.23.31

URL: https://scialert.net/abstract/?doi=jse.2014.23.31
 
Received: November 11, 2013; Accepted: January 15, 2014; Published: March 08, 2014

INTRODUCTION

Petri nets (PNs) (Aziz et al., 2013) are the mathematics representation of a parallel discrete system. PNs have a rigid mathematical definition, with a well-developed mathematical theory for process analysis. They are suitable for describing the concurrent asynchronous of computer system models. With the continuous improvement of PN theory and the increasing popularity of its application, some of their extensions have been defined, such as fuzzy (Bayati and Dideban, 2012), colored (Barzegar et al., 2011) and stochastic (Marin et al., 2012) PNs.

Logic Petri nets (LPNs) (Du and Jiang 2002) are the abstract and extension of inhibitor arcs PNs (IPNs) and high-level PNs. The inputs and outputs of a system can be described by logic transitions in LPNs, respectively. The transitions restricted by logic input and output expressions are called logic transitions. In our initial work, LPNs have been applied efficiently to the modeling and analysis of trading systems (Du and Jiang, 2002), cooperative systems (Du et al., 2009) and electronic commerce (Du and Jiang, 2008). Some weaknesses are found in the analysis of LPNs models. In this study, a new definition of LPNs are proposed. The indeterminate data transmission caused by logic output transitions is solved by introducing the matching expressions. The standard form of logic expressions are defined and some indeterminate minterms of the logic expression are deleted.

BASIC DEFINITIONS

Three basic definitions are reviewed in this section before LPNs are introduced.

Definition 1: N = (P, T, F) is a net, where:

P is a finite set of places
T is a finite set of transitions with P∪T≠ø, P∩T=ø
F⊆(PxT)∪(TxP) is a set of arcs
dom(F)∪cod(F) = P∪T where:

dom(F) = {x∈P∪T | ∃y∈P∪T: (x, y)∈F}

cod(F) = {x∈P∪T | ∃y∈P∪T: (y, x)∈F}

Definition 2: x∈P∪T is called a node in N:

x = {y |(y, x)∈F} is called a pre-set of x

x = {y |(x, y)∈F} is called a post-set of x

If X∈P∪T, its pre-set and post-set are as follows:

X = ∪x∈Xx

X = ∪x∈Xx

Definition 3: PN = (P, T, F, M0) is a marked PN, where:

N = (P, T, F) is a net
M:P→ is a marking function, where M0 is the initial marking and = {1, 2,…}
Transition firing rules:
  t is enabled at M if ∀p∈t: M(p) = 1, represented by M[t>
  If t is enabled, it can fire and a new marking M' is generated from M, represented by M[t >M', where:

Based on the traditional definition PN, the LPN is put forward.

Definition 4: Let LN = (P, T, F, I, O). LPN = (LN, M) is a logic Petri net where:

P is a finite set of places
T = TD∪TI ∪TO is a finite set of transitions, P∪T≠ø, P∩T = ø, ∀t∈TI∪TO: t∩t = ø, where:
  TD denotes a set of traditional transitions
  TI denotes a set of logic input transitions, where ∀t∈TI, the input places of t are restricted by a logic input expression fI(t) and
  TO denotes a set of logic output transitions, where ∀t∈TO, the output places of t are restricted by a logic output expression fO(t)
F⊆(P xT)∪(T xP) is a finite set of directed arcs
I is a mapping from a logic input transition to a logic input expression, i.e.,:

∀t ∈TI, I(t) = fI(t) = A1∨A2∨…∨Au

O is a mapping from a logic output transition to a logic input expression, i.e.,:

∀t ∈TO, O(t) = fO(t) = B1∨B2∨…∨Bv

M: P→{0,1} is a marking function, where ∀p∈P, M(p) is the number of tokens in p
Transition firing rules:
  ∀t∈TD, the firing rules of t are the same as in PNs
  ∀t∈TI, t is enabled only if ∃Ai, make fI(t)|M = T, M[t>M', where ∀p∈t and p∈Ai, M'(p) = M(p)-1; ∀p∈t, M'(p) = M(p)+1; ∀p∉t∪t, M'(p) = M(p);and ∀p∈t and p∉Ai, M'(p) = M(p) and
  ∀t∈TO, t is enabled only if ∀p∈t : M(p) = 1. M[t>M', where ∀p∈t M'(p) = M(p)-1; ∀p∉t∪t: M'(p) = M(p); ∀p∈t and ∀p∈Bi should satisfy fO(t)|M' = T and ∀p∈t and p∉Bi, M'(p) = M(p)

LPNs are the abstract and extension of inhibitor arcs PNs and high-level PNs. A logic input/output transition is restricted by the logic input/output expression fI(t)/fO(t). All logic input/output transitions are called logic transitions. The logic expressions can describe the indeterminacy of values in input and output places. Ai and Bi represent input and output ways of logic transitions, respectively. They are not the disjunctive normal of fI(t)/fO(t), but the elements of Ai/Bi are connected by the logic symbol “∧”.

Figure 1 shows a simple LPN model. t2 is a traditional transition and t1 and t3 are logic transitions restricted by the fI/fO, respectively, where fI = (p1∧p2)∨(p1∧p2∧p3) and fO = (p7∧p8)∨(p7∧p8∧p9). Each place of a logical expression has a logic value at marking M in an LPN and by substituting the values of all places into the logic expression, the expression corresponds to a logical value. In the LPN model of Fig. 1, M=(1, 1, 0, 1, 0, 0, 0, 0, 0)T, I = {p1, p2, p3}, having p1|M = T, p2|M = T, p3|M = F and fI|M = (TvCT)∨(TvCTvCF) = TwCF = T.

Fig. 1: An LPN model

FIRING RULES OF LPN TRANSITIONS

From Definition 4, a logic transition is restricted by the logic expression f(t), next, the standard form of f(t) is putword.

Definition 5: Suppose that a logic input/output transition t is restricted by fI(t)/fO(t) and the standard form is as follow:

For a logic input transition t, the standard form of fI(t) = A1∨A2∨…∨Am can be obtained by:

(1)

For a logic input transition t, the standard form of fO(t) = B1∨B2∨…∨Bn can be obtained by:

(2)

Ai and Bi are called the standard minterms.

Example 1: In Fig. 1, transitions t1 and t2 are restricted by fI/fO, respectively, where fI = (p1∧p2)∨(p1∧p2∧p3) and fO = (p7∧p8)∨(p7∧p8∧p9). From Definition 5, the standard form of fI is fI = (p1∧p2∧5p3)∨(p1∧p2∧p3) and the standard form of fO is fO = (p7∧p8∧5p9)∨(p7∧p8∧p9).

A standard form of an expression consists of several standard minterms and each minterm can be represented by a vector. A standard minterm represented by a vector in this study and a standard form of an expression is described by a vector set. A logic input/output transition corresponds to an enabling vector set and a traditional transition corresponds a vector. Next, the enabling vectors are putford.

Definition 6: Let LPN = (LN, M) be a logic Petri net, where P = {p1, p2,…, pm} and T = {t1, t2,…, tn}:

For t∈TI, the standard form of fI(t) has a minterm Ai and Ai is a logic expression made by t. Vi = (vi1, vi2,…, vim)T is called the enabling vector of t, where:

(3)

For t∈TO, the standard form of fO(t) has a minterm Bi and Bi is a logic expression made by t. Vi = (vi1, vi2,…, vim)T is called the enabling vector of t, where:

(4)

For t∈TD, Vi = (vi1, vi2,…, vim)T is called the enabling vector of t, where:

(5)

In Eq. 3, 4 and 5, j belongs to the set {1, 2,…, m}. Suppose that the standard form of fI(t) consists of u minterms, from Eq. 3, the corresponding vector sets are Vii,1, Vii,2,..., VIi,u-1 and VIi,u and Vii = {VIi,1, VIi,2,…, VIiB,u} is the logic input enabling vector set of t. VI is the logic input enabling set of the LPN and has VIi ∈VI. Likewise, suppose that the standard normal form of fO(t) consists of v minterms, from Eq. 4, the corresponding minterm vector sets are Voi,1, Voi,2,…, Voi,v and VOi = {Voi,1B, VOi,2,…, VOi,v} is the logic input enabling vector set of t. VO is the logic output enabling set of the LPN and has VOi ∈VO. The common enabling set V is composed by all enabling vectors of the traditional transitions, i.e., Vi ∈V.

The matching rule among vectors is proposed in the next.

Definition 7: Suppose that m∈+, X = (x1, x2,…, xm)T is a 0-1vector and Y = (y1, y2,…, ym)T, where ∀i∈m and m = {1, 2,…, m}, yi ∈{0, 1, *}. X matches Y donated by Y≅X, if:

(6)

else Y≠X.

Example 2: Let X = (1, 0, 1, 0, 1)T, Y = (1, 0, 1, *, *)T and Z = (1, 0, 0, *, *)T. By Eq. 4, X ≅Y and X≠Z.

Theorem 1: Let LPN = (LN, M) be a logic Petri net, where P = {p1, p2,…, pm} and T = {t1, t2,…, tn} and M0 is its inital marking, M∈R(M0). t is enabled at M:

For t∈TI, suppose that Vii = {VIi,1, VIi,2,…, VIi,u} is its logic input enabling vector set and VIi∈VI. If ∃x∈{1, 2,…, u}, VIi,x∈VIi and VIi,x≅ M
For t∈TO, suppose that Voi = {VOi,1, VOi,2,…, Voi,v} is its logic output enabling vector set and VOi ∈VO. If ∃x∈{1, 2,…, v}, VOi,x ∈VOi and VOi,x≅M; or
For t∈TD, suppose Vi is its common enabling vector and Vi ≅M

Proof: Suppose that t is enabled at M, i.e. M[t >:

For t∈TI, ∃VIi,k∈VIi and Vii,k = (vi1, vi2, …, vim)T is defined by Eq. 3

If (t, pj)∈F, then vij = 0; if (pj, t) ∈F and pj|Ai = T, then vij = 1; the left vij are marked “*”.

If (t, pj)∈F, then M(j) = 0; if (pj, t)∈F and pj|Ai = T, then M(j) = 1; other elements of M are marked “1/0”.

Therefore, if (pj, t)∈F, M(j) = vij; if (t, pj)∈F and pj|Ai = T, M(j) = vi; the left vij are marked “*” and other elements of M are marked “1/0”. According to Eq. 6, VIi,x ≅M:

For t∈TO, ∃VOi,k∈VOi and Voi,k = (vi1, vi2,…, vim)T is defined by Eq. 4

If (pj, t)∈F, then vij = 1; if (t, pj)∈F and pj|Bi = T, then vij = 0; the left vij are marked “*”.

If (pj, t)∈F, then M(j) = 1. If (t, pj)∈F and pj|Bi = T, then M(j) = 0. other elements of M are marked “1/0”.

Therefore, if (pj, t)∈F, M(j) = vij; if (t, pj)∈F and pj|Bi = T, M(j) = vij; the left vij are marked “*” and other elements of M are marked “1/0”. According to Eq. 6, VOi,x ≅M:

For t∈TD, Vi = (vi1, vi2,…, vim)T is defined by Eq. 5

If (pj, t)∈F, then vij = 1; if (t, pj)∈F, then vij = 0; if pjt∩t , vij = *

If (pj, t)∈F, then M(j) = 1; if (t, pj)∈F, then M(j) = 0; if pjt∩t , M(j) = 1 or M(j) = 0.

Therefore, if (pj, t)∈F, then M(j) = vij; if (t, pj)∈F, then M(j) = vij and if pjt∩t , vij = * and M(j) = 1 or M(j) = 0. According to Eq. 6, Vi ≅M.

For logic transitions, Theorem 1 is the necessary condition of a transition to fire, not the necessary and sufficient condition. For all traditional transitons, Theorem is the necessary and sufficient condition. The firing of logic transitions are restricted by the enabling vectors and logic expressions. Next, the matching expression is put forward.

Definition 8: Suppose that f1 = A1∨A2∨…∨Au and f2 = B1∨B2∨…∨Bu are standard form. f1 and f2 are called matching expressions, if:

The number of standard minterm between is the same, i.e., u = v
The standard minterm Ai of f1 corresponds to the standard minterm Bi of f2 and the elements of Ai corresponds to the elements of Bi, i.e., for ∀pm, pn∈Ai, their corresponding places pk, pl∈Bi, having k-m = l-n

Two matching expressions are causal relationship. Once a standard minterm Ai of f1 fired, the standard minterm Bi of its matching expression could fire directionally in the running of the LPN.

Example 3: In Fig. 1, fI = (p1∧p2)∨(p1∧p2∧p3) and fO = (p7∧p8)∨(p7∧p8∧p9) are two matching expressions. fI = (p1∧p2∧5p3)∨(p1∧p2∧p3) and fO = (p7∧p8∧p9)∨(p7∧p8∧5p9) are their standard forms and they have satisfied the Definiton 8. They will be used in the section IV.

Next, the equation vector used to calculate the marking M is put forward.

Definition 9: Let LPN = (LN, M) be a logic Petri net, where P = {p1, p2,…, pm} and T = {t1, t2,…, tn}, For t∈TI, the standard form of fI(t) has a minterm Ai. V' = (vi1', vi2',…, vim')T is an equation vector of t, where:

(7)

•For t∈TO, the standard form of fO(t) has a minterm Bi. V' = (vi1', vi2',…, vim')T is an equation vector of t, where:

(8)

•For t ∈TD, Vi' = (vi1', vi2',…, vim')T is a equation vector of t, where:

(9)

In Eq. 7-8 and 9, j belongs to the set {1, 2,…, m}. From Definitions 6 and 8, enabling vectors and equation vectors are obtained by the same expression and their number is the same. Each enabling vector corresponds to an equation vector. So Vii,1', VIi,2',..., VIi,u-1' and VIi,u' are equation vectors of t belonging to TI and Vii' = {VIi,1', VIi,2',…, VIiB,u'} is the input equation vector set, Vii'∈VI'; likewise, Voi,1', Voi,2',…, Voi,v' are the equation vectors of t belonging to TO and Voi' = {VOi,1', VOi,2',…, VOi,v'} is the output equation vector set, VOi'∈VO' and Vi'∈V is the common equation of t.

Based on Definitions 6 and 9, a therom and an algorithm are introduced in the following.

Definition 10: Let LPN = (LN, M) be a logic Petri net, where P = {p1, p2,…, pm} and T = {t1, t2,…, tn} and M0 is the initial marking of the LPN, M∈R(M0):

For t∈TI, Vii' = {VIi,1', VIi,2',…, VIi,u'} is the input equation vector set of t and Vii = {VIi,1, VIi,2,…, VIi,v} is its input enabling vector set. If VIi,x≅M, then M[t >M' and:

(10)

For t∈TO, Voi' = {VOi,1', VOi,2',…, VOi,v'} is its output equation vector set and Voi = {VOi,1, VOi,2,…, VOi,v} is its output enabling vector set. If VOi,y≅M, then M[t >M':

(11)

For t∈TD, Vi' is the common equation vector of t and Vi is its enabling vector. If Vi≅M, then M[t >M':

(12)

Equation 10, 11 and 12 are used to calculate the marking M after a transition has fired. Based on the definitions and Theorem 1, an algorithm is proposed:

Algorithm 1: The firing of transitions in LPNs

AN EXAMPLE

In the LPN model of Fig. 1, LPN = (P, T, F, M), where t1∈TI, t2∈TD, t3∈TO, M = (1, 1, 0, 1, 0, 0, 0, 0, 0)T and t1 and t3 are restricted by fI = (p1∧p2)∨(p1∧p2∧p3) and fO = (p7∧p8)∨(p7∧p8∧p9), respectively. fI and fO are matching expressions.

From Example 1, get the standard form fI = (p1∧p2∧5p3)∨(p1∧p2∧p3), fO = (p7∧p8∧5p9)∨(p7∧p8∧p9).

By Definition 6, the input, output and common enabling vector sets can be obtained, where:

VI1 = {VI1,1, VI1,2} is the input enabling vector set of t1, where VI1,1 = (1, 1, *, *, 0, *, *, *, *)T, VI1,2 = (1, 1, 1, *, 0, *, *, *, *)T
V2 is the common enabling vector of t2 and V2 = (*, *, *, 1, 1, 0, *, *, *)T
VO3 = {VO3,1, VO3,2} is the output enabling vector set of t3, where VO3,1 = (*, *, *, *, *, 1, 0, 0, *)T, VO3,2 = (*, *, *, *, *, 1, 0, 0, 0)T

By Definition 9, the equation vector set can be obtained, where:

VI1' = {VI1,1', VI1,2'} is the input equation vector set of t1, where VI1,1' = (-1, -1, 0, 0, 1, 0, 0, 0, 0)T, VI1,2' = (-1, -1, -1, 0, 1, 0, 0, 0, 0)T
V2' is the common equation vector of t2 and V2' = (0, 0, 0, -1, -1, 1, 0, 0, 0)T
VO3' = {VO3,1', VO3,2'} is the output equation vector set of t3, where VO3,1' = (0, 0, 0, 0, 0, -1, 1, 1, 0)T, VO3,2' = (0, 0, 0, 0, 0, -1, 1, 1, 1)T

According to Algorithm 1:

Let M match VI1,1, VI1,2, by Definition 7, have VI1,1≅M; by Eq. 10, M1 = M+VI1,1' = (0, 0, 0, 1, 1, 0, 0, 0, 0)T, M[t1>M1
By Definition 7, have V2≅M1; by Eq. 12, M2 = M1+V2' = (0, 0, 0, 0, 0, 1, 0, 0, 0)T, M1[t2>M2
Let M2 match VO3,1, VO3,2, by Definition 7, have VO3,1≅M and VO3,2≅M. fI and fO are matching expressions and in (a), VI1,1≅M, VO3,1 is the matching vector. By Eq. 11, M3 = M2+VO3,1' = (0, 0, 0, 0, 0, 0, 1, 1, 0)T, M2[t3>M3

At the marking M3, all enabling vectors can not match M3 and the running of the LPN stops.

CONCLUSION

Based on our work, the definition of LPNs is redefined. By introducing the enabling vectors and matching expressions, the indeterminate data transmission caused by logic output transitions is solved. The standard form of a logic expression can delete useless minterms and the analysis of LPN models is more concisionly.

Further work will investigate the fundamental properties of LPNs according to the results proposed in this study, such as state equivalency, liveness and reachability. The Logic Petri Net Workflow will be put forward and be used in progress mining.

ACKNOWLEDGMENTS

This study is supported by the National Natural Science Foundation of China under Grants No. 61170078 and 61173042; the National Basic Research Program of China under Grant No. 2010CB328101; the Doctoral Program of Higher Education of the Specialized Research Fund of China under Grant No. 20113718110004; Basic Research Program of Qingdao City of China under Grant No. 13-1-4-116-jch; the SDUST Research Fund of China under Grant No. 2011KYTD102 and Graduate Innovation Foundation of Shaudong University of Science and Technology under Grant No. YC130107.

REFERENCES
Aziz, M.H., E.L.J. Bohez, R. Pisuchpen and M. Parnichkun, 2013. Petri Net model of repetitive push manufacturing with Polca to minimise value-added WIP. Int. J. Prod. Res., 51: 4464-4483.
CrossRef  |  Direct Link  |  

Barzegar, B., M. Mehrabanian, S. Bandegan and S. Bandegan, 2011. Fuzzy logic for a traffic signal control with colored petri net. Aus. J. Basic. Applied Sci., 5: 2961-2964.
Direct Link  |  

Bayati, M. and A. Dideban, 2012. Controller synthesis using the novel fuzzy petri net. Int. Rev. Autom. Control, 5: 839-843.
Direct 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.

Du, Y.Y. and C.J. Jiang, 2008. On the design and temporal Petri net verification of grid commerce architecture. Chinese J. Electron., 17: 247-251.
Direct Link  |  

Du, Y.Y., C.J. Jiang and M. Zhou, 2009. A petri net-based model for verification of obligations and accountability in cooperative systems. IEEE Trans. Syst. Man Cybern. A, 39: 299-308.
CrossRef  |  Direct Link  |  

Marin, A., S. Balsamo and P.G. Harrison, 2012. Analysis of stochastic Petri nets with signals. Perform. Eval., 69: 551-572.
CrossRef  |  Direct Link  |  

©  2019 Science Alert. All Rights Reserved
Fulltext PDF References Abstract