Closed-loop Live Marked Graphs under Generalized Mutual Exclusion Constraint Enforcement

Discrete Event Dyn Syst (2009) 19:1–30 DOI 10.1007/s10626-008-0050-7

Closed-loop Live Marked Graphs under Generalized Mutual Exclusion Constraint Enforcement Francesco Basile · Laura Recalde · Pasquale Chiacchio · Manuel Silva

Received: 9 July 2006 / Accepted: 18 August 2008 / Published online: 25 September 2008 © Springer Science + Business Media, LLC 2008

Abstract Enforcing a supervisory control policy to avoid forbidden states on a discrete event system modeled by a Petri net may result in a non live system. This may happen even if the admissible states are specified by Generalized Mutual Exclusion Constraints (GMECs). This leads to the problem of synthesizing a maximally permissive control policy preserving liveness of the system under a GMEC. This problem is very interesting in practice, but difficult even for a restricted class of systems. In this paper, we focus on systems which can be modeled as live and safe Marked Graphs (MGs). On such systems, when some of the transitions are uncontrollable, a GMEC can be forced by a monitor place if a not maximally permissive policy is accepted, otherwise a more complex control has to be adopted. Anyway, liveness of the closedloop system (plant plus control) is not guaranteed. Two sufficient conditions to verify the closed-loop liveness of a live and safe MG plant controlled by a monitor are derived. A sufficient condition for closed loop liveness of MGs where a GMEC has been enforced on is derived. In addition, a set of predicates is provided that enforces, in a maximally permissive way, a GMEC while preserving closed-loop liveness on live and safe MG systems under some restrictions. Keywords Supervisory control · Closed-loop liveness · Generalized mutual exclusion constraint · Monitor places · Marked graphs

This research has been partially supported by MIUR, Italy (Progetto PRIN 2007 - Tematiche di controllo in celle robotizzate iperflessibili). F. Basile (B) · P. Chiacchio Dipartimento di Ingegneria dell’Informazione e Ingegneria Elettrica, Università degli Studi di Salerno, Via Ponte don Melillo, 1 – 84084 Fisciano (SA), Italy e-mail: [email protected] L. Recalde · M. Silva Dep. de Informática e Ingeniería de Sistemas, Maria de Luna 3, 50015 Zaragoza, Spain

2

Discrete Event Dyn Syst (2009) 19:1–30

1 Introduction Supervisory control theory for discrete event systems (DESs) was initiated by Ramadge and Wonham (1989). In their seminal work they represent both the plant, i.e. the system to be controlled, and the desired closed-loop behaviour, by regular languages. The specific problem addressed was to synthesize a controller, called supervisor, to achieve the largest subset of the desired language that is nonblocking, i.e. that does not prevent any task to be completed, by disabling or enabling controllable events. The unwanted sequences may be related, for example, to safety requirements. Although regular languages have been an useful framework to start such DES control theory, they are limited in representing systems consisting of numerous interacting subsystems. For this reason, a control theory for DESs modeled by partially-synchronized products of automata and Petri nets (PNs) has been developed (Holloway et al. 1997; Stremersch 2001). PNs are effective particularly when there is a high degree of concurrency and synchronization. In control theory general PN models are extended with the concept of controllable transitions. Two possibilities can be explored. In the first one, a controllable transition may be disabled by an external control input represented by the value of a logical predicate; in this case we speak of controlled PNs and of interpreted supervisor (Giua et al. 1993). In the second one the feedback control policy is implemented by a PN controller, whose marking enables or disables, according to the logical specifications, the controllable transitions it is connected to in the closed-loop net. Input arcs from the controller to uncontrollable transitions are not allowed. In this case we have a compiled supervisor and the closed-loop system properties can be analyzed in a single framework, because both the plant and the controller are represented by PNs. What we lose is the expressive power of the control law, that, in the general case, cannot be implemented by a PN in a maximally permissive form (Holloway et al. 1997). Here we consider the problem of forbidden state specification in conjunction with liveness under control. Avoiding forbidden states is a very common specification for a DES and a lot of work has been done on the subject (Holloway et al. 1997), but unfortunately, the solution may lead the system to deadlocks. However, liveness is a fundamental specification for a DES control problem, like stability in the classical control theory. Furthermore, notice that even if we have a net-based supervisor to enforce a forbidden state specification, the closed-loop net system is in general more complex than the plant net was for the liveness analysis. A forbidden state problem may represent, for example, a resource sharing problem. Enforcing it introduces conflicts not present in the plant model and thus the resulting closed-loop net system belongs generally to a wider net subclass, where the liveness preservation may be a much more complex problem. In this paper we restrict our study to plants modeled by Marked Graphs (MGs). There are several reasons for this: MGs are relevant in the modeling of automated manufacturing systems; MGs are a well studied net subclass and so their behaviour is well known; the difficulty of the addressed problem would not have allowed to get a solution for more complex nets, at least in this initial stage of the research. Furthermore, notice that the closed loop net formed by a MG and the controller

Discrete Event Dyn Syst (2009) 19:1–30

3

enforcing a set of GMECs, as for example a MG plus a monitor, belongs in general to a net subclass wider than MG and thus it is not trivial to guarantee its liveness. The approach presented in this paper consists of two steps at the most. •

•

First, enforce a forbidden-state specification without liveness specification, and then analyze the liveness property of the closed-loop system. In some cases the computational complexity required for the synthesis of a controller without the liveness specification and the checking of the closed-loop liveness, especially when the controller is compiled, may be low compared with the one required if the closed-loop liveness is taken into account directly with the control specification: so, it may be convenient to try. In this paper we consider, as forbidden state specification, a Generalized Mutual Exclusion Constraint (GMEC) that limits a weighted sum of tokens in a subset of places. When all transitions are controllable it was shown that it is possible to impose a GMEC in a maximally permissive way by a monitor (Giua et al. 1992; Yamalidou et al. 1996). The monitor synthesis is very efficient from the computational point of view and it leads to a compiled supervisor. In presence of uncontrollable transitions (Moody and Antsaklis 2000; Basile et al. 2006), monitors are not always able to implement a maximally permissive policy to enforce GMEC. However, because of their simplicity they may represent an acceptable suboptimal solution to the control problem and, thus, in this paper the problem of checking liveness of a MG system controlled by a monitor is considered providing two sufficient conditions which permit the check at very low computational cost. Second, if the controller synthesized without liveness specification is not live, it is necessary to synthesize a control policy for the forbidden state problem that guarantees closed-loop liveness. This is in general more complex. In this paper, if the net system controlled by the monitor results to be nonlive, the problem of synthesizing a controller which guarantees both GMEC and liveness enforcing on MGs is addressed. An interpreted supervisor to enforce in a maximally permissive way a GMEC on a MGs under some restrictions, while keeping liveness, is proposed. The synthesis of the control policy requires a computational effort polynomial with respect to the net size and it is suitable to be executed on line since it requires just the evaluation of logical predicates essentially consisting in the comparison between the values of some counter variables with integer numbers.

This paper has some points of contacts with the one of Reveliotis (Park and Reveliotis 2002) and the ones of Iordache and Antsaklis (Iordache et al. 2002; Iordache and Antsaklis 2003). In Park and Reveliotis (2002) a suboptimal approach is presented. It can be applied to resource allocation problems specified as set of GMECs for a net subclass known as Simple Sequential Process (S2 P) consisting of a number of strongly connected state machines connected by resource places enforcing GMECs. The problem to include GMECs not representing resource allocation problems is treated as an extension. The main difference with this work is that the control law here proposed can be applied to MGs and that it is maximally permissive.

4

Discrete Event Dyn Syst (2009) 19:1–30

In Iordache et al. (2002) and Iordache and Antsaklis (2003) a procedure for the design of supervisors that enforce the transitions in a set T to be live is presented. The procedure is general and no assumption on the PN structure is required. However, the procedure is iterative and termination is not guaranteed unless the PN is bounded and it requires a certain number of off-line steps having exponential computational complexity (Iordache and Antsaklis 2006) since it is required the computation of minimal active siphons. The control law is represented by the conjunction of GMECs enforceable by a set of monitor places or by the disjunction of sets of GMECs which cannot be enforced by monitors; in any case the on-line computational is negligible but it is maximally permissive only when all transitions are controllable and observable. In presence of partial controllability and observability maximal permissiveness is not guaranteed. The main differences with this work are: the main goal is liveness or deadlock-freeness of the plant net and the problem to enforce GMECs is treated as an extension while in this work the plant net is supposed to be live and the control law must avoid deadlocks induced by one or several GMECs; the procedure is general while the control law proposed in this paper can be applied only to MGs but it is maximally permissive and the synthesis has polynomial complexity. Section 2 introduces notations about PNs and presents the problem considered in this paper by a simple example, while in Section 3 control subnet definition, used in the following sections, is introduced. The main results are collected in Sections 4, 5 and 6. Some results are presented in Section 4, aimed to verifying if a net controlled by a monitor is closed-loop live. The given conditions suffer of two main drawbacks: they are sufficient, but not necessary conditions, and can only be applied to monitors. However, the computational complexity of control synthesis and of liveness checking is very low. Therefore, these conditions could result very useful. In Section 5 a sufficient condition is presented to check closed loop liveness for a live and bounded MG system where a GMEC has been imposed on by checking closed loop liveness of proper subnets computed from constrained places (no hypothesis is made on the control technique, the controller may not be a monitor). In this way the problem of checking liveness results to be decomposed and thus it may result simpler. A control policy to enforce a kind of GMEC, under some restrictions, on a cyclic live and safe MG was proposed in Holloway and Krogh (1990) and extended in Krogh and Holloway (1991). In Holloway and Krogh (1992) it was shown that the control policy proposed in Holloway and Krogh (1990) is closed-loop live if the output transition of any forbidden place is not a synchronization transition; the resulting controller is an interpreted supervisor. In Section 6, a control synthesis method to enforce in a maximally permissive way a GMEC on a live and safe MG under some restrictions, while keeping liveness, is presented. It allows a synchronization transition to be an output transition of a forbidden place, generalizing the results in Holloway and Krogh (1990). 2 Preliminaries and formalisms 2.1 Place/transition nets A place/transition (P/T) net (Murata 1989; Silva 1993) is a structure N = (P, T, Pre, Post) where: P is a set of n places represented by circles; T is a set of m

Discrete Event Dyn Syst (2009) 19:1–30

5

transitions represented by bars; P ∩ T = ∅, P ∪ T  = ∅; Pre : P × T → N (Post : P × T → N) is the pre- (post-) incidence function that specifies the input (output) arcs directed from places to transitions (from transitions to places), with N set of non-negative integers. For instance, Pre( p, t) = a (Post(t, p) = a) means that there is an arc from p (t) to t ( p) with weight a. If all arcs have unitary weights, the net is called ordinary. The pre- and post-incidence functions can be represented as n × m matrices Pre and Post with elements Pre( pı , tj ) and Post( pı , tj ), respectively. The incidence matrix C of the net is defined as C = Post − Pre. For pre- and post-sets we use the conventional dot notation, e.g. • t = { p ∈ P | Pre( p, t)  = 0}, which can be naturally extended to sets of nodes. A marking is a n × 1 vector m ∈ N|P| that assigns to each place of a P/T net a non-negative integer number of tokens. A P/T system or net system < N, m0 > is a P/T net N with an initial marking m0 . A transition t ∈ T is enabled at a marking m iff m ≥ Pre(·, t). If t is enabled, then it may fire yielding a new marking m = m + Post(·, t) − Pre(·, t) = m + C(·, t). The notation m[t > m will mean that an enabled transition t may fire at m yielding m . A firing sequence from m0 is a (possibly empty) sequence of transitions σ = t1 ...tk such that m0 [t1 > m1 [t2 > m2 ..[tk > mk . A marking m is reachable in N, m0  iff there exists a firing sequence σ such that m0 [σ > m. Given a net system N, m0 , the set of reachable markings is denoted R(N, m0 ). The firing count vector of the fireable sequence σ will be denoted as σ ∈ N|T| , where σ (t) represents the number of occurrences of t in σ . The support of a firing count vector σ is the set σ = {t ∈ T | σ (t)  = 0}. If m0 [σ > m, then we can write in vector form m = m0 + C(·, t) · σ . This is known as the state equation of the system. The solutions of the state equation that do not correspond to reachable markings will be called spurious. Non negative left annuler vectors of C are called P-semiflows, i.e. y ∈ N|P| , y  = 0, yT C = 0T . The support of a P-semiflow y is the set y = { p ∈ P | y( p)  = 0}. If y is a P-semiflow then yT m = yT m0 , ∀m ∈ R(N, m0 ). Non negative right annuler vectors of C are called T-semiflows, i.e. x ∈ N|T| , x  = 0, Cx = 0. A MG is an ordinary P/T net such that ∀ p ∈ P, | • p |=| p• |= 1. A T-semiflow (P-semiflow) is canonical iff the greatest common divisor of its components is 1. A T-semiflow (P-semiflow) is said to be minimal iff it is canonical and has a minimal support. A P/T system is live when, from every reachable marking, every transition can ultimately occur; and it is deadlock-free when every reachable marking enables some transition. For strongly connected MG, liveness is equivalent to deadlock-freeness. Let w ∈ Nn , k ∈ N, a GMEC (w, k) defines the set of legal markings expressed by the following linear inequality: L = M(w, k) ≡ {m ∈ Nn | w · m ≤ k}. The support of w is the set Qw = { p ∈ P | w( p)  = 0}. We assume that the set of transitions T of a net is partitioned into two disjoint subset: Tu , the set of uncontrollable transitions, and Tc , the set of controllable transitions; T = Tu ∪ Tc and Tu ∩ Tc = ∅. A controllable transition may be disabled by the supervisor, a controlling agent which ensures that the behaviour of the system will be within a legal behaviour. An uncontrollable transition represents an event which may not be prevented from occurring by a supervisor. Controllable transitions will be drawn as empty boxes, and uncontrollable ones as black bars. Given a system N, m0  and a GMEC (w, k), the occurrence of an uncontrollable transition tu , at a certain legal marking m, may lead to a forbidden marking m . Therefore, it is necessary avoid also the set of markings M f u (w, k) = {m ∈

6

Discrete Event Dyn Syst (2009) 19:1–30

Nn | m[σ > m , m ∈ M(w, k), σ ∈ Tu∗ }. So, in presence of uncontrollable transitions, the set of legal markings under control will be Mc (w, k) = (M(w, k) ∩ R(N, m0 )) \ M f u (w, k). A supervisory control policy is said to be maximally permissive if it prevents only transitions firings that yield illegal markings. Observe that Mc (w, k) ⊆ M(w, k), i.e. the cardinality of the set of legal markings may be decreased. 2.2 Monitor fundamentals It has been shown in Giua et al. (1992) that, if all transitions are controllable, the PN controller that enforces (w, k) has the following incidence matrix c c ∈ Z1×m : c c = −w · C p where C p is the incidence matrix of the plant. The initial marking of the controller mc0 ∈ N is given by: mc0 = k − w · m p0 where m p0 is the initial marking of the plant. The controller so constructed is maximally permissive, i.e. it only prevents those transition firings that yield illegal markings. The control net consists in a control place; no transition is added. Such control place is called monitor. The monitor place, denoted as pm , is connected to the plant transition tj as specified by the incidence matrix element c c ( pm , tj ). When the controller is modeled by a PN structure, it is possible to disable a transition t only if there is an arc from a controller place to t, and the marking of the controller place does not enable the transition. Arcs to uncontrollable transitions are not allowed. In terms of monitor places this can be formalized imposing an additional constraint (Moody and Antsaklis 2000): w · Cu ≤ 0

(1)

where Cu ∈ Zn×mu is the incidence matrix of the uncontrollable subnet Nu , i.e. the net obtained from N removing the controllable transitions, and mu is the number of uncontrollable transitions of the plant net. In Moody and Antsaklis (2000) an efficient way to transform the control specification given by a GMEC (w, k) into a more restrictive GMEC (w , k ) that meets Eq. 1 is proposed. Even if a monitor does not represent a maximally permissive way to enforce a GMEC in the general case, it can be an efficient suboptimal solution from the computational point of view, since its incidence matrix and initial marking are obtained by matrix multiplications, and the algorithm to impose Eq. 1 is polynomial w.r.t. the cardinality of the place set. In addition, its implementation is very simple, just adding a single place and its input and output arcs. As we say in the introduction, enforcing a GMEC on a live net system may lead to deadlock states. An example is shown in Fig. 1. For the live plant net system in Fig. 1a, the set of legal markings is M(w, k) = m( p4 ) + m( p5 ) ≤ 1. This restriction is forced by the monitor place pm , as shown in Fig. 1b. In this case, since the plant net is a safe MG, and w ≤ 1, the monitor represents the maximally permissive solution at preventing forbidden states with respect to the GMEC (Giua et al. 1993), even if uncontrollable transitions exist. However, the closed loop system is not live. It is immediate to see that when t1 fires before t2 a deadlock occurs. To make the closedloop system live we have to enable the firing of t1 , only after t4 has been fired. Thus, the control place pc1 is derived as in Fig. 1c.

Discrete Event Dyn Syst (2009) 19:1–30

7 pc1

pc1

p1

p2

p1

p2

p1

p2

t1

t2

t1

t2

t1

t2

t1

t2

p3

p4

p3

p4

t3

t4

p5

p6

p2

p3

p4

p3

p4

t3

t4

t3

t4

t3

t4

p5

p6

p5

p6

p5

t5

pm

t5

a)

t5

b)

c)

t5

d)

Fig. 1 a a live MG system; b the GMEC m( p4 ) + m( p5 ) ≤ 1 is forced on the net system in a by the monitor place pm ; c the GMEC and closed-loop liveness is forced on the net system in a by the control place pc1 ; d the net system in c deleting the implicit places p6 and p1 is reduced to a sequential net system

A place is said to be implicit if its removal preserves the possible firing sequences, i.e., it is never the unique restriction for the firing of its output transitions. The removal of implicit places preserves sequential properties like boundedness and liveness. By means of linear relaxations, a sufficient structural condition for a place to be sequentially implicit can be stated, which can be verified in polynomial time. Proposition 1 (Silva et al. 1998) Let N, m0  be a net system. A place p ∈ P with initial marking m0 ( p) ≥ z, where z is the optimal value of Eq. 2, is (sequential) implicit. z = min y · m0 + μ s.t.

y · C ≤ C( p, T) y · Pre(P, t) + μ ≥ Pre( p, t) ∀t ∈ p• y ≥ 0,

y( p) = 0

(2)

If pm and pc1 are added simultaneously to the net system in Fig. 1a, pm happens to be implicit (m( pm ) = m( pc1 ) + m( p4 ) + m( p6 ) − 1). This means that pc1 is imposing a stronger restriction to the original behaviour. If pc1 is added the closed-loop system can be further simplified as shown in Fig. 1d, because both p1 and p6 are implicit. Moreover, looking at Fig. 1d, it is clear that when pc1 has been added the behaviour of the plant system has been restricted to be sequential. That is, the firings of the controllable transitions, that are concurrent in the non controlled system of Fig. 1a, and that may be forced to be conflicting when only the GMEC specification is present, as in Fig. 1b, are sequential when closed-loop liveness is also required. Even if in general a monitor does not represent a maximally permissive policy, it may represent a good suboptimal solution when the system is closed-loop live. If this is not the case, like for the net system in Fig. 1a, a more complex controller has to be derived.

8

Discrete Event Dyn Syst (2009) 19:1–30

3 Control subnet To enforce a GMEC it may be necessary to prevent some transitions from firing. Since it is not possible to disable the firing of an uncontrollable transition t ∈ Tu , we may only disable the set of controllable transitions whose firing is required in order to enable t. In the case of MG systems, it can be analytically computed on the basis of the net structure. At this aim, the concept of control subnet is introduced. 3.1 Definitions Definition 1 (control subnet of a transition) Let N be a MG net structure, consider a transition tı . The control subnet for tı is Nı = (Pı , Tı , Preı , Postı ) where • • • •

Pı ⊆ P is the set of places connected to tı by a directed path containing only uncontrollable transitions, Tı = • Pı ∪ Pı • , Preı ( p, t) = Pre( p, t), Postı ( p, t) = Post( p, t)

The set of control transitions for tı is Cı = • Pı \ Pı• and Cı ⊆ Tc . A directed path from a transition t ∈ Cı to tı is called control path. Note that if tı ∈ Tc then Cı = {tı }. In the case of MGs, given a constraint (w, k), the problem is to control the firing of the single input transition of each place pi ∈ Qw in order to meet the constraint. We will denote as N Ii = (P Ii , T Ii , Pre Ii , Post Ii ) the control subnet of the input transition mi 1 of pi and as TCIi = {tTCI , ..., tTCI } the set of control transitions for • pi (that we i i assume not empty). Notice that TCIi ⊆ T Ii . Consider the net in Fig. 2a where the GMEC m( p1 ) + m( p2 ) ≤ 1 has to be enforced. Figure 2b shows the control subnet of the input transition of place p1 , named N I1 ; Fig. 2c shows the control subnet of the input transition of place p2 , named N I2 . As shown in the previous section, if we force a GMEC on a live MG a deadlock may occur. So, it is important to be sure that the (unique) output transition of a place in Qw may always be eventually fired. Thus, also the control subnet of an output transition toi = pı • has to be introduced.

Fig. 2 a A net system where the GMEC m( p1 )+m( p2 ) ≤ 1 has to be enforced; b control subnet associated to t1 ; c control subnet associated to t2 ; d control subnet associated to to1 ; e control subnet associated to to2

t3

t4

t3

t4

c)

p2 to2

p1

t1 b)

to1

a)

t4

t2

t2

t1

t3

t1

t4

t2

t2

p2

p2

to2

to2

p1

e) to1

d)

Discrete Event Dyn Syst (2009) 19:1–30

9

We will denote as N Oı = (P Oı , T Oı , Pre Oı , Post Oı ) the control subnet of the output qı 1 transition of the place pı and as TCOı = {tTCO ...tTCO } the set of control transitions ı ı of pı • (that we assume is not empty). Notice that TCOi ⊆ T Oi . Note that if pı • = pj • then N Oı = N Oj . Consider again the net in Fig. 2a where the GMEC m( p1 ) + m( p2 ) ≤ 1 has to be enforced. Figure 2d shows the control subnet of the output transition of place p1 , named N O1 ; Fig. 2e shows the control subnet of the output transition of place p2 , named N O2 . The concept of control subnet of the output transition of pı ∈ Qw is essential to characterize in a MG the reachability of a deadlock state when a GMEC has to be enforced. Consider the net system in Fig. 2a. While for the firing of transition to2 only the marking of p2 is required, for the firing of to1 two control paths have to be marked. The marking of place p2 , is not required directly to enable to1 , but it is required that it has been marked before. Such information is provided by the control subnet of to1 . In section VI this control subnet will be used to obtain a control policy to enforce GMEC and liveness on safe MG systems. The following algorithm computes the control subnet of the output transition of place pi . To obtain the control subnet of the input transition of place pi it is only necessary to set ti = • pi at the beginning of the algorithm. Algorithm 1 [Control Subnet of the output transition of place pi ] Let Nu = (Pu , Tu , Preu , Postu ) the subnet obtained from N removing all the transitions in T \ Tu , and all the places which have not a transition in Tu as input or output transition Let Q = Pu , Ps = ∅, ti = pi• Let Nˆ u the subnet obtained from Nu removing ti and let Cˆu be its incidence matrix. while Q  = • ti do T if ∃x ≥ 0 such that Cˆu x = 0, ∃ p ∈ • ti x( p)  = 0, x( p) = 0 ∀ p ∈ ti • and p∈ Ps x( p) ≥ 1 then Q = (Q \ ( x ∩ Q)) ∪ • ti , Ps = Ps ∪ x else Q = • ti endwhile Let Nu = (Pu , Tu , Pre u , Postu ) the subnet obtained from Nu removing all places in Pu \ Ps and all the transitions which have not a place in Ps as input or output place Let Ps = { p ∈ Pu |  ∃x ≥ 0 such that CuT x = 0, x ( p) = 0 ∀ p ∈ • ti , x ( pi ) > 0} for p¯ ∈ Ps \ Ps do ¯ = 1 then Ps = Ps \ pi if ∃x > 0 such that CuT x = 0, ∃ p ∈ • ti x ( p)  = 0, x ( p) The control subnet of ti is obtained from Nu removing all the places in the set Pu \ Ps , adding ti and the set of controllable transitions C = • (Pu \ Ps )\ (Pu \ Ps )•



The algorithm first work on the incidence matrix of Nˆ u which is the subnet obtained from Nu removing ti . Such a net is not strictly a MG, but each place has at most one input or one output transition. This implies that 1) two places connected along a direct path must belong to the support of a minimal P-semiflow having all components equal to one, 2) the support of a P-semiflow can include in its support all input places and no output place of ti , since ti has been removed.

10

Discrete Event Dyn Syst (2009) 19:1–30

The key idea of the algorithm is that, in order to check if a place is connected to a transition t in a net structure, it is necessary that there exists a P-semiflow including this place and some input place of t. The algorithm starts computing a subnet of Nu having all places along a P-semiflow at least. In this subnet there is a set of places, denoted Ps , which belong only to minimal P-semiflows including input places of t and another one, denoted P¯ s , not including such input places. The two sets are not disjoint. Places in Ps which do not belong to minimal P-semiflows including input places of t must be removed from Nu to obtain the control subnet. If a place in Ps belongs to a P-semiflow including input places of t, such a P-semiflow can be decomposed in a linear combination of minimal P-semiflows, and at least one of such minimal P-semiflows must include in its support places in P¯ s . Then, places in Ps ∩ P¯ s cannot have a component equal to 1 in the P-semiflow. This fact is used in the algorithm to obtain the set of places of the control subnet of t. Algorithm 1 just involves to check the feasibility of linear systems of equations which have polynomial complexity. The number of checks can be at most Pu + Pu + |Ps \ Ps | with |Pu | ≤ |P|, |Pu | ≤ |Pu | and |Ps \ Ps | ≤ |Pu | but in practice it is strictly minor than 3|Pu |. Remark 1 The control subnet of an output transition toi may include directed paths from a controllable transition to toi which does not contain constrained places. As for example, consider the net in Fig. 2a and the GMEC m( p1 ) ≤ 1. The control subnet of to1 is the subnet in Fig. 2d but the directed path from t4 to to1 does not contain constrained places. For the control problem presented in this paper, it is not important if these paths are marked or not. Thus, they can be removed decreasing the complexity of the control subnet. 3.2 Control subnet and supervisory control The dependency between the firing of an uncontrollable transition tı and its control transitions can be computed without recurring to a reachability set computation but only evaluating the number of tokens along directed paths from control transitions of tı to tı , as shown in the next proposition. Let N, m be a MG system and (w, k) a GMEC. Let us denote as td(m, t, tı ) the token distance between transition t and tı , i.e. the minimum token content among all possible paths from t to tı under the marking m; and as DB(m, TCIı , tı ) the deviation bound between tı and TCIı , i.e., the maximum number of times tı may fire without firing any transition in TCIı . Proposition 2 (Giua et al. 1993) Let N, m0  be a MG system and (w, k) a GMEC. For each place pı ∈ Qw , let tı be its input transition, and TCIı the set of control transitions for tı . We have that (a) given a marking m ∈ R(N, m0 ), DB(m, TCIı , tı ) = min{td(m, t, tı )|t ∈ TCIı }. (b) the set of legal markings is: Mc (w, k) = {m ∈ N|P| | w · (m + Dm ) ≤ k}, where Dm ( pı ) = DB(m, TCIı , tı ) if pı ∈ Qw , Dm ( pı ) = 0 otherwise. In Giua et al. (1993) the results of Proposition 2 were used to address the problem of enforcing a GMEC on MG systems. In this paper we want to extend this approach to the problem of enforcing a GMEC and closed-loop liveness on MG systems.

Discrete Event Dyn Syst (2009) 19:1–30

11

4 On the liveness of monitor controlled MG systems Two new sufficient conditions are given that ensure (under some restrictions) that if a MG controlled by a monitor is live, the state equation of the system has no spurious deadlocks. This means that, given a closed-loop system that verifies the restrictions, if its state equation has a deadlock solution, then the system cannot be live. In the last part of this section it is shown how the problem of checking the absence of these solutions for the considered class of systems can be reduced to checking if a system of equations admits a solution (Recalde et al. 1998). 4.1 Two new sufficient conditions for the absence of spurious solutions for a monitor controlled MG system A first result is based on the idea that, when a monitor having ordinary (no weighted) output arcs is marked, at least one of its output transitions can be fired. This property together with the persistency (i.e., once a transition has been enabled, it cannot be disabled by the firing of another transition) of MG systems allows to conclude that no spurious deadlock can exist. Theorem 1 Let N, m0  be a live MG system plus a monitor pm associated to a GMEC, and such that for every t ∈ pm • , Pre( pm , t) = 1. If N, m0  is live, the state equation has no spurious deadlock solution. Proof Assume a spurious deadlock md = m0 + C · σ d exists. Let σ0 be a sequence such that m0 [σ0 >, σ 0 ≤ σ d , and  ∃σ0 s.t. m0 [σ0 >, σ 0 ≤ σ d but σ 0 < σ 0 . Let m1 = m0 + C · σ 0 . The system is live, hence there is at least one transition t enabled in m1 . Since this transition is not enabled in md , and MG are persistent, Pre( pm , t) > 0 and m1 ( pm ) > 0. Live MGs do not have spurious solutions, hence from the MG point of view, there is a fireable sequence that corresponds to σ d − σ 0 . Let t be the first transition of this sequence. Since m1 ( pm ) > 0, this transition cannot violate the   precondition associated to the monitor, i.e., t is fireable. Contradiction. A second result is derived by assuming that a place, that belongs to the control subnet of an output transition of a constrained place, cannot disable transitions of control subnets of the output transition of other constrained places. This result does not require that the monitor has ordinary arcs. Theorem 2 Let N, m0  be a live MG plus a monitor associated to a GMEC and such that 1) for every pi ∈ Qw the only output transition of its control output subnet N Oı is toi , i.e. (T Oı \ toi )• ⊂ P Oı and 2) the output transition of a place pı ∈ Qw is not a control transition for a place pj ∈ Qw , i.e. if pı , pj ∈ Qw then toi  ∈ TCIj . If N, m0  is live, the state equation has no spurious deadlock solution. Proof Let pm be the monitor of the system and w · m ≤ k the GMEC. Assume a spurious deadlock md = m0 + C · σ d exists. We will see that this marking can be

12

Discrete Event Dyn Syst (2009) 19:1–30

effectively reached from m0 , which contradicts liveness of system. This will be done in three steps: 1) Reach a marking in which all the k tokens are in the monitor place, pm . To do this, for each control subnet N Oı fire the shortest sequence that contains all possible firings of output transitions toi , without firing controllable transitions and denote such sequence as σ0 . Let m1 = m0 + C · σ 0 . By hypothesis, an output transition cannot belong to any TCIı , hence this sequence does not mark any other control subnet, i.e., m1 ( pm ) = k. Observe that this firing vector can be decomposed in two parts: the transitions in σ d and the rest. That is, σ 0 = σ d0 + σ x0 , with σ d0 ≤ σ 0 and σ d0 ≤ σ d and  ∃σ d0 s.t. σ d0 ≤ σ 0 and σ d0 ≤ σ d but σ d0 < σ d0 . 2) Let x ≥ σ x0 , be a T-semiflow. It is clear that md = m0 + C · (σ d + x) = m1 + C · (σ d + x − σ 0 ). Consider the support of the firing count vector σ d + x − σ 0 . Denote by S the set of indexes of control subnet whose transitions are completely included in σ d + x − σ 0 , i.e. if Oi ∈ S then T Oi ⊆ σ d + x − σ 0 . Divide σ d + x − σ 0 in two parts: (1) a part σ 1 whose support includes transitions not belonging to any control subnet and “complete” subsets of transitions of a control subnet N Oı , i.e. σ 1 = (T \ ∪i T Oi ) ∪ (∪ Oi ∈S T Oi ), such that all transitions in a certain control subnet have the same value in σ 1 ; 2) another part σ 2 = (σ d + x − σ 0 ) − σ 1 . Notice that σ 0 may not include all transitions of a certain control subnet: this depends on the initial marking. However with a proper choice of the T-semiflow x, it is possible to ensure that all the transitions of a certain control subnet have in σ d + x − σ 0 a component major or equal then the respective output transition. Thus, all the output transitions of the control subnets belong only to the support of σ 1 . We will see that σ 1 corresponds to a fireable sequence. Let m2 = m1 + C · σ 1 . First, we will see that m2 ≥ 0. For the monitor pm and the places in control subnets, p , σ 1 corresponds to a T-semiflow, hence, m2 ( pm ) = m1 ( pm ) ≥ 0 and m2 ( p ) = m1 ( p ) ≥ 0. For the places not belonging to any control subnet, p , m2 ( p ) = md ( p ) − C( p , ·) · σ 2 , and since σ 2 does not contain any output transition toi , m2 ( p ) = md ( p ) + Pre( p , ·) · σ 2 ≥ 0. Therefore, since live MGs do not have spurious solutions of the state equation, σ 1 corresponds to a fireable sequence in the MG. Order the transitions of σ 1 in such a way that: (1) the sequence is fireable in the MG and (2) all the transitions in a certain N Oı are put together, i.e., no input transition of other subnet N Oj is fired till the output transition toi has been fired. It is clear that this corresponds to a fireable sequence. 3) Finally, we must prove that σ 2 is fireable. Since md = m2 + C · σ 2 ≥ 0, the only problem may be due to the monitor. In σ 2 there is no output transition of the control subnets, therefore m2 ( pm ) = md ( pm ) − C( pm , ·) · σ 2 = md ( pm ) + Pre( pm , ·) · σ 2 ≥ Pre( pm , ·) · σ 2 .   In Fig. 3 an example of a net controlled by a monitor and not meeting the hypothesis of Theorems 1 and 2 is presented. In particular, the monitor place pm has output arcs with weight greater than 1 and N O1 has two output transitions, (t1 , to1 ). The

Discrete Event Dyn Syst (2009) 19:1–30 Fig. 3 For the live net system in a the state equation exhibits a spurious deadlock solution: monitor place pm has output arcs with weight greater than 1 and the control subnet of transition to1 , denoted as N O1 and shown in b, has two output transitions (t1 , to1 )

13 pm 2 2 t1 p7 p1 to1

p2

p3

t2

2

p4

t1 t3 2 p5

p1 p6

p7

p2 to1

to2

b)

a)

monitor place pm enforces the GMEC m( p1 ) + m( p2 ) + m( p3 ) + m( p4 ) + m( p5 ) + m( p6 ) ≤ 2. Although the closed-loop system is live, its state equation has a spurious deadlock solution. It can be seen that by firing t2 to2 t3 a spurious deadlock solution is obtained. Spurious deadlock solutions may also be found if more than one monitor is added. 4.2 How to prove liveness of a monitor controlled MG In strongly connected MG systems deadlock-freeness implies liveness. This is still true when a controller is added to such systems, so in the following the study of liveness is reduced to that of deadlock-freeness. Deadlock-freeness can be checked verifying that the system of equations formed by the state equation and a set of equations representing deadlock states has no solution (see Recalde et al. 1998 for further details). If the state equation has no spurious solutions, the fact that solution of such system does not exist guarantees the liveness of the system. Since the computation complexity of checking if a system of linear equations admits a solution has polynomial complexity (Schrijver 2003), the results presented in this section can be used to check in polynomial time if a monitor controlled MG is live.

5 On the liveness of bounded MG systems with a GMEC control specification In this section the problem of checking closed loop liveness of a live and bounded MG system in presence of a control policy enforcing a GMEC is considered. No hypothesis is made on the control technique, the controller may not be a monitor. A sufficient condition based on the closed loop liveness of proper subnets computed from constrained places is presented. In this way the problem is decomposed and it may result simpler. This result is used in Section 6 but it has a general validity. The control subnets are assumed to be independent. This assumption is described in the following. Assumption 1 The control subnets of output transitions of constrained places are independent. We say that two control subnets N Oı , N Oj , ı  = j defined w.r.t. a

14

Discrete Event Dyn Syst (2009) 19:1–30

constraint (w, k)are independent iff ∀ y ≥ 0 such that  y is a minimal P-semiflow, if [P•Oı ∩ T y  = ∅ P•Oj ∩ T y  = ∅] then [N Oı ⊂ N Oj N Oj ⊂ N Oı ], where T y = {t ∈ T|t ∈ p• , p ∈ y } . In words, two control subnets cannot have transitions that belong to the same P-invariant subnet, except when one is contained in the other. Assumption 1 ensures that the marking of a place p ∈ P Oı cannot prevent the enabling of any transition t ∈ T Oj , j  = ı. Under this assumption a place in a subnet N Oı and a place in a subnet N Oj cannot belong to the same minimal P-semiflow support, and thus their markings cannot be in mutual exclusion relation. If pı , pj ∈ y , where y is a minimal P-semiflow, since yT m = yT m0 , ∀m ∈ R(N, m0 ), it follows that in a live and safe MG m( pı ) + m( pj ) ≤ 1, ∀m ∈ R(N, m0 ) holds. Consider the net system in Fig. 4a, and the GMEC m( p1 ) + m( p2 ) + m( p3 ) + m( p4 ) + m( p5 ) ≤ 3. It is immediate to see that transitions t4 and t7 belong to the subnet induced by P-semiflow y = [0 1 0 1 0 1 0 0 1 0], and that any place p ∈ • t4 is in mutual exclusion with p4 since the net admits also the P-semiflows y = [1 0 0 1 0 1 0 1 0 0] and y = [0 0 1 1 0 1 0 0 0 1]. This makes more difficult our control problem. If we enable the firing of t6 we have that a deadlock occurs, being not possible anymore to enable t4 while respecting the GMEC. The computational complexity of checking Assumption 1 is practically equal to the complexity of computing the P-semiflows of a control subnet net (Martinez and   [p]  p where p is the number Silva 1982) whose number is in the worst case equal to 2 of places of a control subnet and thus p < n. Assumption 1 makes more clear the presentation of the results in the rest of the paper but it is not essential. It can be removed by taking into account the additional GMECs induced by P-semiflows having in their support constrained places. Definition 2 Let N be a k-bounded MG on which a GMEC has to be imposed. The controlled subnet is defined as the union of all the control subnets N Oı plus: a) an input place for each transition in TCOı ; b) a new output place for each transition toi ;

Fig. 4 a In this net system with respect to the GMEC m( p1 ) + m( p2 ) + m( p3 ) + m( p4 ) + m( p5 ) ≤ 3 Assumption 1 is not verified; b in this net system with respect to the GMEC m( p1 ) + m( p2 ) + m( p3 ) ≤ 2 Assumption 2 is not verified

p10

p8

p9

t1

t2

t3

p1

p2

p3

t2

t1

t3

p1 t4 p6

p7

t5

t6

p4

p5

t5 t4 p3

p2 t6

t7

a)

b)

Discrete Event Dyn Syst (2009) 19:1–30

15

c) an extra transition having an output arc to all the input places of each control subnet – the places added as in a) – and an input arc from all the output places of each control subnet – the places added as in b). The input places are marked in such a way that there are k tokens in each cycle. Theorem 3 Let N, m0  be a live and bounded MG on which a GMEC has to be imposed. If the control is set in such a way that: • •

all the control subnets are independent; the controlled subnet plus the control is live.

Then the complete system with the control is live. Proof For this considered net subclass just deadlock freeness has to be proved. Assume a deadlock can be reached, i.e., there exists a fireable sequence σd , m0 [σd > md , and md is a deadlock. Consider the projection of σd on the transitions of the controlled subnet. Clearly this is a fireable sequence, and, since this subnet is live under the control, a transition t is enabled in md . This transition cannot be fired in the complete net. Hence, since all control subnets are independent, there exists a place p ∈• t, not belonging to the controlled subnet, that is not marked in md . Observe that t is in the “interface” of the control subnet, hence it is a controlled transition, and there exists a directed path from t to a constrained place. Let t = • p, since t cannot be fired either, and by Assumption 1 it cannot be controlled , there exists p ∈ • t which is unmarked. Repeating this reasoning, an unmarked cycle of N can be found. Contradiction, since

N, m0  is live.  

6 A controller to enforce GMEC and closed loop liveness on live and safe MG The results presented in Section 4 allow a trial-and-error synthesis method for GMEC and closed loop liveness enforcing. Now, a direct synthesis method is presented in presence of some constraints, in particular MG should be safe. In a live and safe MG system a constrained place can be marked, firing only uncontrollable transitions, if and only if all its control paths are marked. Nevertheless, it is not necessary to record which of the controllable transitions that control such paths have been fired, but it is sufficient to check how many of them have been fired. This implies that the reachability of a forbidden state can be characterized in terms of the number of control paths of the places constrained by the GMEC, that are marked under a certain marking. Here we extend this property to the reachability of a deadlock state introduced on such systems by a GMEC. In order to enable a transition all its input places have to be marked. In presence of a GMEC, the marking of some of these places may be constrained. A maximally permissive policy has to disable a controllable transition if and only if it will lead to a marking under which no transition can be fired if the GMEC is fulfilled. Our aim is to characterize the reachability of such states in terms of the number of marked control paths of constrained places having common output transitions. As it has been mentioned in Section 4, closed-loop liveness is obtained by proving that a live and

16

Discrete Event Dyn Syst (2009) 19:1–30

safe MG under the proposed control policy is deadlock-free (showing that tokens can be always removed from all the constrained places). The assumption of safeness reduces the complexity of checking if a place pı ∈ Qw may be marked firing only uncontrollable transitions, as it was shown in Giua et al. (1993). This is due to the fact that it is not necessary to record which transition fires, but just to check the number of firings of transitions in TCIı . From Proposition 2 it follows that ∀ pı ∈ Qw , ∀m ∈ R(N, m0 ), m( pı ) + Dm ( pı ) ≤ 1

(3)

∀ pı ∈ Qw , ∀m ∈ R(N, m0 ), m( pı ) + Dm ( pı ) = 1 ←→ td(m, t, ti ) = 1, ∀t ∈ TCIı (4) and thus a place pı ∈ Qw can be marked firing only uncontrollable transitions iff all its control paths are marked. Assumption 2 Let pı and pj be a couple of constrained places such that TCIı ∩ TCIj  = ∅: 1) |TCIı | = |TCIj | = 1; 2) pı and pj cannot be marked simultaneously. Lemma 1 If the plant net is a live and safe MG and Assumption 2 holds, it exists a control path including all constrained places controlled by the same transition. Proof In a live and safe MG any place belongs to the support of a minimal P-semiflow (Murata 1989). If two places cannot be marked simultaneously, i.e. they are in mutual exclusion relation, they belong to the same P-semiflow support and, then, they both belong to a directed circuit (Murata 1989) and so result to be connected by a directed path.   Assumption 2 allows to consider on equal footing the firing of any transition in TCIı w.r.t. GMEC. Moreover if |TCIı | = 1 we know that, firing the unique control transition of both constrained places, the related control path would be marked. Consider the net system in Fig. 4b, and the GMEC m( p1 ) + m( p2 ) + m( p3 ) ≤ 2. By definition TCI1 = {t1 }, TCI2 = {t1 , t2 }, TCI3 = {t3 }, and thus, t1 is a control transition for the input transition of two constrained places. As a consequence, the firing of t1 and t2 cannot be considered on equal footing, because the firing of t1 will mark a constrained place anyway, but this is not true for t2 . In order to know if a constrained place can be marked by firing a transition in TCI2 it is not enough to know that one of the two control paths will be marked, but it is also necessary to know which one of them. Consider the net in Fig. 5. By Assumption 2, places p5 and p6 cannot be both constrained since TCI5 = TCI6 = {t6 } and if t6 fires, they would be simultaneously marked. Assumption 2 is a technical assumption that allows to know the maximum value that a GMEC can assume by firing uncontrollable transitions simply by evaluating some counter variables that are introduced afterwards. From a practical point of view, this is not a strong limitation since it is not usual to control more constrained places, which can be simultaneously marked, with the same control input. This assumption is useless if all controllable transitions control only one constrained place.

Discrete Event Dyn Syst (2009) 19:1–30 Fig. 5 A net system. If m( p1 ) + 2m( p2 ) + 2m( p3 ) + 2m( p6 ) + m( p7 ) + m( p13 ) + m( p14 ) + 2m( p15 ) ≤ 4 has to be enforced, the control subnets of the constrained places output transitions to1 and to2 are independent and none of them is included in the other

17 pc 3

3 p19

2

2

2 2

2

p20

t6 p8

p6

t5

p23

p24

t11

t12

t13

t14

p15

p16

p17

p18

t8

p7

t3 p4

p3

p22

p10

t4 p5

p21 t7

p9

t2

p11

p12

t9

t10

p13

p14

p2

t1 p1

to2 to1

p26

p25 t15

The computational complexity of checking Assumption 2 is in practice equivalent to the one of obtaining control subnet of constrained places since it consists in evaluating that the intersections of sets TCIi is or not empty. 6.1 Definitions of counter variables C Ii , C Oi , of vectors wi− and wi+ and of function f In the following the counter variables C Ii , C Oi , the vectors wi− and wi+ and the function f associated to a control subnet are introduced. They are useful for the presentation of the control policy in the next subsection. In order to enable a controllable transition only if the GMEC is not violated, it must be checked if its firing causes that a constrained place pı ∈ Qw can be marked by firing only uncontrollable transitions. In other words, it must be checked if the input transition of pı , named tı , can be fired. We say that a transition trTCI ı is constrained under a given marking m, if all the paths from trTCI ı to tı along single token circuits are not marked, otherwise it is unconstrained. Note that if a transition trTCI ı fires, all the paths from trTCI ı to tı become marked. Definition 3 C Iı (m) is equal to the number of transitions belonging to TCIı that are unconstrained under the marking m, and so: • • • •

the firing of a transition trTCI ı will increment the value of C Iı in one unit, notice that trTCI ı cannot fire twice without firing tι ; the firing of the output transition toi will decrement the value of C Iı in mı units, where mı = |TCIı |; the firing of a transition trTCI j , j  = ı, does not change the value of C Iı ; the initial value of C Iı (m0 ) is equal to the sum of unconstrained transitions in the sets TCIı under the initial marking.

In other words, C Iı (m) represents the number of control paths of pı that are marked under the marking m.

18

Discrete Event Dyn Syst (2009) 19:1–30

From Eq. 4 we have that a place pı ∈ Qw can be marked firing only uncontrollable transitions iff C Iı (m) = mı . Notice that, if |TCIı | = 1, C Iı is not useful since the firing of the unique controllable transition causes that pı will be marked by firing only uncontrollable transitions. Consider the net in Fig. 5 – apart from dotted arcs and places – and the GMEC m( p1 )+2m( p2 )+2m( p3 )+2m( p6 )+ m( p7 )+ m( p13 )+ m( p14 )+2m( p15 ) ≤ 4. As for the control subnets of the input transitions of places p ∈ Qw we have that TCI1 = TCI3 = TCI6 = {t6 }, TCI2 = TCI7 = {t7 }, TCI13 = {t12 }, TCI14 = {t13 , t14 }, TCI15 = {t11 }. Under the marking in the figure C I14 = 1 since t13 is unconstrained and t14 is constrained. Thus, being C I14 < m14 = 2, p14 will not be marked by firing only uncontrollable transitions. To evaluate the weighted sum of places in the GMEC that can be marked firing uncontrollable transitions in a control subnet N Oı we define the vector wı− ( p). Definition 4 To define the vector wı− ∈ N|P| two different cases must be considered. 1) If a place p belongs to a directed path from a transition t ∈ TCOı to toi and more than one constrained place is controlled by t, choose a control path named π¯ to which any constrained place controlled by t belongs to (Assumption 2 ensures the existence of such a path). If p ∈ π¯ , let π¯ be the directed sub-path of π¯ from p to toi , wı ( p)− = max pj ∈π¯ w( pj ). If p  ∈ π¯ , wı ( p)− = 0. Note that the choice of the control path π¯ is arbitrary but the same control path has to used for all places p which belong to a directed path from a transition t ∈ TCOı to toi . 2) If a place p belongs to a directed path from a transition t ∈ TCOı to toi and only the constrained place pj is controlled by t, •

if p belongs to one of the directed paths from t to pj , then wı ( p)− = where – –

•

l lj

w( pj ),

l be the number of directed paths from transitions in the set TCOı to toi to which p belongs, lj be the total number of paths from any transition in the set TCOı to pj

otherwise, wı ( p)− = 0

3) If a place p does not belong to a directed path from a transition t ∈ TCOı to toi , wı ( p)− = 0.

Consider again the net in Fig. 5 – apart from dotted arcs and places – and the GMEC m( p1 )+2m( p2 )+2m( p3 )+2m( p6 )+ m( p7 )+ m( p13 )+ m( p14 )+2m( p15 ) ≤ 4. As for the control subnets of the output transitions of places p ∈ Qw we obtain TCO3 = TCO6 = {t6 }, TCO1 = TCO2 = {t6 , t7 }, TCO7 = {t7 }, TCO13 = TCO14 = {t11 , t12 , t13 , t14 }, TCO15 = {t11 }. Let TCOo1 = TCO1 = TCO2 and TCOo2 = TCO13 = TCO14 . As for example, we have w− o2 ( p17 ) = 1/2 since p17 belongs to l = 1 paths from t13 or t14 to to2 , p14 is

Discrete Event Dyn Syst (2009) 19:1–30

19

the only constrained place controlled by t13 or t14 and there are l14 = 2 paths from t13 or t14 to p14 . The term l14l takes into account that a token in place p17 means that only l of the l14 control paths of p14 are marked. Since the transition t6 ∈ TCOo1 controls more than one constrained place, a control path including all such constrained places, named π¯ 6 , has to be defined. Let it be π¯ 6 = t6 p8 t4 p6 t3 p3 t1 p1 to1 . Thus, as for example, wı ( p8 )− = max pj ∈π¯ 6 w( pj ) = 2 where π¯ 6 = p8 t4 p6 t3 p3 t1 p1 to1 and wı ( p9 )− = 0 since p9 does not belong to π¯ 6 . It results w− o1 = [1 w− o2

2

2

0

0

2

2

2

0 0 0 0 0 0] , = 0 0 0 0 0 0 0

0



0

2

0

0

0

0

0

0

0

0

0

0

0

0

0

1

1

2

1

1/2 1/2

0

0

0

0

0

0

2

0

0

0

0 0 0 0 0 0 0 0 . w− 15

= [0

0

0

0

0

0

0

0

0

0

0

0

0

0] .

0

0

0

Note that, if all places in a control subnet would belong to a directed path from a transition t ∈ T Oı to toi which controls more than one constrained place, by Assumption 2 it must exist an index j such that t  ∈ TCIj and |TCIj | = 1. In this case, since all control paths are marked when t fires, p∈POı wı ( p)− m( p) is the maximum value that can be reached by the weighted sum of constrained place that can be marked in the control subnet N Oı by firing only uncontrollable transitions. This is not true when a place belongs to a directed path from a transition t ∈ T Oı to toi which controls only one constrained place, since in this case w− ( p) may be rational and not all control paths of a constrained place in the subnet N Oı can be marked at a time. This motivates the introduction of a binary function f which is true when all control paths of a constrained place in the subnet N Oı are marked. Definition 5 Let us define a binary function f : (P, m) → {0, 1} as follows: f ( p, m) = 1, if it exits an index k such that p ∈ P Ik and C Ik (m) = mk (note that, by definition, ∀t ∈ TCOı , ∃k s.t. t ∈ TCIk ), otherwise f ( p, m) = 0. In words, f ( p, m) = 1 iff all control paths of the constrained places to which p is connected are marked. Lemma 2 Let Ru (N, m) be the set of markings reachable from m by firing   only uncontrollable transition, it results maxm ∈Ru (N,m) p∈POı w( p)m ( p) = p∈POı  − wı ( p)− m( p) f ( p, m). Furthermore p∈P Oı w ı ( p) m( p) f ( p, m) is always non negative integer. Proof The proof follows from the fact that in a live and safe MG system a constrained place can be marked, firing only uncontrollable transitions, iff all its control paths are marked.  

20

Discrete Event Dyn Syst (2009) 19:1–30

For the net in Fig. 5, we have that  P Oo2 = { p11 , . . . , p18 }, and under the marking − in figure f ( p, m) = 0, ∀ p. Note that p∈P O2 w 1 ( p) m( p) f ( p, m) = 0, consistently with the fact that there is not  a constrained place in the subnet N Oo2 that can be uncontrollably marked, but p∈PO w1 ( p)− m( p) = 1/2. 2 Consider the net system in Fig. 6a and the GMEC m( p4 ) + m( p6 ) + m( p11 ) ≤ 1. Even if to11 has only one constrained input place, p11 , its control subnet contains also places p7 , p9 , p10 , and p12 whose marking is a pre-condition to enable to11 . Even if these places are not constrained places, their marking requires that the constrained places p4 and p6 have been marked. To take this into account, we introduce the vector wı ( p)+ , defined as follows. Definition 6 To define the pre-condition weight vector wı+ ∈ N|P| three different cases must be considered. 1) If a place p belongs to a directed path from a transition t ∈ TCOı to toi and more than one constrained place is controlled by t, choose a control path named π¯ which any constrained place controlled by t belongs to (Assumption 2 ensures the existence of such a path). If p ∈ π¯ , let π¯ be the directed sub-path of π¯ from t to p, ( p, toi ) be the set of all directed paths from p to toi ,  then wı ( p)+ = max max pj ∈π¯ w( pj ) − maxπ∈( p,toi ) max pj ∈π w( pj ), 0 . If p  ∈ π¯ , then wı ( p)+ = 0. Note that the choice of the control path π¯ is arbitrary but the same control path has to used for all places p which belong to a directed path from a transition t ∈ TCOı to toi . 2) If a place p belongs to a directed path from a transition t ∈ TCOı to toi and p j is the only constrained place controlled by t • •

•

if along any control path controlled by t the place p is not preceded by pj , then wı+ ( p) = 0;

pc2

pc1 p1

p3

p2

t1

t2

t3

p4

p5

p6

t4

t5

t6

p1

p3

p2

t1

t2

t3

p4

p5

p6

t4 =to4

t5

t6 =to6

p7

p8

p9

p7

p8

p9

t7

t8

t9

t7

t8

t9

p10

p11

p12

p10

p11

pm

2

t1

t2

p4 t4 =to4

t1

p6

p4

t2

t3 p6

t4 =to4

t6 =to6 pc2

2

p12 p11

t10 =to11 t10 =to11

a)

t3

t6 =to6

p11 t10

pc1

pc3 3

b)

c)

t10 =to11

d)

Fig. 6 a A live MG net system; b the GMEC m( p4 ) + m( p6 ) + m( p11 ) ≤ 1 is enforced on the system in a by the monitor place pm but this leads to a dead closed-loop system; c the GMEC and closedloop liveness are enforced on the system in a via a more evolved net controller; d a simplification of the system in c

Discrete Event Dyn Syst (2009) 19:1–30

•

21

if along such paths p is preceded by pj , then wı+ ( p) = – –

rj r

w( pj ), where

rj is the number of directed paths in N Oı from pj to p, r is the number of directed paths in N Oı from pj to toi ,

3) If a place p does not belong to a directed path from a transition t ∈ TCOı to toi , wı+ ( p) = 0. For the net in Fig. 6a and the GMEC m( p4 ) + m( p6 ) + m( p11 ) ≤ 1 we have: w+ o11 ( p7 ) = 1 since p7 is preceded by p4 ∈ Qw only along the control path t1 p4 t4 p7 t7 p10 to11 and there is only one directed path from p4 to p7 and only one directed path from p4 to to1 ; w+ o11 ( p8 ) = 0 since p8 is not preceded by a place p ∈ Qw along any control path. For the net in Fig. 5 – apart from dotted arcs and places – and the GMEC m( p1 ) + 2m( p2 ) + 2m( p3 ) + 2m( p6 ) + m( p7 ) + m( p13 ) + m( p14 ) + 2m( p15 ) ≤ 4 we have: w + ¯ 6 = t6 p8 t4 p6 t3 p3 t1 p1 to1 o1 ( p1 ) = 1 since p1 belongs to the control path π to which belong three constrained places and max pj ∈π¯ 6 w( pj ) = 2, where π¯ 6 = t6 p8 t4 p6 t3 p3 t1 p1 is the directed sub-path of π¯ 6 from t6 to p1 , and maxπ∈( p1 ,to1 ) max pj ∈π w( pj ) = 1 since ( p1 , to1 ) = { p1 to1 }; w+ o2 ( p11 ) = 1 since p11 is preceded by p15 ∈ Qw along the path t11 p15 t8 p11 to2 , p15 is the only constrained place controlled by t11 , there are r15 = 1 directed paths in N Oo2 from p15 to p11 and r = 2 directed paths in N O2 from p15 to to2 . It results w+ o1 = [ 1

0

0

0

0

0

0

0

0

0

0

0

0

0] ,

= [0

0

0

0

0

0

0

0

0

0

0

0

0

0] ,

w+ o2 w+ 15

0

0

0

0

0

0

0

0

0

0

0

0

0

0

0

1

1

0

0

0

0

0

0

0

= 0.

The terms nı and nı are now introduced:  • nı = p∈TCOı • wı ( p)− , that is the maximum value that can assume the weighted sum of places in the GMEC by firing all transitions in the set TCOı . Thus, nı −  + p∈P Oı w ı ( p)m( p) represents the maximum value that can assume the weighted sum of constrained places in N Oı that are not yet marked. It is immediate to see that

nı ≥ wı+ ( p)m( p) (5) p∈P Oı

•

 nı = p w( p), p ∈ • toi ∩ Qw , that is the weighted sum of places in the GMEC that have to be marked for the firing of toi , because they belong to the set • toi (note that nı ≥ nı ). For the net in Fig. 6a, it is immediate to verify that no11 = 3 but n o11 = 1, since to11 has only one input place constrained.

Definition 7 Given a control subnet N Oj , if there is not a control subnet N O j such that TCO j ⊂ TCO j , we call N Oj maximal.

22

Discrete Event Dyn Syst (2009) 19:1–30

Let us denote by M the set of indexes of maximal control subnets. For the net of Fig. 6c N Oo11 is the unique maximal control subnet since TCO4 ⊂ TCOo11 and TCO6 ⊂ TCOo11 , thus M = {o11}. In order to ensure the deadlock-freeness of the closed-loop net, when a controllable transition is enabled, if it belongs to the control subnet of the output transition of a constrained place, it must be guaranteed that all the input places of such transition can be simultaneously marked without violating the GMEC, otherwise the transition would be dead. Thus, we introduce the set of counter variables C Oı (m). Given a GMEC (w, k), C Oı (m) represents, under the current marking, the complement to k of the maximum value that the weighted sum of the constrained places can assume by firing only uncontrollable transitions that belong to a maximal control subnet N Oj, except for ones that eventually belong to N Oı , plus the complement to ni of the maximum value that can assume the weighted sum of constrained places that belong to the control subnet of toi and that have to be still marked to enable toi . Then its value can be obtained from k minus the weighted sum of the marking of places p  ∈ P Oı but p ∈ P Oj where N Oj is maximal, with weights given by elements of vector w − j f , plus the weighted sum of the marking of places p with p ∈ P Oı with weights given by elements of vector wı+ .   Definition 8 C Oı (m) = k − j∈M p∈P Oj wı ( p)+ m( p). So we have that: •

• •

• •



p ∈ P Oı

w j ( p)− m( p) f ( p, m) +

 p∈P Oı

the firing of a transition trTCOj , j  = ı will decrement the value of C Oı (m) by  r − p∈TCIk • w ı ( p) units if C Ik (m) = mk − 1 (by definition, ∃k s.t. tTCOj ∈ TCIk .), r unless tTCOj ∈ TCOı ; in this way the value of C Oı (m) is updated when ∀ p ∈ TCIk • it results f ( p, m ) = 1 with m[trTCOj > m . the firing of a transition trTCOı does not change the value of C Oı (m); the firing  of output transitions toj, j  = ı will increment the value of C Oı (m) by n j − p∈toj• wj¯ ( p)− units where j¯ ∈ M is the maximal subnet index such that  TCOj ⊆ TCOj¯ if n j > p∈toj• wj¯ ( p)− , otherwise it does not change the value of C Oı ; the firing of output transitions toi will decrement the value of C Oı (m) in nı − nı units;   the initial value of C Oı (m) is equal C Oı (m0 ) = k − j∈M p∈POj  p∈ POı  wj ( p)− m0 ( p) f ( p, m0 ) + p∈POı wı ( p)+ m0 ( p).

Notice that counter variables are natural valued and they cannot assume negative values.

For the net of Fig. 6c by definition w− o11 = [0 0 0 1 1 1 0 1 0 0 1 0] , + + w+ 4 = 0, w6 = 0, w11 = [0

0

0

0

0

0

1

0

1

1

0

1] , then

Discrete Event Dyn Syst (2009) 19:1–30

23

C O4 (m) = 1 − m( p5 ) f ( p5 , m) − m( p6 ) f ( p6 , m) − m( p8 ) f ( p8 , m) − m( p11 ) f ( p11 , m)   

−  w ( p) m( p) f ( p) p∈P Oo11 p∈ P O4 o11 +

,

0  p∈P O4 w 4 ( p)

+

m( p)

C O6 (m) = 1 − m( p4 ) f ( p4 , m) − m( p5 ) f ( p5 , m) − m( p8 ) f ( p8 , m) − m( p11 ) f ( p11 , m)   

−  w ( p) m( p) f ( p) p∈P O011 p∈ P O6 o11 +,

C Oo11 (m) = 1 +

,

0  p∈P O6 w 6 ( p)

+

m( p)

+ m( p7 ) + m( p9 )) + m( p10 ) + m( p12 ) .   

− + p∈ P Oo11 w o11 ( p) m( p) f ( p) p∈P O w 11 ( p) m( p) 0 

o11

In Fig. 6c C Oo11 (m) is equal to the marking of the place pc2 and under the marking in figure it results f ( p, m) = 0 ∀ p. Definition 9 We say that a control subnet N Ok is included in a control subnet N Oı maximal according to Definition 7 and we write N Ok ≺ N Oı if there is place p ∈ • toi such that p  ∈ Qw and there is a directed path from any transition t ∈ TCOk to p. Consider the net in Fig. 6 and the GMEC m( p4 ) + m( p6 ) + m( p11 ) ≤ 1, the control subnet N O4 is included in N O11 since p10 ∈ • t11 , p10  ∈ Qw and there is a directed path from any transition t ∈ TCO4 to p10 . 6.2 The control policy In the following the control policy will be exposed to enforce a GMEC while keeping liveness on a live and safe MG. The control policy ensures the firing of any transition toi , so the closed-loop system is deadlock-free in a maximally permissive way. For the clarity of presentation, we present the results in two propositions. In the first proposition, requiring that only Assumption 2 is fulfilled, the case with only one maximal control subnet is considered, while in the second proposition, requiring that Assumption 1 and Assumption 2 are fulfilled, the case with two independent maximal control subnets is considered. Thus, from Theorem 3 it follows that also the closedloop system is live in both cases. In presence of a set of GMECs as control specification, since for the considered net subclass deadlock-freeness implies liveness and the control law designed considering separately each GMEC ensures that the single GMEC is not violated and that the unique output transition of each constrained place can be fired, it is immediate to conclude that a controllable transition must be enabled iff it is enabled by all the control laws of each GMECs. Thus, the control policy is modular. Proposition 3 Let us consider a live and safe MG and a GMEC (w, k) such that Assumption 2 is verified. Suppose that there is only one maximal control subnet named

24

Discrete Event Dyn Syst (2009) 19:1–30

N O1 , i.e. any other control subnet N Ok verifies that TCOk ⊂ TCO1 , k  = 1. Firing a j transition tTCO1 ∈ TCIı , it is possible, after a fireable sequence, to enable to1 without violating the GMEC iff [C1] C I1 (m) < mı − 1(note that by definition, ∀t ∈ TCO1 , ∃ı s.t. t ∈ TCIı ) or one of the following conditions is true [C2] C O1 (m) ≥ n1    [C2a]



C Ok (m) ≥ nk if t ∈ TCOk s.t. N Ok ≺ N O1    [C2b ]

If |TCIı | = 1 ∀ı, condition [C1] is never true. j

Proof (If) If [C1] is true, by firing tTCO1 the place pı ∈ P O1 could not be uncontrollably marked (because of Assumption 2), being at least one of its control paths unmarked. Nothing changes in the system as for GMEC meeting and closed-loop liveness. Now, suppose that the net system reaches a marking m such that C Iı (m) = mı − 1 j and so firing the transition tTCO1 will cause pı to become uncontrollably marked.   If [C2a] is true, by the definition of C O1 (m), we have that k − j∈M p∈POj  p∈ PO   1 w1 ( p)− m( p) f ( p, m) + p∈NO w1 ( p)+ m( p) ≥ n1 , and thus it follows that k− j∈M 1    − +  p∈ P O1 w 1 ( p) m( p) f ( p,m) ≥ n1 − p∈P Oj p∈P O1 w 1 ( p) m( p) ≥ 0 since n1 ≥ p∈P O1   + −  w1 ( p) m( p) by Eq. 5. By noticing that k− j∈M p∈POj p∈ PO w1 ( p) m( p) f ( p, m) 1

represents the complement to k of the maximum value of the weighted sum of the constrained places of places p  ∈ P O1 that can be uncontrollably marked, we conclude that the GMEC will be not violated. The same occurs if [C2b] is true. As for firing to1 , note that all the transitions in the net N O1 can be disabled only by the marking of places in the N O1 . If condition [C2a] is verified under themark net  ing m we have that k − j∈M p∈POj  p∈ PO w1 ( p)− m( p) f ( p, m) ≥ n1 − p∈PO 1  1  w1 ( p)+ m( p) ≥ 0. By noticing that k − j∈M p∈POj  p∈ PO w1 ( p)− m( p) f ( p, m) 1 represents the weighted sum of the constrained places of places p  ∈ P O1 that can be  uncontrollably marked and that n1 − p∈PO w1 ( p)+ m( p) represents the maximum 1 value that can assume the weighted sum of the constrained places in N O1 that have to be still marked to enable to1 , we deduce it is possible to enable all the transitions j tTCO1 , ∀ j so that all the control paths of to1 can be marked and to1 can be fired. If [C2a] is not true, by the same reasoning, we conclude that, if [C2b] is true, it is possible to fire all transitions tok such that N Ok ≺ N O1 without violating the GMEC. The counter C O1 is so incremented until [C2b] becomes true.   (Only if) If [C1] and [C2a] are not true, it follows that k − j∈M p∈NOj  p∈ PO 1  w1 ( p)− m( p) f ( p, m) < n1 − p∈PO w1 ( p)+ m( p). This means that under current 1 marking it is not possible to mark all places needed to enable to1 . Since N Ok ⊂ N O1 , k  = 1 and [C2b] is not true, no other output transition of a  constrained place included in N O1 can be fired before to1 fires, i.e. the quantity n1 − p∈PO w 1 ( p)+ m( p) 1

cannot be decremented. Thus, by firing tTCO1 a marking m will be reached from m under which to1 is deadlocked.   j

Discrete Event Dyn Syst (2009) 19:1–30

25

Example 1 Consider again the net system shown in Fig. 6a, and the GMEC m( p4 ) + m( p6 ) + m( p11 ) ≤ 1. The monitor controlled net system shown in Fig. 6b enforces the GMEC, but it can be proved to be not live by using the results shown in Section 4. By definition we have that |TCIı | = 1, ∀ı and the following set of control transitions result to be defined TCO4 = {t1 }, TCO6 = {t3 }, TCOo11 = {t1 , t2 , t3 }. Also, recall that for this net system and for the specified GMEC the subnet N Oo11 is the only maximal control subnet. It results N O4 ≺ N O1 and N O6 ≺ N O1 . The plant net is a live and safe MG, and the hypothesis of Proposition 3 are verified. A control policy is: enable a transition t ∈ TCOo11 iff C Oo11 (m) ≥ 3, being no11 = 3; enable a transition t ∈ TCO6 iff C O6 (m) ≥ 1, being n6 = 1; enable a transition t ∈ TCO4 iff C O4 (m) ≥ 1, being n4 = 1. The resulting controller is shown in Fig. 6c, where the places pc1 , pc2 , pc3 implement respectively C O4 (m), C Oo11 (m), C O6 (m). The closed-loop net system can be simplified as shown in Fig. 6d. Proposition 4 Let us consider a live and safe MG and a GMEC (w, k) such that Assumption 1 and Assumption 2 are verified. Suppose that two independent and maximal control subnets N O1 and N O2  are defined, i.e. any other control subnet N Ok verifies that TCOk ⊂ TCO1 , k  = 1 TCOk ⊂ TCO2 , k  = 2. Firing a transij tion tTCO1 ∈ TCIı , it is possible, after a fireable sequence, to enable to1 without violating the GMEC iff [C1] C Iı (m) < mı −1 with i = 1, 2, (note that by definition, ∀t ∈ TCOj , ∃ı s.t. t ∈ TCIı ) or C Iı (m) = mı − 1 but one of the two following conditions is verified  C Ok (m) ≥ nk if t ∈ TCOk s.t. N Ok ≺ N O1 [C2] C O1 (m) ≥ n1 

C O1 (m) + n 2 ≥ n1 [C3] C O2 (m) ≥ n2 + wı ( p)− • p∈TCI1

If |TCIı | = 1 ∀ı, condition [C1] is never true. Proof Only condition [C3] will be proved since the proof of conditions [C1], [C2] can be derived from the proof of Proposition 3. In the proof of Proposition 3 we have not used  that −  j∈M p∈P Oj p∈ P O1 w 1 ( p) m( p) = 0 when M = {1} and thus it works also in presence of two maximal independent control subnets. j j (If) By firing tTCO1 , m[tTCO1 > m . From condition [C3] it follows that C O2 (m ) ≥ n2 , so it is possible to enable to2 . By firing of to2 C O1 is incremented by n 2 , then it is possible to reach a marking m such that C O1 (m ) ≥ n1 . From Proposition 3 we conclude that to1 can be fired. [C3] is not true, even if we assume that C O2 (m) ≥ n2 +  (Only if) If − p∈TCI1 • w ı ( p) and thus to2 can be fired, C O1 is incremented by n2 units but it results C O1 (m ) < n1 being C O1 (m) + n2 < n1 . From Proposition 3 we conclude that a marking m will be reached from m under which to1 is deadlocked.   Example 2 Consider the net system in Fig. 5 – apart from dotted arcs and places – and the GMEC m( p1 ) + 2m( p2 ) + 2m( p3 ) + 2m( p6 ) + m( p7 ) + m( p13 ) + m( p14 ) + 2m( p15 ) ≤ 4. The monitor pc enforces the GMEC but the closed-loop system can be proved to be not live by using the results shown in Section 4.

26

Discrete Event Dyn Syst (2009) 19:1–30

Since N Oo1 and N Oo2 are independent and they are the only two maximal control subnets, the hypothesis of Proposition 4 are verified. The control subnet N O15 is included in N Oo2 according to Definition 9, i.e. N O15 ≺ N O02 . No other control subnet is included in N Oo1 or in N Oo2 . We proceed to apply the control policy given in Proposition 4. To be consistent with notations, we use no1 = 4, n o1 = 3, no2 = 4, n o2 = 2, no15 = 2, n o15 = 2. COo1 (m) = 4−m( p13 )−m( p14 ) f ( p14 ,m)−2m( p15 )−m( p16 )−1/2m( p17 ) f ( p17 ,m)−1/2m( p18 ) f ( p18 ,m)+    

p∈P O

+

m( p1 )   

 p∈P O

o1

wo1

o2

w o2 ( p)− m( p) f ( p,m)

,

( p)+ m( p)

C O15 (m) = 4 − m( p1 ) − 2m( p2 ) − 2m( p3 ) − 2m( p6 ) − 2m( p7 ) − 2m( p8 ) − 2m( p10 ) +    

p∈P O

o1

wo1 ( p)− m( p) f ( p,m)

+ m( p13 ) − m( p14 ) f ( p14 , m) − m( p16 ) − 1/2m( p17 ) f ( p17 , m) − 1/2m( p18 ) f ( p18 , m)    

p∈P O

+

0 

 p∈P O

15

w 15



o2

p ∈ P O

15

wo2 ( p)− m( p) f ( p,m)

,

( p)+ m( p)

C Oo2 (m) = 4 − m( p1 ) − 2m( p2 ) − 2m( p3 ) − 2m( p6 ) − 2m( p7 ) − 2m( p8 ) − 2m( p10 )    

p∈P O

o1

wo1 ( p)− m( p) f ( p,m)

+ m( p11 ) + m( p12 ) .    

p∈P O

o2

wo2 ( p)+ m( p)

Note that in the expressions of C Oo1 , C O15 and C Oo2 , for sake of brevity, we omitted the term f ( p, m) for all places which belong to a subnet N Ik with |Ik | = 1 (e.g. p13 ) since it results f ( p, m) = 1 when m( p) = 1.  A transition t ∈ TCOo1 is enabled iff C Oo1 ≥ 4 or C Oo2 (m) ≥ 4 + 2 = 6 C O1 (m) + 2 ≥ 4  A transition t ∈ TCOo2 is enabled iff C Oo2 ≥ 4 or C Oo1 (m) ≥ 4 + 3 = 7 C O2 (m) + 3 ≥ 4 A transition t ∈ TCOo2 ∩ TCO15 is enabled iff C Oo2 ≥ 4 or C Oo15 ≥ 2 or C Oo1 (m) ≥ 4 + 4 = 7 C O2 (m) + 3 ≥ 4 Under the marking in Fig. 5 it results C Oo1 (m) = 4, C Oo2 (m) = 4, C O15 (m) = 4. Indeed, all controllable transitions can be left free to fire. Assume t14 fires, it results C Oo1 (m) = 3, C Oo2 (m) = 4, C O15 (m) = 3. Then, only a transition t ∈ TCOo2 may be left free to fire. Indeed, if a transition t ∈ TCOo1 fires, a deadlock state is reached. Note 1 The result presented in Proposition 4 is referred to the case where only two maximal independent control subnets are considered. It can be generalized to r > 2 maximal independent control subnets, by considering for the enabling of a controllable transition t ∈ TCOı under a given marking the fact that the output transition toi may fire after a sequence that includes the firing of some (at most all) r − 1 output transitions.

Discrete Event Dyn Syst (2009) 19:1–30

27

The control policy is suitable to be executed on-line since it only requires: for each constrained place the allocation of two counter variables C Ii and C Oi ; the evaluation of logical predicates essentially consisting in the comparison between the values of such counters with an integer number.

7 Concluding remarks Some results on the liveness of plant MG, where a GMEC has been forced via a monitor place, have been presented in this paper. First, two sufficient conditions have been obtained which guarantee that no solution of the state equation is a spurious deadlock. As a consequence, checking liveness in these cases can be reduced to check if a system of equations admits a solution. In addition, a sufficient condition has been presented for closed loop liveness of MGs where a GMEC has been enforced on. Also, a maximally permissive control policy to enforce a GMEC and closed-loop liveness on live and safe controlled MGs has been proposed.

References Basile F, Chiacchio P, Giua A (2006) Suboptimal supervisory control of Petri nets in presence of uncontrollable transitions via monitor places. Automatica 42:995–1004, June Giua A, DiCesare F, Silva M (1992) Generalized mutual exclusion constraints on nets with uncontrollable transitions. In: 1992 IEEE Int. Conf. on Systems, Man, and Cybernetics, Chigago, IL, 19–21 October 1992, pp 974–979 Giua A, Cesare FD, Silva M (1993) Petri net supervisors for generalized mutual exclusion constraints. In: Proc. 1993 IFAC World Congress, Sydney, July 1993, pp 267–270 Holloway L, Krogh B (1990) Synthesis of feedback control logic for a class of controllable Petri nets. IEEE Trans Automat Contr 35(5):514–523, May Holloway L, Krogh B (1992) On closed-loop liveness of discrete-event systems under maximally permissive control. IEEE Trans Automat Contr 37(5):622–697, May Holloway LE, Krogh BH, Giua A (1997) A survey of Petri nets methods for controlled discrete event systems. Discret Event Dyn Syst Theory Appl 7(7):151–190 Iordache M, Antsaklis P (2003) Design of T-liveness enforcing supervisors in Petri nets. IEEE Trans Automat Contr 48(11):1962–1974, November Iordache M, Antsaklis P (2006) Supervision control of concurrent system: a Petri net structural approach. Birkh¨auser, Boston Iordache M, Moody J, Antsaklis P (2002) Synthesis of deadlock prevention supervisors using Petri nets. IEEE Trans Robot Autom 18(1):59–68, February Krogh B, Holloway L (1991) Synthesis of feedback control logic for discrete maufacturing systems. Automatica 27(4):641–651, July Martinez J, Silva M (1982) A simple and fast algorithm to obtain all invariants of a generalized Petri net. In: Application and theory of Petri nets: selected papers from the first and second European workshop on application and theory of Petri nets, Strasbourg, Sep. 23–26, 1980, Bad Honnef, Sep. 28–30, 1981. Springer, Heidelberg, pp 301–310 Moody J, Antsaklis P (2000) Petri net supervisors for DES with uncontrollable and unobservable transitions. IEEE Trans Automat Contr 45(3):462–476, March Murata T (1989) Petri nets: properties, analysis and applications. Proc IEEE 77(4):541–580, April Park J, Reveliotis S (2002) Liveness-enforcing supervision for resource allocation systems with uncontrollable behavior and forbidden states. IEEE Trans Robot Autom 18(2):234–240, April Recalde L, Teruel E, Silva M (1998) On linear algebraic tecniques for liveness analysis of p/t systems. J Circuits Syst Comput 1(8):223–265 Schrijver A (2003) Combinatorial optimization. Springer, Heidelberg Silva M (1993) Introducing Petri nets, in practice of Petri nets in manufacturing. Chapman & Hall, London, pp 1–62

28

Discrete Event Dyn Syst (2009) 19:1–30

Silva M, Teruel E, Colom JM (1998) Linear algebraic and linear programming techniques for the analysis of net systems. In: Rozenberg G, Reisig W (eds) Lectures in Petri nets. I: basic models, ser. Lecture notes in computer science, vol 1491. Springer, Heidelberg, pp 309–373 Stremersch G (2001) Supervision of Petri nets. Kluwer Academic, Boston Wonham W (1989) The control of vector discrete-event systems. Proc IEEE 77(1):81–98, January Yamalidou K, Moody J, Lemmon M, Antsaklis P (1996) Feedback control of Petri nets based on place invariants. Automatica 32(1):15–28, January

Francesco Basile was born in Naples, Italy, in 1971. He received the Laurea degree in Electronic Engineering in 1995 and the Ph.D. degree in Electronic and Computer Engineering in 1999 from the University of Naples. In 1999 he was visiting researcher for six months at the Departamento de Ingenieria Informatica y Systems of the University of Saragoza, Spain. He is currently assistant professor of Automatic Control at the Dipartimento di Ingegneria dell’Informazione e Ingegneria Elettrica of the University of Salerno, Italy. He is a member of the editorial board of the International Journal of Robotics and Automation. His current research interest are: modelling and control of discrete event systems, automated manufacturing and robotic.

Laura Recalde received the M.S. degree in mathematics and the Ph.D. degree in computer engineering from the University of Zaragoza, Zaragosa, Spain, in 1995 and 1998, respectively. She is currently an Assistant Professor with the Departamento de Informática e Ingeniería de Sistemas, University of Zaragoza, where she is in charge of courses in systems theory and discrete event systems. Her main research interest is the modeling and analysis of distributed concurrent systems using Petri nets.

Discrete Event Dyn Syst (2009) 19:1–30

29

Pasquale Chiacchio was born in Naples, Italy on Sep. 7, 1963. He received the Laurea and the Research Doctorate degrees in Electronics Engineering at the University of Naples, Italy in 1987 and 1992, respectively. He currently is Full Professor of Automatic Control in the Engineering Faculty of the University of Salerno, Italy. His research interests include manipulator inverse kinematics techniques, redundant manipulator control, cooperative robot systems, analysis and control of discret event systems. He has published 23 international journal papers, 59 international conference papers, 3 textbooks and is co-editor of the book “Complex Robotic Systems” (Springer-Verlag, 1998).

Manuel Silva received the Industrial-Chemical Eng. degree from the University of Sevilla, Sevilla, Spain, in 1974 and the postgraduate and Ph.D. degrees in control engineering from the Institut National Polytechnique de Grenoble, Grenoble, France, in 1975 and 1978, respectively. From 1975 to 1978, he was with the Centre National de la Recherche Scientifique, Laboratoire d’Automatique de Grenoble. In 1978, he started the group of Systems Engineering and Computer Science at the University of Zaragoza, Zaragosa, Spain, where he was named Professor of systems engineering and automatic control in 1982. His research interests include modeling, validation, performance evaluation, and implementation of distributed concurrent systems using Petri nets, binary decision graphs, and robotic programming and control. He is author of the book Las Redes de Petri en la Automática y la Informática (AC, 1985) and coauthor of the book Practice of Petri Nets in Manufacturing (London, UK: Chapman & Hall, 1993), He was Dean of the Centro Politécnico Superior, University of Zaragoza, from 1986 to 1992 and President of the Aragonese Research Council (CONAI) and of the Research and Innovation Committee of the French, Spanish Comisión de Trabajo de los Pirineos (CTP) from 1993 to 1995. He was an associate editor of the European

30

Discrete Event Dyn Syst (2009) 19:1–30

Journal of Control. Dr. Silva is an advisory member of the IEICE Transactions on Fundamentals on Electronics, Communications and Computer Sciences, a member of the Steering Committee of the International Conference on Application and Theory of Petri Nets, a founder member of the Asociación Española de Robótica, and member of IFAC and EATCS. Interested in the history of technology and engineering, he received a medal from Lille and from the Association of Telecommunication Engineers of Aragón. He is a member of the National Academy of Engineering of Spain and was an associate editor of the IEEE TRANSACTIONS ON ROBOTICS AND AUTOMATION and co-editor of the special issue on CIM of that TRANSACTIONS.