# Mixed integer programming-based liveness test for FMS with full routing flexibility.

1. IntroductionFlexible manufacturing systems (FMS) utilize computers and shared resources (such as robots, machines, and automated guided vehicles) to automatically produce products [1]. Owing to the competition of shared resources, there may be some processes in FMS, which once started cannot be finished, that is, deadlocks [2]. Hence, it should be ensured that no deadlocks will occur in FMS; in other words, all working processes should be live. Usually, liveness property of FMS might be tested by analyzing their models (such as Petri nets) before using. Since the model complexity will increase with job shop flexibility (alternative machines, alternative operation sequences, and full routing flexibility) [3], the work for detecting liveness of FMS will also increase correspondingly.

At present, there are two categories of techniques for liveness test: one category is relied on the classic state enumeration analysis of Petri nets, which grows exponentially with the size of the net [4]; the other one is based on standardized tools of mixed integer programming (MIP), which is originally proposed by Chu and Xie [5] and is more efficient than the former. The basic idea of the latter is that if there does not exist any siphon becoming empty in a Petri net, then the net is deadlock free. It has been verified that for some subclasses of ordinary Petri nets such as ES2PR nets [6], [S.sup.3]PR nets [7], L[S.sup.3]PR [8] nets, and E[S.sup.3]PR [9] nets the net is live if and only if it is deadlock free. So, the liveness of these subclasses of ordinary Petri nets can be tested by MIP-based algorithms [10,11]. The natural thing is to extend MIP-based method of liveness test for general Petri nets. Park and Reveliotis [12] introduced an MIP-based algorithm for testing the weakly liveness of FMS with alternative machines flexibility modeled by [S.sup.3]G[R.sup.2] nets, which is in view of the conclusion that a net is weakly live if there exist no dead marked siphons (DMS). Shih et al. [13] has obtained some similar results for [S.sup.3]G[R.sup.2] nets, in which DMS is found on the grounds of the conception of max,-controlled siphons. Moreover, Liu and Li [14] provided a general MIP algorithm of liveness test for [S.sup.3]G[R.sup.2] nets, which is based on the result that a net is live if there is no extended deadly marked siphons (EDMS). Owing to the shortage of liveness conditions of [S.sup.*]PR nets, which can model FMS with full routing flexibility [15, 16], there is no MIP-based method of liveness test for [S.sup.*]PR net. The liveness of Gadara nets [17] (a subclass of [S.sup.*] PR nets) maybe detected by the original MIP approach [5], because of the conclusion that a Gadara net is live if and only if there does not exist any empty siphons [17,18].

This paper defined a subclass of [S.sup.*] PR nets firstly, namely, OSC-[S.sup.*] PR nets, in which all output transitions of each choice working place are restricted to use the same type and quantity of resources. The main structure characteristic of OSC-[S.sup.*] PR nets is that an OSC-[S.sup.*] PR net is live if there exists no non-max'-controlled siphons. Accordingly, an MIPbased algorithm is proposed to determine whether or not an OSC-[S.sup.*]PR net is live. It is worth to say that OSC-[S.sup.*]PR nets are an extension of Gadara nets, which are usually used to model multithreaded programs [17]. Considering the structure complexity of [S.sup.*] PR nets, it is difficult to develop an MIP-based algorithm for testing their liveness directly. So, an indirect method is given here, which comprises two steps as follows: first, for a given [S.sup.*] PR net, constructing an OSC-[S.sup.*] PR net to ensure that if the latter is live then the former must be live; second, testing liveness of the constructed OSC-[S.sup.*] PR net by the aforementioned MIP-based algorithm. In order to verify the performance of our method, a typical case of FMS is taken as example.

This paper is organized as follows. Section 2 introduces the basic knowledge about Petri nets. Section 3 presents OSC-[S.sup.*]PR nets and their structure characteristics. Section 4 proposes an MIP-based algorithm for testing liveness of OSC[S.sup.*] PR nets. Section 5 discusses an indirect method for testing liveness of [S.sup.*] PR nets. A typical example is presented in Section 6.

2. Preliminaries

This section, we briefly introduce the basic definitions and notations of a Petri net, which will be discussed in the rest of this paper. More details can be found in [4,19].

A generalized Petri net is a four-tuple N = (P, T, F, W), where P and T are finite, nonempty and disjoint sets. P denotes the set of places and T denotes the set of transitions with P [union] T [not equal to] [phi] and P [intersection] T = [phi]. F [subset or equal to] (P x T)[union](T x P) is called a flow relation of the net, represented by arcs with arrows from places to transitions or from transitions to places. W : (P x T)[union](T x P) [right arrow] N is a mapping that assigns a weight to an arc: W(x, y) > 0 if and only if (x, y) [member of] F, and W(x, y) = 0 otherwise, where x, y [member of] P [union] T and N denotes the set of natural numbers.

A marking M of a Petri net N is a mapping from P to N. M(p) denotes the number of tokens in the place p. We usually describe markings and vectors using a multiset (bag) or formal sum notation for economy of space. As a result, [[summation].sub.p[member of]P] M(p)p is used to denote vector M. For instance, a marking that puts four tokens in place [p.sub.2] and two tokens in place [p.sub.4] only in a net with P = {[p.sub.1] - [p.sub.6]} is denoted by 4[p.sub.2] + 2[p.sub.4] instead of (0, 4, 0, 2, 0, 0). A place p is marked by marking M if and only if M(p) > 0.A subset S [subset or equal to] P is marked by M if and only if at least one place in S is marked by M. The sum of tokens of all places in S is denoted by M(S); that is, M(S) = [[summation].sub.p[member of]S] M(p). S is said to be empty at M if and only if M(S) = 0. (N, [M.sub.0]) is called a net system or marked net and [M.sub.0] is called an initial marking of N. In general, (N, [M.sub.0]) is directly called a net where there is no confusion.

Let x [member of] P [union] T be a node of net N = (P, T, F, W). [sup.*]x = [y [member of] P [union] T | (y, x) [member of] F] denotes the preset of x, while x' = [y e PJT I (x,y) e F] denotes its postset of x. Furthermore, this notation can be extended to a set of nodes. For example, given X [subset or equal to] p [union] T, [sup.*]X = [[union].sub.x[member of]X] and [X.sup.*] = [[union].sub.x[member of]X] [x.sup.*]. Given a place p, we denote max[W(p, t) | t [member of] [p.sup.*]} by [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and min[W(t, p) | t [member of] [sup.*]p] by [min.sub.*p].

A transition t [member of] T is enabled at marking M if and only if for all p e 't, M(p) > W(p, t). This fact is denoted by M[t>. Firing it yields a new marking M1 such that for all p [member of] P, M'(p) = M(p) - W(p,t) + W(t,p), as denoted by M[t)M'. M' is called a immediately reachable marking from M. Marking M1 is said to be reachable from M if there exists a sequence of transitions [sigma] = [t.sub.0][t.sub.1] ... [t.sub.n] and markings [M.sub.1], [M.sub.2], ..., and Mn such that M[[t.sub.0])[M.sub.1] [[t.sub.1]>[M.sub.2] ... [M.sub.n][[t.sub.n]>M' holds. The set of markings reachable from M in N is called the reachability set of Petri net (N, M) and denoted by R(N, M).

Let N = (P, T, F, W) be a Petri net. N is pure (self-loop free) if and only if for all x [member of] P [union] T, [sup.*]x [union] [x.sup.*] = [phi]. N is called an ordinary net, denoted by N = (P, T, F) if for all f e F, W(f) = 1. N = (P, T, F) is called a state machine if for all t [member of] T, [absolute value of ([sup.*]t)] = [absolute value of ([t.sup.*]) = 1. It is strongly connected if for all x, y [member of] P [union] T, there is a sequence of nodes x, a, b, ..., c, y such that (x, a), (a, b), ..., (c, y) [member of] F, where [a, b, ..., c] [subset or equal to] P [union] T. An extended free-choice net is an ordinary Petri net such that for all [t.sub.1], [t.sub.2] [member of] T, [sup.*][t.sub.1] [intersection] [sup.*][t.sub.2] [not equal to] [phi] [??][sup.*][t.sub.1] = [sup.*][t.sub.2]. A pure net N = (P, T, F, W) can be represented by its incidence matrix [N], where [N] is a [absolute value of (P)] x [absolute value of (T)] integer matrix with [N](p, t) = W(t, p) - W(p, t). For a place p (transition t), its incidence vector, a row (column) in [N], is denoted by [N](p, *), ([N](*, t)). The structural bound of a place p is defined as B(p) = max[M(p) | M = [M.sub.0] + [N] x Y, M [greater than or equal to] 0, Y [greater than or equal to] 0].

A P-invariant Y is a P-dimensional vector which satisfies Y [not equal to] 0, [Y.sup.T] x [N] = [0.sup.T]. For any reachable marking M' [member of] R(N,M) and a P-invariant Y of N, [M.sup.T] x Y = [M'.sup.T] x Y. [parallel]Y[parallel] = [p | Y(p) [not equal to] 0] is called the support of Y. [[parallel]Y[parallel].sup.+] = {[p | Y(p) > 0] denotes the positive support of P-invariant Y and [[parallel]Y[parallel].sup.-] = [p | Y(p) < 0] denotes the negative support of P-invariant Y. Y is said to be minimal if [parallel]Y[parallel] is not a superset of the support of any other one and its components are mutually prime. If for all p [member of] [parallel]Y[parallel], Y(p) > 0, then Y is a P-semiflow.

Let S be a nonempty subset of places in N. S is a siphon (trap) if and only if [sup.*]S [subset or equal to] [S.sup.*] ([S.sup.*] [subset or equal to] [sup.*]S). A siphon S is said to be minimal if and only if it contains no other siphons as its proper subset. A minimal siphon is strict if it does not contain a trap (SMS for short).

Given a net (N, [M.sub.0]), a transition t [member of] T is live under [M.sub.0] if and only if for all M [member of] R(N, [M.sub.0]), [there exists]M' [member of] R(N, M) such that M'[t>. A transition t [member of] T is said to be dead under marking M [member of] R(N, [M.sub.0]) if and only if [not there exists][M.sup.*] [member of] R(N, M) such that [M.sup.*][t>. (N, [M.sub.0]) is quasi-live under [M.sub.0] if and only if for all t [member of] T, [there exists]M [member of] R(N, [M.sub.0]) such that M[t>. (N, [M.sub.0]) is live if and only if for all t [member of] T, t is live. In this paper, we will denote the set of live transition under M by [T.sub.L] and the set of dead transition for marking M by [T.sub.D]. From the definition above, it can be known that a live transition can be fired infinitely in R(N, [M.sub.0]). A dead transition for marking M can never be fired in R(N, M).

A number of nodes [n.sub.1], [n.sub.2], ..., [n.sub.k] is called a path of N if for all i [member of] {1, 2, ..., k - 1}, [n.sub.i+1] [member of] [n.sub.i]. An simple path (not a circuit) from [n.sub.1] to [n.sub.k] is a path whose nodes are all different, which can be denoted as SP([n.sub.1], [n.sub.k]). A circuit is an simple path with [n.sub.1] = [n.sub.k].

3. Definitions and Properties of OSC-[S.sup.*]PR Nets

In order to model FMS with full routing flexibility and multiple copies of different resources, [S.sup.*] PR nets are proposed by Ezpeleta et al. [15], which are defined as follows.

Definition 1 (see [15]). Let [I.sub.N] = {1, 2, ..., m} be a finite set of indexes. An [S.sup.*] PR net is a connected generalized self-loop-free Petri net N = (P, T, P, W) where

(i) P = [P.sub.A] [union] [P.sub.0] [union] [P.sub.R] is a partition such that (a) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is called the set of operation places, where [P.sub.A,i] [not equal to] [phi] and [P.sub.A,i] [intersection] [P.sub.A,j] = [phi] for all i [not equal to] j; (b) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is called the set of idle places; (c) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is called the set of resource places;

(ii) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]; for all j [not equal to] i, [T.sub.i] [intersection] [T.sub.j] = [phi];

(iii) W = [W.sub.A] [union] [W.sub.R], where

[W.sub.A]:(([P.sub.A] [union] [P.sub.0]) x T) [union] (T x ([P.sub.A] [union] [P.sub.0])) [right arrow] {0,1} and for all j [not equal to] i, [W.sub.A] : (([P.sub.A,j] [union] {[p.sub.0,j]) x [T.sub.i]) [union] ([T.sub.i] x ([P.sub.A,j] [union]{[P.sub.0,j]})) [right arrow] {0};

[W.sub.R] : ([P.sub.R] x T) [union] (T x [P.sub.R]) [right arrow] N, where N is the set of natural number;

(iv) for all i [member of] [I.sub.N], the subnet [N.sub.i] generated by [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is a strongly connected state machine;

(v) for all r [member of] [P.sub.R], there exists a unique minimal P-semiflow [I.sub.r], such that [parallel][I.sub.r][parallel] [union] [P.sub.R] = {r}, [parallel][I.sub.r][parallel] [union] [P.sub.0] = [phi], [parallel][I.sub.r][parallel] [intersection] [P.sub.A] [not equal to] [phi] and [I.sub.r](r) = 1;

(vi) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII];

(vii) N is pure and strongly connected.

Definition 2 (see [15]). A well-marked [S.sup.*]PR net (N, [M.sub.0]) is a marked Petri net N = (P, T, F, W) with initial marking [M.sub.0] such that for all p [member of] [P.sub.A], [M.sub.0](p) = 0; for all [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]; and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

Due to the structure complexity of [S.sup.*] PR nets, the liveness problem usually relies on the classic state enumeration analysis. Obviously, it is time-consuming due to the state explosion problem. Fortunately, Gadara nets, a subclass of [S.sup.*]PR nets, may utilize some efficient methods such as MIP-based approach for testing their liveness. In fact, Gadara nets are a simplified subclass of [S.sup.*] PR nets with the restriction that no resources are required in all branches and quantity of the same type of resources equals one. The definition is shown as follows.

Definition 3 (see [10]). Let [I.sub.N] = {1, 2, ..., m} be a finite set of indexes. A Gadara net is an ordinary, self-loop-free Petri net N = (P, T, F, [M.sub.0]) where

(i) P = [P.sub.A] [union] [P.sub.0] [union] [P.sub.R] is a partition such that (a) [P.sub.A] = [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is called the set of operation places, where [P.sub.A,i] [not equal to] [phi] and [P.sub.A,i] [intersection] [P.sub.A,j] = [phi] for all i [not equal to] j; (b)[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is called the set of idle places; (c) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is called the set of resource places;

(ii) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]; for all j [not equal to] i, [T.sub.i] [intersection] [T.sub.j] = [phi];

(iii) for all i [member of] [I.sub.N], the subnet [N.sub.i] generated by [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is a strongly connected state machine;

(iv) for all p [member of] [P.sub.A], if [absolute value of ([p.sup.*])] > 1, then for all t [member of] [p.sup.*], [sup.*]t [intersection] [P.sub.R] = [phi];

(v) for all r [member of] [P.sub.R], there exists a unique minimal P-semiflow [I.sub.r], such that [parallel][I.sub.r][parallel] [intersection] [P.sub.R] = {r} (for all p [member of] [parallel][I.sub.r][parallel], [I.sub.r](p) = 1), [parallel][I.sub.r][parallel] [intersection] [P.sub.0] = [phi], [parallel][I.sub.r][parallel] [P.sub.A] [not equal to] [phi], and [I.sub.r](r) = 1;

(vi) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII];

(vii) for all r [member of] [P.sub.R], [M.sub.0](r) = 1. For all p [member of] [P.sub.A], [M.sub.0] (p) = 0. For all [p.sub.0] [member of] [P.sub.0], [M.sub.0]([p.sub.0]) [greater than or equal to] 1.

In most cases, the modeling ability of Gadara nets is not enough. Here, a new subclass of [S.sup.*] PR nets, namely, OSC-[S.sup.*]PR nets, is introduced as follows.

Definition 4. Let (N, [M.sub.0]) be a well-marked [S.sup.*] PR net. A place p is said to be a choice operation place if and only if p [member of] [P.sub.A] and [absolute value of ([p.sup.*])] [greater than or equal to] 2. The set of choice operation places in (N, [M.sub.0]) is denoted by [P.sub.C]; that is, [P.sub.C] = {p [member of] [P.sub.A] | [absolute value of ([p.sup.*])] [greater than or equal to] 2}.

Definition 5. Let (N, [M.sub.0]) be a well-marked [S.sup.*]PR net. A choice operation place p [member of] [P.sub.C] is said to be satisfied operation symmetry choice condition (OSC-Condition) if and only if

[for all][t.sub.1], [t.sub.2] [member of] [p.sup.*], [sup.*][t.sub.1] = [sup.*][t.sub.2],

[for all]p' [member of] [sup.*][t.sub.1] = [sup.*][t.sub.2], w(p', [t.sub.1]) = w(p', [t.sub.2]). (1)

(N, [M.sub.0]) is said to be a well-marked OSC-[S.sup.*] PR net if and only if for all p [member of] [P.sub.C], p satisfies OSC-Condition.

The OSC-Condition confirms that each output transition of each choice operation place must use the same kind and quantity of resources. From Definition 5, it is apparent that OSC-[S.sup.*]PR nets are a subclass of [S.sup.*]PR nets. Since any branch in a Gadara net cannot be associated with any resource [17], it satisfies OSC-Condition as well; that is, Gadara nets are a special case of OSC-[S.sup.*]PR nets.

Example 6. Consider the net shown in Figure 1. For the choice operation places [p.sub.3] and [p.sub.7], all output transitions [t.sub.v1], [t.sub.v2], [t.sub.v3], and [t.sub.v4] use none of resources. So it is an OSC-[S.sup.*]PR net but is not a Gadara net because initial tokens in [r.sub.1], [r.sub.2], [r.sub.3], [r.sub.A], and [r.sub.B] are greater than one.

Similar to the technique in [20,21], the definition of max'-controlled siphon of [S.sup.*]PR nets is introduced as follows.

Definition 7. Let S be a siphon of a [S.sup.*]PR net (N, [M.sub.0]), where S = [S.sub.R] [union] [S.sub.A], [S.sub.R] = S [intersection] [P.sub.R] [not equal to] [empty set], and [S.sub.A] = S [intersection] [P.sub.A] [not equal to] [empty set]. The holder of resource r is defined as the difference of two sets [parallel][I.sub.r][parallel] and {r}: H(r) = [parallel][I.sub.r][parallel] - {r}, and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is the complementary set of siphon S.

Definition 8. Let S be a siphon of a well-marked [S.sup.*]PR net (N, [M.sub.0]). S is said to be max'-marked at marking M [member of] R(N, [M.sub.0]) if and only if [there exists]p [member of] [S.sub.A] such that M(p) [greater than or equal to] 1 or [there exists]r [member of] [S.sub.R] such that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. S is said to be max'-controlled if and only if it is max'-marked under any reachable marking. (N, [M.sub.0]) is said to be max'-controlled if and only if each siphon of it is max'-controlled.

Before proving the liveness condition of OSC-[S.sup.*]PR nets, some lemmas are established first.

Lemma 9. Let p be a choice operation place in a well-marked OSC-[S.sup.*]PR net (N, [M.sub.0]). For all M [member of] R(N, [M.sub.0]), the following conclusions hold.

(i) If [there exists][t.sub.1] [member of] p' such that M[[t.sub.1]>, then for all [t.sub.2] [member of] [p.sup.*] we have M[[t.sub.2]>.

(ii) If [there exists][t.sub.1] [member of] [p.sup.*] such that [t.sub.1] is disabled under M, then for all [t.sub.2] [member of] [p.sup.*] we have that [t.sub.2] is disabled under M.

Proof. This is trivial. Because from Definition 5, for all [t.sub.1], [t.sub.2] [member of] [p.sup.*], [sup.*][t.sub.1] = [sup.*][t.sub.2] and for all p [member of] [sup.*][t.sub.1], w(p, [t.sub.1]) = w(p, [t.sub.2]). Therefore, all of them are enabled for making M if one of them is enabled and all of them are disabled for making M if one of them is disabled.

Lemma 10. Let (N, [M.sub.0]) be a well-marked [S.sup.*]PR net. For all [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], there must exist a simple path SP([p.sub.i], [p.sup.0.sub.i]) from [p.sub.i] to [p.sup.0.sub.i].

Proof. This is trivial, since by condition (iv) in Definition 1, [N.sub.i] generated by [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is strongly connected.

Lemma 11. Let (N, [M.sub.0]) be a well-marked [S.sup.*]PR net. Then, N is quasi-live under [M.sub.0].

Proof. From [M.sub.0], by Definition 2, for all [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], [t.sub.0] is enabled. For the transition [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], since (N, [M.sub.0]) is well-marked, we can construct a trivial firing sequence s = [t.sub.0,i], [t.sub.1,i], ..., from [M.sub.0] by only allowing the execution of only one sequential process i and only one token flowing into process i, reaching a marking M such that M[[t.sub.j,i]>. This is valid for each t [member of] T.

Lemma 12. Let (N, [M.sub.0]) be a well-marked [S.sup.*]PR net, and let M [member of] R(N, [M.sub.0]) be a reachable marking so that t e T is a dead transition under M. Then, [M.sub.0] [not member of] R(N, M).

Proof. Assume that [M.sub.0] [member of] R(N, M). By Lemma 11, [there exists]M' [member of] R(N, M) such that M'[t). This contradicts the hypothesis that t [member of] T is a dead transition under M. Thus, Lemma 12 holds.

Similar to the method in [7], Lemma 13 is proposed which means that if there is a reachable marking such that a transition is dead, then there exists a set of processes where some tokens cannot evolve any more.

Lemma 13. Let (N, [M.sub.0]) be a well-marked OSC-[S.sup.*]PR net. M [member of] R(N, [M.sub.0]) and [t.sup.*] [member of] T is a dead transition under M; then there exist M' [member of] R(N, M) and two subsets J, H [member of] [I.sub.N] such that [I.sub.N] = J [union] H, [I.sub.N] = {1, 2, ..., n}, J [intersection] H = [empty set], J [not equal to] [empty set], and (i) for all h [member of] H, M'([p.sup.0.sub.h]) = [M.sub.0]([p.sup.0.sub.h]); (ii) for all j [member of] J, M'([p.sup.0.sub.j]) < [M.sub.0]([p.sup.0.sub.j]), and [OMEGA] = {[p.sup.*] | p [member of] [P.sub.A], M'(p) > 0} is a set of dead transitions.

Proof. By condition (ii) of Definition 1, for all i [member of] [I.sub.N] and for all M' [member of] R(N, M'), M'([p.sup.0.sub.i]) [less than or equal to] [M.sub.0]([p.sup.0.sub.i]). Therefore, there must exist M' [member of] R(N, M) and two subsets J, H [member of] IN such that [I.sub.N] = J [union] H, [I.sub.N] = {1, 2, ..., n}, J [intersection] H = [empty set] and (i) for all h [member of] H, M'([p.sup.0.sub.h]) = [M.sub.0]([p.sup.0.sub.h]); (ii) for all j [member of] J, M'([p.sup.0.sub.j]) < [M.sub.0]([p.sup.0.sub.j]).

First, prove J [not equal to] 0. Assume that J = [empty set]. Then, it can be concluded that H = [I.sub.N]. Therefore, for all h [member of] [I.sub.N], we have M'([p.sup.0.sub.h]) = [M.sub.0]([p.sup.0.sub.h]), M' = [M.sub.0]. Since (N, [M.sub.0]) is a well-marked OSC-[S.sup.*]PRnet, by Lemma 11, it is quasi-live. Therefore, for all t" [member of] T, [there exists]M" [member of] (N, M'), such that M"[t"). This contradicts the condition that [t.sup.*] [member of] T is a dead transition. Thus, J [not equal to] [empty set].

Then, prove [there exists]M' [member of] R(N, M) such that for all j [member of] J, [OMEGA] = {[p.sup.*] | p [member of] [P.sub.A], M'(p) > 0} is a set of dead transitions. From the marking M' mentioned before and move all processes one by one corresponding to indexes in J as follows approach. By Lemma 10, for all [p.sub.j] [member of] [P.sub.Aj] there must exist a simple path SP([p.sub.j], [p.sup.0.sub.j]) from [p.sub.j] to [p.sup.0.sub.j]. Then, for all [p.sub.j] [member of] {p [member of] [P.sub.Aj], M'(p) > 0}, moving the process along SP([p.sub.j], [p.sup.0.sub.j]), the process will be either dead (since by Lemma 9, all the transitions in the postset of a choice place are disabled as long as one of them is disabled) or back to initial state, in which the tokens in [p.sub.j] will flow back to [p.sup.0.sub.j]. Repeat this for each process corresponding to indexes in J. The net reaches a marking M" [member of] R(N, M') verifying condition (ii) in the hypothesis, because, on the contrary, all process corresponding to indexes in J will get back to the initial state; that is, [M.sub.0] [member of] R(N, M') which is in contradiction with Lemma 12. Let M1 := M"; Lemma 13 holds.

From these lemmas, the main theorems can be obtained as follows.

Theorem 14. Let (N, [M.sub.0]) be a well-marked OSC-[S.sup.*]PR net, M [member of] R(N,[M.sub.0]), and t [member of] T is a dead transition for M. Then [there exists]M' [member of] R(N, M), [there exists]S is a siphon such that S is nonempty and non-max'-marked.

Proof. Consider the making M1 given in Lemma 13.

Let

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. (2)

[S'.sub.R] is the set of resource places which have at least one disabled output transition and this transition is disabled only because of the lack of this resource. [S'.sub.p] is the set of nonmarked places in H(r). It is apparent that S [not equal to] [phi] (otherwise [S'.sub.R] = [phi], then for all p [member of] [P.sub.A] [intersection] {p | M'(p) > 0}, it is true that for all t' [member of] [p.sup.*], M'[t'>, which contradicts the condition that [OMEGA] is a set of dead transitions).

Now we prove that S = [S'.sub.R] [union] [S'.sub.P] is a non-max'-marked siphon under M'.

First, we prove that S is a siphon; that is, for all t' [member of] [sup.*]S, [t.sup.'] [member of] [S.sup.*]. Then, two cases should be considered.

Case 1. t' [member of] [sup.*]r, where r [member of] [S'.sub.R]. By Definition 1, the subnet of an [S.sup.*]PR net is a state machine. Thus, [absolute value of ([sup.*]t' [intersection] [P.sub.A])] = 1. Let [sup.*]t' [intersection] [P.sub.A] = {p'}. Since t' [member of] [sup.*]r, it can be obtained that p' [member of] H(r). Then, two subcases should be considered as follows.

Subcase 1.1. If M'(p') = 0, by the definition of [S'.sub.p], it can be obtained that p' [member of] [S'.sub.p]. Therefore, t' [member of] [S'.sup.*.sub.p] [subset or equal to] [S.sup.*].

Subcase 1.2. If M'(p') [not equal to] 0, by the definition of [OMEGA] in Lemma 13, t' [member of] [OMEGA]. By Lemma 13, t' is a dead transition for M'. Therefore, [there exists]r' [member of] [sup.*]t' [intersection] [P.sub.R] satisfies M'(r') < W(r', t'). By the definition of [S'.sub.R], it can be obtained that r' [member of] [S.sub.R]. Thus, t' [member of] [S'.sup.*.sub.R] [subset or equal to] [S.sup.*].

Case 2. t'[member of] [sup.*]p, where p [member of] [S'.sub.p]. By the definition of [S'.sub.p], [there exists]r [member of] [S'.sub.R], such that p [member of] H(r). If t' [member of] [r.sup.*], then t' [member of] [S'.sup.*.sub.R] [subset or equal to] [S.sup.*] If t' [not member of] [r.sup.*], since p [member of] H(r), there must exist p' [member of] H(r) [intersection] [P.sub.A], such that t' [member of] [(p').sup.*]. Similarly, the two following subcases should be considered.

Subcase 2.1. If M(p') = 0, by definition of [S'.sub.p], it can be obtained that p' [member of] [S'.sub.p]. Therefore, t' [member of] [S'.sup.*.sub.p] [subset or equal to] [S.sup.*].

Subcase 2.2. If M(p') [not equal to] 0, similar to the proof in Subcase 1.2, t' [member of] [S'.sup.*.sub.R] [subset or equal to] [S.sup.*] holds.

In conclusion, [for all]t' [member of] [sup.*]S, t' [member of] [S.sup.*]. Thus, S is a siphon.

Then, we prove siphon S is non-max'-marked under M'. [for all]p [member of] [S'.sub.p], by definition of [S'.sub.p], M'(p) = 0. [for all]r [member of] [S'.sub.R], by definition of [S'.sub.R], [there exists]t [member of] [r.sup.*] such that M' (r) < w(r, t). Thus, by Definition 8, siphon S is non-max'-marked under M'.

In summary, [there exists]M' [member of] R(N, M) and [there exists]S is a siphon such that S is nonempty and non-max'-marked.

Theorem 15. Let (N, [M.sub.0]) be a well-marked OSC-[S.sup.*]PR net. (N, [M.sub.0]) is live if all siphons of (N, [M.sub.0]) are max'-controlled.

Proof. Assume that each siphon in (N,[M.sub.0]) is max'-controlled while (N,[M.sub.0]) not live. Then, [there exists]M [member of] R(N,[M.sub.0]) and [there exists]t [member of] T is a dead transition under M. By Theorem 14, [there exists]M' [member of] R(N, M), [there exists]S is a siphon which is non-max7-marked under M1. This contradicts the assumption that (N,[M.sub.0]) is max'-controlled. Thus (N, [M.sub.0]) is live.

It should be noticed that Theorem 15 is a sufficient liveness condition for OSC-[S.sup.*] PR nets. Thus, there may be some live OSC-[S.sup.*]PR nets which are not max'-controlled.

4. Liveness Test Algorithm for OSC-[S.sup.*]PR Nets

In this section, an MIP-based liveness test algorithm is proposed, which is based on Theorem 15 in Section 3. The operators set of an operation place is introduced here, which is similar to [14].

Definition 16. Let N be an [S.sup.*]PR net. For p [member of] [P.sub.A], [R.sub.p] = {r | r [member of] [P.sub.R], p [member of] [H.sub.r]} the resource places that are required by p are called the set of operators of p.

According to Theorems 14 and 15, the following theorem can be obtained, which is also a liveness test algorithm for testing liveness of OSC-[S.sup.*]PR nets.

Theorem 17 (Algorithm 1). Let (N,[M.sub.0]) be a well-marked [S.sup.*] PR net. Then, the minimal non-max -marked siphon S under M is determined by S = [p [member of] P | [s.sub.p] = 1}, where [s.sub.p] and M are obtained by the following MIP formulation:

min [summation over (p[member of]P\[P.sup.0])] [s.sub.P] (3)

such that

[absolute value of ([t.sup.*])][summation over (p[member of] [sup.*]t)] [s.sub.p] [greater than or equal to] [summation over (p[member of][t.sup.*])] [s.sub.p], t [member of] T, p [member of] P (4)

M = [M.sub.0] + [N] x Y, M [greater than or equal to] 0, Y [greater than or equal to] 0 (5)

[summation over (p[member of][P.sup.0])] = 0 (6)

[summation over (p[member of][P.sub.A])] [S.sub.p] [greater than or equal to] 1 (7)

[summation over (p[member of][P.sub.R])] [S.sub.p] [greater than or equal to] 1 (8)

p [member of] [P.sub.A], t [member of] [P.sup.*]

[e.sub.t] [greater than or equal to] M(p)/B(p) (9)

M (p) [greater than or equal to] [e.sub.t] (10)

[s.sub.p] + [e.sub.t] [less than or equal to] 1 (11)

r [member of] [P.sub.R], t [member of] [r.sup.*], p [member of] [P.sub.A] [intersection] [sup.*]t, r' [member of] [R.sub.p]

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (12)

[s.sub.p], [e.sub.t] [member of] {0,1} (13)

Y (p) [member of] N, (14)

where M [member of] R(N, [M.sub.0]), B(p) is the structural bound of place p.

Then, the minimal non-max'-marked siphon is the set of places with [s.sub.p] = 1.

Proof. Let S be a non-max'-marked siphon. By Definition 8, the following conclusions hold:

(i) for all p [member of] [S.sub.A], M(p) = 0;

(ii) for all [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

Then, let us explain the meaning of the constraints one by one.

Objective (3) ensures that the siphon is a minimal siphon.

Constraint (4) ensures that [s.sub.p] is the characteristic vector of the siphon [22].

Constraint (5) ensures that M [member of] R(N, [M.sub.0]). This is trivial.

Constrains (6)-(8) ensure that the siphon contains no idle place and has one operation place and one resource place at least.

In constrains (9)-(11), p [member of] [P.sub.A], t [member of] [p.sup.*]. [e.sub.t] means whether transition t is disabled by the operation place p which is in the preset of it. If t is disabled by the operation place p, [e.sub.t] = 0. Otherwise, [e.sub.t] =1. This comes from the following facts. If M(p) [greater than or equal to] 1, then transition t is enabled by the operation place p. From constraint (9) and definition of structural bound B(p) in Section 2, it can be obtained that [e.sub.t] [greater than or equal to] M(p)/B(p) > 0. Since [e.sub.t] [member of] [0,1}, we have [e.sub.t] = 1, which follows the meaning of [e.sub.t]; if M(p) = 0, then transition t is disabled by the operation place p. From constraints (9) and 10), it can be obtained that [e.sub.t] [greater than or equal to] M(p)/B(p) = 0 and [e.sub.t] [greater than or equal to] M(p) = 0. Thus, [e.sub.t] = 1 which follows the meaning of [e.sub.t].

Then, constraint (11) ensures that in the siphon S condition (i) holds. This comes from the following fact: for all p [member of] [S.sub.A], by the meaning of [s.sub.p], we have sp = 1. By constraint (11), it can be obtained that [e.sub.t] [less than or equal to] 1 - [s.sub.p] = 0. Since [s.sub.p], [e.sub.t] [member of] [0,1}, we have [e.sub.t] = 0. By the conclusions above, it can be obtained that transition t is disabled by the operation place p and M(p) = 0. This follows condition (i).

Constraint (12) ensures that in siphon S condition (ii) will hold. Since [s.sub.p] [member of] [0,1}, the following two cases should be considered.

Case 1. If [s.sub.r] = 0, that is, r is not an element of siphon S, then [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Constrain (10) is equivalent to M(r) [greater than or equal to] 0 which is trivial and will not add extra constraints to the formulations.

Case 2. If [s.sub.r] = 1, that is, r is an element of siphon S, then constrain (10) is equivalent to

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. (15)

Then we explain that constraint (15) indicates condition (ii). Two cases should be considered. If p [member of] [s], that is, ter' Hits]", then we can obtain that p [not member of] S and p [member of] H(r'). Since p [not member of] S, (1 - [s.sub.p]) = 1. By Definition 16 and p [member of] H(r'), it can be obtained that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Thus, (15) can be transferred into [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], which means [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. If p [not member of] [s], that is, t [not member of] [r.sup.*] [intersection] [[S].sup.*], then we can obtain that p [member of] S or p [not member of] H(r'). Similarly, it can be obtained that (1 - [s.sub.p]) = 0 or [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Then, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], this kind of transitions will not be taken into comparison [14].

Therefore, constraint (12) ensures that in the siphon S condition (ii) holds.

In conclusion, constraints (11) and (12) ensure that the obtained siphon satisfies conditions (i) and (ii), that is, is a non-max'-marked siphon.

In summary, if the MIP formulation has a feasible solution, the obtained siphon is the minimal non-max'-marked siphon.

Thus, Theorem 17 can find a non-max'-controlled siphon at a bad marking. It utilizes some MIP tools to find non-max'controlled siphons rather than traverse the state space of the net. Following Theorem 17, Corollary 18 can be obtained.

Corollary 18. Let (N,[M.sub.0]) be a well-marked OSC-[S.sup.*] PR net. It is live if Algorithm 1 has no feasible solution.

Proof. For a well-marked OSC-[S.sup.*] PR net, Algorithm 1 having no feasible solution means that all siphons of this net are max'-controlled. By Theorem 15, it is live.

Example 19. Applying Algorithm 1 to the OSC-[S.sup.*] PR net in Figure 1 and solving by Lingo [23] no feasible solution can be found. By Corollary 18, it is live, which follows the fact that it is a live net.

5. Liveness Test for [S.sup.*]PR Nets

In order to test liveness of the [S.sup.*] PR nets, an indirect method is given in this section, which comprises two steps as follows: first, for a given [S.sup.*] PR net, constructing an OSC-[S.sup.*] PR net to ensure that if the latter is live then the former must be live; second, testing liveness of the constructed OSC-[S.sup.*] PR net by the aforementioned MIP-based algorithm.

Remark 20. In the following sections, we assume that for all [P.sub.0i] [member of] [P.sub.0], [absolute value of [P.sup.*.sub.0i]] = 1.

Remark 20 restricts that each process in the net can only have one start action.

In the following, the constructing algorithm is proposed.

Insertion 1. Let (N,[M.sub.0]) be a well-marked [S.sup.*]PR net. For all p [member of] P, t [member of] [p.sup.*], a pair of virtual place and virtual transition {[p.sub.v], [t.sub.v]} is inserted into (p, t) as follows:

(i) F = (F [union] (p, [t.sub.v]) [union] ([t.sub.v], [P.sub.v]) [union] ([P.sub.v], t))/(p, t);

(ii) [P.sub.A] = [P.sub.A] [union] {[P.sub.v]}, T = T [union] {[t.sub.v]};

(iii) w(p, [t.sub.v]) = 1, w([t.sub.v], [p.sub.v]) = 1, w([p.sub.v], t) = 1;

(iv) [M.sub.0] ([p.sub.v]) = 0.

Then, for a given [S.sup.*] PR net, an OSC-[S.sup.*] PR net can be constructed by the following algorithm.

Algorithm 2

Input. [S.sup.*]PR net (N, [M.sub.0]).

Output. A constructed net ([MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]).

Step 1. [OMEGA] := [P.sub.C], [P.sub.v] := [phi], [T.sub.v] := [phi], (N', [M'.sub.0]) := (N, [M.sub.0]);

Step 2. while [OMEGA] [not equal to] [phi], for the net (N', [M'.sub.0]) do the following:

Step 2.1. Post := [p.sup.*]:

Step 2.2. while Post [not equal to] [phi], do the following:

Step 2.1.1. for all t [member of] Post, insert {[p.sub.vi], [t.sub.vi]} to (p, t) by Insertion 1 and obtain (N", [M".sub.0]);

Step 2.1.2. Post = Post/{t}, [P.sub.v] = [P.sub.v] [union] {[p.sub.vi]}, [T.sub.v] = [T.sub.v] [union] {[t.sub.vi]}, i+ = 1, (N', [M'.sub.0]):= (N", [M".sub.0]);

end while

Step 2.3. [OMEGA] := [OMEGA]/{p};

endwhile

Step 3. [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII];

Step 4. Output the constructed net [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

Since [P.sub.c] and [p.sup.*] are finite sets, it can be obtained that Algorithm 2 will end in finite steps. What is more, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is called the constructed net of (N, [M.sub.0]), and (N, [M.sub.0]) is called original [S.sup.*]PR net of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

Remark 21. By Algorithm 2 and Insertion 1, it is trivial that for all p [member of] [P.sub.V], [[??].sub.0](p) = 0 and for all p [member of] P, [[??].sub.0](p) = [M.sub.0](p); that is, [[??].sub.0](p) = [[summation].sub.p[member of]P] [M.sub.0](p)p.

Lemma 22. Let (N, [M.sub.0]) be a well-marked [S.sup.*]PR net and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is the constructed net obtained by Algorithm 2. Then, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is a well-marked OSC-[S.sup.*]PR net.

Proof. First, we prove that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is a well-marked S * PR net. By Insertion 1, the virtual places are considered as operation places. Thus, it is apparent that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] satisfies conditions (i), (ii), (iii), (iv), and (v) in Definition 1. Then, we prove that it satisfies conditions (vi) and (vii). Without loss of generality, assume that [p.sub.1] [member of] [P.sub.c] and [t.sub.1] [member of] [p.sup.*sub.1] in (N,[M.sub.0]). Then by Insertion 1, [p.sub.V] and [t.sub.V] will be inserted to ([p.sub.1], [t.sub.1]). Since [sup.*][t.sub.V] = {[p.sub.1]}, [t.sup.*.sub.v] = {[p.sub.v]} and [p.sup.*.sub.v] = {[t.sub.1]}, it can be obtained that no self-loop is inserted to [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] by Insertion 1. This is valid for each insertion in Algorithm 2. Therefore, it can be concluded that no self-loop will be inserted to [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]; that is, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] will still be a pure net. What is more, [p.sub.1] and [t.sub.1] are still connected by the path [p.sub.1], [t.sub.V], [p.sub.V], [t.sub.1]. This is also valid for all the insertions in Algorithms. Hence, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] will still be strongly connected; that is, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] satisfy condition (vii) in Definition 1. Since [t.sub.V] do not attach to any resources, [p.sub.V] will use the resources that p [member of] [P.sub.C] [intersection] [sup.*][t.sub.V] has used. Therefore, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] satisfies condition (vi) of Definition 1. Henceforth, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is an [S.sup.*]PR net. What is more, by Remark21, the initial marking of virtual place is zero and the initial marking of other places stays the same. Thus, regarding virtual places as members of operation places, (N, [M.sub.0]) satisfies Definition 2 as well; that is, (N, [M.sub.0]) is a well-marked [S.sup.*]PR net.

Second, we prove that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is an OSC-[S.sup.*]PR net. Considering Step 2.1 in Algorithm 2 with Remark 20, it is guaranteed that for all p [member of] [P.sub.A] if [absolute value of ([p.sup.*])] [greater than or equal to] 2, then for all t [member of] [p.sup.*], [sup.*]t = {p} and t [member of] [T.sub.V]. Thus [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] satisfies Definition 5; that is, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is an OSC-S * PR net.

In summary, (N,[M.sub.0]) is a well-marked OSC-[S.sup.*]PR net.

Example 23. The Petri net plant in Figure 2 is an [S.sup.*] PR. Since [p.sup.*.sub.3] = {[t.sub.3], [t.sub.5]}, [sup.*][t.sub.3] [not equal to] [sup.*][t.sub.5] and [p.sup.*.sub.7] = {[t.sub.8], [t.sub.9]}, [sup.*][t.sub.8] [not equal to] [sup.*][t.sub.9], it does not satisfy the OSC-Condition. By Algorithm 2, the constructed net is shown as Figure 1, and it is an OSC-[S.sup.*]PR net.

Then, we will prove that the original [S.sup.*] PR net must be live if its constructed net is live.

Theorem 24. Let (N, [M.sub.0]) be an [S.sup.*]PR net and let [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] be its constructed net. If [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is live, (N, [M.sub.0]) is live.

Proof. The liveness of Petri nets is determined by the firing sequence of transitions and the number of tokens consumed and produced by transitions. If the each firing sequence of (N,[M.sub.0]) has a corresponding firing sequences of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and the number of tokens consumed and produced by those firing sequences is the same, then it can be obtained that if [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is live, (N, [M.sub.0]) is live. In other words, (N, [M.sub.0]) must retain the number or direction of flow of tokens in [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. What is more, by Remark 21, the initial making of (N, [M.sub.0]) and (N[M.sub.0]) satisfies [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Thus, this theorem could be proved by checking whether each firing sequence of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] has a corresponding firing sequence in [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] which consumes and produces the same number of tokens in the same places.

The only difference between an [S.sup.*]PR net and its constructed net is the virtual transitions and virtual places that are inserted by Algorithm 2. Without loss of generality, we could assume that in (N,[M.sub.0]), p [member of] [P.sub.C], t [member of] [p.sup.*] and in [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], [sup.*][t.sub.v] = {p}, [t.sup.*.sub.v] = {[p.sub.v]} and [p.sup.*.sub.v] = {t}. In the firing sequence of transitions, the insertion means a replacement of the firing of t by a subfiring sequence [t.sub.v]t. From the viewpoint of token number, the subfiring sequence produces tokens to each p' [member of] [t.sup.*] by the weight of w(t, p) and it demands tokens from r [member of] [sup.*]t [intersection] [P.sub.R] and p by the weight of w(r, t) and w(p, [t.sub.v]) (the token in [p.sub.v] remains zero). Since in [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] which is equal to w(p,t) = 1 in (N,[M.sub.0]), the number of tokens demand and produced by the subfiring sequence is equal to that number of transition t. Therefore, the number of tokens in each place changed by firing [t.sub.v]t is the same as that of firing t. This is valid for each t e [P.sup.*.sub.C]. Therefore, for any firing sequence a of (N,[M.sub.0]), each transition [t.sub.i] (which satisfies [t.sub.i] [member of] [([P.sub.C]).sup.*]) in a is replaced by the subfiring sequence [t.sub.vi][t.sub.i], a new firing sequence [??] will be obtained for [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], and the token in each place changed by firing [??] must be the same to that of firing a (the token in [p.sub.v] remains zero). Thus, it can be obtained that if [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is live, then (N, [M.sub.0]) is live.

So, the liveness of an [S.sup.*]PR net (N, [M.sub.0]) can be tested the algorithm shown as follows.

Algorithm 3

Input. [S.sup.*]PR net (N, [M.sub.0]).

Output. a non-max'-marked siphon S.

Step 1. Construct an OSC-[S.sup.*]PR [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] from (N,[M.sub.0]) by Algorithm 2;

Step 2. Obtain a non-max'-marked siphon S of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] by Algorithm 1;

Step 3. Output S of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

Theorem 25. Let (N,[M.sub.0]) be a well-marked [S.sup.*]PR net. If Algorithm 3 has no feasible solution, then (N, [M.sub.0]) is live.

Proof. By Algorithm 3, (N,[M.sub.0]) will be transformed to its constructed [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. By Lemma 22, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is an OSC-[S.sup.*]PR net. By Step 2 and Step 3, Algorithm 3 has no feasible solution which means that applying Algorithm 1 to [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] there is no feasible solution obtained. Then, by Corollary 18, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is live. Therefore, by Theorem 24, it can be obtained that (N, [M.sub.0]) is live.

Example 26. The Petri net model in Figure 2 is an [S.sup.*]PR net, but not an OSC-[S.sup.*]PR net. The choice places [p.sub.3] and [p.sub.7] dissatisfy the OSC-Condition. By Algorithm 2, {[t.sub.v1], [p.sub.v1]} and {[t.sub.v2], [p.sub.v2]} are inserted at the rear of [p.sub.3], and {[t.sub.v3], [p.sub.v3]} and {[t.sub.v4], [p.sub.v4]} are inserted at the rear of [p.sub.7]. The constructed net is obtained as Figure 1. Then, by Algorithm, it can be obtained that the constructed net is live. By Theorem 24, the original in Figure 2 is live.

6. Examples

In this section, a typical example (shown as Figure 3) is quoted to illustrate Algorithm 2, which is a classic FMS cell with 2 buffers, 4 machines, and 3 robots [15]. And it can be modeled as Figure 4.

Since the choice operation places [P.sub.1][R.sub.1], [P.sub.1][R.sub.2], and [P.sub.2][R.sub.2] dissatisfy the OSC-Condition, the net in Figure 4 is not an OSC-[S.sup.*]PR net. By the Step 2.1 of Algorithm 2, pairs of virtual transitions and places should be inserted at the rear of each branch of choice places; in other words, {T[V.sub.1], [P.sub.1][R.sub.1][V.sub.1]}, {T[V.sub.2][P.sub.1][R.sub.1] [V.sub.2]}, {T[V.sub.3], [P.sub.1][R.sub.2][V.sub.1]}, {T[V.sub.4], [P.sub.1][R.sub.2][V.sub.2]}, {T[V.sub.5], [P.sub.2][R.sub.2][V.sub.1]}, and {T[V.sub.6], [P.sub.2][R.sub.2][V.sub.2]} are inserted. Then, the constructed net is shown as Figure 5.

After applying the MIP formulation in Theorem 17 to Figure 5 and solving it with LINGO [23] we obtain a minimal non-max'-marked siphon S = [P.sub.1][R.sub.3] + [P.sub.2][M.sub.4] + [H.sub.4] + [R.sub.3], which follows the fact that the net is nonlive.

Generally, some structural controllers can be added to enforce the liveness of the net (referring to [9, 10, 15, 21]). Here, four controllers V[S.sub.1], V[S.sub.2], V[S.sub.3], and V[S.sub.4] are added into the net in Figure 5, and the resulted [S.sup.*]PR net is shown as Figure 6. Then, the constructed net in Figure 7 can be obtained by Algorithm 2. It can be verified that the net in Figure 7 is live. By Algorithm 3, the net in Figure 6 must be live.

7. Conclusions

It is well-known that [S.sup.3]PR nets and [S.sup.4]PR nets can model sequential FMS, while full routine flexibilities can be modeled by [S.sup.*]PR nets. As a subclass of [S.sup.*]PR nets, OSC-[S.sup.*]PR nets have some modeling abilities about routine flexibilities with the restriction of each choice operation using the same type and quantity of resources. Obviously, Gadara nets [17] are a special case of OSC-[S.sup.*]PR nets satisfying no resources needed in all choice operations. Henceforth, their modeling capabilities can be illustrated as Figure 8 approximately.

It is worth to say that Theorem 15 is just a sufficient condition, and some live OSC-[S.sup.*] PR nets may contain non-max'-controlled siphons. In other words, sometimes Theorem 15 is a little strict though, so there maybe exist ways to loosen the sufficient condition. Moreover, the liveness property of [S.sup.*] PR nets still cannot be tested directly by using standardized mixed integer programming (MIP) tools in this paper. And we should make great efforts to develop more efficient algorithms for testing liveness of [S.sup.*] PR nets.

http://dx.doi.org/10.1155/2014/319281

Conflict of Interests

The authors declare that there is no conflict of interests

regarding the publication of this paper.

Acknowledgments

The authors would like to thank the National Nature Science Foundation of China under Grant no. 61071062, the Provincial Nature Science Foundation of Zhejiang under Grant no. Y12F02030, and the School Funding of Hangzhou Normal University under Grant no. 2013JGJ001.

References

[1] G. Liu, D. Y. Chao, and M. Uzam, "Maximally permissive deadlock prevention via an invariant controlled method," International Journal of Production Research, vol. 51, no. 15, pp. 4431-4442, 2013.

[2] J. Ezpeleta, F. Garcia-Valles, and J. M. Colom, "A class of well structured Petri nets for flexible manufacturing systems," in Application and Theory of Petri Nets, pp. 64-83, Springer, Berlin, Germany, 1998.

[3] M. D. Byrne and P. Chutima, "Real-time operational control of an FMS with full routing flexibility," International Journal of Production Economics, vol. 51, no. 1-2, pp. 109-113, 1997.

[4] T. Murata, "Petri nets: properties, analysis and applications," Proceedings of the IEEE, vol. 77, no. 4, pp. 541-580, 1989.

[5] F. Chu and X.-L. Xie, "Deadlock analysis of Petri nets using siphons and mathematical programming," IEEE Transactions on Robotics and Automation, vol. 13, no. 6, pp. 793-804, 1997.

[6] F. Tricas, F. Garcia-Valles, J. M. Colom, and J. Ezpeleta, "A structural approach to the problem of deadlock prevention in process with resources," in Proceedings of the 4th International Workshop on Discrete Event Systems (WODES '98), pp. 273-278, Cagliari, Italy, August 1998.

[7] J. Ezpeleta, J. M. Colom, and J. Martinez, "A petri net based deadlock prevention policy for flexible manufacturing systems," IEEE Transactions on Robotics and Automation, vol. 11, no. 2, pp. 173-184, 1995.

[8] J. Ezpeleta, F. Garcia-Valles, and M. Colom J, "A class of well structured Petri nets for flexible manufacturing systems," in Application and Theory of Petri Nets, pp. 64-83, Springer, Berlin, Germany, 1998.

[9] Z. Li and M. Shpitalni, "Smart deadlock prevention policy for flexible manufacturing systems using Petri nets," IET Control Theory and Applications, vol. 3, no. 3, pp. 362-374, 2009.

[10] Y. Huang, M. Jeng, X. Xie, and S. Chung, "Deadlock prevention policy based on Petri nets and siphons," International Journal of Production Research, vol. 39, no. 2, pp. 283-305, 2001.

[11] A. Giua and C. Seatzu, "Liveness enforcing supervisors for railway networks using ES2 PR Petri nets," in Proceedings of the 6th IEEE International Workshop on Discrete Event Systems, pp. 55-60, 2002.

[12] J. Park and S. A. Reveliotis, "Deadlock avoidance in sequential resource allocation systems with multiple resource acquisitions and flexible routings," IEEE Transactions on Automatic Control, vol. 46, no. 10, pp. 1572-1583, 2001.

[13] Y.-Y. Shih, D. Y. Chao, and C.-Y. Chiu, "A new MIP test for S3 PGR2," in Global Perspective for Competitive Enterprise, Economy and Ecology, Advanced Concurrent Engineering, pp. 41-52, Springer, London, UK, 2009.

[14] G. Liu and Z. Li, "General mixed integer programming-based liveness test for system of sequential systems with shared resources nets," IET Control Theory & Applications, vol. 4, no. 12, pp. 2867-2878, 2010.

[15] J. Ezpeleta, F. Tricas, F. Garcia-Valles, and J. M. Colom, "A banker's solution for deadlock avoidance in FMS with flexible routing and multiresource states," IEEE Transactions on Robotics and Automation, vol. 18, no. 4, pp. 621-625, 2002.

[16] Z. Zhang and W. Wu, "Sequence control of essential siphons for deadlock prevention in petri nets," Transactions on Embedded Computing Systems, vol. 12, article 8, no. 1, 2013.

[17] Y. Wang, H. Liao, S. Reveliotis, T. Kelly, S. Mahlke, and S. Lafortune, "Gadara nets: modeling and analyzing lock allocation for deadlock avoidance in multithreaded software," in Proceedings of the 48th IEEE Conference on Decision and Control and 28th Chinese Control Conference (CDC/CCC 09), pp. 4971-4976, Shanghai, China, December 2009.

[18] H. Liao, Y. Wang, H. K. Cho et al., "Concurrency bugs in multithreaded software: modeling and analysis using Petri nets," Discrete Event Dynamic Systems: Theory and Applications, vol. 23, no. 2, pp. 157-195, 2013.

[19] Z. W. Li and M. C. Zhou, Deadlock Resolution in Automated Manufacturing Systems: A Novel Petri Net Approach, Springer, London, UK, 2009.

[20] D. Y. Chao, "Max'-controlled siphons for liveness of [S.sup.3]PG[R.sup.2]," IET Control Theory and Applications, vol. 1, no. 4, pp. 933-936, 2007.

[21] C. Zhong and Z. Li, "Self-liveness of a class of Petri net models for flexible manufacturing systems," IET Control Theory & Applications, vol. 4, no. 3, pp. 403-410, 2010.

[22] F. Basile, P. Chiacchio, A. Giua, and C. Seatzu, "Deadlock recovery of Petri net models controlled using observers," in Proceedings of the 8th International Conference on Emerging Technologies and Factory Automation (ETFA '01), vol. 2, pp. 441-449, Antibes-Juan les Pins, France, October 2001.

[23] LINGO, "Premier optimization modeling tools," http://www .lingo.com/.

Lida Dong, (1,2) Tianyang Chi, (1) Chengcheng Zhu, (2) and Jun Yin (2)

(1) Hangzhou Institution of Service Engineering, Hangzhou Normal University, Hangzhou 310027, China

(2) Institution of Electronic Circuit & Information Systems, Zhejiang University, Hangzhou 310027, China

Correspondence should be addressed to Tianyang Chi; tianyang_chi@hotmail.com

Received 31 December 2013; Revised 20 June 2014; Accepted 2 July 2014; Published 7 August 2014

Academic Editor: Javier Oliver

Printer friendly Cite/link Email Feedback | |

Title Annotation: | Research Article; flexible manufacturing systems |
---|---|

Author: | Dong, Lida; Chi, Tianyang; Zhu, Chengcheng; Yin, Jun |

Publication: | Journal of Applied Mathematics |

Article Type: | Report |

Date: | Jan 1, 2014 |

Words: | 10427 |

Previous Article: | A postverification method for solving forced Duffing oscillator problems without prescribed periods. |

Next Article: | A fast independent component analysis algorithm for geochemical anomaly detection and its application to soil geochemistry data processing. |

Topics: |