Augmented marked graphs.

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 tranformation-based characterisations for boundedness and conservativeness aye 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.

Keywords: augmented marked graph, Petri net, liveness, boundedness, reversibility, conservativeness

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 locus 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.

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 [subset or equal to] (P x T) [union] (T x P) is a flow relation and W : F [right arrow] {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 [member of] (P [union] T), *x = {y | (y,x) [member of] F} and [x*] = {y | (x, y) [member of] 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 = {[x.sub.1], [x.sub.2] ..., [x.sub.n]} can be written as *X and X* respectively, where *X = *[x.sub.1] [union] * [x.sub.2] [union] ... [union] *[x.sub.n] and X* = [x.sub.1]* [union] [x.sub.2]* [union] ... [union] [x.sub.n]*.

Definition 3. For a PT-net N = < P, T, F, W >, a path is a sequence of places and transitions [rho] : < [x.sub.1], [x.sub.2] ..., [x.sub.n]>, such that ([x.sub.i], [x.sub.i+1]) [member of] F for i = 1, 2 ..., n-l. [rho] 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 < [p.sub.1], [p.sub.2] ..., [p.sub.n], > is called a cycle if and only if there exists a set of transitions {[t.sub.1], [t.sub.2] ..., [t.sub.n]}, such that ([p.sub.1], [t.sub.1], [p.sub.2], [t.sub.2] ..., [p.sub.n], [t.sub.n] > forms an elementary path and ([t.sub.n], [p.sub.1]) [member of] F.

Definition 5. For a PT-net N = < P, T, F, W >, a marking is a function M : P [right arrow] {0, 1, 2 ...}, where M(p) is the number of tokens in p. (N, [M.sub.0]) represents N with an initial marking [M.sub.0].

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, [M.sub.0]), a transition t is said to be enabled at a marking M if and only if [for all] p [member of] *t: M(p) [greater than or equal to] W(p,t). On firing t, M is changed to M' such that [for all] p [member of] 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, [M.sub.0]), a sequence of transitions [sigma] = <[t.sub.1], [t.sub.2], ..., [t.sub.n]> is called a firing sequence if and only if [M.sub.0] [[t.sub.n]> ... [[t.sub.n]> [M.sub.n]. In notation, [M.sub.0] [N,[sigma]> [M.sub.n] or [M.sub.0] [[sigma]> [M.sub.n].

Definition 8. For a PT-net (N, [M.sub.0]), a marking M is said to be reachable if and only if there exists a firing sequence [sigma] such that [M.sub.0] [[sigma]> M. In notation, [M.sub.0] [N,*> M or [M.sub.0] [*> M. [N, [M.sub.0]> or [[M.sub.0]> represents the set of all reachable markings of (N, [M.sub.0]).

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 = {[p.sub.1], [p.sub.2] ..., [p.sub.m]} and T = {[t.sub.1], [t.sub.2] ..., [t.sub.n]}. The incidence matrix of N is an m x n matrix V whose typical entry [v.sub.ij] = W([p.sub.i],[t.sub.i]) - W([t.sub.j],[p.sub.i]) represents the change in number of tokens in [p.sub.i] after firing [t.sub.j] 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, [M.sub.0]), a transition t is said to be live if and only if [for all] M [member of] [[M.sub.0]>, [there exists] M' : M [*> M' [t>. (N, [M.sub.0]) is said to be live if and only if every transition is live.

Definition i 1. For a PT-net (N, [M.sub.0]), a place p is said to be k-bounded if and only if [for all] M [member of] [[M.sub.0]> : M(p) [less than or equal to] k, where k is a positive integer. (N, [M.sub.0]) 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, [M.sub.0]) is said to be reversible if and only if [for all] M [member of] [[M.sub.0]> : M [*> [M.sub.0].

Definition 13. For a PT-net N = (P, T, F, W), a place invariant is a [absolute value P]-vector [alpha] [greater than or equal to] 0 such that [alpha]V = 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 [alpha] > 0.

Figure 1 shows an ordinary PT-net which is live, bounded, safe, reversible and conservative.

[FIGURE 1 OMITTED]

Property 1. A PT-net (N, [M.sub.0]) is bounded if it is conservative [14, 15].

Definition 15. For a PT-net N, a set of places S is called a siphon if and only if *S [subset or equal to] S*. S is said to be minimal if and only if there does not exist another siphon S' in N such that S' [subset] S.

Definition 16. For a PT-net, a set of places T is called a trap if and only if T* [subset or equal to] *T.

Definition 17. A PT-net (N, [M.sub.0]) 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 [for all] p [member of] P: [absolute value of *p] = [absolute value of p*] = 1.

Property 2. A marked graph (N, [M.sub.0]) is live if and only if every cycle is marked by [M.sub.0] [13, 14].

Property 3. A live marked graph (N, [M.sub.0]) is bounded if and only if every place belongs to a cycle marked by [M.sub.0] [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 < [p.sub.1], [p.sub.3], [p.sub.6], [p.sub.7], [p.sub.4] > form a cycle. The place vector is a place invariant.

[FIGURE 2 OMITTED]

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, [M.sub.0]; R) is a PT-net (N, [M.sub.0]) with a specific subset of places R, such that : (a) Every place in R is marked by M0. (b) The net (N', [M.sub.0]') obtained from (N, [M.sub.0]; R) by removing the places in R and their associated arcs is a marked graph. (c) For each r [member of] R, there exist [k.sub.r] [greater than or equal to] 1 pairs of transitions [D.sub.r] = {<[t.sub.s1], [t.sub.h1]>, [t.sub.s2], [t.sub.h2]> ..., <[t.sub.skr], [t.sub.hkr]>}, such that r* = {[t.sub.s1], [t.sub.s2] ..., [t.sub.skr]} [subset or equal to] T and *r = {[t.sub.h1], [t.sub.h2], ..., [t.sub.hkr]} [subset or equal to] T and that, for each <[t.sub.si], [t.sub.hi]> [member of] [D.sub.r], there exists in (N', [M.sub.0]') an elementary path [[rho].sub.ri] connecting [t.sub.si] to [t.sub.hi]. (d) In (N', [M.sub.0]'), every cycle is marked and no [[rho].sub.ri] is marked.

Figure 3 shows a typical augmented marked graph (N, [M.sub.0]; R), where R = {[r.sub.1], [r.sub.2]}. For [r.sub.1], [D.sub.r1] = {<[t.sub.1], [t.sub.11]>, <[t.sub.3], [t.sub.g]>}. For [r.sub.2], [D.sub.r2] = {<[t.sub.2], [t.sub.11]>, <[t.sub.4], [t.sub.10]>}.

[FIGURE 3 OMITTED]

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 [l]. (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, [M.sub.0]; R) is live and reversible if every minimal siphon, which contains at least one place of R, contains a marked trap [11.

For the augmented marked graph (N, [M.sub.0]; R) shown in Figure 3, the minimal siphons are : {[p.sub.1], [p.sub.5], [p.sub.8]}, {[r.sub.1], [p.sub.2], [p.sub.4], [p.sub.6], [p.sub.7], [].sub.9]}, {[r.sub.1], [p.sub.2], [p.sub.4], [p.sub.6], [p.sub.7], [p.sub.10]}, {[r.sub.2], [p.sub.3], [p.sub.5], [p.sub.6], [p.sub.8], [p.sub.9]} and {[r.sub.2], [p.sub.3], [p.sub.5], [p.sub.6], [p.sub.8], [p.sub.10]}. Each of these minimal siphons contains a marked trap, and would never become empty. (N, [M.sub.0]; R) is live and reversible.

The places and transitions generated by cycles are defined as follows.

Definition 20. For a PT-net N, [[OMEGA].sub.N] is defined as the set of all cycles in N.

Definition 21. Let N be a PT-net. For a subset of cycles Y [subset or equal to] [[OMEGA].sub.N], P[Y] is defined as the set of places in Y, and T[Y] = *P[Y] [intersection] P[[Y]*] is defined as the set of transitions generated by Y.

For clarity in presentation, P[{[gamma]}] and T[{[gamma]}] can be written as P[[gamma]] and T[[gamma]], to denote the set of places in a cycle 7 and the set of transitions generated by [gamma], respectively.

Definition 22. For a [p.sub.7]-net N, an elementary path p = <[x.sub.1], [x.sub.2] ..., [x.sub.n] > is said to be conflict-free if and only if, for any transition [x.sub.i] in [rho], j [not [member of] (i -1) [??] [x.sub.j] [not member of] *[x.sub.i].

Property 10. Let S be a minimal siphon of a [p.sub.7]-net. For any p, p' [member of] 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, [M.sub.0]; R), there exists a set of cycles Y [subset or equal to] [[OMEGA].sub.N] 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, [M.sub.0]; R) be an augmented marked graph. For every r [member of] R, there exists a minimal siphon which contains only one marked place r.

Consider the augmented marked graph (N, [M.sub.0]; R) shown in Figure 3. Every minimal siphon is covered by cycles. Consider a minimal siphon [S.sub.1] = {[r.sub.1], [p.sub.2], [p.sub.4], [p.sub.6], [p.sub.7], [p.sub.9]}. There exists a set of cycles [Y.sub.1] = {[[gamma].sub.11], [[gamma].sub.12]}, where [[gamma].sub.11] = < [r.sub.1], [p.sub.4], [p.sub.7] > and [[gamma].sub.12] = < [r.sub.1], [p.sub.2], [p.sub.6], [p.sub.9] >, such that [S.sub.1] = P[[Y.sub.1]]. Consider another minimal siphon [S.sub.2] = [[r.sub.2], [p.sub.3], [p.sub.5], [p.sub.6], [p.sub.s], [p.sub.10]}. There exists a set of cycles [Y.sub.2] = {[[gamma].sub.21], [[gamma].sub.22]}, where [[gamma].sub.21] = ([r.sub.2], [p.sub.5], [p.sub.8]) and [[gamma].sub.22] = < [r.sub.2], [p.sub.3], [p.sub. 10] >, such that [S.sub.2] = P[[Y.sub.2]]. For [S.sub.1], [r.sub.1] [member of] R is the only one marked place. Also, for [S.sub.2], [r.sub.1] [member of] 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, [M.sub.0]; 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, [M.sub.0]; 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 [p.sub.7]-net. For a set of places Q in N, [[OMEGA].sub.N][Q] is defined as the set of cycles that contains at least one place in Q.

For clarity in presentation, [[OMEGA].sub.N][{p}] can be written as [[OMEGA].sub.N][p] to denote the set of cycles that contains a place p.

Property 15. For an augmented marked graph (N, [M.sub.0]; R), a R-siphon is covered by a set of cycles Y [subset or equal to] [[OMEGA].sub.N][R].

Figure 4 shows another augmented marked graph (N, [M.sub.0]; R), where R = {[r.sub.1], [r.sub.2]}. There are five minimal siphons, namely, [S.sub.1] = {[r.sub.1], [p.sub.3], [p.sub.4], [p.sub.7], [p.sub.8]}, [S.sub.2] = [[r.sub.1], [p.sub.3], [p.sub.5], [p.sub.7], [p.sub.8]}, [S.sub.3] = {[r.sub.2], [p.sub.2], [p.sub.4], [p.sub.6], [p.sub.8], [p.sub.9], [p.sub.10]}, [S.sub.4] = {[r.sub.2], [p.sub.2], [p.sub.5], [p.sub.6], [p.sub.8], [p.sub.9], [p.sub.10]} and [S.sub.5] = {[p.sub.1], [p.sub.3], [p.sub.7]}. [S.sub.1], [S.sub.2], [S.sub.3] and [S.sub.4] are R-siphon as they contain at least one place in R. [S.sub.5] is a NR-siphon which does not contain any place in R. For (N, [M.sub.0]; R), every R-siphon is covered by a set of cycles in [[OMEGA].sub.N][R]. For example, [S.sub.1] = {[r.sub.1], [p.sub.3], [p.sub.4], [p.sub.7], [p.sub.8]] is covered by a set of cycles [Y.sub.1] = {[[gamma].sub.11], [[gamma].sub.12]} [subset or equal to] [[OMEGA].sub.N][R], where [[gamma].sub.11] = < [r.sub.1], [p.sub.3], [p.sub.7] > and [[gamma].sub.12] = < [r.sub.1], [p.sub.4], [p.sub.8] >.

[FIGURE 4 OMITTED]

Property 16. Let S be a R-siphon of an augmented marked graph (N, [M.sub.0]; R). For every t [member of] (S* \ *S), there does not [member of]xist any s [member of] (S \ R) such that t [member of] s*.

Property 17. For an augmented marked graph (N, [M.sub.0]; R), a NR-siphon contains itself as a marked trap and would never become empty.

Property 18. An augmented marked graph (N, [M.sub.0]; R) is live and reversible if and only if no R-siphons eventually become empty.

Property 19. An augmented marked graph (N, [M.sub.0]; R) satisfies the siphon-trap property if and only if every R-siphon contains a marked trap.

Consider the augmented marked graph (N, [M.sub.0]; R) shown in Figure 4. Every R-siphon contains a marked trap. Each of the R-siphons [S.sub.1] = {[r.sub.1], [p.sub.3], [p.sub.4], [p.sub.7], [p.sub.8]}, [S.sub.2] = {[r.sub.1], [p.sub.3], [p.sub.5], [p.sub.7], [p.sub.8]}, [S.sub.3] = {[r.sub.2], [p.sub.2], [p.sub.4], [p.sub.6], [p.sub.8], [p.sub.9], [p.sub.10]} and [S.sub.4] = {[r.sub.2], [p.sub.2], [p.sub.5], [p.sub.6], [p.sub.8], [p.sub.9], [p.sub.10]} contains a marked trap and would never become empty. (N, [M.sub.0]; R) is live and reversible.

Property 20. (characterisation of Property 9) An augmented marked graph (N, [M.sub.0]; R) is live and reversible if every R-siphon contains a marked trap.

Property 18 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 [[OMEGA].sub.N][R]. We may now derive a strategy for checking the liveness and reversibility of an augmented marked graph (N, [M.sub.0]; R):

(a) Find all R-siphons based on [[OMEGA].sub.N][R].

(b) Check if every R-siphon contains a marked trap. If yes, report (N, [M.sub.0]; 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, [M.sub.0]; R) is live and reversible. Otherwise, report (N, [M.sub.0]; R) is neither live nor reversible.

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 [p.sub.7]-net N, a set of cycles Y [subset or equal to] [[OMEGA].sub.N] is said to be conflict-free if and only if, for any q, q' [member of] P[Y], there exists in P[Y] a conflict-free path from q to q'.

Figure 5 shows a [p.sub.7]-net N. Consider three cycles [[gamma].sub.1] [[gamma].sub.2], [[gamma].sub.3] [member of] [[OMEGA].sub.N][[p.sub.3]], where [[gamma].sub.1] = < [p.sub.3], [p.sub.2], [p.sub.7] >, [[gamma].sub.2] = < [p.sub.3], [p.sub.4] > and [[gamma].sub.3] = < [p.sub.3], [p.sub.1], [p.sub.6], [p.sub.10], [p.sub.8] >. The set of cycles [Y.sub.1] = {[[gamma].sub.1], [[gamma].sub.2]} is conflict-free because for any q, q' [member of] P[[Y.sub.1]], there exists in P[[Y.sub.1]] a conflict-free path from q to q'. The set of cycles [Y.sub.2] = {[[gamma].sub.2], [[gamma].sub.3]} is not conflict-free. We have [p.sub.4], [p.sub.8] [member of] P[[Y.sub.2]]. [p.sub.4] is connected to [p.sub.8] via only one path [rho] = < [p.sub.4], [t.sub.5], [p.sub.3], [t.sub.1], [p.sub.1], [t.sub.3], [p.sub.6], [t.sub.6], [p.sub.10], [t.sub.9], [p.sub.8] > in [Y.sub.2], and [rho] is not conflict-free because [p.sub.4], [p.sub.8] [member of] *[t.sub.5].

[FIGURE 5 OMITTED]

Property 21. Let S be a minimal siphon of an augmented marked graph (N, [M.sub.0]; R), and Y [subset or equal to] [[OMEGA].sub.N] be a set of cycles such that S = P[Y]. Then, Y is conflict-free.

For the augmented marked graph shown in Figure 3, {[r.sub.1], [p.sub.2], [p.sub.4], [p.sub.6], [p.sub.7], [p.sub.9]} is a minimal siphon covered by a set of cycles {< [r.sub.1], [p.sub.4], [p.sub.7] >, < [r.sub.1], [p.sub.2], [p.sub.6], [p.sub.9] >} which is conflict free. {[r.sub.2], [p.sub.3], [p.sub.5], [p.sub.6], [p.sub.8], [p.sub.10]} is another minimal siphon covered by a set of cycles {< [r.sub.2], [p.sub.5], [p.sub.8] >, ([r.sub.2], [p.sub.3], [p.sub.6], [p.sub.10] >} which is conflict-free. For the augmented marked graph shown in Figure 4, {[r.sub.1], [p.sub.3], [p.sub.4], [p.sub.7], [p.sub.8]} is a minimal siphon covered by a set of cycles {([r.sub.1], [p.sub.3], [p.sub.7]), ([r.sub.1], [p.sub.4], [p.sub.8])} which is conflict free. {[r.sub.1], [p.sub.3], [p.sub.5], [p.sub.7], [p.sub.8]} is another minimal siphon covered by a set of cycles {< [r.sub.1], [p.sub.3], [p.sub.7] >, < [r.sub.1], [p.sub.5], [p.sub.8] >} which is conflict free.

Definition 27. Let (N, [M.sub.0]; R) be an augmented marked graph. A place r [member of] R is said to satisfy the R-inclusion if and only if, for any set of cycles Y [subset or equal to] [[OMEGA].sub.N][R] such that Y is conflict-free, *r [subset or equal to] T[Y] [??] r* [subset or equal to] T[Y].

Figure 6 shows an augmented marked graph (N, [M.sub.0]; R), where R - {[r.sub.1], [r.sub.2]}. Consider [r.sub.1]. For any set of cycles [Y.sub.1] [subset or equal to] [[OMEGA].sub.N][R] such that [Y.sub.1] is conflict-free, *[r.sub.1] [subset or equal to] T[[Y.sub.1]] [r.sub.1]* [subset or equal to] T[[Y.sub.1]]. Next, consider [r.sub.2]. For any set of cycles [Y.sub.2] [subset or equal to] [[OMEGA].sub.N][R] such that [Y.sub.2] is conflict-free, *[r.sub.2] [subset or equal to] T[[Y.sub.2]] [??] [r.sub.2]* [subset or equal to] T[Y]. Both [r.sub.1] and [r.sub.2] satisfy the R-inclusion.

[FIGURE 6 OMITTED]

Figure 7 shows another augmented marked graph (N, [M.sub.0]; R). For [r.sub.1] [member of] R, there exists a set of cycles [Y.sub.1] = {[[gamma].sub.11], [[gamma].sub.12]} [subset or equal to] [[OMEGA].sub.N][R], where [[gamma].sub.11] = < [r.sub.1], [p.sub.5] > and [[gamma].sub.12] = < [r.sub.1], [p.sub.5], [r.sub.2], [p.sub.6] >. *[r.sub.1] = {[t.sub.5], [t.sub.6]} [subset or equal to] T[[Y.sub.2]] = {[t.sub.3], [t.sub.4], [t.sub.5], [t.sub.6]} but [r.sub.1]* = {[t.sub.2], [t.sub.3]} [not subset or equal to] T[[Y.sub.1]]. For [r.sub.2] [member of] R, there exist a set of cycles [Y.sub.2] = {[[gamma].sub.21], [[gamma].sub.22]} [subset or equal to] [[OMEGA].sub.N][R], where [[gamma].sub.21] = < [r.sub.2], [p.sub.6] > and [[gamma].sub.22] = < [r.sub.2], [p.sub.6], [r.sub.1], [p.sub.5] >. *[r.sub.2] = {[t.sub.5], [t.sub.6]} [subset or equal to] T[[Y.sub.2]] = {[t.sub.3], [t.sub.4], [t.sub.5], [t.sub.6]} but [r.sub.2]* = {[t.sub.1], [t.sub.4]} [not subset or equal to] T[[Y.sub.2]]. Both [r.sub.1] and [r.sub.2] do not satisfy the R- inclusion property.

[FIGURE 7 OMITTED]

Property 22. For an augmented marked graph (N, [M.sub.0]; R), a R-siphon S contains itself as a marked trap if every place r [member of] R in S satisfies the R-inclusion property.

Property 23. An augmented marked graph (N, [M.sub.0]; R) satisfies the siphon-trap property if and only if every place r [member of] R satisfies the R-inclusion property.

Property 24. An augmented marked graph (N, [M.sub.0]; R) is live and reversible if every place r x R satisfies the R-inclusion property.

Consider the augmented marked graph (N, [M.sub.0]; R) shown in Figure 6. We have R - {[r.sub.1], [r.sub.2]}, where both [r.sub.1] and [r.sub.2] satisfy the R-inclusion property. Any R-siphon, such as {[r.sub.1], [p.sub.3], [p.sub.4]} or {[r.sub.2], [p.sub.5], [p.sub.6]}, contains itself as a marked trap. (N, [M.sub.0]; 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 preset and post-sets.

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, [M.sub.0]; R) with the use of the R-inclusion property, as follows.

(a) Check if every r [member of] R satisfies the R-inclusion property. If yes, report (N, [M.sub.0]; R) is live and reversible. Otherwise go to (b).

(b) Let R' [subset or equal to] R be the set of places which do not satisfy the R-inclusion property. Based on [[OMEGA].sub.N][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, [M.sub.0]; 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, [M.sub.0]; R) is live and reversible. Otherwise, report (N, [M.sub.0]; 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, [M.sub.0]; R) into a number of marked graphs by replacing each place in R by a set of places.

Property 25. Let (N, [M.sub.0]; R) be an augmented marked graph to be transformed into (N', [M.sub.0]') as follows. For each place r e R, where Dr = {<[t.sub.s1], [t.sub.h1]>, <[t.sub.s2], [t.sub.h2]> ..., ([t.sub.skr], [t.sub.hkr])}, replace r with a set of places {[p.sub.1], [p.sub.2] ..., [p.sub.kr]}, such that [M.sub.0]'[[p.sub.i]] = [M.sub.0][r] and [p.sub.i]* = {[t.sub.si]} and *[p.sub.i] = {[t.sub.hi]} for i = 1, 2, ..., [k.sub.r]. Then, (N', [M.sub.0]') is a marked graph.

Definition 28. Let (N, [M.sub.0]; R) be an augmented marked graph. The marked graph (N', [M.sub.0]') transformed from (N, [M.sub.0]; R) as stated in Property 25 is called the R-transform of (N, [M.sub.0]; 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 {[q.sub.1], [q.sub.2]}.

[FIGURE 8 OMITTED]

[FIGURE 9 OMITTED]

Property 27. Let (N', [M.sub.0]') be the R-transform of an augmented marked graph (N, [M.sub.0]; R), where r [member of] R is replaced by a set of places Q = {[q.sub.1], [q.sub.2], ..., [q.sub.k]}, and [P.sub.0] be the set of marked places in N'. Then, for each [q.sub.i] in N', there exists a place invariant [[alpha].sub.i] of N' such that [[alpha].sub.i][[q.sub.i]] = 1 and [[alpha].sub.i][s] = 0 for any place s [member of] [P.sub.0] \ {[q.sub.i]}.

Property 28. Let (N, [M.sub.0]; R) be an augmented marked graph, where R = {[r.sub.1], [r.sub.2], ..., [r.sub.n]}. Let (N', [M.sub.0]') be the R-transform of (N, [M.sub.0]; R), where each [r.sub.i] is replaced by a set of places [Q.sub.i], for i - 1, 2, ..., n. If every place in (N', [M.sub.0]') belongs to a cycle, then there exists a place invariant [alpha] of N' such that [alpha] > 0 and [alpha][[q.sub.1]] = [alpha][[q.sub.2]] = ... [alpha] [[q.sub.k]] for each [Q.sub.i] = {[q.sub.1], [q.sub.2], ..., [q.sub.k]}.

Consider the R-transform (N', [M.sub.0]') shown in Figure 9. It is a live marked graph. For [q.sub.1], there exists a place invariant [[alpha].sub.1], such that [[alpha].sub.1][[q.sub.1]] = 1 and [[alpha].sub.1][[q.sub.2]] = [[alpha].sub.1][[p.sub.1]] = [[alpha].sub.1][[p.sub.2]] = 0. For [q.sub.2], there also exists a place invariant [[alpha].sub.2], such that [[alpha].sub.1][[q.sub.2]] = 1 and [[alpha].sub.1][[q.sub.1]] = [[alpha].sub.2][[p.sub.1]] = [[alpha].sub.2][[p.sub.2]] = 0. In (N', [M.sub.0]'), every place belongs to a cycle. There also exists a place invariant [alpha] > 0, where [alpha][[q.sub.1]] = [alpha][[q.sub.2]].

Based on R-transform, a necessary and sufficient condition for bounded and conservative augmented marked graphs is proposed.

Property 29. Let (N', [M.sub.0]') be the R-transform of an augmented marked graph (N, [M.sub.0]; R). (N, [M.sub.0]; R) is bounded and conservative if and only if every place in (N', [M.sub.0]') belongs to a cycle.

With Properties 29, we derive the following strategy for checking the boundedness and conservativeness of an augmented marked graph (N, [M.sub.0]; R) :

(a) Create the R-transform (N', [M.sub.0]') of(N, [M.sub.0]; R).

(b) For each place p in (N', [M.sub.0]'), check if there exists a cycle that contains p. If yes, report (N, [M.sub.0]; R) is bounded and conservative. Otherwise, report (N, [M.sub.0]; R) is neither bounded nor conservative.

Property 30. Let (N', [M.sub.0]') be the R-transform of an augmented marked graph (N, [M.sub.0]; R). (N, [M.sub.0]; R) is bounded and conservative if and only if (N', [M.sub.0]') is bounded.

Consider the augmented marked graph (N, [M.sub.0]; R) shown in Figure 8, and the R-transform (N', [M.sub.0]') of (N, Mo; R) in Figure 9. Every place in (N', [M.sub.0]') belongs to a cycle. (N, [M.sub.0]; R) is bounded and conservative. (N', [M.sub.0]') is also bounded and conservative.

Figure 10 shows an augmented marked graph (N, [M.sub.0], R), and Figure 11 shows the R-transform (N', [M.sub.0]') of (N, [M.sub.0]; R). For (N', [M.sub.0]'), [p.sub.3] does not belong to any cycle. Also, [p.sub.8] does not belong to any cycle. (N, [M.sub.0]; R) is neither bounded nor conservative.

[FIGURE 10 OMITTED]

[FIGURE 11 OMITTED]

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 ([H.sub.1], [H.sub.2], [H.sub.3], [H.sub.4], [H.sub.5] and [H.sub.6]) 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 ([C.sub.1], [C.sub.2], [C.sub.3], [C.sub.4], [C.sub.5] and [C.sub.6]) 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, [M.sub.0]; R) which represents the dining philosopher problem (version 1).

[FIGURE 12 OMITTED]

[FIGURE 13 OMITTED]

For (N, [M.sub.0]; 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, [M.sub.0]; 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, [M.sub.0]; R) which represents the dining philosopher problem (version 2). The set of places {[r.sub.1], [p.sub.l3], [r.sub.2], [p.sub.23], [r.sub.3], [p.sub.33], [r.sub.4], [p.sub.43], [r.sub.5], [p.sub.53], [r.sub.6], [p.sub.63]} is a R-siphon which would become empty after firing the sequence of transitions <[t.sub.11], [t.sub.12], [t.sub.13], [t.sub.14], [t.sub.15], [t.sub.16]>. Deadlock would occur after firing <[t.sub.11], [t.sub.12], [t.sub.13], [t.sub.14], [t.sub.15], [t.sub.16]>. Based on the results obtained in Section 4, (N, [M.sub.0]; R) is neither live nor reversible. On the other hand, for the R-transform of (N, [M.sub.0]; R), every place belongs to a cycle. Based on the results obtained in Section 5, (N, [M.sub.0]; R) is bounded and conservative.

7 Conclusion

In the past decade, augmented marked graphs have evolved into a sub-class of Petri nets for modelling shared resource systems. One major reason is that augmented marked graphs possess a structure which is desirable for modelling shared resources. However, the properties of augmented marked graphs are not extensively studied.

In this paper, a number of new characterisations for live and reversible augmented marked graphs are proposed. In particulars, some of these characterisations are based on cycles, instead of siphons. Besides, a R-transform is introduced. Based on the R-transform, a number of new characterisations for bounded and conservative augmented marked graphs are proposed. Consolidating these results, pretty simple conditions and procedures for checking the liveness, reversibility, boundedness and conservativeness of augmented marked graphs are derived. These have been illustrated using the dining philosopher problem.

Augmented marked graphs are often used for modelling shared-resource systems wherein the system analyst need to achieve the system 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, such as deadlock and capacity overflow', due to sharing of resources should be avoided. For a shared-resource system modelled as an augmented marked graph, essential properties such as liveness, reversibility, boundedness and conservativeness can be effectively analysed with the new characterisations for augmented marked graphs. These contribute to ensuring the design correctness of shared resource systems.

[FIGURE 14 OMITTED]

Appendix

For clarify in presentation, proofs of the proposed properties for augmented marked graphs are shown in this appendix as follows.

Proof of Property 8. ([??]) For an augmented marked graph, if every minimal siphon would never become empty, every siphon which contains at least one minimal siphon would never become empty. It follows from Properties 6 and 7 that the augmented marked graph is live and reversible. ([??]) It follows from Property 6 that every siphon (and hence, every minimal siphon) would never become empty.

Proof of Property 11. Let S = {[p.sub.1], [p.sub.2], ..., [p.sub.n]}. For each [p.sub.i], by definition of augmented marked graphs that *[p.sub.i] [not equal to] [empty set]. Then, there exists [p.sub.j] [member of] S, where [p.sub.j] [not equal to] [p.sub.i], such that ([p.sub.j]* [intersection] *[p.sub.i]) [not equal to] [empty set]. Since S is a minimal siphon, according to Property 10, [p.sub.i] connects to [p.sub.j] via a conflict-free path in S. Since [p.sub.j] connects to [p.sub.i], this forms a cycle [[gamma].sub.i] in S, where [p.sub.i] [member of] P[[[gamma].sub.i]] [subset or equal to] S. Let Y = {[[gamma].sub.1], [[gamma].sub.2], ..., [[gamma].sub.n]}.}. We have P[Y] = P[[[gamma].sub.1]] [union] P[[[gamma].sub.2]] [union] ... [union] P[[[gamma].sub.n]] [subset or equal to] S. On the other hand, S [subset or equal to] (P[[[gamma].sub.1]] [union] P[[[gamma].sub.2]] [union] ... [union] P[[[gamma].sub.n]]) = PlY] because S = {[p.sub.1], [p.sub.2], ..., [p.sub.n]}. Hence, P[Y] = S.

Proof of Property 12. (by contradiction) Let (N, [M.sub.0]; R) be an augmented marked graph. Suppose there exists a cycle [gamma] in (N, [M.sub.0]; R), such that [gamma] is not marked. [gamma] does not contain any place in R, and also exists in the net (N', [M.sub.0]') obtained from (N, [M.sub.0]; R) after removing the places in R and their associated arcs. However, by definition of augmented marked graphs, [gamma] 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 - {<[t.sub.s1], [t.sub.h1]), ([t.sub.s2], [t.sub.h2]>, ..., <[ts.sub.n], [t.sub.hn]?}, where r* = {[t.sub.s1], [t.sub.s2], ..., [t.sub.sn]} and *r = {[t.sub.h1], [t.sub.h2], ..., [t.sub.hn]}. For each <[t.sub.si], [t.sub.hi]> [member of] [D.sub.r], [t.sub.si] connects to [t.sub.hi] via an elementary path [[rho].sub.1] which is not marked. Let S = [P.sub.1] [union] [P.sub.2] [union] ... [union] [P.sub.n] [union] {r}, where [P.sub.i] is the set of places in [[rho].sub.i]. We have *[P.sub.1] [subset or equal to] ([P.sub.i]* [union] r*) because, for each p [member of] [P.sub.i], [absolute value of *p] = [absolute value of p*] = 1. Then, (*[P.sub.1] [union] *[P.sub.2] [union] ... [union] *[P.sub.n]) [subset or equal to] ([P.sub.1]* [union] [P.sub.2]* [union] ... [union] [P.sub.n]* [union] r*). Besides, *r = {[t.sub.h1], [t.sub.h2], ..., [t.sub.hn]} [subset or equal to] ([P.sub.1]* [union] [P.sub.2]* [union] ... [union] [P.sub.n]*). Hence, *S = (*[P.sub.1] [union] *[P.sub.2] [union] ... [union] *[P.sub.n] [union] *r]) [subset or equal to] ([P.sub.1]* [union] [P.sub.2]* [union] ... [union] [P.sub.n]* [union] 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 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 [gamma] in S, such that [gamma] [not equal to] [[OMEGA].sub.N][R]. By definition of augmented marked graphs, for any p [member of] P[[gamma]], [absolute value of *p] = [absolute value of p*] = 1. Hence, *P[[gamma]] = P[[gamma]]*, and P[[gamma]] is a siphon. Since there exists a place r [member of] R such that r [member of] S but r [not member of] P[[gamma]], we have P[[gamma]] [subset] S. However, since S is a minimal siphon, there does not exists any siphon S' = P[[gamma]] [subset] S.

Proof of Property 16. (by contradiction) Suppose there exists s [member of] (S \ R) such that t [member of] s*. By definition of augmented marked graphs, [absolute value of *s] = [absolute value of 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 [member of] T[Y] = (S* [intersection] *S). This however contradicts t [member of] (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 [member of] S, [absolute value of *s] = [absolute value of 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, [M.sub.0]; 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, [M.sub.0]; 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, [M.sub.0]; R) is live and reversible.

Proof of Property 21. Since S is a minimal siphon, according to Property 10, for any q, q' [member of] 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 = {[p.sub.1], [p.sub.2], ..., [p.sub.n]}. According to Property 13, S is marked. It follows from Properties 15 and 21 that there exists a set of cycles Y [subset or equal to] [[OMEGA].sub.N][R], such that Y is conflict-free and P[Y] = S. Since S is a siphon, for each [p.sub.i] [member of] S, *[p.sub.i] [subset or equal to] (*S [intersection] S*) = (*P[Y] [intersection] P[Y]*) = T[Y]. In case [p.sub.i] [not equal to] R, [p.sub.i]* [subset or equal to] T[Y] because [absolute value of *[p.sub.i]] = [absolute value of [p.sub.i]] = 1. In case [p.sub.i] [member of] R, given that [p.sub.i] satisfies the R-inclusion property, [p.sub.i]* [subset or equal to] T[Y]. Every [p.sub.i]* [subset or equal to] T[Y] = (*P[Y] [intersection] PLY]*) and [p.sub.i]* [subset or equal to] *P[Y] = *S. Since S* = ([p.sub.1]* [union] [p.sub.2]* [union] ... [union] [p.sub.n]*) [subset or equal to] *S, S is also a trap.

Proof of Property 23. ([??]) It follows from Properties 19 and 22. ([??] by contradiction) Suppose there exists r [member of] 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 [subset or equal to] [[OMEGA].sub.N][R], such that Y is conflict-free and S = P[Y]. According to Property 19, S contains a marked trap Q. Then, r [member of] Q and r* [subset or equal to] (*Q [intersection] Q*). Since S is a siphon, we have *r [subset or equal to] (*S [intersection] S*) = (*P[Y] [intersection] P[Y]*) = T[Y]. However, as r does not satisfy the R-inclusion property, r* [not subset or equal to] T[Y] = (*P[Y] P[Y]*) = (*S [intersection] S*), implying r* [not subset or equal to] (*Q [intersection] Q*).

Proof of Property 24. According to Property 23, (N, [M.sub.0]; R) satisfies the siphon-trap property. It follows from Property 20 that (N, [M.sub.0]; R) is live and reversible.

Proof of Property 25. For each place p [not member of] R in N, [M.sub.0]; R), [absolute value of *p] = [absolute value of p*] = 1. Each place r [member of] R is replaced by a set of places {[p.sub.1], [p.sub.2], ..., [p.sub.kr]}, where [absolute value of *[p.sub.i]] = [absolute value of [p.sub.i]*] I = 1 for i = 1, 2, ..., [k.sub.r]. Hence, for every place q in N', [absolute value of *q] = [absolute value of q*] = 1. (N', [M.sub.0]') is a marked graph.

Proof of Property 26. Let (N', [M.sub.0]') be the R-transform of an augmented marked graph (N, [M.sub.0]; R). As the transformation does not create cycles, cycles in (N', [M.sub.0]') exist in (N, [M.sub.0]; R). According to Property 12, cycles in (N, [M.sub.0]; R) are marked, and hence, cycles in (N', [M.sub.0]') are marked. Since (N', [M.sub.0]') is a marked graph, it follows from Property 2 that (N', [M.sub.0]') is live.

Proof of Property 27. Let [D.sub.r] = {<t.sub.h1], [t.sub.h1]>, <[t.sub.s2], [t.sub.h2]>, ..., <[t.sub.skr], [t.sub.hkr]>}. By definition of augmented marked graphs, for each ([t.sub.si], [t.sub.hi]), there exists an umnarked path [rho] = <[t.sub.s1], ..., [t.sub.h1]>) in (N, [M.sub.0]; R). Hence, [rho] also exists as an unmarked path in (N', [M.sub.0]'), and [rho] together with [q.sub.i] forms a cycle [[gamma].sub.i] which is marked at [q.sub.i] only. Since (N', [M.sub.0]') is a marked graph, according to Property 5, the corresponding vector of [[gamma].sub.i] is a place invariant [[alpha].sub.i] of N'. Since [q.sub.i] is the only one marked place in [[gamma].sub.i], [[alpha].sub.i][[q.sub.i]] = 1 and [[alpha].sub.i][s] = 0 for any s [member of] [P.sub.0] {[q.sub.i]}.

Proof of Property 28. Let P = {[p.sub.1], [p.sub.2], ..., [p.sub.n]} be the places in N', and [P.sub.0] [subset or equal to] P be those marked places. Since each Pi belongs to a cycle [[gamma].sub.i] and (N', [M.sub.0]') is a marked graph, according to Property 5, the corresponding vector of [[gamma].sub.i] is a place invariant [[alpha].sub.i]' of N'. Then, [[alpha].sub.i]' = [[alpha].sub.1]' + [[alpha].sub.2]' + ... + [[alpha].sub.n]' > 0 is a place invariant of N'. Consider [Q.sub.i] = {[q.sub.1], [q.sub.2], ..., [q.sub.k]}. Let [q.sub.m] [member of] [Q.sub.i] such that [alpha]'[[q.sub.m]] > [alpha]'[[q.sub.m]] for any [q.sub.i] [member of] [Q.sub.i]. For each % according to Property 27, there exists a place invariant [[alpha].sub.j]' > 0 such that [[alpha].sub.j]'[[q.sub.j]] = 1 and [[alpha].sub.j]'[s] = 0 for any s [member of] [P.sub.0] {[q.sub.i]}. There also exists a place invariant [alpha]" = [alpha]'+ h[[alpha].sub.j]', where h [greater than or equal to] 1, such that [alpha]"[[q.sub.j]] = [alpha]"[[q.sub.m]] and [alpha]"[s] = [alpha]'[s] for any s [member of] [P.sub.0] {[q.sub.i]}. Therefore, there eventually exists a place invariant [alpha] of N' such that [alpha][[q.sub.1]] = [alpha][[q.sub.2]] = ... = [alpha][[q.sub.k]].

Proof of Property 29. ([??]) Let R = {[r.sub.1], [r.sub.2], ..., [r.sub.n]}, where each [r.sub.i] is being replaced by a set of places [Q.sub.i], for i = 1, 2, ..., n. Since every place in (N', [M.sub.0]') belongs to a cycle, according to Property 28, there exists a place invariant [alpha]' of N' such that [alpha]' > 0 and [alpha]'[[q.sub.1]] = [alpha]'[[q.sub.2]] = ... = [alpha]'[[q.sub.k]] for each [Q.sub.i] = {[q.sub.1], [q.sub.2], ... [q.sub.k]}. Intuitively, there also exists a place invariants [alpha] of N such that [alpha] > 0 and [alpha][[r.sub.i]] = [alpha]'[[q.sub.1]] = [alpha]'[[q.sub.2]] = ... = [alpha]'[[q.sub.k]] for each [Q.sub.i]. Hence, (N, [M.sub.0]; R) is conservative. According to Property 1, (N, [M.sub.0], R) is also bounded. ([??]) Since (N, [M.sub.0]; R) is conservative, there exists a place invariant [alpha] of N such that [alpha] > 0. Consider each [r.sub.i] [member of] R which is being replaced by [Q.sub.i] = {[q.sub.1], [q.sub.2], ..., [q.sub.k]}. Intuitively, there also exists a place invariant [alpha]' of N' such that [alpha]' > 0 and [alpha]'[[q.sub.1]] = [alpha][[q.sub.2] = ... = [alpha]'[[q.sub.k]] = [alpha][[r.sub.i]] and [alpha]'[s] = [alpha][s] for any s [member of] P'\[Q.sub.i]. Hence, (N', [M.sub.0]') is conservative. It follows from Property 1 that (N', [M.sub.0]') is also bounded. Since (N', [M.sub.0]') is a marked graph, according to Property 3, every place in (N', [M.sub.0]') belongs to a cycle.

Proof of Property 30. It follows from Properties 3 and 29.

Received: August 27, 2007

References

[1] Chu, F. and Xie, X. (1997), Deadlock Analysis of Petri Nets Using Siphons and Mathematical Programming, IEEE Transactions on Robotics and Automation, Vol. 13, No. 6, pp. 793-804.

[2] Desel, J. and Esparza, J. (1995), Free Choice Petri Nets, Cambridge University Press.

[3] Zhou, M.C. and Venkatesh, K. (1999), Modeling, Simulation and Control of Flexible Manufacturing Systems : A Petri Net Approach, World Scientific.

[4] Jeng, M.D. et al. (2000), Manufacturing Modeling Using Process Nets with Resources, Proceedings of the IEEE International Conference on Robotics and Automation, pp. 2185-2190, I EEE Press.

[5] Jeng, M.D. et al. (2002), Process Nets with Resources for Manufacturing Modeling and their Analysis, IEEE Transactions on Robotics and Automation, Vol. 18, No. 6, pp. 875-889.

[6] Huang, H.J. et al. (2003), Property-Preserving Composition of Augmented Marked Graphs that Share Common Resources, Proceedings of the IEEE International Conference on Robotics and Automation, pp. 1446-1451, IEEE Press.

[7] Cheung, K.S. and Chow, K.O. (2005), Manufacturing System Design Using Augmented Marked Graph, Proceedings of the Chinese Control Conference, pp. 1209-1213, SCUT Press.

[8] Cheung, K.S. (2004), New Characterisations for Live and Reversible Augmented Marked Graphs, Information Processing Letters, Vol. 92, No. 5, pp. 239-243.

[9] Cheung, K.S. and Chow, K.O. (2005), Cycle-Inclusion Property of Augmented Marked Graphs, Information Processing Letters, Vol. 94, No. 6, pp. 271-276.

[10] Cheung, K.S. and Chow, K.O. (2005), A Synthesis Approach to Deriving Object-Based Specifications from Object Interaction Scenarios, In : Nilsson, A.G. et al. (Eds.), Advances in Information Systems Development, pp. 647-656, Springer.

[11] Cheung, K.S., et al. (2005), A Petri-Net-Based Synthesis Methodology for Use-Case-Driven System Design, Journal of Systems and Software, Vol. 79, No. 6, pp. 772-790.

[12] Peterson, J.L. (1981), Petri net theory and the modeling of systems, Prentice Hall.

[13] Reisig, W. (1985), Petri Nets : An Introduction, Springer-Verlag.

[14] Murata, T. (1989), Petri Nets : Properties, Analysis and Applications, Proceedings of the IEEE, Vol. 77, No. 4., pp. 541-580.

[15] Desel, J. and Reisig, W. (1998), Place Transition Petri Nets, Lectures on Petri Nets I : Basic Models, Lecture Notes in Computer Science, Vol. 1491, pp. 122-173, Springer-Verlag.

[16] Barkaoui, K. et al. (1995), On Liveness in Extended Non Self-Controlling Nets, Application and Theory of Petri Nets, Lecture Notes in Computer Science, Vol. 935, pp. 25-44, Springer-Verlag.

King-Sing Cheung

University of Hong Kong 

Pokfulam, Hong Kong 

E-mail: [e-mail]