Informatica 32 (2008) 85-94 85 Augmented Marked Graphs King-Sing Cheung University of Hong Kong Pokfulam, Hong Kong E-mail: ks.cheung@hku.hk Keywords: augmented marked graph, Petri net, liveness, boundedness, reversibility, conservativeness Received: August 27, 2007 Augmented marked graphs possess some structural characteristics desirable for modelling shared resource systems such as manufacturing systems. However, there are only a few known properties on augmented marked graphs, and these known properties are mainly on liveness and reversibility. In this paper, the properties of augmented marked graphs are reviewed extensively. Siphon-based and cycle-based characterisations for liveness and reversibility as well as transformation-based characterisations for boundedness and conservativeness are proposed. Pretty simple conditions and procedures are then derived for checking the liveness, reversibility, boundedness and conservativeness of augmented marked graphs. The dining philosopher problem is used for illustration. Povzetek: Opisane so lastnosti grafov za predstavitev sistemov z deljenimi viri. 1 Introduction Augmented marked graphs were first introduced by Chu and Xie [1]. They are not well known as compared to other sub-classes of Petri nets such as free-choice nets [2], 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 [1, 3, 4, 5, 6, 7]. In the literature, the studies of augmented marked graphs mainly focus on deadlock-freeness, liveness and reversibility. Based on 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 [1]. However, this involves analysis on the flow of tokens during execution and the checking cannot be simply made by looking into the structure. Chu and Xie also proposed a siphon-based characterisation for live and reversible augmented marked graphs but it provides a sufficient condition only. The boundedness and conservativeness of augmented marked graphs were not investigated. There are other studies of augmented marked graphs, which are mainly on the property-preserving synthesis or composition of augmented marked graphs. Jeng proposed a synthesis method of process nets for manufacturing system design [4, 5]. (Note : Process nets broadly cover augmented marked graphs.) Based on siphons and the firability of transitions, sufficient conditions for liveness and reversibility are derived. Huang also investigated the composition of augmented marked graphs via common resource places, so that some essential properties such as liveness, boundedness and reversibility can be preserved under certain conditions [6]. In our previous works on augmented marked graphs, we proposed new characterisations for live and reversible augmented marked graphs as well as the synthesis of augmented marked graphs for system design [7, 8, 9, 10, 11]. This paper extends our previous works with a focus on the properties of augmented marked graphs. It reports the following two contributions. First, we propose a number of characterisations for live and reversible augmented marked graphs, based on siphons and cycles. In particular, a new property called R-inclusion property is introduced to characterise the siphon-trap property of augmented marked graphs. With this property, a pretty simple necessary and sufficient condition for live and reversible augmented marked graphs is then proposed. Second, for analysis of the boundedness and conservativeness of augmented marked graphs, a R-transform is introduced to transform an augmented marked graph into marked graphs. With the R-transform, a pretty simple necessary and sufficient condition for bounded and conservative augmented marked graphs is proposed. These characterisations will be illustrated using the dining philosopher problem. 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 briefly introduces augmented marked graphs. Section 4 focus on liveness and reversibility of augmented marked graphs, where siphon-based and cycle-based characterisations are proposed. Section 5 then focus on boundedness and conservativeness of augmented marked graphs, where transformation-based characterisations are proposed. Section 6 illustrates these characterisations using the dining philosopher example. Finally, Section 7 concludes our results. It should be noted that, in this paper, proofs of the proposed properties are shown in the appendix. 82 Informatica 32 (2008) 79-84 M. Grobelnik et al. 2 Preliminary This section provides the preliminaries to be used in this paper for those readers who are not familiar with Petri nets [12, 13, 14, 15]. A place-transition net (PT-net) is a directed graph consisting of two sorts of nodes called places and transitions, such that no arcs connect two nodes of the same sort. Graphically, a place is denoted by a circle, a transition by a box, and an arc by a directed line. A Petri net is a PT-net with tokens assigned to its places, and the token distribution is denoted by a marking. A Petri net is usually used to represent a discrete system, where the places denote conditions, the transitions denote events and the arcs between places and transitions denote the relationship between conditions and events. Definition 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 c (P x T) u (T x 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. Let N = < P, T, F, W ) be a PT-net. For any x e (P u T), •x = { y | (y, x) e F } and x^ = { y | (x, y) e 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 = { xu x2, ..., xn } can be written as •X and X^ respectively, where •X = •xi u % u ... u •xn and X^ = x/ u x/ u ... u xnV Definition 3. For a PT-net N = < P, T, F, W ), a path is a sequence of places and transitions p = ( x1, x2, ..., xn ), such that (x;, x1+1) e F for i = 1, 2, ..., n-1. p is said to be elementary if and only if it contains no duplicate places or transitions. Definition 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) e F. Definition 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. Semantically, a marking represents the state of a Petri net. The initial marking specifically represents the initial state of a Petri net. A transition is enabled and can be fired at a state (marking) where all the places in its pre-set hold tokens. On firing the transition, tokens will be moved from the places in its pre-set to the places in its post-set. The firing of a transition is formally defined as follows. Definition 6. For a PT-net (N, M0), a transition t is said to be enabled at a marking M if and only if V p e •t : M(p) > W(p,t). On firing t, M is changed to M' such that V p e P : M'(p) = M(p) - W(p,t) + W(t,p). In notation, M [N,t) M' or M [t) M'. Definition 7. For a PT-net (N, M0), a sequence of transitions ct = ( t1, t2, ..., tn ) is called a firing sequence if and only if M0 [t1) ... [tn) Mn. In notation, M0 [N,ct) Mn or M0 [ct) Mn. Definition 8. For a PT-net (N, M0), a marking M is said to be reachable if and only if there exists a firing sequence ct such that M0 [ct) M. In notation, M0 [N,*) M or M0 [*) M. [N, M0) or [M0) represents the set of all reachable markings of (N, M0). The structure of a PT-net can be represented by a matrix called incidence matrix. Definition 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 x 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. Liveness, boundedness, safeness, reversibility and conservativeness are best known properties of Petri nets. Liveness implies freeness of deadlocks. Boundedness and safeness imply freeness of capacity overflow. Reversibility refers to the capability of being reinitialised from any reachable states. Conservativeness is a special form of boundedness. Definition 10. For a PT-net (N, M0), a transition t is said to be live if and only if V M e [M0), 3 M' : M [*) M' [t). (N, M0) is said to be live if and only if every transition is live. Definition 11. For a PT-net (N, M0), a place p is said to be k-bounded if and only if V M e [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 12. A PT-net (N, Mc) is said to be reversible if and only if V M e [M0) : M [*) M0. Definition 13. For a PT-net N = < P, T, F, W ), a place invariant is a |P|-vector a > 0 such that aV = 0, where V is the incidence matrix of N. Definition 14. A PT-net is said to be conservative if and only if there exists a place invariant a > 0. Figure 1 shows an ordinary PT-net which is live, bounded, safe, reversible and conservative. Figure 1: A live, bounded, safe, reversible and conservative PT-net. Property 1. A PT-net (N, M0) is bounded if it is conservative [14, 15]. AUGMENTED MARKED GRAPHS Informatica 32 (2008) 85-94 87 Definition 15. For a PT-net N, a set of places S is called a siphon if and only if •S c S*. S is said to be minimal if and only if there does not exist another siphon S' in N such that S' c S. Definition 16. For a PT-net, a set of places T is called a trap if and only if T* c •T. Definition 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). A well known sub-class of Petri nets, marked graphs possess many special properties pertaining to its liveness, boundedness and reversibility. Definition 18. A marked graph is an ordinary PT-net N = < P, T, F, W > such that V p e P : |*p| = |p*| = 1. Property 2. A marked graph (N, M0) is live if and only if every cycle is marked by M0 [13, 14]. Property 3. A live marked graph (N, M0) is bounded if and only if every place belongs to a cycle marked by M0 [13, 14]. Property 4. A live and bounded marked graph is reversible [13, 14]. Property 5. For a marked graph, the corresponding place vector of a cycle is a place invariant [13, 14]. Figure 2 shows a marked graph which is live, bounded, safe and reversible. Places < pi, p3, p6, p7, p4 > form a cycle. The place vector is a place invariant. Figure 3 shows a typical augmented marked graph (N, M0; R), where R = { ru r2 }. For rb Dri = { , }. For r2, Dr2 = { , }. Pi L-Jti ( • ) P2 t2 C) P3 CP t3 P4 nh t4 f J P5 t5 (jP6 qb te P7 ( ; Pa t7 ( • ) pi Figure 2: A live, bounded, safe and reversible marked graph. 3 Augmented marked graphs Augmented marked graphs were first introduced by Chu and Xie [1]. This section briefly describes augmented marked graphs. Definition 19. An augmented marked graph (N, M0; R) is a PT-net (N, M0) with a specific subset of places R, such that : (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 e R, there exist kr > 1 pairs of transitions Dr = { , , ..., }, such that r* = { ts1, ts2, ..., tskr } C T and *r = { tM, th2, ..., thkr } c T and that, for each e Dr, there exists in (N', M0') an elementary path pri connecting tsi to thi. (d) In (N', M0'), every cycle is marked and no pri is marked. Figure 3: An augmented marked graph. Augmented marked graphs possesses a number of special properties pertaining to liveness, boundedness, reversibility and conservativeness. In the following sections, these properties are thoroughly investigated. 4 Liveness and reversibility This section focus on the liveness and reversibility of augmented marked graphs. After reporting several known properties, some siphon-based and cycle-based characterisations for live and reversible augmented marked graphs are proposed. Property 6. An augmented marked graph is live if and only if it does not contain any potential deadlock [1]. (Note : A potential deadlock is a siphon which would eventually become empty.) Property 7. An augmented marked graph is reversible if it is live [1]. Property 8. An augmented marked graph is live and reversible if and only if every minimal siphon would never become empty. Property 9. An augmented marked graph (N, Mo; R) is live and reversible if every minimal siphon, which contains at least one place of R, contains a marked trap [1]. For the augmented marked graph (N, M0; R) shown in Figure 3, the minimal siphons are : { p1, p5, p8 }, { r1, p2, p4, p6, p7, p9 }, { r1, p2, p4, p6, p7, p10 }, { r2, p3, p5, p6, p8, p9 } and { r2, ps, 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. The places and transitions generated by cycles are defined as follows. Definition 20. For a PT-net N, On is defined as the set of all cycles in N. Definition 21. Let N be a PT-net. For a subset of cycles Y c On, P[Y] is defined as the set of places in Y, and T[Y] = *P[Y] n P[Y]* is defined as the set of transitions generated by Y. 82 Informatica 32 (2008) 79-84 M. Grobelnik et al. For clarity in presentation, P[{y}] and T[{y}] can be written as P[y] and T[y], to denote the set of places in a cycle y and the set of transitions generated by y, respectively. Definition 22. For a PT-net N, an elementary path p = ( xi, x2, ..., xn ) is said to be conflict-free if and only if, for any transition xi in p, j ^ (i -1) ^ Xj g ^Xj. Property 10. Let S be a minimal siphon of a PT-net. For any p, p' e S, there exists in S a conflict-free path from p to p' [16]. Property 11. For a minimal siphon S of an augmented marked graph (N, M0; R), there exists a set of cycles Y ç On such that P[Y] = S. Property 12. Every cycle in an augmented marked graph is marked. Property 13. Every siphon in an augmented marked graph is marked. Property 14. Let (N, M0; R) be an augmented marked graph. For every r e R, there exists a minimal siphon which contains only one marked place r. Consider the augmented marked graph (N, M0; R) shown in Figure 3. Every minimal siphon is covered by cycles. Consider a minimal siphon S1 = { r1, p2, p4, p6, p7, p9 }. There exists a set of cycles Y1 = { Yn, Y12 }, where Yii = < ri, p4, p7 ) and Y12 = < rb p2, p6, p9 ), such that Si = P[Y1]. Consider another minimal siphon S2 = { r2, p3, p5, p6, p8, p10 }• There exists a set of cycles Y2 = { y21, y22 }, where Y21 = < r2, p5, p8 ) and Y22 = < r2, p3, p6, pi0 ), such that S2 = P[Y2]. For S1, r1 e R is the only one marked place. Also, for S2, r2 e R is the only one marked place. For an augmented marked graph, minimal siphons can be classified into R-siphons and NR-siphons. Based on R-siphons and NR-siphons, some characterisations for augmented marked graphs are proposed. Definition 23. 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 24. 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 25. Let N be a PT-net. For a set of places Q in N, On[Q] is defined as the set of cycles that contains at least one place in Q. For clarity in presentation, 0N[{p}] can be written as 0N[p] to denote the set of cycles that contains a place p. Property 15. For an augmented marked graph (N, M0; R), a R-siphon is covered by a set of cycles Y ç on[R]. Figure 4 shows another augmented marked graph (N, M0; R), where R = { r1, r2 }. There are five minimal siphons, namely, Si = { ru p3, p4, p7, p8 }, S2 = { ru p3, p5, p7, p8 }, S3 = { r2, p2, p4, p6, p8, p9, pi0 }, S4 = { r2, p2, p5, p6, p8, p9, pi0 } and S5 = { pi, p3, p7 }. Si, S2, S3 and S4 are R-siphon as they contain at least one place in R. S5 is a NR-siphon which does not contain any place in R. For (N, M0; R), every R-siphon is covered by a set of cycles in On[R]. For example, Si = { ri, p3, p4, p7, p8 } is covered by a set of cycles Yi = { Yn, Yi2 } Ç On[R], where Yii = < ri, p3, p7 ) and Yi2 = < ri, p4, p8 ). Figure 4: Another augmented marked graph. Property 16. Let S be a R-siphon of an augmented marked graph (N, M0; R). For every t e (S^ \ •S), there does not exist any s e (S \ R) such that t e s^. Property 17. For an augmented marked graph (N, M0; R), a NR-siphon contains itself as a marked trap and would never become empty. Property 18. An augmented marked graph (N, M0; R) is live and reversible if and only if no R-siphons eventually become empty. Property 19. An augmented marked graph (N, M0; R) satisfies the siphon-trap property if and only if every R-siphon contains a marked trap. Consider the augmented marked graph (N, M0; R) shown in Figure 4. Every R-siphon contains a marked trap. Each of the R-siphons Si = { rb p3, p4, p7, p8 }, S2 = { ri, p3, p5, p7, p8 }, S3 = { r2, p2, p4, p6, ps, p9, pi0 } and S4 = { r2, p2, p5, p6, p8, p9, pi0 } contains a marked trap and would never become empty. (N, M0; R) is live and reversible. Property 20. (characterisation of Property 9) An augmented marked graph (N, M0; R) is live and reversible if every R-siphon contains a marked trap. Property i8 provides a simple necessary and sufficient condition for live and reversible augmented marked graphs. With Properties 18 and 20, we can determine if an augmented marked graph is live and reversible based on R-siphons. Besides, Property 15 provides a characterisation for R-siphons so that R-siphons can be identified by finding cycles in Qn[R]- We may now derive a strategy for checking the liveness and reversibility of an augmented marked graph (N, Mo; R) : (a) Find all R-siphons based on Qn[R]- (b) Check if every R-siphon contains a marked trap. If yes, report (N, M0; R) is live and reversible. Otherwise, go to (c). (c) For each R-siphon which does not contain any marked trap, check if it would never become empty. If yes, report (N, M0; R) is live and reversible. Otherwise, report (N, M0; R) is neither live nor reversible. AUGMENTED MARKED GRAPHS Informatica 32 (2008) 85-94 89 In the following, conflict-free cycles are introduced. Based on conflict-free cycles, a new property called R-inclusion is proposed. It is then used for characterising liveness and reversibility of augmented marked graphs. Definition 26. For a PT-net N, a set of cycles Y c Qn is said to be conflict-free if and only if, for any q, q' e P[Y], there exists in P[Y] a conflict-free path from q to q'. Figure 5 shows a PT-net N. Consider three cycles y1; Y2, Ys e QnIpb], where yi = < ps, p2, pv X Y2 = < ps, p4 > and Ys = < ps, pi, p6, pio, ps >. The set of cycles Yj = { y1; Y2 } is conflict-free because for any q, q' e P[Y1], there exists in P[Y1] a conflict-free path from q to q'. The set of cycles Y2 = { y2, y3 } is not conflict-free. We have p4, p8 e P[Y2]. p4 is connected to p8 via only one path p = ( p4, t5, ps, ti, pi, ts, p6, t6, pio, t9, p8 > in Y2, and p is not conflict-free because p4, p8 e *t5. Figure 6: An augmented marked graph for illustration of R-inclusion. Figure 7 shows another augmented marked graph (N, M0; R). For ri e R, there exists a set of cycles Yi = { yn, Y12 } ç Qn[R], where yn = < ri, ps > and yi2 = < rb ps, r2, P6 >. 'ri = { ts, t6 } ç T[Yi] = { t3, t4, ts, t6 } but rr = { t2, t3 } £ T[Yi]. For r2 e R, there exists a set of cycles Y2 = { Y2i, Y22 } Ç Qn[R], where y2i = < r2, p6 > and Y22 = < r2, p6, ri, ps >. • r2 = { ts, t6 } ç T[Y2] = { t3, t4, ts, t6 } but r2* = { ti, t4 } £ T[Y2]. Both ri and r2 do not satisfy the R-inclusion property. Figure 5: A PT-net for illustration of conflict-free cycles. Property 21. Let S be a minimal siphon of an augmented marked graph (N, M0; R), and Y ç QN be a set of cycles such that S = P[Y]. Then, Y is conflict-free. For the augmented marked graph shown in Figure 3, { ri, p2, p4, p6, p7, p9 } is a minimal siphon covered by a set of cycles { ( ri, p4, p7 ), ( ri, p2, p6, p9 ) } which is conflict free. { r2, p3, p5, p6, p8, pi0 } is another minimal siphon covered by a set of cycles { ( r2, p5, p8 ), ( r2, p3, p6, pi0 ) } which is conflict-free. For the augmented marked graph shown in Figure 4, { ri, p3, p4, p7, p8 } is a minimal siphon covered by a set of cycles { ( ri, p3, p7 ), ( ri, p4, p8 ) } which is conflict free. { ri, p3, p5, p7, p8 } is another minimal siphon covered by a set of cycles { ( ri, p3, p7 ), < ri, p5, p8 ) } which is conflict free. Definition 27. Let (N, M0; R) be an augmented marked graph. A place r e R is said to satisfy the R-inclusion if and only if, for any set of cycles Y ç QN[R] such that Y is conflict-free, •r ç T[Y] ^ r^ ç T[Y]. Figure 6 shows an augmented marked graph (N, M0; R), where R = { ri, r2 }. Consider ri. For any set of cycles Yi ç Qn[R] such that Yi is conflict-free, •ri ç T[Yi] ^ r/ ç T[Yi]. Next, consider r2. For any set of cycles Y2 ç Qn[R] such that Y2 is conflict-free, 'r2 ç T[Y2] ^ r/ ç T[Y]. Both ri and r2 satisfy the R-inclusion. P5 / X^ \ 1 )P6 V / \ \ CPV Figure 7: Another augmented marked graph for illustration of R-inclusion. Property 22. For an augmented marked graph (N, M0; R), a R-siphon S contains itself as a marked trap if every place r e R in S satisfies the R-inclusion property. Property 23. An augmented marked graph (N, M0; R) satisfies the siphon-trap property if and only if every place r e R satisfies the R-inclusion property. Property 24. An augmented marked graph (N, M0; R) is live and reversible if every place r e R satisfies the R-inclusion property. Consider the augmented marked graph (N, M0; R) shown in Figure 6. We have R = { ri, r2 }, where both ri and r2 satisfy the R-inclusion property. Any R-siphon, such as { ri, ps, p4 } or { r2, p5, p6 }, contains itself as a marked trap. (N, M0; R) satisfies the siphon-trap property, and is live and reversible. Property 24 provides a cycle-based condition for live and reversible augmented marked graphs. We need to check the R-inclusion property which involves finding cycles and checking their pre-sets and post-sets. 82 Informatica 32 (2008) 79-84 M. Grobelnik et al. Based on Properties 15, 18, 20, 22 and 24, we 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. (a) Check if every r e R satisfies the R-inclusion property. If yes, report (N, M0; R) is live and reversible. Otherwise go to (b). (b) Let R' c R be the set of places which do not satisfy the R-inclusion property. Based on QN[R'], find all R-siphons which contain at least one place in R'. (c) For each R-siphon identified in (b), check if it contains a marked trap. If yes, report (N, M0; R) is live and reversible. Otherwise, go to (d). (d) For each R-siphon identified in (b) that does not contain any marked trap, check if it would never become empty. If yes, report (N, M0; R) is live and reversible. Otherwise, report (N, M0; R) is neither live nor reversible. 5 Boundedness and conservativeness This section focus on the boundedness and conservativeness of augmented marked graphs, which are less studied in the literature. Some transform-based characterisations for bounded and conservative augmented marked graphs are proposed. In the following, we introduce a new transformation called R-transform for augmented marked graphs. It simply transforms an augmented marked graphs (N, M0; R) into a number of marked graphs by replacing each place in R by a set of places. Property 25. Let (N, M0; R) be an augmented marked graph to be transformed into (N', M0') as follows. For each place r e 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 p^ = { tsi } and •pi = { th } for i = 1, 2, ..., kr. Then, (N', M0') is a marked graph. Definition 28. Let (N, M0; R) be an augmented marked graph. The marked graph (N', M0') transformed from (N, M0; R) as stated in Property 25 is called the R-transform of (N, M0; R). Property 26. The R-transform of an augmented marked graph is live. Figure 8 shows an augmented marked graph. Figure 9 shows its R-transform, where r is replaced by { q1, q2 }. / Hp t, rp t2 \ / rp ts \ / C)P4 v)P5\ ()P6\ •J p, r~| t4 (•) r, ¿p t5 (•) P2 \ ()p? Cjp®/ \ C)P9/ \ czzi t6 cb ty / \ iz::] ta Figure 8: An augmented marked graph for illustration of R-transform. Figure 9: The R-transform of the augmented marked graph shown in figure 8. Property 27. Let (N', M0') be the R-transform of an augmented marked graph (N, M0; R), where r e 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 ai of N' such that ai[qi] = 1 and ai[s] = 0 for any place s e P0 \ {qi}. Property 28. Let (N, M0; R) be an augmented marked graph, where R = { ru 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 a of N' such that a > 0 and a[qi] = a[q2] = ... = a[qk] for each Qi = { qu q2, ..., qk }. Consider the R-transform (N', M0') shown in Figure 9. It is a live marked graph. For q1, there exists a place invariant a1, such that a1[q1] = 1 and a1[q2] = a1[p1] = ai[p2] = 0. For q2, there also exists a place invariant a2, such that a2[q2] = 1 and a2[q1] = a2[p1] = a2[p2] = 0. In (N', M0'), every place belongs to a cycle. There also exists a place invariant a > 0, where a[q1] = a[q2]. Based on R-transform, a necessary and sufficient condition for bounded and conservative augmented marked graphs is proposed. Property 29. 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. With Properties 29, we derive the following strategy for checking the boundedness and conservativeness of an augmented marked graph (N, M0; R) : (a) Create the R-transform (N', M0') of (N, M0; R). (b) For each place p in (N', M0'), check if there exists a cycle that contains p. If yes, report (N, M0; R) is bounded and conservative. Otherwise, report (N, M0; R) is neither bounded nor conservative. Property 30. 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. Consider the augmented marked graph (N, M0; R) shown in Figure 8, and the R-transform (N', M0') of (N, M0; R) in Figure 9. Every place in (N', M0') belongs to a cycle. (N, M0; R) is bounded and conservative. (N', M0') is also bounded and conservative. AUGMENTED MARKED GRAPHS Informatica 32 (2008) 85-94 91 Figure 10 shows an augmented marked graph (N, M0; R), and Figure 11 shows the R-transform (N', M0') of (N, M0; R). For (N', M0'), p3 does not belong to any cycle. Also, p8 does not belong to any cycle. (N, M0; R) is neither bounded nor conservative. Figure 10: Another augmented marked graph for illustration of R-transform. Figure 11: The R-transform of the augmented marked graph shown in figure 10. 6 The dining philosopher problem This section illustrates the properties of augmented marked graphs obtained in the previous sections using the dining philosopher problem. The dining philosopher problem (version 1) : Six philosophers (Hi, 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 12. 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 13 shows the augmented marked graph (N, M0; R) which represents the dining philosopher problem (version 1). © _ © /^C © ) © © © Figure 12: The dinning philosopher problem. Figure 13 : The dining philosopher problem (version 1). Semantic meaning for places and transitions p11 H is meditating. p12 H has got C and C2 and takes the food. p21 H2 is meditating. p22 H2 has got C2 and C3 and takes the food. p31 H3 is meditating. p32 H3 has got C3 and C4 and takes the food. p41 H4 is meditating. p42 H4 has got C4 and C5 and takes the food. p51 H5 is meditating. p52 H5 has got C5 and C6 and takes the food. p61 H6 is meditating. p62 H6 has got C6 and C1 and takes the food. r1 C1 is available for pick. r2 C2 is available for pick. r3 C3 is available for pick. r4 C4 is available for pick. r5 C5 is available for pick. r6 C6 is available for pick. t11 H1 takes the action to grasp C1 and C2. t12 H1 takes the action to return C1 and C2. t21 H1 takes the action to grasp C2 and C3. t22 H1 takes the action to return C2 and C3. t31 H1 takes the action to grasp C3 and C4. t32 H1 takes the action to return C3 and C4. t41 H1 takes the action to grasp C4 and C5. t42 H1 takes the action to return C4 and C5. t51 H1 takes the action to grasp C5 and C6. t52 H1 takes the action to return C5 and C6. t61 H1 takes the action to grasp C6 and C1. t62 H1 takes the action to return C6 and C1. 82 Informatica 32 (2008) 79-84 M. Grobelnik et al. For (N, M0; R), every R-siphons contains a marked trap and would never become empty. Every place in its R-transform belongs to a cycle. Based on the results obtained in Sections 4 and 5, (N, M0; R) is live, bounded, reversible and conservative. The dining philosopher problem (version 2) : The Dining Philosopher Problem is revised. 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 14 shows the augmented marked graph (N, M0; R) which represents the dining philosopher problem (version 2). 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 ) It follows from Property 6 that every siphon (and hence, every minimal siphon) would never become empty. Proof of Property 11. Let S = { pi, p2, ..., pn }. For each pi, by definition of augmented marked graphs that •p! ^ 0. Then, there exists pj e S, where pj ^ p;, such that (pj n •pO ^ 0. Since S is a minimal siphon, according to Property 10, pi connects to pj via a conflict-free path in S. Since pj connects to p;, this forms a cycle in S, where pi e P[yj] ç S. Let Y = { yb Y2, ..., Yn }. We have P[Y] = P[Y1] u P[Y2] u .. u P[Yn] Ç S. On the other hand, S ç (P[Y1] u P[Y2] u ... u P[Yn]) = P[Y] because S = { pu p2, ..., pn }. Hence, P[Y] = S. Proof of Property 12. (by contradiction) Let (N, Mo; R) be an augmented marked graph. Suppose there exists a cycle y in (N, M0; R), such that y is not marked. y does not contain any place in R, and also exists in the net (N', Mo') obtained from (N, M0; R) after removing the places in R and their associated arcs. However, by definition of augmented marked graphs, y is marked. Proof of Property 13. For an augmented marked graph, according to Properties 11 and 12, every minimal siphon contains cycles and is marked. Hence, every siphon, which contains at least one minimal siphon, is marked. Proof of Property 14. Let Dr = { , , ..., }, where r^ = { t^, t^,..., U } and •r = { tM, tK, ... , thn }. For each e Dr, tsi connects to thi via an elementary path pi which is not marked. Let S = P1 u P2 u ... u Pn u { r }, where Pj is the set of places in pi. We have •Pi ç (Pf u r^) because, for each p e Pi, | •p | = | p^ | = 1. Then, (•P1 u T2 u ... u ^Pn) ç (P/ u P/ u ... u P^ u r^). Besides, •r = { th1, th2, ..., thn } ç (P/ u P/ u ... u Pn7 Hence, •S = (•P1 u *P2 u ... u *Pn u •r) ç (Pj u P/ u ... u Pn^ u r^) = SV 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 13, S' is marked. Since r is the only one marked place in S, r is also the only one marked place in S'. Proof of Property 15. (By contradiction) Let S be a R-siphon. According to Property 11, S is covered by cycles. Suppose there exists a cycle y in S, such that y g qn[R]. By definition of augmented marked graphs, for any p e P[y], | •p | = | p^ | = 1. Hence, *P[y] = P[YT, and P[Y] is a siphon. Since there exists a place r e R such that r e S but r g P[y], we have P[y] c S. However, since S is a minimal siphon, there does not exists any siphon S' = P[Y] c S. 82 Informatica 32 (2008) 79-84 M. Grobelnik et al. Proof of Property 16. (by contradiction) Suppose there exists s e (S \ R) such that t e sV By definition of augmented marked graphs, | •s | = | s^ | = 1. S is covered by cycles in accordance with Property 15. Hence, t is the one and only one transition in s^, where t e T[Y] = (S^ n •S). This however contradicts t e (S^ \ •S). Proof of Property 17. Let S be a NR-siphon. According to Property 13, S is marked. By definition of augmented marked graphs that, for any s e 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. Proof of Property 18. (<^) According to Property 17, a NR-siphon would never become empty. Given that no R-siphons (and hence, no minimal siphon) eventually become empty, according to Property 8, (N, M0; R) is live and reversible. It follows from Property 6 that no R-siphons eventually become empty. Proof of Property 19. (<^) According to Property 17, a NR-siphon contains a marked trap. Given that every R-siphon contains a marked trap, every minimal siphon contains a marked trap. Since R-siphons are minimal siphons, every R-siphon contains a marked trap. Proof of Property 20. For (N, M0; R), if every R-siphon contains a marked trap, according to Property 19, the siphon-trap property is satisfied. Hence, every minimal siphon contains a marked trap and would never become empty. It then follows from Property 8 that (N, M0; R) is live and reversible. Proof of Property 21. Since S is a minimal siphon, according to Property 10, for any q, q' e S = P[Y], there exists in S = P[Y] a conflict-free path from q to q'. Hence, Y is conflict free. Proof of Property 22. Let S = { pi, p2, ..., pn }. According to Property 13, S is marked. It follows from Properties 15 and 21 that there exists a set of cycles Y c On[R], such that Y is conflict-free and P[Y] = S. Since S is a siphon, for each pi e S, •pi c (•S n S^) = CP[Y] n P[Yf) = T[Y]. In case pi g R, pf c T[Y] because | •pi | = | pf | = 1. In case pi e R, given that pi satisfies the R-inclusion property, pf c T[Y]. Every p^ c T[Y] = fP[Y] n P[Yf) and p' c ^P[Y] = •S. Since S^ = (p/ u p2^ u ... u pO c •S, S is also a trap. Proof of Property 23. It follows from Properties 19 and 22. (^ by contradiction) Suppose there exists r e R, not satisfying the R-inclusion property. According to Property 14, there exists a R-siphon S, in which r is the only marked place. It follows from Properties 15 and 21 that there exists Y c QN[R], such that Y is conflict-free and S = P[Y]. According to Property 19, S contains a marked trap Q. Then, r e Q and r^ c CQ n Q^). Since S is a siphon, we have •r c fS n S^) = CP[Y] n P[Yf) = T[Y]. However, as r does not satisfy the R-inclusion property, r^ & T[Y] = fP[Y] n P[Yf) = CS n S^), implying r^ & CQ n Q^). Proof of Property 24. According to Property 23, (N, M0; R) satisfies the siphon-trap property. It follows from Property 20 that (N, M0; R) is live and reversible. Proof of Property 25. For each place p g R in N, M0; R), | •p | = | p^ | = 1. Each place r e R is replaced by a set of places { p1, p2, ..., pkr }, where | ^ | = | p^ | = 1 for i = 1, 2, ..., kr. Hence, for every place q in N', | •q | = | q^ | = 1. (N', M0') is a marked graph. Proof of Property 26. Let (N', M0') be the R-transform of an augmented marked graph (N, M0; R). As the transformation does not create cycles, cycles in (N', M0') exist in (N, M0; R). According to Property 12, cycles in (N, M0; R) are marked, and hence, cycles in (N', M0') are marked. Since (N', M0') is a marked graph, it follows from Property 2 that (N', M0') is live. Proof of Property 27. Let Dr = {, , ..., }. By definition of augmented marked graphs, for each , there exists an unmarked path p = in (N, M0; R). Hence, p also exists as an unmarked path in (N', Mo'), and p together with qi forms a cycle yi which is marked at qi only. Since (N', M0') is a marked graph, according to Property 5, the corresponding vector of yi is a place invariant ai of N'. Since qi is the only one marked place in yi, ai[qi] = 1 and ai[s] = 0 for any s e P0 \ {qi}. Proof of Property 28. Let P = { p1, p2, ..., pn } be the places in N', and P0 c P be those marked places. Since each pi belongs to a cycle yi and (N', M0') is a marked graph, according to Property 5, the corresponding vector of yi is a place invariant ai' of N'. Then, a' = a1' + a2' + ... + an' > 0 is a place invariant of N'. Consider Qi = { q1, q2, ..., qk }. Let qm e Qi such that a'[qm] > a'[qj] for any qj e Qi. For each qj, according to Property 27, there exists a place invariant a/ > 0 such that aj'[qj] = 1 and aj'[s] = 0 for any s e P0 \ {qj}. There also exists a place invariant a" = a' + ha/, where h > 1, such that a"[qj] = a"[qm] and a"[s] = a'[s] for any s e P0 \ {qj}. Therefore, there eventually exists a place invariant a of N' such that a[q1] = a[q2] = ... = a[qk]. Proof of Property 29. (<^) Let R = { rb r2, ..., rn }, where each ri is being 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 28, there exists a place invariant a' of N' such that a' > 0 and a'[q1] = a'[q2] = ... = a'[qk] for each Qi = { q1, q2, ..., qk }. Intuitively, there also exists a place invariants a of N such that a > 0 and a[ri] = a'[q1] = a'[q2] = ... = a'[qk] for each Qi. Hence, (N, M0; R) is conservative. According to Property 1, (N, M0; R) is also bounded. Since (N, M0; R) is conservative, there exists a place invariant a of N such that a > 0. Consider each ri e R which is being replaced by Qi = { q1, q2, ..., qk }. Intuitively, there also exists a place invariant a' of N' such that a' > 0 and a'[q1] = a'[q2] = ... = a'[qk] = a[ri] and a'[s] = a[s] for any s e P'\Qi. Hence, (N', M0') is conservative. It follows from Property 1 that (N', M0') is also bounded. Since (N', M0') is a marked graph, according to Property 3, every place in (N', M0') belongs to a cycle. Proof of Property 30. It follows from Properties 3 and 29.