Open Access is an initiative that aims to make scientific research freely available to all. To date our community has made over 100 million downloads. It’s based on principles of collaboration, unobstructed discovery, and, most importantly, scientific progression. As PhD students, we found it difficult to access the research we needed, so we decided to create a new Open Access publisher that levels the playing field for scientists across the world. How? By making research easy to access, and puts the academic needs of the researchers before the business interests of publishers.
We are a community of more than 103,000 authors and editors from 3,291 institutions spanning 160 countries, including Nobel Prize winners and some of the world’s most-cited researchers. Publishing on IntechOpen allows authors to earn citations and find new collaborators, meaning more people see your work not only from your own field of study, but from other related fields too.
To purchase hard copies of this book, please contact the representative in India:
CBS Publishers & Distributors Pvt. Ltd.
www.cbspd.com
|
customercare@cbspd.com
Augmented marked graphs were first introduced in 1997 (Chu & Xie, 1997). They are not well known as compared to other sub-classes of Petri nets such as free-choice nets (Desel & Esparza, 1995), and the properties of augmented marked graphs are not studied extensively. However, augmented marked graphs possess a structure which is desirable for modelling shared resources, and for this reason, they are often used in modelling shared resource systems, such as manufacturing systems (Chu & Xie, 1997; Zhou & Venkatesh, 1999; Jeng et al., 2000; Jeng et al., 2002; Huang et al., 2003; Cheung & Chow, 2005).
There are a few published works on augmented marked graphs. Based on siphons and mathematical programming, Chu and Xie proposed a necessary and sufficient condition of live and reversible augmented marked graphs, which checks the existence of potential deadlocks (Chu & Xie, 1997). However, this involves the flow of tokens during execution and cannot be checked simply by looking into the structure. Chu and Xie also proposed another siphon-based characterisation for live and reversible augmented marked graphs but it provides a sufficient condition only. On the other hand, the boundedness and conservativeness of augmented marked graphs were not investigated.
In the literature, apart from (Chu & Xie, 1997), the studies of augmented marked graphs mainly focus on their property-preserving synthesis or composition. Jeng et al. proposed a synthesis of process nets (covering augmented marked graphs) for manufacturing system design, where the condition of liveness and reversibility are based on siphons and the firability of transitions (Jeng et al., 2000; Jeng et al., 2002). Huang et al. also investigated the composition of augmented marked graphs so that properties such as liveness, boundedness and reversibility can be preserved (Huang et al., 2003).
In our earlier works on augmented marked graphs, we proposed characterisations for their liveness, boundedness, reversibility and conservativeness and applied the characterisations to the analysis and design of manufacturing systems, object-oriented systems and shared resource systems (Cheung, 2004; Cheung, 2005; Cheung & Chow, 2005a; Cheung & Chow, 2005b; Cheung & Chow, 2005c; Cheung, 2006; Cheung & Chow, 2006; Cheung et al., 2006; Cheung, 2007). This paper consolidates our previous works with a special focus on the properties of augmented marked graphs.
First, we provide a number of characterisations for live and reversible augmented marked graphs, based on siphons and cycles. In particular, a property called R-inclusion property is introduced to characterise the siphon-trap property of augmented marked graphs. With this property, the liveness and reversibility of an augmented marked graph can be analysed through cycles instead of siphons. Second, we introduce R-transformation which transforms an augmented marked graph into a marked graph. Its boundedness and conservativeness can be determined by checking the cycles of the transformed marked graph. Based on these characterisations, some pretty simple conditions and procedures are derived for checking the liveness, reversibility, boundedness and conservativeness of an augmented marked graph. These will be illustrated using the dining philosophers problem. We then show the application to manufacturing system design.
The rest of this paper is organised as follows. Following this introduction, Section 2 provides the preliminaries to be used in this paper. Section 3 describes augmented marked graphs and their known properties. Section 4 shows characterisations for liveness and reversibility while Section 5 shows characterisations for boundedness and conservativeness. Section 6 then illustrates these characterisations using the dining philosophers example. Section 7 describes the application to manufacturing system design. Finally, Section 8 concludes this paper with a brief discussion.
Definition 2.1. A place-transition net (PT-net) is a 4-tuple N = P, T, F, W , where P is a set of places, T is a set of transitions, F ((P T) (T P)) is a flow relation, and W : F { 1, 2,... } is a weight function. N is said to be ordinary if and only if the range of W is { 1 }.
An ordinary PT-net is usually written as P, T, F . In the rest of this paper, unless specified otherwise, all PT-nets refer to ordinary PT-nets.
Definition 2.2. Let N = P, T, F, W be a PT-net. For any x (P T), x = { y | (y, x) F } and x = { y | (x, y) F } are called the pre-set and post-set of x, respectively.
For clarity in presentation, the pre-set and post-set of a set of places or transitions X = { x1, x2,..., xn } can be written as X and X respectively, where X = x1x2 ... xn and X = x1 x2 ... xn.
Definition 2.3. For a PT-net N = P, T, F, W , a path is a sequence of places and transitions = x1, x2,..., xn , such that (xi, xi+1) F for i = 1, 2,..., n-1. is said to be elementary if and only if it contains no duplicate places or transitions.
Definition 2.4. For a PT-net N = P, T, F, W , a sequence of places p1, p2,..., pn is called a cycle if and only if there exists a set of transitions { t1, t2,..., tn }, such that p1, t1, p2, t2,..., pn, tn forms an elementary path and (tn, p1) F.
Definition 2.5. For a PT-net N = P, T, F, W , a marking is a function M : P { 0, 1, 2,...}, where M(p) is the number of tokens in p. (N, M0) represents N with an initial marking M0.
Definition 2.6. For a PT-net (N, M0), a transition t is said to be enabled at a marking M if and only if p t : M(p) W(p,t). On firing t, M is changed to M' such that p P : M'(p) = M(p) - W(p,t) + W(t,p). In notation, M [N,t M' or M [t M'.
Definition 2.7. For a PT-net (N, M0), a sequence of transitions = t1, t2,..., tn is called a firing sequence if and only if M0 [t1... [tn Mn. In notation, M0 [N, Mn or M0 [ Mn.
Definition 2.8. For a PT-net (N, M0), a marking M is said to be reachable if and only if there exists a firing sequence such that M0 [ M. In notation, M0 [N, M or M0 [ M. [N, M0 or [M0 represents the set of all reachable markings of (N, M0).
Definition 2.9. Let N = P, T, F, W be a PT-net, where P = { p1, p2,..., pm } and T = { t1, t2,..., tn }. The incidence matrix of N is an m n matrix V whose typical entry vij = W(pi,tj) - W(tj,pi) represents the change in number of tokens in pi after firing tj once, for i = 1, 2,..., m and j = 1, 2,..., n.
Definition 2.10. For a PT-net (N, M0), a transition t is said to be live if and only if M [M0, M' : M [ M' [t. (N, M0) is said to be live if and only if every transition is live.
Definition 2.11. For a PT-net (N, M0), a place p is said to be k-bounded if and only if M [M0 : M(p) k, where k is a positive integer. (N, M0) is said to be bounded if and only if every place is k-bounded, and safe if and only if every place is 1-bounded.
Definition 2.12. A PT-net (N, M0) is said to be reversible if and only if M [M0 : M [ M0.
Definition 2.13. A PT-net N = P, T, F, W is said to be conservative if and only if there exists a |P|-vector > 0 such that V = 0, where V is the incidence matrix of N.
Definition 2.14. For a PT-net N = P, T, F, W , a place invariant is a |P|-vector 0 such that V = 0, where V is the incidence matrix of N.
Definition 2.15. For a PT-net N, a set of places S is called a siphon if and only if S S. S is said to be minimal if and only if there does not exist another siphon S' in N such that S' S.
Definition 2.16. For a PT-net, a set of places T is called a trap if and only if TT.
Definition 2.17. A PT-net (N, M0) is said to satisfy the siphon-trap property if and only if every siphon contains a marked trap (or every minimal siphon contains a marked trap).
Definition 2.18. A marked graph is an ordinary PT-net N = P, T, F, W such that p P : |p| = |p| = 1.
Property 2.2. A marked graph (N, M0) is live if and only if every cycle is marked by M0 (Reisig, 1985; Murata, 1989).
Property 2.3. A live marked graph (N, M0) is bounded if and only if every place belongs to a cycle marked by M0 (Reisig, 1985; Murata, 1989).
This section describes augmented marked graphs and their known properties on liveness and reversibility.
Definition 3.1. An augmented marked graph (N, M0; R) is a PT-net (N, M0) with a specific subset of places R, satisfying the following conditions : (a) Every place in R is marked by M0. (b) The net (N', M0') obtained from (N, M0; R) by removing the places in R and their associated arcs is a marked graph. (c) For each r R, there exist kr 1 pair of transitions Dr = { ts1, th1, ts2, th2,..., tskr, thkr }, such that r = { ts1, ts2,..., tskr } T and r = { th1, th2,..., thkr } T and that, for each tsi, thi Dr, there exists in N' an elementary path ri connecting tsi to thi. (d) In (N', M0'), every cycle is marked and no ri is marked.
Figure 1 shows an augmented marked graph (N, M0; R), where R = { r1, r2 }. For r1, Dr1 = { t1, t11, t3, t9 }. For r2, Dr2 = { t2, t11, t4, t10 }.
Figure 1.
A typical augmented marked graph.
Property 3.1. An augmented marked graph is live if and only if it does not contain any potential deadlock - a siphon which would eventually become empty (Chu & Xie, 1997).
Property 3.2. An augmented marked graph is reversible if it is live (Chu & Xie, 1997).
Property 3.3. An augmented marked graph is live and reversible if and only if every minimal siphon would never become empty.
Proof. () It follows from Properties 3.1 and 3.2 that an augmented marked graph is live and reversible if every minimal siphon would never become empty. () It follows from Property 3.1 that every minimal siphon would never become empty.
Property 3.4. An augmented marked graph (N, M0; R) is live and reversible if every minimal siphon, which contains at least one place of R, contains a marked trap (Chu & Xie, 1997).
For the augmented marked graph (N, M0; R) in Figure 1, the minimal siphons include : { p1, p5, p8}, { r1, p2, p4, p6, p7, p9 }, { r1, p2, p4, p6, p7, p10 }, { r2, p3, p5, p6, p8, p9 } and { r2, p3, p5, p6, p8, p10 }. Each of these minimal siphons contains a marked trap, and would never become empty. (N, M0; R) is live and reversible.
This section provides characterisations for live and reversible augmented marked graphs, based on siphons and cycles. Strategies for checking liveness and reversibility are then presented.
Definition 4.1. For a PT-net N, N is defined as the set of all cycles in N.
Definition 4.2. Let N be a PT-net. For a subset of cycles Y N, P[Y] is defined as the set of places in Y, and T[Y] = P[Y] P[Y] is defined as the set of transitions generated by Y.
For clarity in presentation, P[{}] and T[{}] can be written as P[] and T[], to denote the set of places in a cycle and the set of transitions generated by , respectively.
Definition 4.3. For a PT-net N, an elementary path = x1, x2,..., xn is said to be conflict-free if and only if, for any transition xi in , j (i -1) xjxi (Barkaoui, 1995).
Lemma 4.1. Let S be a minimal siphon of a PT-net. For any p, p' S, there exists in S a conflict-free path from p to p' (Barkaoui, 1995).
Property 4.1. For a minimal siphon S of an augmented marked graph (N, M0; R), there exists a set of cycles Y N such that P[Y] = S.
Proof. Let S = { p1, p2,..., pn }. For each pi, it follows from the definition of augmented marked graphs that pi . Then, there exists pj S, where pj pi, such that (pjpi) . According to Lemma 4.1, pi connects to pj via a conflict-free path in S. Since pj connects to pi, this forms a cycle i in S, where pi P[i] S. Let Y = { 1, 2,..., n }. We have P[Y] = P[1] P[2] ... P[n] S. On the other hand, S (P[1] P[2] ... P[n]) = P[Y] since S = { p1, p2,..., pn }. Hence, P[Y] = S.
Property 4.2. Every cycle in an augmented marked graph is marked.
Proof. (by contradiction) Let (N, M0; R) be an augmented marked graph. Suppose there exists a cycle in (N, M0; R), such that is not marked. Then, does not contain any place in R. Hence, also exists in the net (N', M0') obtained from (N, M0; R) after removing the places in R and their associated arcs. However, by definition of augmented marked graphs, every cycle in (N', M0') is marked.
Property 4.3. Every siphon in an augmented marked graph is marked.
Proof. For an augmented marked graph, according to Properties 4.1 and 4.2, every minimal siphon contains cycles and is marked. Hence, every siphon, which contains at least one minimal siphon, is marked.
Property 4.4. Let (N, M0; R) be an augmented marked graph. For every r R, there exists a minimal siphon which contains only one marked place r.
Proof. Let Dr = { ts1, th1, ts2, th2,..., tsn, thn }, where r = { ts1, ts2,..., tsn } and r = { th1, th2,..., thn }. By definition of augmented marked graphs, for each tsi, thi Dr, tsi connects to thi via an elementary path i which is not marked. Let S = P1 P2 ... Pn { r }, where Pi is the set of places in i. We have Pi (Pi r) because, for each p Pi, | p | = | p | = 1. Then, (P1P2 ... Pn) (P1 P2 ... Pn r). Besides, r = { th1, th2,..., thn } (P1 P2 ... Pn). Hence, S = (P1P2 ... Pnr) (P1 P2 ... Pn r) = S. Therefore, S is a siphon, in which r is the only one marked place. Let S' be a minimal siphon in S. According to Property 4.3, S' is marked. Since r is the only one marked place in S, r is also the only one marked place in S'.
Consider the augmented marked graph (N, M0; R) shown in Figure 1. Every minimal siphon is covered by cycles. For example, for a minimal siphon S1 = { r1, p2, p4, p6, p7, p9 }, there exists a set of cycles Y1 = { 11, 12 }, where 11 = r1, p4, p7 and 12 = r1, p2, p6, p9 , such that S1 = P[Y1]. For another minimal siphon S2 = { r2, p3, p5, p6, p8, p10 }, there exists a set of cycles Y2 = { 21, 22 }, where 21 = r2, p5, p8 and 22 = r2, p3, p6, p10 , such that S2 = P[Y2]. S1 is a minimal siphon, in which r1 R is the only one marked place. Also, S2 is a minimal siphon, in which r2 R is the only one marked place.
Definition 4.4. For an augmented marked graph (N, M0; R), a minimal siphon is called a R-siphon if and only if it contains at least one place in R.
Definition 4.5. For an augmented marked graph (N, M0; R), a minimal siphon is called a NR-siphon if and only if it does not contain any place in R.
Definition 4.6. Let N be a PT-net. For a set of places Q in N, N[Q] is defined as the set of cycles that contains at least one place in Q.
For clarity in presentation, N[{p}] can be written as N[p] to denote the set of cycles that contains a place p.
Figure 2 shows an augmented marked graph (N, M0; R), where R = { r1, r2 }. There are five minimal siphons, namely, S1 = { r1, p3, p4, p7, p8 }, S2 = { r1, p3, p5, p7, p8 }, S3 = { r2, p2, p4, p6, p8, p9, p10 }, S4 = { r2, p2, p5, p6, p8, p9, p10 } and S5 = { p1, p3, p7 }. S1, S2, S3 and S4 are R-siphons while S5 is a NR-siphon.
Property 4.5. For an augmented marked graph (N, M0; R), a R-siphon is covered by a set of cycles Y N[R].
Proof. (By contradiction) Let S be a R-siphon. By Property 4.1, S is covered by cycles. Suppose there exists a cycle in S, such that N[R]. According to the definition of augmented marked graphs, for any p P[], | p | = | p | = 1. Hence, P[] = P[], and P[] is also a siphon. Since there exists a place r R such that r S but r P[], we have P[] S. However, by definition of minimal siphons, there does not exists any siphon S' = P[] in S, such that S' = P[] S.
For the augmented marked graph (N, M0; R) shown in Figure 2. every R-siphon is covered by a set of cycles in N[R]. For example, a R-siphon S1 = { r1, p3, p4, p7, p8 } is covered by a set of cycles Y1 = { 11, 12 } N[R], where 11 = r1, p3, p7 and 12 = r1, p4, p8 . Another R-siphon S2 = { r1, p3, p5, p7, p8 } is covered by a set of cycles Y2 = { 21, 22 } N[R], where 21 = r1, p3, p7 and 22 = r1, p5, p8 .
Figure 2.
An augmented marked graph for illustration of R-siphons.
Property 4.6. Let S be a R-siphon of an augmented marked graph (N, M0; R). For every t (S \ S), there does not exist any s (S \ R) such that t s.
Proof. (by contradiction) Suppose s exists. By definition of augmented marked graphs, | s | = | s | = 1. S is covered by cycles in accordance with Property 4.5. Hence, t is the one and only one transition in s, where t T[Y] = (SS). This however contradicts t (S \ S).
Property 4.7. For an augmented marked graph (N, M0; R), a NR-siphon contains itself as a marked trap and would never become empty.
Proof. Let S be a NR-siphon. According to Property 4.3, S is marked. It follows from the definition of augmented marked graphs that, for any s S, | s | = | s | = 1. Then, S = S and S is also a trap. Hence, S contains itself as a marked trap and would never become empty.
Property 4.8. An augmented marked graph (N, M0; R) is live and reversible if and only if no R-siphons eventually become empty.
Proof. () According to Property 4.7, a NR-siphon would never become empty. Given that no R-siphons eventually become empty, every minimal siphon would never become empty. According to Property 3.3, (N, M0; R) is live and reversible. () It follows from Property 3.1 that no R-siphons eventually become empty.
Property 4.9. An augmented marked graph (N, M0; R) satisfies the siphon-trap property if and only if every R-siphon contains a marked trap.
Proof. () According to Property 4.7, a NR-siphon contains a marked trap. Given that every R-siphon contains a marked trap, every minimal siphon contains a marked trap. () Every minimal siphon contains marked trap implies that every R-siphon contains a marked trap.
Consider the augmented marked graph (N, M0; R) shown in Figure 2. Every R-siphon contains marked trap. Each of the R-siphons S1 = { r1, p3, p4, p7, p8 }, S2 = { r1, p3, p5, p7, p8 }, S3 = { r2, p2, p4, p6, p8, p9, p10 } and S4 = { r2, p2, p5, p6, p8, p9, p10 } contains a marked trap and would never become empty. Also, the NR-siphon S5 = { p1, p3, p7 } contains itself as a marked trap and would never become empty. (N, M0; R) is live and reversible.
Property 4.10. (characterisation of Property 3.4) An augmented marked graph (N, M0; R) is live and reversible if every R-siphon contains a marked trap.
Proof. For (N, M0; R), if every R-siphon contains a marked trap, according to Property 4.9, the siphon-trap property is satisfied. Hence, every minimal siphon would never become empty. It then follows from Property 3.3 that (N, M0; R) is live and reversible.
Property 4.8 provides a simpler necessary and sufficient condition for live and reversible augmented marked graphs, as compared to Properties 3.1 and 3.2. According to Property 4.8, only R-siphons are considered. Typically, for an augmented marked graph (N, M0; R), the set R is small, so only a small number of siphons need to be considered. Properties 3.4 and 4.10 also refers to the same set of siphons but only a sufficient condition is provided.
With Properties 4.8 and 4.10, we can determine if an augmented marked graph is live and reversible based on R-siphons. On the other hand, Property 4.5 provides a characterisation for R-siphons so that R-siphons can be easily identified by finding cycles in N[R].
We may now derive the following strategy for checking the liveness and reversibility of an augmented marked graph (N, M0; R) :
Find all R-siphons based on N[R].
Check if every R-siphon contains a marked trap. If yes, report (N, M0; R) is live and reversible. Otherwise, go to (c).
For each R-siphon which does not contain any marked trap, check if it would never become empty. If yes, (N, M0; R) is live and reversible. Otherwise, (N, M0; R) is neither live nor reversible.
In the following, a property called R-inclusion is introduced for characterising the liveness and reversibility of augmented marked graphs.
Definition 4.7. For a PT-net N, a set of cycles Y N is said to be conflict-free if and only if, for any q, q' P[Y], there exists in P[Y] a conflict-free path from q to q'.
For the PT-net N shown in Figure 3, consider three cycles 1, 2, 3N[p3], where 1 = p3, p2, p7 , 2 = p3, p4 and 3 = p3, p1, p6, p10, p8 . Y1 = { 1, 2 } is conflict-free because for any q, q' P[Y1], there exists in P[Y1] a conflict-free path from q to q'. Y2 = { 2, 3 } is not conflict-free. Consider Y2. We have p4, p8 P[Y2]. p4 is connected to p8 via only one path = p4, t5, p3, t1, p1, t3, p6, t6, p10, t9, p8 in Y2, and is not conflict-free because p4, p8t5.
Figure 3.
A PT-net N for illustration of conflict-free cycles.
Property 4.11. Let S be a minimal siphon of an augmented marked graph (N, M0; R), and Y N be a set of cycles such that S = P[Y]. Then, Y is conflict-free.
Proof. It follows from Lemma 4.1 that, for any q, q' S = P[Y], there exists in S = P[Y] a conflict-free path from q to q'. Hence, Y is conflict free.
For the augmented marked graph shown in Figure 1, { r1, p2, p4, p6, p7, p9 } is a minimal siphon covered by a set of cycles { r1, p4, p7 , r1, p2, p6, p9 } which is conflict free. { r2, p3, p5, p6, p8, p10 } is another minimal siphon covered by a set of cycles { r2, p5, p8 , r2, p3, p6, p10 } which is conflict-free. For the augmented marked graph shown in Figure 2, { r1, p3, p4, p7, p8 } is a minimal siphon covered by a set of cycles { r1, p3, p7 , r1, p4, p8 } which is conflict free. { r1, p3, p5, p7, p8 } is another minimal siphon covered by a set of cycles { r1, p3, p7 , r1, p5, p8 } which is conflict free.
Definition 4.8. Let (N, M0; R) be an augmented marked graph. A place r R is said to satisfy the R-inclusion if and only if, for any set of cycles Y N[R] such that Y is conflict-free, r T[Y] r T[Y].
Figure 4 shows an augmented marked graph (N, M0; R), where R = { r1, r2 }. Consider r1. For any set of cycles Y1N[R] such that Y1 is conflict-free, r1 T[Y1] r1 T[Y1]. Next, consider r2. For any set of cycles Y2N[R] such that Y2 is conflict-free, r2 T[Y2] r2 T[Y]. Both r1 and r2 satisfy the R-inclusion.
Figure 5 shows an augmented marked graph (N, M0; R), where R = { r1, r2 }. For r1, there exists a set of cycles Y1 = { 11, 12 } N[R], where 11 = r1, p5 and 12 = r1, p5, r2, p6 . r1 = { t5, t6 } T[Y1] = { t3, t4, t5, t6 }, but r1 = { t2, t3 } T[Y1]. For r2, there exists a set of cycles Y2 = { 21, 22 } N[R], where 21 = r2, p6 and 22 = r2, p6, r1, p5 . r2 = { t5, t6 } T[Y2] = { t3, t4, t5, t6 }, but r2 = { t1, t4 } T[Y2]. Hence, r1 and r2 do not satisfy the R-inclusion property.
Figure 4.
An augmented marked graph for illustration of R-inclusion.
Figure 5.
Another augmented marked graph for illustration of R-inclusion.
Property 4.12. For an augmented marked graph (N, M0; R), a R-siphon S contains itself as a marked trap if every place r R in S satisfies the R-inclusion property.
Proof. Let S = { p1, p2,..., pn }. According to Property 4.3, S is marked. It follows from Properties 4.5 and 4.11 that there exists a set of cycles Y N[R], such that Y is conflict-free and P[Y] = S. Since S is a siphon, for each pi S, pi (S S) = (P[Y] P[Y]) = T[Y]. In case pi R, pi T[Y] because | pi | = | pi | = 1. In case pi R, given that pi satisfies the R-inclusion property, pi T[Y]. Every pi T[Y] = (P[Y] P[Y]) and piP[Y] = S. Since S = (p1 p2 ... pn) S, S is also a trap. S contains itself as a marked trap.
Consider the augmented marked graph (N, M0; R), where R = { r1, r2 }, shown in Figure 4. Both r1 and r2 satisfy the R-inclusion property. { r1, p3, p4 } is a minimal siphon which contains itself as a marked trap. { r2, p5, p6 } is another minimal siphon which contains itself as a marked trap.
Property 4.13. An augmented marked graph (N, M0; R) satisfies the siphon-trap property if and only if every place r R satisfies the R-inclusion property.
Proof. () It follows from Properties 4.12 and 4.9. ( by contradiction) Suppose there exists r R, such that r does not satisfy the R-inclusion property. According to Property 4.4, there exists a R-siphon S, in which r is the only marked place. It follows from Properties 4.5 and 4.11 that there exists Y N[R], such that Y is conflict-free and S = P[Y]. According to Property 4.9, S contains a marked trap Q. Then, r Q and r (Q Q). Since S is a siphon, we have r (S S) = (P[Y] P[Y]) = T[Y]. However, as r does not satisfy the R-inclusion property, r T[Y] = (P[Y] P[Y]) = (S S), implying r (Q Q).
Property 4.14. An augmented marked graph (N, M0; R) is live and reversible if every place r R satisfies the R-inclusion property.
Proof. According to Property 4.13, (N, M0; R) satisfies the siphon-trap property. It follows from Property 4.10 that (N, M0; R) is live and reversible.
Consider the augmented marked graph (N, M0; R), where R = { r1, r2 }, shown in Figure 4. Both r1 and r2 satisfy the R-inclusion property. (N, M0; R) satisfies the siphon-trap property, and is live and reversible.
Property 4.14 provides a cycle-based sufficient condition for live and reversible augmented marked graphs. Without finding siphons and checking if each of these siphons contains a marked trap, we need to check the R-inclusion property which involves finding cycles and checking their pre-sets and post-sets. This provides an alternative characterisation for live and reversible augmented marked graphs, apart from the existing siphon-based ones.
Based on Properties 4.5, 4.8, 4.10, 4.12 and 4.14, we may revise the strategy for checking the liveness and reversibility of an augmented marked graph (N, M0; R) with the use of the R-inclusion property, as follows.
Check if every r R satisfies the R-inclusion property. If yes, report (N, M0; R) is live and reversible. Otherwise go to (b).
Let R' R be the set of places which do not satisfy the R-inclusion property. Based on N[R'], find all R-siphons which contain at least one place in R'.
For each R-siphon identified in (b), check if it contains a marked trap. If yes, (N, M0; R) is live and reversible. Otherwise, go to (d).
For each R-siphon identified in (b) that does not contain any marked trap, check if it would never become empty. If yes, (N, M0; R) is live and reversible. Otherwise, (N, M0; R) is neither live nor reversible.HHHHHH
This section first introduces a transformation, called R-transform, for augmented marked graphs. Based on R-transform, a number of characterisations for bounded and conservative augmented marked graphs are then derived. Strategies for checking boundedness and conservativeness are then presented.
Property 5.1. Let (N, M0; R) be an augmented marked graph to be transformed into (N', M0') as follows. For each place r R, where Dr = { ts1, th1, ts2, th2,..., tskr, thkr }, replace r with a set of places { p1, p2,..., pkr }, such that M0'[pi] = M0[r] and pi = { tsi } and pi = { thi } for i = 1, 2,..., kr. Then, (N', M0') is a marked graph.
Proof. According to the definition of augmented marked graphs, for each place p R in N, M0; R), | p | = | p | = 1. Each place r R is replaced by a set of places { p1, p2,..., pkr }, where | pi | = | pi | = 1 for i = 1, 2,..., kr. Hence, for every place q in N', | q | = | q | = 1. (N', M0') is a marked graph.
Definition 5.1. Let (N, M0; R) be an augmented marked graph. The marked graph (N', M0') obtained from (N, M0; R) after the transformation as stated in Property 5.1 is called the R-transform of (N, M0; R).
Property 5.2. The R-transform of an augmented marked graph is live.
Proof. Let (N', M0') be the R-transform of an augmented marked graph (N, M0; R). Since the transformation process does not create new cycles, cycles in (N', M0') also exist in (N, M0; R). According to Property 4.1, every cycle in (N, M0; R) is marked, and hence, every cycle in (N', M0') is marked. Since (N', M0') is a marked graph, it follows from Property 2.2 that (N', M0') is live.
Figure 6 shows an augmented marked graph (N, M0; R). Figure 7 shows the R-transform of (N, M0; R), where r is replaced by { q1, q2 }. It is a live marked graph.
Figure 6.
An augmented marked graph for illustration of R-transform.
Property 5.3. Let (N', M0') be the R-transform of an augmented marked graph (N, M0; R), where r R is replaced by a set of places Q = { q1, q2,..., qk }, and P0 be the set of marked places in N'. Then, for each qi in N', there exists a place invariant i of N' such that i[qi] = 1 and i[s] = 0 for any place s P0 \ {qi}.
Figure 7.
The R-transform of the augmented marked graph shown in figure 6.
Proof. Let Dr = { ts1, th1, ts2, th2,..., tskr, thkr }. According to the definition of augmented marked graphs, for each tsi, thi, there exists an unmarked path = ts1,..., th1 in (N, M0; R). Obviously, also exists as an unmarked path in (N', M0'), and together with qi forms a cycle i which is marked at qi only. As (N', M0') is a marked graph, according to Property 2.5, the corresponding vector of i is a place invariant i of N'. Since qi is the only one marked place in i, i[qi] = 1 and i[s] = 0 for any place s P0 \ {qi}.
Property 5.4. Let (N, M0; R) be an augmented marked graph, where R = { r1, r2,..., rn }. Let (N', M0') be the R-transform of (N, M0; R), where each ri is replaced by a set of places Qi, for i = 1, 2,..., n. If every place in (N', M0') belongs to a cycle, then there exists a place invariant of N' such that > 0 and [q1] = [q2] =... = [qk] for each Qi = { q1, q2,..., qk }.
Proof. Let P = { p1, p2,..., pn } be the set of places in N', and P0 be those marked places. Since each pi belongs to a cycle i and (N', M0') is a marked graph, according to Property 2.5, the corresponding vector of i is a place invariant i' of N'. Then, ' = 1' + 2' +... + n' > 0 is a place invariant of N'. Consider Qi = { q1, q2,..., qk }. Let qm Qi such that '[qm] '[qj] for any qj Qi. For each qj, according to Property 5.3, there exists an invariant j' > 0 such that j'[qj] = 1 and j'[s] = 0 for any place s P0 \ {qj}. There also exists a place invariant " = ' + hj', where h 1, such that "[qj] = "[qm] and "[s] = '[s] for any s P0 \ {qj}. Hence, there eventually exists a place invariant of N' such that [q1] = [q2] =... = [qk].
Consider the R-transform (N', M0') of an augmented marked graph, as shown in Figure 7. For q1, there exists a place invariant 1, such that 1[q1] = 1 and 1[q2] = 1[p1] = 1[p2] = 0. For q2, there also exists a place invariant 2, such that 2[q2] = 1 and 2[q1] = 2[p1] = 2[p2] = 0. In (N', M0'), every place belongs to a cycle. There also exists a place invariant > 0, where [q1] = [q2].
Lemma 5.1. Let N = P, T, F be a PT-net and N' = P', T', F' be the PT-net obtained from N after fusing a set of places Q = { q1, q2,..., qn } P into a single place r P'. If there exists a place invariant of N such that [q1] = [q2] =... = [qn] = k 0, then there also exists a place invariant ' of N' such that '[r] = k and '[s] = [s] for any s P'\{r} = P\Q.
Proof. Since N' is obtained from N by fusing Q = { q1, q2,..., qn } into r, we have P' = (P\Q) { r }. Let V be the incidence matrix of N. Then, the incidence matrix V' of N' satisfies that V'[r] = i=1,2,...,nV[qi] and V'[s] = V[s] for any s P'\{r} = P\Q. Since is a place invariant of N, V = 0. Let ' be a place vector of N' such that '[r] = [q1] = [q2] =... = [qn] = k and '[s] = [s] for every s P'\{r} = P\Q. Then, 'V' = '[r]V'[r] + p(P'\{r})'[p]V'[p] = i=1,2,...,n[qi]V[qi] + p(P\Q)[p]V[p] = V = 0. Hence, ' is a place invariant of N'.
Lemma 5.2. Let N = P, T, F be a PT-net and N' = P', T', F' be the PT-net obtained from N after fusing a set of places Q = { q1, q2,..., qn } P into a single place r P'. If there exists a place invariant ' of N' such that '[r] = k 0, then there also exists a place invariant of N such that [q1] = [q2] =... = [qn] = k and [s] = '[s] for any s P\Q = P'\{r}.
Proof. Since N' is obtained from N by fusing Q = { q1, q2,..., qn } into r, we have P' = (P\Q) { r }. Let V be the incidence matrix of N. Then, the incidence matrix V' of N' satisfies that V'[r] = i=1,2,...,nV[qi] and V'[s] = V[s] for any s P'\{r} = P\Q. Since ' is a place invariant of N', 'V' = 0. Let be a place vector of N such that [q1] = [q2] =... = [qn] = k and [s] = '[s] for every s P\Q = P'\{r}. Then, V = i=1,2,...,n[qi]V[qi] + p(P\Q)[p]V[p] = '[r]V'[r] + p(P'\{r})'[p]V'[p] = 'V'. Hence, is a place invariant of N.
Property 5.5. Let (N', M0') be the R-transform of an augmented marked graph (N, M0; R). (N, M0; R) is bounded and conservative if and only if every place in (N', M0') belongs to a cycle.
Proof. () Let R = { r1, r2,..., rn }. (N', M0') is the R-transform of (N, M0; R), where each ri is replaced by a set of places Qi, for i = 1, 2,..., n. Since every place in (N', M0') belongs to a cycle, according to Property 5.4, there exists a place invariant ' of N' such that ' > 0 and '[q1] = '[q2] =... = '[qk] for each Qi = { q1, q2,..., qk }. It follows from Lemma 5.1 that there also exists a place invariants of N such that > 0 and [ri] = '[q1] = '[q2] =... = '[qk] for each Qi. Hence, (N, M0; R) is conservative. According to Property 2.1, (N, M0; R) is bounded. () Since (N, M0; R) is conservative, there exists a place invariant of N such that > 0. Consider each ri R which is replaced by Qi = { q1, q2,..., qk }. According to Lemma 5.2, there also exists a place invariant ' of N' such that ' > 0 and '[q1] = '[q2] =... = '[qk] = [ri] and '[s] = [s] for any s P'\Qi. Hence, (N', M0') is conservative. It follows from Property 2.1 that (N', M0') is bounded. Since (N', M0') is a marked graph, according to Property 2.3, every place in (N', M0') belongs to a cycle.
Property 5.6. Let (N', M0') be the R-transform of an augmented marked graph (N, M0; R). (N, M0; R) is bounded and conservative if and only if (N', M0') is bounded.
Proof. It follows from Properties 2.3 and 5.5.
Consider the augmented marked graph (N, M0; R) shown in Figure 6, and the R-transform (N', M0') of (N, M0; R). Every place in (N', M0') belongs to a cycle. (N, M0; R) is bounded and conservative. (N', M0') is also bounded and conservative.
Figure 8 shows another augmented marked graph (N, M0; R). Figure 9 shows the R-transform (N', M0') of (N, M0; R), where r is replaced by { q1, q2 }. For (N', M0'), places p3 and p10 do not belong to any cycle. (N, M0; R) is neither bounded nor conservative.
Figure 8.
Another augmented marked graph for illustration of R-transform.
Figure 9.
The R-transform of the augmented marked graph shown in figure 8.
Based on Properties 5.5, the following strategy is derived for checking the boundedness and conservativeness of an augmented marked graph (N, M0; R) :
Create the R-transform of (N, M0; R).
Let (N', M0') be the R-transform. For each place p in N', check if there exists a cycle that contains p. If yes, (N, M0; R) is bounded and conservative. Otherwise, (N, M0; R) is neither bounded nor conservative.
This section illustrates the properties of augmented marked graphs obtained in the previous two sections using the dining philosophers problem. By modelling the dining philosophers problem by an augmented marked graph, the system is analysed on its liveness, reversibility, boundedness and conservativeness based on the properties of augmented marked graphs.
Example 1 : The Dining Philosophers Problem (Version 1)
Six philosophers (H1, H2, H3, H4, H5 and H6) are sitting around a circular table for dinner. They are either meditating or eating the food placed at the centre of the table. There are six pieces of chopsticks (C1, C2, C3, C4, C5 and C6) shared by them for getting the food to eat, as shown in Figure 10. For one to get the food to eat, both the chopstick at the right hand side and the chopstick at the left hand side must be available. The philosopher then grasps both chopsticks simultaneously and then takes the food to eat. Afterwards, the chopsticks are released and returned to their original positions simultaneously.
Figure 10.
The dinning philosophers problem.
Figure 11 shows an augmented marked graph (N, M0; R), representing the dining philosophers problem (version 1). Table 1 shows the semantic meanings of the places and transitions. There are 24 R-siphons, namely, {r1, p61, p11}, {r1, p61, p12}, {r1, p62, p11}, {r1, p62, p12}, {r2, p11, p21}, {r2, p11, p22}, {r2, p12, p21}, {r2, p12, p22}, {r3, p21, p31}, {r3, p21, p32}, {r3, p22, p31}, {r3, p22, p32}, {r4, p31, p41}, {r4, p31, p42}, {r4, p32, p41}, {r4, p32, p42}, {r5, p41, p51}, {r5, p41, p52}, {r5, p42, p51}, {r5, p42, p52}, {r6, p51, p61}, {r6, p51, p62}, {r6, p52, p61} and {r6, p52, p62}. Each of these R-siphons contains a marked trap and would never become empty. Based on the results obtained in Section 4, (N, M0; R) is live and reversible. On the other hand, for the R-transform of (N, M0; R), every place belongs to a cycle. Based on the results obtained in Section 5, (N, M0; R) is bounded and conservative.
Example 2 : The Dining Philosophers Problem (Version 2)
The Dining Philosophers Problem is now modified as follows. For one to get the food to eat, he or she first grasps the chopstick at the right hand side if available, then grasps the chopstick at the left hand side if available, and then takes the food to eat. Afterwards, the chopsticks are released and returned to their original positions simultaneously.
Figure 11.
Augmented marked graph (Example 1).
Semantic meaning for places
Semantic meaning for transitions
p 11
H 1 is meditating.
t 11
H 1 takes the action to grasp C 1 and C 2 .
p 12
H 1 has got C 1 and C 2 and takes the food.
t 12
H 1 takes the action to return C 1 and C 2 .
p 21
H 2 is meditating.
t 21
H 1 takes the action to grasp C 2 and C 3 .
p 22
H 2 has got C 2 and C 3 and takes the food.
t 22
H 1 takes the action to return C 2 and C 3 .
p 31
H 3 is meditating.
t 31
H 1 takes the action to grasp C 3 and C 4 .
p 32
H 3 has got C 3 and C 4 and takes the food.
t 32
H 1 takes the action to return C 3 and C 4 .
p 41
H 4 is meditating.
t 41
H 1 takes the action to grasp C 4 and C 5 .
p 42
H 4 has got C 4 and C 5 and takes the food.
t 42
H 1 takes the action to return C 4 and C 5 .
p 51
H 5 is meditating.
t 51
H 1 takes the action to grasp C 5 and C 6 .
p 52
H 5 has got C 5 and C 6 and takes the food.
t 52
H 1 takes the action to return C 5 and C 6 .
p 61
H 6 is meditating.
t 61
H 1 takes the action to grasp C 6 and C 1 .
p 62
H 6 has got C 6 and C 1 and takes the food.
t 62
H 1 takes the action to return C 6 and C 1 .
r 1
C 1 is available for pick.
r 2
C 2 is available for pick.
r 3
C 3 is available for pick.
r 4
C 4 is available for pick.
r 5
C 5 is available for pick.
r 6
C 6 is available for pick.
Table 1.
Semantic meaning for the places and transitions in Fig. 11.
Figure 12 shows an augmented marked graph (N, M0; R), representing the dining philosophers problem (version 2). Table 2 shows the semantic meanings of the places and transitions. The set of places {r1, p13, r2, p23, r3, p33, r4, p43, r5, p53, r6, p63} is a R-siphon which would become empty after firing the sequence of transitions t11, t12, t13, t14, t15, t16. Based on the results obtained in Section 4, (N, M0; R) is neither live nor reversible. Deadlocks would occur, for example, after firing t11, t12, t13, t14, t15, t16. On the other hand, for the R-transform of (N, M0; R), every place belongs to a cycle. Based on the results obtained in Section 5, (N, M0; R) is bounded and conservative.
Manufacturing systems are typically shared resource systems, wherein the resources used to be maximally shared among different asynchronous processes. Moreover, every resource has a pre-defined capacity limit that can never be exceeded. Therefore, in manufacturing system design, a major design objective is to achieve a live, bounded and reversible system - liveness implies freeness of deadlock, boundedness implies absence of capacity overflow, and reversibility allows system recovery. Verification of the system liveness, boundedness and reversibility is essentially required, though very time-consuming.
Possessing a specific structure for representing shared resources, augmented marked graphs are often used for modelling manufacturing systems. By modelling a manufacturing system as an augmented marked graph, this section shows how the system liveness, boundedness and reversibility can be analysed, based on the properties of augmented marked graphs.
Semantic meaning for places
Semantic meaning for transitions
p 11
H 1 is meditating.
t 11
H 1 takes the action to grasp C 1 .
p 12
H 1 has got C 1 and prepares to pick C 2 .
t 12
H 1 takes the action to grasp C 2 .
p 13
H 1 has got C 1 and C 2 and takes the food.
t 13
H 1 takes the action to return C 1 and C 2 .
p 21
H 2 is meditating.
t 21
H 2 takes the action to grasp C 2 .
p 22
H 2 has got C 2 and prepares to pick C 3 .
t 22
H 2 takes the action to grasp C 3 .
p 23
H 2 has got C 2 and C 3 and takes the food.
t 23
H 2 takes the action to return C 2 and C 3 .
p 31
H 3 is meditating.
t 31
H 3 takes the action to grasp C 3 .
p 32
H 3 has got C 3 and prepares to pick C 4 .
t 32
H 3 takes the action to grasp C 4 .
p 33
H 3 has got C 3 and C 4 and takes the food.
t 33
H 3 takes the action to return C 3 and C 4 .
p 41
H 4 is meditating.
t 41
H 4 takes the action to grasp C 4 .
p 42
H 4 has got C 4 and prepares to pick C 5 .
t 42
H 4 takes the action to grasp C 5 .
p 43
H 4 has got C 4 and C 5 and takes the food.
t 43
H 4 takes the action to return C 4 and C 5 .
p 51
H 5 is meditating.
t 51
H 5 takes the action to grasp C 5 .
p 52
H 5 has got C 5 and prepares to pick C 6 .
t 52
H 5 takes the action to grasp C 6 .
p 53
H 5 has got C 5 and C 6 and takes the food.
t 53
H 5 takes the action to return C 5 and C 6 .
p 61
H 6 is meditating.
t 61
H 6 takes the action to grasp C 6 .
p 62
H 6 has got C 6 and prepares to pick C 1 .
t 62
H 6 takes the action to grasp C 1 .
p 63
H 6 has got C 6 and C 1 and takes the food.
t 63
H 6 takes the action to return C 6 and C 1 .
r 1
C 1 is available for pick.
r 2
C 2 is available for pick.
r 3
C 3 is available for pick.
r 4
C 4 is available for pick.
r 5
C 5 is available for pick.
r 6
C 6 is available for pick.
Table 2.
Semantic meaning for the places and transitions in Fig. 12.
Example 3. It is a FWS-200 Flexible Workstation System, extracted from the literature (Zhou & Venkatesh, 1999, pp. 121-124). The system consists of two robots R1 and R2, one feeder area and one PCB area, as shown in Figure 13. There are two asynchronous processes.
Production process 1 : R1 picks components from the feeder area, and moves into the PCB area for inserting components. The finished product is then moved out from the PCB area.
Production process 2 : R2 picks components from the feeder area, and moves into the PCB area for inserting components. The finished product is then moved out from the PCB area.
Figure 14 shows an augmented marked graph (N, M0; R), representing the FWS-200 flexible workstation system. Table 3 shows the semantic meanings of the places and transitions.
Figure 13.
The FWS-200 flexible workstation system.
Figure 14.
Augmented marked graph (Example 3).
For the augmented marked graph (N, M0; R) shown in Figure 14, every R-siphon would never become empty. Based on the results obtained in Section 4, (N, M0; R) is live and reversible. For the R-transform of (N, M0; R), every place belongs to a cycle. Based on the results obtained in Section 5, (N, M0; R) is bounded and conservative. It is then concluded that the FWS-200 flexible workstation system is live, bounded, reversible and conservative.
Semantic meaning for places
Semantic meaning for transitions
p 11
R 1 is ready
t 11
R 1 starts picking components
p 12
Components for R 1 are available
t 12
R 1 starts inserting components
p 13
R 1 is picking components from feeder
t 13
R 1 starts moving out the product
p 14
R 1 is inserting components in PCB area
t 21
R 2 starts picking components
p 21
R 2 is ready
t 22
R 2 starts inserting components
p 22
Components for R 2 are available
t 23
R 2 starts moving out the finished product
p 23
R 2 is picking components from feeder
p 24
R 2 is inserting components in PCB area
r 1
Feeder area is available
r 2
PCB area is available
Table 3.
Semantic meaning for the places and transitions in Fig. 14.
Example 4. It is a flexible assembly system, extracted from the literature (Proth & Xie, 1996, pp. 58-61). The system consists of three conveyors C1, C2 and C3 and three robots R1, R2 and R3, as shown in Figure 15. There are three asynchronous processes.
Assembly process 1 : C1 requests R1. After acquiring R1, it requests R2. After acquiring R2, it performs assembling and then releases both R1 and R2 simultaneously.
Assembly process 2 : C2 requests R2. After acquiring R2, it requests R3. After acquiring R3, it perform assembling and then releases both R2 and R3 simultaneously.
Assembly process 3 : C3 requests R3. After acquiring R3, it requests R1. After acquiring R1, it perform assembling and then releases both R3 and R1 simultaneously.
Figure 15.
The flexible assembly system.
Figure 16 shows an augmented marked graph (N, M0; R), representing the flexible assembly system. Table 4 shows the semantic meanings of the places and transitions.
Figure 16.
Augmented marked graph (Example 4).
Semantic meaning for places
Semantic meaning for transitions
p 12
C 1 is occupying R 1
t 11
C 1 starts acquiring R 1
p 13
C 1 is occupying R 1 and R 2
t 12
C 1 starts acquiring R 2
p 21
C 2 is ready
t 13
C 1 finishes assembling and release R 1 and R 2
p 22
C 2 is occupying R 2
t 21
C 2 starts acquiring R 2
p 23
C 2 is occupying R 2 and R 3
t 22
C 2 starts acquiring R 3
p 21
C 3 is ready
t 23
C 2 finishes assembling and release R 2 and R 3
p 22
C 3 is occupying R 3
t 31
C 3 starts acquiring R 3
p 23
C 3 is occupying R 3 and R 1
t 32
C 3 starts acquiring R 1
r 1
R 1 is available
t 33
C 3 finishes assembling and release R 3 and R 1
r 2
R 2 is available
r 3
R 3 is available
Table 4.
Semantic meaning for the places and transitions in Fig. 16.
For the augmented marked graph (N, M0; R) shown in Figure 16, there exists a R-siphon S = { p13, p23, p33, r1, r2, r3 } which becomes empty after firing the sequence of transitions t11, t21, t31 . Based on the results obtained in Section 4, (N, M0; R) is neither live nor reversible. A deadlock would occur after firing t11, t21, t31 . For the R-transform of (N, M0; R), every place belongs to a cycle. Based on the results obtained in Section 5, (N, M0; R) is bounded and conservative. It is then concluded that the flexible assembly system is non-live, non-reversible but bounded and conservative.
In the past decade, augmented marked graphs have evolved into a sub-class of Petri nets. They are often used for modelling shared resource systems, such as manufacturing systems. One major reason is that augmented marked graphs possess a special structure which is desirable for modelling shared resources. However, the properties of augmented marked graphs are not extensively studied. In the literature, there are a few published works on augmented marked graphs.
This paper consolidates our earlier works on augmented marked graphs with a special focus on liveness, boundedness, reversibility and conservativeness. We provide a number of characterisations for live and reversible augmented marked graphs. In particulars, some of these characterisations are based on cycles, instead of siphons. Besides, we introduce the R-transformation, on which characterisations for bounded and conservative augmented marked graphs are obtained. With these characterisations, some pretty simple conditions and procedures for checking the liveness, reversibility, boundedness and conservativeness of an augmented marked graph are derived. These have been illustrated using the dining philosophers problem.
Typically, in designing shared resource systems, one need to achieve design objectives on two folds. On one hand, the resources are scarce and should be maximally shared. On the other hand, the system should be carefully designed so that erroneous situations due to the sharing of resources, such as deadlock and capacity overflow, can be avoided. Yet, the verification of liveness, boundedness and reversibility is very difficult and time-consuming. This paper contributes to provide an effective means to analysing these essential properties. By modelling a shared resource system as an augmented marked graph, its liveness, boundedness, reversibility and conservativeness can be effectively analysed, based on the characterisations and properties of augmented marked graphs. We specifically show the application to the analysis of manufacturing systems which are typically shared resource systems. Promising results are obtained.
References
1.BarkaouiK.CouvreurJ. M.DutheilletC.1995 On Liveness in Extended Non Self-Controlling Nets, Application and Theory of Petri Nets, Lecture Notes in Computer Science, 9352544 , Springer-Verlag.
2.CheungK. S.2004 New Characterisations for Live and Reversible Augmented Marked Graphs, Information Processing Letters, 925239243 .
3.CheungK. S.2005 A Synthesis Method for Designing Shared-Resource Systems, Computing and Informatics, 246629653 .
4.CheungK. S.2006 Modelling and Analysis of Manufacturing Systems Using Augmented Marked Graphs, Information Technology and Control, 3511926 .
5.CheungK. S.2007 Boundedness and Conservativeness of Augmented Marked Graphs, IMA Journal of Mathematical Control and Information, 242235244 .
6.CheungK. S.ChowK. O.2005a Cycle-Inclusion Property of Augmented Marked Graphs, Information Processing Letters, 946271276 .
7.CheungK. S.ChowK. O.2005b Analysis of Manufacturing Systems Based on Augmented Marked Graphs, Proceedings of the IEEE International Conference on Computational Intelligence for Modelling, Control and Automation, 2847851 .
8.CheungK. S.ChowK. O.2005c A Synthesis Approach to Deriving Object-Based Specifications from Object Interaction Scenarios, In : Nilsson et al. (eds.), Advances in Information Systems Development- Bridging the Gap Between Academic and Industry, 647656 , Springer.
9.CheungK. S.ChowK. O.2006 Analysis of Capacity Overflow for Manufacturing Systems, Proceedings of the IEEE Conference on Automation Science and Engineering, 287292 .
10.CheungK. S.CheungT. Y.ChowK. O.2006 A Petri-Net-Based Synthesis Methodology for Use-Case-Driven System Design, Journal of Systems and Software, 796772790 .
11.ChuF.XieX.1997 Deadlock Analysis of Petri Nets Using Siphons and Mathematical Programming, IEEE Transactions on Robotics and Automation, 136793804 .
12.DeselJ.EsparzaJ.1995Free Choice Petri Nets, Cambridge University Press.
13.DeselJ.ReisigW.1998 Place Transition Petri Nets, Lectures on Petri Nets I : Basic Models, Lecture Notes in Computer Science, 1491122173 , Springer-Verlag.
14.HuangH. J.JiaoL.CheungT. Y.2003 Property-Preserving Composition of Augmented Marked Graphs that Share Common Resources, Proceedings of the IEEE International Conference on Robotics and Automation, 14461451 .
15.JengM. D.XieX.HuangY.2000 Manufacturing Modeling Using Process Nets with Resources, Proceedings of the IEEE International Conference on Robotics and Automation, 21852190 .
16.JengM. D.XieX.PengM. Y.2002 Process Nets with Resources for Manufacturing Modeling and their Analysis, IEEE Transactions on Robotics and Automation, 186875889 .
17.MurataT.1989 Petri Nets : Properties, Analysis and Applications, Proceedings of the IEEE, 774 , 541580 .
18.PetersonJ. L.1981Petri net theory and the modeling of systems, Prentice Hall.
19.ProthJ. M.XieX.1996Petri Nets : A Tool for Design and Management of Manufacturing Systems, Wiley.
20.ReisigW.1985Petri Nets : An Introduction, Springer-Verlag.
21.ZhouM. C.VenkateshK.1999Modeling, Simulation and Control of Flexible Manufacturing Systems : A Petri Net Approach, World Scientific.
Open access
