## 1. Introduction

Augmented marked graphs were first introduced in 1997 (Chu & Xie, 1997). They are not well known as compared to other sub-classes of Petri nets such as free-choice nets (Desel & Esparza, 1995), and the properties of augmented marked graphs are not studied extensively. However, augmented marked graphs possess a structure which is desirable for modelling shared resources, and for this reason, they are often used in modelling shared resource systems, such as manufacturing systems (Chu & Xie, 1997; Zhou & Venkatesh, 1999; Jeng et al., 2000; Jeng et al., 2002; Huang et al., 2003; Cheung & Chow, 2005).

There are a few published works on augmented marked graphs. Based on siphons and mathematical programming, Chu and Xie proposed a necessary and sufficient condition of live and reversible augmented marked graphs, which checks the existence of potential deadlocks (Chu & Xie, 1997). However, this involves the flow of tokens during execution and cannot be checked simply by looking into the structure. Chu and Xie also proposed another siphon-based characterisation for live and reversible augmented marked graphs but it provides a sufficient condition only. On the other hand, the boundedness and conservativeness of augmented marked graphs were not investigated.

In the literature, apart from (Chu & Xie, 1997), the studies of augmented marked graphs mainly focus on their property-preserving synthesis or composition. Jeng et al. proposed a synthesis of process nets (covering augmented marked graphs) for manufacturing system design, where the condition of liveness and reversibility are based on siphons and the firability of transitions (Jeng et al., 2000; Jeng et al., 2002). Huang et al. also investigated the composition of augmented marked graphs so that properties such as liveness, boundedness and reversibility can be preserved (Huang et al., 2003).

In our earlier works on augmented marked graphs, we proposed characterisations for their liveness, boundedness, reversibility and conservativeness and applied the characterisations to the analysis and design of manufacturing systems, object-oriented systems and shared resource systems (Cheung, 2004; Cheung, 2005; Cheung & Chow, 2005a; Cheung & Chow, 2005b; Cheung & Chow, 2005c; Cheung, 2006; Cheung & Chow, 2006; Cheung et al., 2006; Cheung, 2007). This paper consolidates our previous works with a special focus on the properties of augmented marked graphs.

First, we provide a number of characterisations for live and reversible augmented marked graphs, based on siphons and cycles. In particular, a property called R-inclusion property is introduced to characterise the siphon-trap property of augmented marked graphs. With this property, the liveness and reversibility of an augmented marked graph can be analysed through cycles instead of siphons. Second, we introduce R-transformation which transforms an augmented marked graph into a marked graph. Its boundedness and conservativeness can be determined by checking the cycles of the transformed marked graph. Based on these characterisations, some pretty simple conditions and procedures are derived for checking the liveness, reversibility, boundedness and conservativeness of an augmented marked graph. These will be illustrated using the dining philosophers problem. We then show the application to manufacturing system design.

The rest of this paper is organised as follows. Following this introduction, Section 2 provides the preliminaries to be used in this paper. Section 3 describes augmented marked graphs and their known properties. Section 4 shows characterisations for liveness and reversibility while Section 5 shows characterisations for boundedness and conservativeness. Section 6 then illustrates these characterisations using the dining philosophers example. Section 7 describes the application to manufacturing system design. Finally, Section 8 concludes this paper with a brief discussion.

## 2. Preliminaries

This section provides the preliminaries to be used in this paper for those readers who are not familiar with Petri nets (Peterson, 1981; Reisig, 1985; Murata, 1989; Desel & Reisig, 1998).

*Definition 2.1.* A place-transition net (PT-net) is a 4-tuple N = P, T, F, W , where P is a set of places, T is a set of transitions, F ((P T) (T P)) is a flow relation, and W : F { 1, 2,... } is a weight function. N is said to be ordinary if and only if the range of W is { 1 }.

An ordinary PT-net is usually written as P, T, F . In the rest of this paper, unless specified otherwise, all PT-nets refer to ordinary PT-nets.

*Definition 2.2.* Let N = P, T, F, W be a PT-net. For any x (P T), ^{}x = { y | (y, x) F } and x^{} = { y | (x, y) F } are called the pre-set and post-set of x, respectively.

For clarity in presentation, the pre-set and post-set of a set of places or transitions X = { x_{1}, x_{2},..., x_{n} } can be written as ^{}X and X^{} respectively, where ^{}X = ^{}x_{1} ^{}x_{2} ... ^{}x_{n} and X^{} = x_{1}^{} x_{2}^{} ... x_{n}^{}.

*Definition 2.3.* For a PT-net N = P, T, F, W , a path is a sequence of places and transitions = x_{1}, x_{2},..., x_{n} , such that (x_{i}, x_{i+1}) F for i = 1, 2,..., n-1. is said to be elementary if and only if it contains no duplicate places or transitions.

*Definition 2.4.* For a PT-net N = P, T, F, W , a sequence of places p_{1}, p_{2},..., p_{n} is called a cycle if and only if there exists a set of transitions { t_{1}, t_{2},..., t_{n} }, such that p_{1}, t_{1}, p_{2}, t_{2},..., p_{n}, t_{n} forms an elementary path and (t_{n}, p_{1}) F.

*Definition 2.5.* For a PT-net N = P, T, F, W , a marking is a function M : P { 0, 1, 2,...}, where M(p) is the number of tokens in p. (N, M_{0}) represents N with an initial marking M_{0}.

*Definition 2.6.* For a PT-net (N, M_{0}), a transition t is said to be enabled at a marking M if and only if p ^{}t : M(p) W(p,t). On firing t, M is changed to M' such that p P : M'(p) = M(p) - W(p,t) + W(t,p). In notation, M [N,t M' or M [t M'.

*Definition 2.7.* For a PT-net (N, M_{0}), a sequence of transitions = t_{1}, t_{2},..., t_{n} is called a firing sequence if and only if M_{0} [t_{1}... [t_{n} M_{n}. In notation, M_{0} [N, M_{n} or M_{0} [ M_{n}.

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

*Definition 2.9.* Let N = P, T, F, W be a PT-net, where P = { p_{1}, p_{2},..., p_{m} } and T = { t_{1}, t_{2},..., t_{n} }. The incidence matrix of N is an m n matrix V whose typical entry v_{ij} = W(p_{i},t_{j}) - W(t_{j},p_{i}) represents the change in number of tokens in p_{i} after firing t_{j} once, for i = 1, 2,..., m and j = 1, 2,..., n.

*Definition 2.10.* For a PT-net (N, M_{0}), a transition t is said to be live if and only if M [M_{0}, M' : M [ M' [t. (N, M_{0}) is said to be live if and only if every transition is live.

*Definition 2.11.* For a PT-net (N, M_{0}), a place p is said to be k-bounded if and only if M [M_{0} : M(p) k, where k is a positive integer. (N, M_{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 2.12.* A PT-net (N, M_{0}) is said to be reversible if and only if M [M_{0} : M [ M_{0}.

*Definition 2.13.* A PT-net N = P, T, F, W is said to be conservative if and only if there exists a |P|-vector > 0 such that V = 0, where V is the incidence matrix of N.

*Property 2.1.* A PT-net is bounded if it is conservative (Murata, 1989; Desel & Reisig, 1998).

*Definition 2.14.* For a PT-net N = P, T, F, W , a place invariant is a |P|-vector 0 such that V = 0, where V is the incidence matrix of N.

*Definition 2.15.* For a PT-net N, a set of places S is called a siphon if and only if ^{}S S^{}. S is said to be minimal if and only if there does not exist another siphon S' in N such that S' S.

*Definition 2.16.* For a PT-net, a set of places T is called a trap if and only if T^{} ^{}T.

*Definition 2.17.* A PT-net (N, M_{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).

*Definition 2.18.* A marked graph is an ordinary PT-net N = P, T, F, W such that p P : |^{}p| = |p^{}| = 1.

*Property 2.2.* A marked graph (N, M_{0}) is live if and only if every cycle is marked by M_{0} (Reisig, 1985; Murata, 1989).

*Property 2.3.* A live marked graph (N, M_{0}) is bounded if and only if every place belongs to a cycle marked by M_{0} (Reisig, 1985; Murata, 1989).

*Property 2.4.* A live and bounded marked graph is reversible (Reisig, 1985; Murata, 1989).

*Property 2.5.* For a marked graph, the corresponding place vector of a cycle is a place invariant (Reisig, 1985; Murata, 1989).

## 3. Augmented marked graphs

This section describes augmented marked graphs and their known properties on liveness and reversibility.

*Definition 3.1.* An augmented marked graph (N, M_{0}; R) is a PT-net (N, M_{0}) with a specific subset of places R, satisfying the following conditions : (a) Every place in R is marked by M_{0}. (b) The net (N', M_{0}') obtained from (N, M_{0}; R) by removing the places in R and their associated arcs is a marked graph. (c) For each r R, there exist k_{r} 1 pair of transitions D_{r} = { t_{s1}, t_{h1}, t_{s2}, t_{h2},..., t_{skr}, t_{hkr} }, such that r^{} = { t_{s1}, t_{s2},..., t_{skr} } T and ^{}r = { t_{h1}, t_{h2},..., t_{hkr} } T and that, for each t_{si}, t_{hi} D_{r}, there exists in N' an elementary path _{ri} connecting t_{si} to t_{hi}. (d) In (N', M_{0}'), every cycle is marked and no _{ri} is marked.

Figure 1 shows an augmented marked graph (N, M_{0}; R), where R = { r_{1}, r_{2} }. For r_{1}, D_{r1} = { t_{1}, t_{11}, t_{3}, t_{9} }. For r_{2}, D_{r2} = { t_{2}, t_{11}, t_{4}, t_{10} }.

*Property 3.1.* An augmented marked graph is live if and only if it does not contain any potential deadlock - a siphon which would eventually become empty (Chu & Xie, 1997).

*Property 3.2.* An augmented marked graph is reversible if it is live (Chu & Xie, 1997).

*Property 3.3.* An augmented marked graph is live and reversible if and only if every minimal siphon would never become empty.

*Proof.* () It follows from Properties 3.1 and 3.2 that an augmented marked graph is live and reversible if every minimal siphon would never become empty. () It follows from Property 3.1 that every minimal siphon would never become empty.

*Property 3.4.* An augmented marked graph (N, M_{0}; R) is live and reversible if every minimal siphon, which contains at least one place of R, contains a marked trap (Chu & Xie, 1997).

For the augmented marked graph (N, M_{0}; R) in Figure 1, the minimal siphons include : { p_{1}, p_{5}, p_{8}}, { r_{1}, p_{2}, p_{4}, p_{6}, p_{7}, p_{9} }, { r_{1}, p_{2}, p_{4}, p_{6}, p_{7}, p_{10} }, { r_{2}, p_{3}, p_{5}, p_{6}, p_{8}, p_{9} } and { r_{2}, p_{3}, p_{5}, p_{6}, p_{8}, p_{10} }. Each of these minimal siphons contains a marked trap, and would never become empty. (N, M_{0}; R) is live and reversible.

## 4. Liveness and reversibility

This section provides characterisations for live and reversible augmented marked graphs, based on siphons and cycles. Strategies for checking liveness and reversibility are then presented.

*Definition 4.1.* For a PT-net N, _{N} is defined as the set of all cycles in N.

*Definition 4.2.* Let N be a PT-net. For a subset of cycles Y _{N}, P[Y] is defined as the set of places in Y, and T[Y] = ^{}P[Y] P[Y]^{} is defined as the set of transitions generated by Y.

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

*Definition 4.3.* For a PT-net N, an elementary path = x_{1}, x_{2},..., x_{n} is said to be conflict-free if and only if, for any transition x_{i} in , j (i -1) x_{j} ^{}x_{i} (Barkaoui, 1995).

*Lemma 4.1.* Let S be a minimal siphon of a PT-net. For any p, p' S, there exists in S a conflict-free path from p to p' (Barkaoui, 1995).

*Property 4.1.* For a minimal siphon S of an augmented marked graph (N, M_{0}; R), there exists a set of cycles Y _{N} such that P[Y] = S.

*Proof.* Let S = { p_{1}, p_{2},..., p_{n} }. For each p_{i}, it follows from the definition of augmented marked graphs that ^{}p_{i} . Then, there exists p_{j} S, where p_{j} p_{i}, such that (p_{j}^{} ^{}p_{i}) . According to Lemma 4.1, p_{i} connects to p_{j} via a conflict-free path in S. Since p_{j} connects to p_{i}, this forms a cycle _{i} in S, where p_{i} P[_{i}] S. Let Y = { _{1}, _{2},..., _{n} }. We have P[Y] = P[_{1}] P[_{2}] ... P[_{n}] S. On the other hand, S (P[_{1}] P[_{2}] ... P[_{n}]) = P[Y] since S = { p_{1}, p_{2},..., p_{n} }. Hence, P[Y] = S.

*Property 4.2.* Every cycle in an augmented marked graph is marked.

*Proof.* (by contradiction) Let (N, M_{0}; R) be an augmented marked graph. Suppose there exists a cycle in (N, M_{0}; R), such that is not marked. Then, does not contain any place in R. Hence, also exists in the net (N', M_{0}') obtained from (N, M_{0}; R) after removing the places in R and their associated arcs. However, by definition of augmented marked graphs, every cycle in (N', M_{0}') is marked.

*Property 4.3.* Every siphon in an augmented marked graph is marked.

*Proof.* For an augmented marked graph, according to Properties 4.1 and 4.2, every minimal siphon contains cycles and is marked. Hence, every siphon, which contains at least one minimal siphon, is marked.

*Property 4.4.* Let (N, M_{0}; R) be an augmented marked graph. For every r R, there exists a minimal siphon which contains only one marked place r.

*Proof.* Let D_{r} = { t_{s1}, t_{h1}, t_{s2}, t_{h2},..., t_{sn}, t_{hn} }, where r^{} = { t_{s1}, t_{s2},..., t_{sn} } and ^{}r = { t_{h1}, t_{h2},..., t_{hn} }. By definition of augmented marked graphs, for each t_{si}, t_{hi} D_{r}, t_{si} connects to t_{hi} via an elementary path _{i} which is not marked. Let S = P_{1} P_{2} ... P_{n} { r }, where P_{i} is the set of places in _{i}. We have ^{}P_{i} (P_{i}^{} r^{}) because, for each p P_{i}, | ^{}p | = | p^{} | = 1. Then, (^{}P_{1} ^{}P_{2} ... ^{}P_{n}) (P_{1}^{} P_{2}^{} ... P_{n}^{} r^{}). Besides, ^{}r = { t_{h1}, t_{h2},..., t_{hn} } (P_{1}^{} P_{2}^{} ... P_{n}^{}). Hence, ^{}S = (^{}P_{1} ^{}P_{2} ... ^{}P_{n} ^{}r) (P_{1}^{} P_{2}^{} ... P_{n}^{} r^{}) = S^{}. Therefore, S is a siphon, in which r is the only one marked place. Let S' be a minimal siphon in S. According to Property 4.3, S' is marked. Since r is the only one marked place in S, r is also the only one marked place in S'.

Consider the augmented marked graph (N, M_{0}; R) shown in Figure 1. Every minimal siphon is covered by cycles. For example, for a minimal siphon S_{1} = { r_{1}, p_{2}, p_{4}, p_{6}, p_{7}, p_{9} }, there exists a set of cycles Y_{1} = { _{11}, _{12} }, where _{11} = r_{1}, p_{4}, p_{7} and _{12} = r_{1}, p_{2}, p_{6}, p_{9} , such that S_{1} = P[Y_{1}]. For another minimal siphon S_{2} = { r_{2}, p_{3}, p_{5}, p_{6}, p_{8}, p_{10} }, there exists a set of cycles Y_{2} = { _{21}, _{22} }, where _{21} = r_{2}, p_{5}, p_{8} and _{22} = r_{2}, p_{3}, p_{6}, p_{10} , such that S_{2} = P[Y_{2}]. S_{1} is a minimal siphon, in which r_{1} R is the only one marked place. Also, S_{2} is a minimal siphon, in which r_{2} R is the only one marked place.

*Definition 4.4.* For an augmented marked graph (N, M_{0}; R), a minimal siphon is called a R-siphon if and only if it contains at least one place in R.

*Definition 4.5.* For an augmented marked graph (N, M_{0}; R), a minimal siphon is called a NR-siphon if and only if it does not contain any place in R.

*Definition 4.6.* Let N be a PT-net. For a set of places Q in N, _{N}[Q] is defined as the set of cycles that contains at least one place in Q.

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

Figure 2 shows an augmented marked graph (N, M_{0}; R), where R = { r_{1}, r_{2} }. There are five minimal siphons, namely, S_{1} = { r_{1}, p_{3}, p_{4}, p_{7}, p_{8} }, S_{2} = { r_{1}, p_{3}, p_{5}, p_{7}, p_{8} }, S_{3} = { r_{2}, p_{2}, p_{4}, p_{6}, p_{8}, p_{9}, p_{10} }, S_{4} = { r_{2}, p_{2}, p_{5}, p_{6}, p_{8}, p_{9}, p_{10} } and S_{5} = { p_{1}, p_{3}, p_{7} }. S_{1}, S_{2}, S_{3} and S_{4} are R-siphons while S_{5} is a NR-siphon.

*Property 4.5.* For an augmented marked graph (N, M_{0}; R), a R-siphon is covered by a set of cycles Y _{N}[R].

*Proof.* (By contradiction) Let S be a R-siphon. By Property 4.1, S is covered by cycles. Suppose there exists a cycle in S, such that _{N}[R]. According to the definition of augmented marked graphs, for any p P[], | ^{}p | = | p^{} | = 1. Hence, ^{}P[] = P[]^{}, and P[] is also a siphon. Since there exists a place r R such that r S but r P[], we have P[] S. However, by definition of minimal siphons, there does not exists any siphon S' = P[] in S, such that S' = P[] S.

For the augmented marked graph (N, M_{0}; R) shown in Figure 2. every R-siphon is covered by a set of cycles in _{N}[R]. For example, a R-siphon S_{1} = { r_{1}, p_{3}, p_{4}, p_{7}, p_{8} } is covered by a set of cycles Y_{1} = { _{11}, _{12} } _{N}[R], where _{11} = r_{1}, p_{3}, p_{7} and _{12} = r_{1}, p_{4}, p_{8} . Another R-siphon S_{2} = { r_{1}, p_{3}, p_{5}, p_{7}, p_{8} } is covered by a set of cycles Y_{2} = { _{21}, _{22} } _{N}[R], where _{21} = r_{1}, p_{3}, p_{7} and _{22} = r_{1}, p_{5}, p_{8} .

*Property 4.6.* Let S be a R-siphon of an augmented marked graph (N, M_{0}; R). For every t (S^{} \ ^{}S), there does not exist any s (S \ R) such that t s^{}.

*Proof.* (by contradiction) Suppose s exists. By definition of augmented marked graphs, | ^{}s | = | s^{} | = 1. S is covered by cycles in accordance with Property 4.5. Hence, t is the one and only one transition in s^{}, where t T[Y] = (S^{} ^{}S). This however contradicts t (S^{} \ ^{}S).

*Property 4.7.* For an augmented marked graph (N, M_{0}; R), a NR-siphon contains itself as a marked trap and would never become empty.

*Proof.* Let S be a NR-siphon. According to Property 4.3, S is marked. It follows from the definition of augmented marked graphs that, for any s S, | ^{}s | = | s^{} | = 1. Then, ^{}S = S^{} and S is also a trap. Hence, S contains itself as a marked trap and would never become empty.

*Property 4.8.* An augmented marked graph (N, M_{0}; R) is live and reversible if and only if no R-siphons eventually become empty.

*Proof.* () According to Property 4.7, a NR-siphon would never become empty. Given that no R-siphons eventually become empty, every minimal siphon would never become empty. According to Property 3.3, (N, M_{0}; R) is live and reversible. () It follows from Property 3.1 that no R-siphons eventually become empty.

*Property 4.9.* An augmented marked graph (N, M_{0}; R) satisfies the siphon-trap property if and only if every R-siphon contains a marked trap.

*Proof.* () According to Property 4.7, a NR-siphon contains a marked trap. Given that every R-siphon contains a marked trap, every minimal siphon contains a marked trap. () Every minimal siphon contains marked trap implies that every R-siphon contains a marked trap.

Consider the augmented marked graph (N, M_{0}; R) shown in Figure 2. Every R-siphon contains marked trap. Each of the R-siphons S_{1} = { r_{1}, p_{3}, p_{4}, p_{7}, p_{8} }, S_{2} = { r_{1}, p_{3}, p_{5}, p_{7}, p_{8} }, S_{3} = { r_{2}, p_{2}, p_{4}, p_{6}, p_{8}, p_{9}, p_{10} } and S_{4} = { r_{2}, p_{2}, p_{5}, p_{6}, p_{8}, p_{9}, p_{10} } contains a marked trap and would never become empty. Also, the NR-siphon S_{5} = { p_{1}, p_{3}, p_{7} } contains itself as a marked trap and would never become empty. (N, M_{0}; R) is live and reversible.

*Property 4.10.* (characterisation of Property 3.4) An augmented marked graph (N, M_{0}; R) is live and reversible if every R-siphon contains a marked trap.

*Proof.* For (N, M_{0}; R), if every R-siphon contains a marked trap, according to Property 4.9, the siphon-trap property is satisfied. Hence, every minimal siphon would never become empty. It then follows from Property 3.3 that (N, M_{0}; R) is live and reversible.

Property 4.8 provides a simpler necessary and sufficient condition for live and reversible augmented marked graphs, as compared to Properties 3.1 and 3.2. According to Property 4.8, only R-siphons are considered. Typically, for an augmented marked graph (N, M_{0}; R), the set R is small, so only a small number of siphons need to be considered. Properties 3.4 and 4.10 also refers to the same set of siphons but only a sufficient condition is provided.

With Properties 4.8 and 4.10, we can determine if an augmented marked graph is live and reversible based on R-siphons. On the other hand, Property 4.5 provides a characterisation for R-siphons so that R-siphons can be easily identified by finding cycles in _{N}[R].

We may now derive the following strategy for checking the liveness and reversibility of an augmented marked graph (N, M_{0}; R) :

Find all R-siphons based on _{N}[R].

Check if every R-siphon contains a marked trap. If yes, report (N, M_{0}; R) is live and reversible. Otherwise, go to (c).

For each R-siphon which does not contain any marked trap, check if it would never become empty. If yes, (N, M_{0}; R) is live and reversible. Otherwise, (N, M_{0}; R) is neither live nor reversible.

In the following, a property called R-inclusion is introduced for characterising the liveness and reversibility of augmented marked graphs.

*Definition 4.7.* For a PT-net N, a set of cycles Y _{N} is said to be conflict-free if and only if, for any q, q' P[Y], there exists in P[Y] a conflict-free path from q to q'.

For the PT-net N shown in Figure 3, consider three cycles _{1}, _{2}, _{3} _{N}[p_{3}], where _{1} = p_{3}, p_{2}, p_{7} , _{2} = p_{3}, p_{4} and _{3} = p_{3}, p_{1}, p_{6}, p_{10}, p_{8} . Y_{1} = { _{1}, _{2} } is conflict-free because for any q, q' P[Y_{1}], there exists in P[Y_{1}] a conflict-free path from q to q'. Y_{2} = { _{2}, _{3} } is not conflict-free. Consider Y_{2}. We have p_{4}, p_{8} P[Y_{2}]. p_{4} is connected to p_{8} via only one path = p_{4}, t_{5}, p_{3}, t_{1}, p_{1}, t_{3}, p_{6}, t_{6}, p_{10}, t_{9}, p_{8} in Y_{2}, and is not conflict-free because p_{4}, p_{8} ^{}t_{5}.

*Property 4.11.* Let S be a minimal siphon of an augmented marked graph (N, M_{0}; R), and Y _{N} be a set of cycles such that S = P[Y]. Then, Y is conflict-free.

*Proof.* It follows from Lemma 4.1 that, for any q, q' S = P[Y], there exists in S = P[Y] a conflict-free path from q to q'. Hence, Y is conflict free.

For the augmented marked graph shown in Figure 1, { r_{1}, p_{2}, p_{4}, p_{6}, p_{7}, p_{9} } is a minimal siphon covered by a set of cycles { r_{1}, p_{4}, p_{7} , r_{1}, p_{2}, p_{6}, p_{9} } which is conflict free. { r_{2}, p_{3}, p_{5}, p_{6}, p_{8}, p_{10} } is another minimal siphon covered by a set of cycles { r_{2}, p_{5}, p_{8} , r_{2}, p_{3}, p_{6}, p_{10} } which is conflict-free. For the augmented marked graph shown in Figure 2, { r_{1}, p_{3}, p_{4}, p_{7}, p_{8} } is a minimal siphon covered by a set of cycles { r_{1}, p_{3}, p_{7} , r_{1}, p_{4}, p_{8} } which is conflict free. { r_{1}, p_{3}, p_{5}, p_{7}, p_{8} } is another minimal siphon covered by a set of cycles { r_{1}, p_{3}, p_{7} , r_{1}, p_{5}, p_{8} } which is conflict free.

*Definition 4.8.* Let (N, M_{0}; R) be an augmented marked graph. A place r R is said to satisfy the R-inclusion if and only if, for any set of cycles Y _{N}[R] such that Y is conflict-free, ^{}r T[Y] r^{} T[Y].

Figure 4 shows an augmented marked graph (N, M_{0}; R), where R = { r_{1}, r_{2} }. Consider r_{1}. For any set of cycles Y_{1} _{N}[R] such that Y_{1} is conflict-free, ^{}r_{1} T[Y_{1}] r_{1}^{} T[Y_{1}]. Next, consider r_{2}. For any set of cycles Y_{2} _{N}[R] such that Y_{2} is conflict-free, ^{}r_{2} T[Y_{2}] r_{2}^{} T[Y]. Both r_{1} and r_{2} satisfy the R-inclusion.

Figure 5 shows an augmented marked graph (N, M_{0}; R), where R = { r_{1}, r_{2} }. For r_{1}, there exists a set of cycles Y_{1} = { _{11}, _{12} } _{N}[R], where _{11} = r_{1}, p_{5} and _{12} = r_{1}, p_{5}, r_{2}, p_{6} . ^{}r_{1} = { t_{5}, t_{6} } T[Y_{1}] = { t_{3}, t_{4}, t_{5}, t_{6} }, but r_{1}^{} = { t_{2}, t_{3} } T[Y_{1}]. For r_{2}, there exists a set of cycles Y_{2} = { _{21}, _{22} } _{N}[R], where _{21} = r_{2}, p_{6} and _{22} = r_{2}, p_{6}, r_{1}, p_{5} . ^{}r_{2} = { t_{5}, t_{6} } T[Y_{2}] = { t_{3}, t_{4}, t_{5}, t_{6} }, but r_{2}^{} = { t_{1}, t_{4} } T[Y_{2}]. Hence, r_{1} and r_{2} do not satisfy the R-inclusion property.

*Property 4.12.* For an augmented marked graph (N, M_{0}; R), a R-siphon S contains itself as a marked trap if every place r R in S satisfies the R-inclusion property.

*Proof.* Let S = { p_{1}, p_{2},..., p_{n} }. According to Property 4.3, S is marked. It follows from Properties 4.5 and 4.11 that there exists a set of cycles Y _{N}[R], such that Y is conflict-free and P[Y] = S. Since S is a siphon, for each p_{i} S, ^{}p_{i} (^{}S S^{}) = (^{}P[Y] P[Y]^{}) = T[Y]. In case p_{i} R, p_{i}^{} T[Y] because | ^{}p_{i} | = | p_{i}^{} | = 1. In case p_{i} R, given that p_{i} satisfies the R-inclusion property, p_{i}^{} T[Y]. Every p_{i}^{} T[Y] = (^{}P[Y] P[Y]^{}) and p_{i}^{} ^{}P[Y] = ^{}S. Since S^{} = (p_{1}^{} p_{2}^{} ... p_{n}^{}) ^{}S, S is also a trap. S contains itself as a marked trap.

Consider the augmented marked graph (N, M_{0}; R), where R = { r_{1}, r_{2} }, shown in Figure 4. Both r_{1} and r_{2} satisfy the R-inclusion property. { r_{1}, p_{3}, p_{4} } is a minimal siphon which contains itself as a marked trap. { r_{2}, p_{5}, p_{6} } is another minimal siphon which contains itself as a marked trap.

*Property 4.13.* An augmented marked graph (N, M_{0}; R) satisfies the siphon-trap property if and only if every place r R satisfies the R-inclusion property.

*Proof.* () It follows from Properties 4.12 and 4.9. ( by contradiction) Suppose there exists r R, such that r does not satisfy the R-inclusion property. According to Property 4.4, there exists a R-siphon S, in which r is the only marked place. It follows from Properties 4.5 and 4.11 that there exists Y _{N}[R], such that Y is conflict-free and S = P[Y]. According to Property 4.9, S contains a marked trap Q. Then, r Q and r^{} (^{}Q Q^{}). Since S is a siphon, we have ^{}r (^{}S S^{}) = (^{}P[Y] P[Y]^{}) = T[Y]. However, as r does not satisfy the R-inclusion property, r^{} T[Y] = (^{}P[Y] P[Y]^{}) = (^{}S S^{}), implying r^{} (^{}Q Q^{}).

*Property 4.14.* An augmented marked graph (N, M_{0}; R) is live and reversible if every place r R satisfies the R-inclusion property.

*Proof.* According to Property 4.13, (N, M_{0}; R) satisfies the siphon-trap property. It follows from Property 4.10 that (N, M_{0}; R) is live and reversible.

Consider the augmented marked graph (N, M_{0}; R), where R = { r_{1}, r_{2} }, shown in Figure 4. Both r_{1} and r_{2} satisfy the R-inclusion property. (N, M_{0}; R) satisfies the siphon-trap property, and is live and reversible.

Property 4.14 provides a cycle-based sufficient condition for live and reversible augmented marked graphs. Without finding siphons and checking if each of these siphons contains a marked trap, we need to check the R-inclusion property which involves finding cycles and checking their pre-sets and post-sets. This provides an alternative characterisation for live and reversible augmented marked graphs, apart from the existing siphon-based ones.

Based on Properties 4.5, 4.8, 4.10, 4.12 and 4.14, we may revise the strategy for checking the liveness and reversibility of an augmented marked graph (N, M_{0}; R) with the use of the R-inclusion property, as follows.

Check if every r R satisfies the R-inclusion property. If yes, report (N, M

_{0}; R) is live and reversible. Otherwise go to (b).Let R' R be the set of places which do not satisfy the R-inclusion property. Based on

_{N}[R'], find all R-siphons which contain at least one place in R'.For each R-siphon identified in (b), check if it contains a marked trap. If yes, (N, M

_{0}; R) is live and reversible. Otherwise, go to (d).For each R-siphon identified in (b) that does not contain any marked trap, check if it would never become empty. If yes, (N, M

_{0}; R) is live and reversible. Otherwise, (N, M_{0}; R) is neither live nor reversible.HHHHHH

## 5. Boundedness and conservativeness

This section first introduces a transformation, called R-transform, for augmented marked graphs. Based on R-transform, a number of characterisations for bounded and conservative augmented marked graphs are then derived. Strategies for checking boundedness and conservativeness are then presented.

*Property 5.1.* Let (N, M_{0}; R) be an augmented marked graph to be transformed into (N', M_{0}') as follows. For each place r R, where D_{r} = { t_{s1}, t_{h1}, t_{s2}, t_{h2},..., t_{skr}, t_{hkr} }, replace r with a set of places { p_{1}, p_{2},..., p_{kr} }, such that M_{0}'[p_{i}] = M_{0}[r] and p_{i}^{} = { t_{si} } and ^{}p_{i} = { t_{hi} } for i = 1, 2,..., k_{r}. Then, (N', M_{0}') is a marked graph.

*Proof.* According to the definition of augmented marked graphs, for each place p R in N, M_{0}; R), | ^{}p | = | p^{} | = 1. Each place r R is replaced by a set of places { p_{1}, p_{2},..., p_{kr} }, where | ^{}p_{i} | = | p_{i}^{} | = 1 for i = 1, 2,..., k_{r}. Hence, for every place q in N', | ^{}q | = | q^{} | = 1. (N', M_{0}') is a marked graph.

*Definition 5.1.* Let (N, M_{0}; R) be an augmented marked graph. The marked graph (N', M_{0}') obtained from (N, M_{0}; R) after the transformation as stated in Property 5.1 is called the R-transform of (N, M_{0}; R).

*Property 5.2.* The R-transform of an augmented marked graph is live.

*Proof.* Let (N', M_{0}') be the R-transform of an augmented marked graph (N, M_{0}; R). Since the transformation process does not create new cycles, cycles in (N', M_{0}') also exist in (N, M_{0}; R). According to Property 4.1, every cycle in (N, M_{0}; R) is marked, and hence, every cycle in (N', M_{0}') is marked. Since (N', M_{0}') is a marked graph, it follows from Property 2.2 that (N', M_{0}') is live.

Figure 6 shows an augmented marked graph (N, M_{0}; R). Figure 7 shows the R-transform of (N, M_{0}; R), where r is replaced by { q_{1}, q_{2} }. It is a live marked graph.

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

*Proof.* Let D_{r} = { t_{s1}, t_{h1}, t_{s2}, t_{h2},..., t_{skr}, t_{hkr} }. According to the definition of augmented marked graphs, for each t_{si}, t_{hi}, there exists an unmarked path = t_{s1},..., t_{h1} in (N, M_{0}; R). Obviously, also exists as an unmarked path in (N', M_{0}'), and together with q_{i} forms a cycle _{i} which is marked at q_{i} only. As (N', M_{0}') is a marked graph, according to Property 2.5, the corresponding vector of _{i} is a place invariant _{i} of N'. Since q_{i} is the only one marked place in _{i}, _{i}[q_{i}] = 1 and _{i}[s] = 0 for any place s P_{0} \ {q_{i}}.

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

*Proof.* Let P = { p_{1}, p_{2},..., p_{n} } be the set of places in N', and P_{0} be those marked places. Since each p_{i} belongs to a cycle _{i} and (N', M_{0}') is a marked graph, according to Property 2.5, the corresponding vector of _{i} is a place invariant _{i}' of N'. Then, ' = _{1}' + _{2}' +... + _{n}' > 0 is a place invariant of N'. Consider Q_{i} = { q_{1}, q_{2},..., q_{k} }. Let q_{m} Q_{i} such that '[q_{m}] '[q_{j}] for any q_{j} Q_{i}. For each q_{j}, according to Property 5.3, there exists an invariant _{j}' > 0 such that _{j}'[q_{j}] = 1 and _{j}'[s] = 0 for any place s P_{0} \ {q_{j}}. There also exists a place invariant " = ' + h_{j}', where h 1, such that "[q_{j}] = "[q_{m}] and "[s] = '[s] for any s P_{0} \ {q_{j}}. Hence, there eventually exists a place invariant of N' such that [q_{1}] = [q_{2}] =... = [q_{k}].

Consider the R-transform (N', M_{0}') of an augmented marked graph, as shown in Figure 7. For q_{1}, there exists a place invariant _{1}, such that _{1}[q_{1}] = 1 and _{1}[q_{2}] = _{1}[p_{1}] = _{1}[p_{2}] = 0. For q_{2}, there also exists a place invariant _{2}, such that _{2}[q_{2}] = 1 and _{2}[q_{1}] = _{2}[p_{1}] = _{2}[p_{2}] = 0. In (N', M_{0}'), every place belongs to a cycle. There also exists a place invariant > 0, where [q_{1}] = [q_{2}].

*Lemma 5.1.* Let N = P, T, F be a PT-net and N' = P', T', F' be the PT-net obtained from N after fusing a set of places Q = { q_{1}, q_{2},..., q_{n} } P into a single place r P'. If there exists a place invariant of N such that [q_{1}] = [q_{2}] =... = [q_{n}] = k 0, then there also exists a place invariant ' of N' such that '[r] = k and '[s] = [s] for any s P'\{r} = P\Q.

*Proof.* Since N' is obtained from N by fusing Q = { q_{1}, q_{2},..., q_{n} } into r, we have P' = (P\Q) { r }. Let V be the incidence matrix of N. Then, the incidence matrix V' of N' satisfies that V'[r] = _{i=1,2,...,n}V[q_{i}] and V'[s] = V[s] for any s P'\{r} = P\Q. Since is a place invariant of N, V = 0. Let ' be a place vector of N' such that '[r] = [q_{1}] = [q_{2}] =... = [q_{n}] = k and '[s] = [s] for every s P'\{r} = P\Q. Then, 'V' = '[r]V'[r] + _{p(P'\{r})}'[p]V'[p] = _{i=1,2,...,n}[q_{i}]V[q_{i}] + _{p(P\Q)}[p]V[p] = V = 0. Hence, ' is a place invariant of N'.

*Lemma 5.2.* Let N = P, T, F be a PT-net and N' = P', T', F' be the PT-net obtained from N after fusing a set of places Q = { q_{1}, q_{2},..., q_{n} } P into a single place r P'. If there exists a place invariant ' of N' such that '[r] = k 0, then there also exists a place invariant of N such that [q_{1}] = [q_{2}] =... = [q_{n}] = k and [s] = '[s] for any s P\Q = P'\{r}.

*Proof.* Since N' is obtained from N by fusing Q = { q_{1}, q_{2},..., q_{n} } into r, we have P' = (P\Q) { r }. Let V be the incidence matrix of N. Then, the incidence matrix V' of N' satisfies that V'[r] = _{i=1,2,...,n}V[q_{i}] and V'[s] = V[s] for any s P'\{r} = P\Q. Since ' is a place invariant of N', 'V' = 0. Let be a place vector of N such that [q_{1}] = [q_{2}] =... = [q_{n}] = k and [s] = '[s] for every s P\Q = P'\{r}. Then, V = _{i=1,2,...,n}[q_{i}]V[q_{i}] + _{p(P\Q)}[p]V[p] = '[r]V'[r] + _{p(P'\{r})}'[p]V'[p] = 'V'. Hence, is a place invariant of N.

*Property 5.5.* Let (N', M_{0}') be the R-transform of an augmented marked graph (N, M_{0}; R). (N, M_{0}; R) is bounded and conservative if and only if every place in (N', M_{0}') belongs to a cycle.

*Proof.* () Let R = { r_{1}, r_{2},..., r_{n} }. (N', M_{0}') is the R-transform of (N, M_{0}; R), where each r_{i} is replaced by a set of places Q_{i}, for i = 1, 2,..., n. Since every place in (N', M_{0}') belongs to a cycle, according to Property 5.4, there exists a place invariant ' of N' such that ' > 0 and '[q_{1}] = '[q_{2}] =... = '[q_{k}] for each Q_{i} = { q_{1}, q_{2},..., q_{k} }. It follows from Lemma 5.1 that there also exists a place invariants of N such that > 0 and [r_{i}] = '[q_{1}] = '[q_{2}] =... = '[q_{k}] for each Q_{i}. Hence, (N, M_{0}; R) is conservative. According to Property 2.1, (N, M_{0}; R) is bounded. () Since (N, M_{0}; R) is conservative, there exists a place invariant of N such that > 0. Consider each r_{i} R which is replaced by Q_{i} = { q_{1}, q_{2},..., q_{k} }. According to Lemma 5.2, there also exists a place invariant ' of N' such that ' > 0 and '[q_{1}] = '[q_{2}] =... = '[q_{k}] = [r_{i}] and '[s] = [s] for any s P'\Q_{i}. Hence, (N', M_{0}') is conservative. It follows from Property 2.1 that (N', M_{0}') is bounded. Since (N', M_{0}') is a marked graph, according to Property 2.3, every place in (N', M_{0}') belongs to a cycle.

*Property 5.6.* Let (N', M_{0}') be the R-transform of an augmented marked graph (N, M_{0}; R). (N, M_{0}; R) is bounded and conservative if and only if (N', M_{0}') is bounded.

*Proof.* It follows from Properties 2.3 and 5.5.

Consider the augmented marked graph (N, M_{0}; R) shown in Figure 6, and the R-transform (N', M_{0}') of (N, M_{0}; R). Every place in (N', M_{0}') belongs to a cycle. (N, M_{0}; R) is bounded and conservative. (N', M_{0}') is also bounded and conservative.

Figure 8 shows another augmented marked graph (N, M_{0}; R). Figure 9 shows the R-transform (N', M_{0}') of (N, M_{0}; R), where r is replaced by { q_{1}, q_{2} }. For (N', M_{0}'), places p_{3} and p_{10} do not belong to any cycle. (N, M_{0}; R) is neither bounded nor conservative.

Based on Properties 5.5, the following strategy is derived for checking the boundedness and conservativeness of an augmented marked graph (N, M_{0}; R) :

## 6. The Dining philosophers problem

This section illustrates the properties of augmented marked graphs obtained in the previous two sections using the dining philosophers problem. By modelling the dining philosophers problem by an augmented marked graph, the system is analysed on its liveness, reversibility, boundedness and conservativeness based on the properties of augmented marked graphs.

*Example 1 : The Dining Philosophers Problem (Version 1)*

Six philosophers (H_{1}, H_{2}, H_{3}, H_{4}, H_{5} and H_{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_{1}, C_{2}, C_{3}, C_{4}, C_{5} and C_{6}) shared by them for getting the food to eat, as shown in Figure 10. For one to get the food to eat, both the chopstick at the right hand side and the chopstick at the left hand side must be available. The philosopher then grasps both chopsticks simultaneously and then takes the food to eat. Afterwards, the chopsticks are released and returned to their original positions simultaneously.

Figure 11 shows an augmented marked graph (N, M_{0}; R), representing the dining philosophers problem (version 1). Table 1 shows the semantic meanings of the places and transitions. There are 24 R-siphons, namely, {r_{1}, p_{61}, p_{11}}, {r_{1}, p_{61}, p_{12}}, {r_{1}, p_{62}, p_{11}}, {r_{1}, p_{62}, p_{12}}, {r_{2}, p_{11}, p_{21}}, {r_{2}, p_{11}, p_{22}}, {r_{2}, p_{12}, p_{21}}, {r_{2}, p_{12}, p_{22}}, {r_{3}, p_{21}, p_{31}}, {r_{3}, p_{21}, p_{32}}, {r_{3}, p_{22}, p_{31}}, {r_{3}, p_{22}, p_{32}}, {r_{4}, p_{31}, p_{41}}, {r_{4}, p_{31}, p_{42}}, {r_{4}, p_{32}, p_{41}}, {r_{4}, p_{32}, p_{42}}, {r_{5}, p_{41}, p_{51}}, {r_{5}, p_{41}, p_{52}}, {r_{5}, p_{42}, p_{51}}, {r_{5}, p_{42}, p_{52}}, {r_{6}, p_{51}, p_{61}}, {r_{6}, p_{51}, p_{62}}, {r_{6}, p_{52}, p_{61}} and {r_{6}, p_{52}, p_{62}}. Each of these R-siphons contains a marked trap and would never become empty. Based on the results obtained in Section 4, (N, M_{0}; R) is live and reversible. On the other hand, for the R-transform of (N, M_{0}; R), every place belongs to a cycle. Based on the results obtained in Section 5, (N, M_{0}; R) is bounded and conservative.

*Example 2 : The Dining Philosophers Problem (Version 2)*

The Dining Philosophers Problem is now modified as follows. For one to get the food to eat, he or she first grasps the chopstick at the right hand side if available, then grasps the chopstick at the left hand side if available, and then takes the food to eat. Afterwards, the chopsticks are released and returned to their original positions simultaneously.

Figure 12 shows an augmented marked graph (N, M_{0}; R), representing the dining philosophers problem (version 2). Table 2 shows the semantic meanings of the places and transitions. The set of places {r_{1}, p_{13}, r_{2}, p_{23}, r_{3}, p_{33}, r_{4}, p_{43}, r_{5}, p_{53}, r_{6}, p_{63}} is a R-siphon which would become empty after firing the sequence of transitions t_{11}, t_{12}, t_{13}, t_{14}, t_{15}, t_{16}. Based on the results obtained in Section 4, (N, M_{0}; R) is neither live nor reversible. Deadlocks would occur, for example, after firing t_{11}, t_{12}, t_{13}, t_{14}, t_{15}, t_{16}. On the other hand, for the R-transform of (N, M_{0}; R), every place belongs to a cycle. Based on the results obtained in Section 5, (N, M_{0}; R) is bounded and conservative.

## 7. Application to manufacturing system

Manufacturing systems are typically shared resource systems, wherein the resources used to be maximally shared among different asynchronous processes. Moreover, every resource has a pre-defined capacity limit that can never be exceeded. Therefore, in manufacturing system design, a major design objective is to achieve a live, bounded and reversible system - liveness implies freeness of deadlock, boundedness implies absence of capacity overflow, and reversibility allows system recovery. Verification of the system liveness, boundedness and reversibility is essentially required, though very time-consuming.

Possessing a specific structure for representing shared resources, augmented marked graphs are often used for modelling manufacturing systems. By modelling a manufacturing system as an augmented marked graph, this section shows how the system liveness, boundedness and reversibility can be analysed, based on the properties of augmented marked graphs.

*Example 3.* It is a FWS-200 Flexible Workstation System, extracted from the literature (Zhou & Venkatesh, 1999, pp. 121-124). The system consists of two robots R_{1} and R_{2}, one feeder area and one PCB area, as shown in Figure 13. There are two asynchronous processes.

Production process 1 : R_{1} picks components from the feeder area, and moves into the PCB area for inserting components. The finished product is then moved out from the PCB area.

Production process 2 : R_{2} picks components from the feeder area, and moves into the PCB area for inserting components. The finished product is then moved out from the PCB area.

Figure 14 shows an augmented marked graph (N, M_{0}; R), representing the FWS-200 flexible workstation system. Table 3 shows the semantic meanings of the places and transitions.

For the augmented marked graph (N, M_{0}; R) shown in Figure 14, every R-siphon would never become empty. Based on the results obtained in Section 4, (N, M_{0}; R) is live and reversible. For the R-transform of (N, M_{0}; R), every place belongs to a cycle. Based on the results obtained in Section 5, (N, M_{0}; R) is bounded and conservative. It is then concluded that the FWS-200 flexible workstation system is live, bounded, reversible and conservative.

*Example 4.* It is a flexible assembly system, extracted from the literature (Proth & Xie, 1996, pp. 58-61). The system consists of three conveyors C_{1}, C_{2} and C_{3} and three robots R_{1}, R_{2} and R_{3}, as shown in Figure 15. There are three asynchronous processes.

Assembly process 1 : C_{1} requests R_{1}. After acquiring R_{1}, it requests R_{2}. After acquiring R_{2}, it performs assembling and then releases both R_{1} and R_{2} simultaneously.

Assembly process 2 : C_{2} requests R_{2}. After acquiring R_{2}, it requests R_{3}. After acquiring R_{3}, it perform assembling and then releases both R_{2} and R_{3} simultaneously.

Assembly process 3 : C_{3} requests R_{3}. After acquiring R_{3}, it requests R_{1}. After acquiring R_{1}, it perform assembling and then releases both R_{3} and R_{1} simultaneously.

Figure 16 shows an augmented marked graph (N, M_{0}; R), representing the flexible assembly system. Table 4 shows the semantic meanings of the places and transitions.

For the augmented marked graph (N, M_{0}; R) shown in Figure 16, there exists a R-siphon S = { p_{13}, p_{23}, p_{33}, r_{1}, r_{2}, r_{3} } which becomes empty after firing the sequence of transitions t_{11}, t_{21}, t_{31} . Based on the results obtained in Section 4, (N, M_{0}; R) is neither live nor reversible. A deadlock would occur after firing t_{11}, t_{21}, t_{31} . For the R-transform of (N, M_{0}; R), every place belongs to a cycle. Based on the results obtained in Section 5, (N, M_{0}; R) is bounded and conservative. It is then concluded that the flexible assembly system is non-live, non-reversible but bounded and conservative.

## 8. Conclusion

In the past decade, augmented marked graphs have evolved into a sub-class of Petri nets. They are often used for modelling shared resource systems, such as manufacturing systems. One major reason is that augmented marked graphs possess a special structure which is desirable for modelling shared resources. However, the properties of augmented marked graphs are not extensively studied. In the literature, there are a few published works on augmented marked graphs.

This paper consolidates our earlier works on augmented marked graphs with a special focus on liveness, boundedness, reversibility and conservativeness. We provide a number of characterisations for live and reversible augmented marked graphs. In particulars, some of these characterisations are based on cycles, instead of siphons. Besides, we introduce the R-transformation, on which characterisations for bounded and conservative augmented marked graphs are obtained. With these characterisations, some pretty simple conditions and procedures for checking the liveness, reversibility, boundedness and conservativeness of an augmented marked graph are derived. These have been illustrated using the dining philosophers problem.

Typically, in designing shared resource systems, one need to achieve design objectives on two folds. On one hand, the resources are scarce and should be maximally shared. On the other hand, the system should be carefully designed so that erroneous situations due to the sharing of resources, such as deadlock and capacity overflow, can be avoided. Yet, the verification of liveness, boundedness and reversibility is very difficult and time-consuming. This paper contributes to provide an effective means to analysing these essential properties. By modelling a shared resource system as an augmented marked graph, its liveness, boundedness, reversibility and conservativeness can be effectively analysed, based on the characterisations and properties of augmented marked graphs. We specifically show the application to the analysis of manufacturing systems which are typically shared resource systems. Promising results are obtained.