Repositorio Institucional de Documentos

M´ aster en Ingenier´ ıa de Sistemas e Inform´ atica Trabajo Fin de M´aster Redes de Petri h´ ıbridas adaptativas: alcanzabilidad y ausencia de bloqueos Mar´ ıa Est´ ıbaliz Fraca Santamar´ ıa Director: Jorge Emilio J´ulvez Bueno Codirector: Manuel Silva Su´arez Departamento de Inform´atica e Ingenier´ıa de Sistemas Escuela de Ingenier´ıa y Arquitectura Universidad de Zaragoza Septiembre 2011 Redes de Petri h´ ıbridas adaptativas: alcanzabilidad y ausencia de bloqueos RESUMEN Las redes de Petri(RdP) [3]constituyen unparadigma formal ampliamente aceptado para el modelado de sistemas de eventos discretos. No obstante, con poblaciones de gran tama˜no, padecen del problema de la explosi´on de estados (crecimiento exponencial del tama˜no del conjunto de estados alcanzables con respecto a la poblaci´on inicial del sistema). Una manera de paliar este problema consiste en relajar la restricci´on de integralidad del formalismo y considerar redes de Petri continuas [5, 8]. Las redes de Petri continuas permiten abordar de manera eficiente el estudio de los sistemas mediante t´ecnicas lineales de an´alisis. Sin embargo, siendo las redes continuas una relajaci´on de las discretas, no siempre preservan sus propiedades, como por ejemplo la ausencia de bloqueos [9]. En este Trabajo se introduce, formaliza y estudia un formalismo nuevo, denominado redes de Petri h´ıbridas adaptativas (HAPN), basado en una relajaci´on alternativa de la integralidad. En una red de Petri discreta, continua o h´ıbrida, las transiciones son definidas a priori como discretas o como continuas, lo que determina su modo de comportamiento en todo instante de tiempo [11]. Esta definici´on est´atica no permite adaptar el comportamiento del modelo a la carga, que var´ıa din´amicamente. En cambio, el comportamiento de las transiciones de la red adaptativa es variable: una transici´on se comporta como continua si su carga de trabajo supera un umbral establecido inicialmente, en caso contrario se comporta como discreta. Dado que las inconsistencias entre las redes discretas y las continuas suelen darse cuando las poblaciones son peque˜nas, se ha intentado que las redes adaptativas no presenten estos problemas, ya que en ese caso el comportamiento es discreto. Adem´as, cuando las poblaciones son elevadas el comportamiento es continuo, por lo que las t´ecnicas lineales son aplicables, evitando el problema de la explosi´on de estados. En primer lugar, se ha definido formalmente el formalismo de redes de Petri adaptativas. En el ´ambito de este Proyecto Fin de M´aster, el formalismo no considera ninguna interpretaci´on temporal. Tras estudiar diversas alternativas para determinar el comportamiento de las transiciones en funci´on de su carga, la opci´on elegida consiste en establecer un umbral para la carga de trabajo de cada transici´on. Para toda carga inferior al umbral, el comportamiento de la transici´on es discreto, mientras que el comportamiento es continuo para cargas superiores. A partir de la definici´on de las HAPNs, se ha caracterizado el conjunto de sus marcados alcanzables de las redes dePetri adaptativas. El conjunto global de marcados alcanzables no ser´a, en general, convexo como lo es el de las redes continuas, pero es caracterizable como una uni´on de conjuntos convexos. Por ´ultimo, se estudia la ausencia de bloqueos, una propiedad b´asica y necesaria para que las acciones de un sistema tengan un comportamiento adecuado. Se intenta no tanto determinar si una red puede bloquearse, sino si la red adaptativa preserva la ausencia de bloqueos de la red discreta con misma estructura y marcado inicial. En conclusi´on, se ha definido el formalismo de las HAPN, en el cual cada transici´on combina comportamientos discretos y continuos en funci´on de la carga de trabajo, con el objetivo de realizar una fluidificaci´on parcial de las RdP discretas que preserve algunas propiedades que las RdP completamente continuas no siempre preservan. Este formalismo incluye a las redes de Petri discretas, continuas e h´ıbridas. Adem´as, se han estudiado las propiedades de alcanzabilidad y ausencia de bloqueos del formalismo en relaci´on a las Redes de Petri discretas. Contents 1 Introduction 3 1.1 Context . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.2 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.3 Objectives and scope . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.4 Document organization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2 Preliminary Concepts 7 2.1 Petri nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.2 Discrete Petri nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.3 Continuous Petri nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.4 Hybrid Petri nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.5 Some net subclasses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 3 Hybrid adaptive Petri nets 11 3.1 Formal definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 3.2 Reachability and liveness definitions . . . . . . . . . . . . . . . . . . . . . . . . . . 14 4 Reachability Space of HAPNs 17 4.1 Reachability space of discrete and hybrid adaptive PN . . . . . . . . . . . . . . . . . 17 4.2 Reachability space of continuous and hybrid adaptive PN . . . . . . . . . . . . . . . 19 4.3 An algorithm to obtain the reachability space of HAPN . . . . . . . . . . . . . . . . 20 5 Deadlock-freeness in HAPNs 25 5.1 Preliminary results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 5.2 Deadlock-freeness in ordinary, deadlock-free nets . . . . . . . . . . . . . . . . . . . 25 6 Conclusions and future work 29 6.1 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 6.2 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 v List of Figures 1.1 A Petri net example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.2 Reachability space of the Petri net in Fig. 1.1 (discrete) . . . . . . . . . . . . . . . . 4 1.3 Reachability space of the Petri net in Fig. 1.1 (adaptive) . . . . . . . . . . . . . . . . 5 1.4 Reachability space of the Petri net in Fig. 1.1 (adaptive) . . . . . . . . . . . . . . . . 5 3.1 Simple Petri net and its reachability space . . . . . . . . . . . . . . . . . . . . . . . 11 3.2 An hybrid adaptive Petri net (a) and the behaviour of its transitions (b) and (c). . . . 13 3.3 Example of a live hybrid adaptive Petri net (a) and its reachability space (b). . . . . . 14 4.1 Example of a Petri net . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 4.2 RS of the PN in Figure 4.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 4.3 RS of the PN in the Figure 1.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 4.4 Example of a Petri net . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 4.5 Reachability space of the net of Fig. 4.4 when discrete . . . . . . . . . . . . . . . . 22 4.6 Reachability space of the net of Fig. 4.4 when continuous . . . . . . . . . . . . . . . 22 4.7 Reachability space of the net of Fig. 4.4 when HAPN . . . . . . . . . . . . . . . . . 23 5.1 A Petri net example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 1 Chapter 1 Introduction This “Trabajo Fin de M´aster” (TFM) introduces and studies Hybrid Adaptive Petri Nets (HAPNs) [1], a formalism in the paradigm of Petri nets (PN) [3]. HAPNs combine discrete and continuous behaviours from the discrete and continuous Petri nets, and attempt to partially fluidify discrete PN models mantaining their relevant properties. The results obtained in this work have been published in the proceedings of an international conference [1]. 1.1 Context Discrete event systems appear in many fields, for instance in manufacturing, logistics, computer networks, traffic systems, etc. Having suitable modeling formalisms and formal techniques for its design, development and implementation is essential to achieve correct and eficient systems behaviour. Petri nets are a formal paradigm widely used for the modeling of discrete event systems, due to its powerful analysis and synthesis techniques and its direct graphical representation. However, as in most formalisms for discrete event systems, the set of reachable states grows exponentially with respect to the initial population of the system. Thus, many analysis techniques based on the exploration of the state space are inefficient for the analysis of high populated systems: this is the well known state explosion problem. It is a crucial drawback in the analysis of discrete event systems. An interesting technique to overcome this difficulty is to relax the original discrete model and deal with a continuous approximation. Such a relaxation aims at computationally more efficient analysis methods, at the price of losing some precision. Unfortunately, the transformation to a continuous model may not always preserve important properties of the original discrete model. In the context of Petri nets (PNs), the transformation from discrete to continuous [6, 5, 8] does not preserve, in general, properties as deadlock-freeness, liveness, reversibility, etc [7]. 1.2 Motivation This TFM focuses on hybrid adaptive Petri nets [2], a Petri net based formalism in which the firing of transitions is partially relaxed. Transitions of HAPN can behave in two different modes: continuous and discrete. The continuous mode will be chosen when the transition workload is higher than a given threshold. It makes sense because, in general, the higher the workload the better the continuous approximation. Consequently, it also makes sense to switch to a discrete mode when the workload becomes low. This way, a HAPN is able to adapt its behaviour to the net workload; it offers the possibility to represent more faithfully the discrete system and simplifies analysis techniques by behaving as 3 10 Definition 9 A hybrid Petri net system is a tuple hNH,m0i, where m0∈(R≥0)|P|is the initial marking. In the same way that HAPN include discrete and continuous Petri net, also hybrid adaptive Petri nets are included in the HAPN formalism. To define an hybrid Petri net, an infinite threshold should be associated to each discrete transition, ∀i∈Td, µi=∞and a threshold equal to 0 to each continuous transition: ∀j∈Tc, µj= 0. 2.5 Some net subclasses Typically, Petri net subclasses are defined by imposing some constraints on the structure of the net. The following ones are among the most usual net subclasses: Definition 10 (Some Petri net subclasses). •Ordinary Petri nets are those nets whose arc weights are 1, i.e., ∀p∈P∀t∈T, P re[p, t]∈ {0,1}and P ost[p, t]∈ {0,1}. •Choice free Petri nets are PN where each place has at most one output transition, i.e., ∀p|p•| ≤ 1. •State machines (SM) are ordinary Petri nets where each transition has one input and one output place, i.e., ∀t, |•t|=|t•|= 1. •Marked graphs (MG) are ordinary Petri nets where each place has one input and one output transition, i.e., ∀p|•p|=|p•|= 1. •Join free (JF) nets are Petri nets in which each transition has at most one input place, i.e., ∀t∈T, |•t| ≤ 1). •Choice free (CF) nets are Petri nets in which each place has at most one output transition, i.e., forallp, |p•| ≤ 1. •Free choice (FC) nets are ordinary Petri nets in which conflicts are always equal, i.e., ∀t, t′,if •t∩•t′=,then •t=•t′. •Equal Conflict (EQ) nets are Petri nets in which conflicts are always Chapter 3 Hybrid adaptive Petri nets This Chapter introduces the formalism of hybrid adaptive Petri nets, which consists on a partial fluidification of the firing of transitions. 3.1 Formal definition Hybrid adaptive PNs are a relaxation of discrete PNs, such that a threshold is associated to each transition, which determines the behaviour mode. The following example illustrates the behaviour of an adaptive transition, explaining the behaviour of a PN with just one place and one transition. Example 11 Figure 3.1 (b) explains the behaviour of the Petri net in Figure 3.1 (a), from the initial marking m0= (7). Firstly, the possible markings reachable from the PN when it is a discrete Petri net are shown in blue color. The net starts with the initial marking m[p] = 7, and it decreases with the discrete firings of tuntil it reaches m[p] = 0. Secondly, the red line of the Figure represents the possible reachable markings of the net when it is a continuous PN. The marking of place pcan decrease in any amount by the firing of the continuous transition t. As explained in the section 2.3, the marking m[p] = 0 will be reached just in the limit. 0 1 2 3 4 5 6 7 Discrete Petri Net Continuous Petri Net Hyb Adap Petri Net Hyb Adap Petri Net Hyb Adap Petri Net 7 (a) (b) . Figure 3.1: Example of a Petri net system and the possible markings of the place p. Finally, the net is considered as HAPN. Different values of the threshold µare considered, and the reachable markings for each µare sketched in green color in the Figure 3.1. Notice that transition t has an associated threshold µ. When the marking of p, is bigger than µ, the firings of tare continuous. 11 12 Otherwise, the firings are discrete. For example, when the threshold is µ= 2.5, the firings are continuous from m[p] = 7 to m[p] = 2.5, and it is discrete for m[p]≤2.5. In this example, half token will remain in p. The formal definition of the HAPNs is inspired in the definition of discrete Petri nets, adding the thresholds that are asociated to each transitions. The hybrid adaptive Petri nets are defined mathematically below. Definition 12 A HAPN is a tuple NA=hP, T, Pre,Post,µiwhere: •P={p1, p2, ..., pn}and T={t1, t2, ..., tm}are disjoint and finite sets of places and transitions. •Pre and Post are |P| × |T|sized, natural valued, incidence matrices. •µ∈(R≥0∪ ∞)|T|is the vector of thresholds. Given a place (transition) v∈P(T), its preset,•v, is defined as the set of its input transitions (places), and its postset v•as the set of its output transitions (places). Definition 13 A HAPN system is a tuple hNA,m0i, where m0∈(R≥0)|P|is the initial marking. A threshold µis associated with each transition t. When the marking of •tis above the threshold, tbehaves in continuous mode (C); and otherwise it behaves in discrete mode (D) As in continuous PNs, the enabling degree of tiat mis defined as: enab(ti, m) = minp∈•tim[p] Pre[p, ti](3.1) The threshold µiof a transition tidetermines the values of the enabling degree for which the transition behaves in continuous (C) or in discrete (D) mode: mode(ti, m) = Cif enab(ti, m)> µi Dotherwise (3.2) If a transition tiis in continuous mode then enab(ti, m)> µiwhat implies that tiis enabled as continuous. On the other hand, if tiis in discrete mode then it is enabled iff enab(ti, m)≥1. This two conditions together imply that tiis enabled (either as discrete or continuous) iff the following expression is true: (mode(ti, m) = C)∨(mode(ti, m) = D∧enab(ti, m)≥1) This expression is equivalent to: (enab(ti, m)> µi)∨(enab(ti, m)≤µi∧enab(ti, m)≥1) what simplifies to: enab(ti, m)> µi∨enab(ti, m)≥1, with µ∈R≤0 A transition tithat is enabled can fire. The admissible firing amounts depend on its mode. If mode(ti, m) = C,tican fire in any real amount α∈R≥0that does not make the enabling degree 13 cross the threshold µi, i.e., 0< α ≤enab(ti, m)−µi. If mode(ti, m) = D,tican fire as a usual discrete transition in any natural amount α∈Nsuch that 0< α ≤enab(ti, m). As in discrete or continuous PN, the firing of a transition tin a certain amount α≤enab(t,m) leads to a new marking m′, and it is denoted as mαt −→m′. It holds m′=m+α·C[P, t], where C=P ost−P re is the token flowmatrix (incidence matrix if Nis self-loop free). Hence, as in discrete systems, m=m0+C·σ, the state (or fundamental) equation summarizes the way the marking evolves, where σis the firing count vector of the fired sequence. Right and left natural annullers of the token flow matrix are called T- and P-semiflows, respectively. As in discrete systems, when y·C=0,y>0the net is said to be conservative, and when C·x=0,x>0the net is said to be consistent. The following example illustrates which isthe behaviour mode ofeach transition of agiven HAPN 10 2 10 C2 D2 D1 C1 C3 D3 A D C D B D C C C C C C D C C D E D D C F C D C G C D D (a) (b) (c) Figure 3.2: An hybrid adaptive Petri net (a) and the behaviour of its transitions (b) and (c). Example 14 Figure 3.2 (b) illustrates the behaviour of the transitions of the HAPN in Figure 3.2 (a), with any µ= (µ1, µ2, µ3). Notice that the three arrows (t1,t2,t3) of Figure 3.2 (b) indicate the “direction” in which the marking “moves” when t1,t2or t3are fired. The Figure shows the regions in which t1,t2and t3behave as discrete (regions D1,D2,D3) or continuous (C1,C2,C3). For example, t3behaves as continuous (C3) below the dotted line corresponding to µ3and discrete above the line (D3). In the triangular grey region of the center of Figure 3.2 (b), the PN behaves as continuous, and in the other regions, it has a partially discrete behaviour (some transitions behave as discrete and some as continuous). Figure 3.2 (c) summarizes the behaviour of each one of the transitions in the different areas identified in the Figure 3.2 (b). For example, in the area A,t1and t3behave as discrete while t2 behaves as continuous. Finally, notice that if µ=0, all transitions will behave as continuous, and if µ=∞all transition will behave as discrete. Hence, the HAPN formalism includes both the continuous and discrete PN formalisms. 14 3.2 Reachability and liveness definitions The set of all the reachable markings of a given HAPN system hN,m0iis denoted as reachability space, RS(N,m0), and it is defined as follows. Definition 15 RS(N,m0) = {m| ∃ σ=α1tγ1. . . αktγksuch that m0 α1tγ1 −→ m1 α2tγ2 −→ m2···αktγk −→ mk=mwhere αi∈R+if mode(tγi, mi−1) = C, and αi∈N+if mode(tγi, mi−1) = D} Liveness and deadlock-freeness properties are defined in a similar way to those of discrete systems. Definition 16 Let hN,m0ibe a HAPN system. • hN,m0ideadlocks iff a marking m∈RS (N,m0) exists such that ∀t∈T,tis not enabled. • hN,m0iis live iff for every transition tand for any marking m∈RS (N,m0) there exists m’ ∈RS(N,m) such that tis enabled at m’. • N is structurally live (deadlock-free) iff ∃m0such that hN,m0iis live (deadlock-free). The example below illustrates the concepts defined in this Chapter. p3 p4 3 5 1 t3 t1 p1 t2 p2 2 0 0.5 1 1.5 2 2.5 3 3.5 4 4.5 5 0 0.5 1 1.5 2 2.5 (1,1,2,0) (0,0,2,1) (3,1,1,0) (5,1,0,0) (4,0,0,1) (2,0,1,1) 3 .(a) (b) . Figure 3.3: Example of a live hybrid adaptive Petri net (a) and its reachability space (b). Example 17 The Petri net of Figure 3.3 can be defined mathematically as follows. NA=hP, T, P re, P ost, µi, where P={p1, p2, p3, p4} T={t1, t2, t3} Pre =    2 1 0 0 1 0 0 0 1 0 0 1     15 Post =    0 0 3 0 0 1 1 0 0 0 1 0     µ={µ1= 1.5, µ2= 1, µ3= 1} And the HAPN system is the tuple hN , m0= (5,1,0,0)i. In the initial marking m0= (5,1,0,0), the transition t1is enabled as continuous (mode(t1,m0) = C), and enab(t1,m0) = 2.5 . The transition can be fired any real amount αsuch that 0< α ≤ enab(t1,m0) - µ1. It is 0< α ≤1, where α∈R. Moreover, transition t2is enabled as discrete (mode(t2,m0) = D), and enab(t2,m0) = 1. Since it is in discrete mode, it can be fired any natural amount αsuch that 0< α ≤enab(t2,m0). It is 0< α ≤1, where α∈N. The reachability space of hNA, m0= (5,1,0,0)iis defined as: RS(NA,m0) = {m| ∃ σ= α1tγ1. . . αktγksuch that m0 α1tγ1 −→ m1 α2tγ2 −→ m2... αktγk −→ mk=mwhere αi∈R+if mode(tγi, mi−1)= C, and αi∈N+if mode(tγi, mi−1) = D} From m0, transition t1can be fired, and the reachable markings are all the possible markings between (5,1,0,0) (the initial marking) and (3,1,1,0) (given by the maximal firing). The set of all these markings form a straight line in the R|P|space. From all the markings of this “straight line”, transition t2can be fired from m0, resulting another straight line in the Reachability Space: the line from (4,0,0,1) to (2,0,1,1). Finally, (1,1,2,0) and (0,0,2,1) are reachable from (3,1,1,0) and (2,1,1,1) respectively when t1is fired as discrete an amount of 1. It can be observed that m[p3]and m[p4]are linearly dependent if m[p1]and m[p2]:m[p3] = 4−m[p1]+m[p2]and m[p4] = 1−m[p2]. Because of that, the reachablity space can be represented just with the axes m[p1]and m[p2], as it can be observed in Figure 3.3(b). Regarding to the deadlock-freeness property, the HAPN system of this example is deadlockfree becasuse none of the reachable markings is a deadlock. It is also liven because from any of the reachable markings, there exists a reachable marking from which any transition can also be fired. If the marking (0,1,2.5,0) would be reachable then the system would be not live (and not deadlock-free). Chapter 4 Reachability Space of HAPNs In this Chapter, the reachability space (RS) of HAPN systems is studied and compared to the RS of discrete and continuous systems. In the first section, RS of discrete, continuous and hybrid adaptive PN are compared. In the second one, a method to calculate the reachability space of HAPN is presented. The following definitions will be used in the rest of the document: NDdenotes a discrete Petri net with a given structure hP, T, Pre,Posti,NCdenotes the continuous net with the same structure, and NAdenotes the hybrid adaptive Petri net with the same structure and an arbitrary µ. In order to compare the reachability spaces, the same initial marking m0∈N|P|is considered for all three types of Petri nets (discrete, continuous or adaptive). For simplicity, it was decided to start the study the RS in the HAPN by considerig ordinary PNs; the subclass of Petri nets in which all the arc weights are equal to 1. Notice that although ordinary PNs are a subclass of general PNs, any non-ordinary Petri net can be converted to an ordinary PN [3]. It will be proved that, under rather general conditions, the RS of a HAPN NAcontains the RS of ND, and that the RS of NCcontains the RS of NA. This is a straightforward consequence of the fact that, in contrast to continuous nets, HAPNs are a partial relaxation of discrete nets. 4.1 Reachability space of discrete and hybrid adaptive PN Theorem 18 RS(ND,m0)⊆RS(NA,m0) for any ordinary HAPN NAwith µ∈N|T|. Proof Let m∈RS(ND,m0). Then, there exists σd=tγ1. . . tγksuch that m0 1tγ1 −→ m1 1tγ2 −→ m2··· 1tγk −→ mk=min hND,m0i. We will prove that there exists a sequence σa=β1tγ1. . . βktγk such that m0 β1tγ1 −→ m1 β2tγ2 −→ m2···βktγk −→ mk=min hNA,m0i. Let us start with tγ1, and let us check if β1= 1 can be chosen. Two cases must be considered. a) enab(tγ1,m0)≤µtγ1. From the definition of HAPN, tγ1behaves as discrete, i. e., mode(tγ1, m0) = D. Given that tγ1is enabled in hND,m0i, it holds that enab(tγ1,m0)=minp∈•tγ1{m0[p]} ≥ 1. Hence, it is also enabled in hNA,m0iin the same amount. Therefore, β1= 1 can be chosen, and the same m1of the discrete system is reached. b) enab(tγ1,m0)> µtγ1. From the definition of HAPN, tγ1behaves as continuous, i. e., mode(tγ1,m0) = C. 17 18 Since µtγ1∈Nand enab(tγ1,m0)> µtγ1, it holds that enab(tγ1,m0)−µtγ1≥1. Therefore, β1= 1 ≤enab(tγ1) - µtγ1can be chosen and m1is reached. The same reasoning can be applied to the rest of the transitions in the sequence tγ2. . . tγk. However, if non ordinary PNs or non natural thresholds are considered, RS(ND,m0) is in general not contained in RS(NA,m0). Let us show both cases through examples. •When non natural thresholds, µ6∈ N|T|, are considered, RS(ND,m0) is in general not contained in RS(NA,m0) for ordinary HAPN. Let us show it with the following example. Consider the net of the Figure 4.1 as discrete, ND, with the initial marking m0= (3,4). Both t1and t2can be fired until the place p1is empty (when enabling degree is 0). Its reachability space RS(ND,m0) is represented in Figure 4.2 (a). Let us consider now the net as adaptive, with µ= (1.5,1.5) Thus, t1can fire as continuous while m[p1]>1.5. And t2can fire as continuous while m[p1]>1.5and m[p2]>1.5. When m[p1] = 1.5,t1changes from continuos to discrete, and it can fire a discrete amount. Analogously, t2changes to discrete and can fire as discrete when m[p1] = 1.5. Its reachability space is shown in Figure 4.2 (c). Notice that RS(ND,m0) contains some markings that are not reachable in hNA,m0i. For example, the marking m2= (1, 4) ∈RS(ND,m0), but m26∈ RS(NA,m0). Figure 4.1: A net whose reachability space as discrete is not contained in the reachability space as adaptive with with µ= (1.5,1.5), see Figure 4.2. •If non-ordinary PN are considered, RS(ND) is in general no contained in RS(NA), with µ∈ N|T|. This can be shown through an example. The reachability space of the HAPN in Figure 0 1 2 3 4 5 0123450 1 2 3 4 5 0123450 1 2 3 4 5 012345 (a) (b) (c) Figure 4.2: Reachability space of the Petri Net of Figure 4.1 behaving as Discrete (a), HAPN with µ= (2,2) (b) or HAPN with µ= (1.5,1.5) (c). 19 1.1 with µ= (1,1) is shown in Figure 4.3. Transition t2is enabled as continuous from marking (5,0) to (2,1.5), where it changes to discrete. If t2is fired as discrete (from (2,1.5)), (0,2.5) is reached. In (0,2.5) none of the transitions are enabled (and the net deadlocks). Transition t1is enabled as continuous from (2,1.5) to (3,1), where it is enabled as discrete. When t1is fired as discrete from (3,1),(5,0) is reached and t1becomes not enabled. The marking m= (1,2) is reachable in the discrete Petri net, but not in the adaptive one with ∀µ, µ = 1. Therefore, RS(ND,m0) is not, in general, included in RS(NA,m0) with µ∈N|T| for non ordinary HAPNs. On the other hand, it is straightforward to prove that, given that HAPNs allow real-valued markings, the RS of hNA,m0iis not, in general, included in RS(ND,m0). Nonetheless, if µ=∞, the HAPN always behaves as discrete and its RS is trivially identical to that of the discrete PN. 4.2 Reachability space of continuous and hybrid adaptive PN Let us now compare the RS of the HAPN to the RS of its associated continuous PN. Theorem 19 RS(NA,m0)⊆RS(NC,m0) with µ∈R|T| ≥0. Proof Let m∈RS(NA,m0). Therefore, there exists σa=β1tγ1. . . βktγksuch that m0 β1tγ1 −→ m1 β2tγ2 −→ m2··· β3tγk −→ mk=mwhere βi∈R+if mode (tγi, mi−1) = C and βi∈ N+if mode(tγi, mi−1) = D For any of the βiof σa, if mode(tγi,mi-1) = C, then tγiwill be also enabled in hNC,mi-1,iand the same βi∈Tcan be chosen. If mode(tγi, mi−1) = D, then tγiwill be also enabled in hNC,mi-1,i and also the same βi∈N+can be chosen because βi∈R. Consequently, the same firing sequence σaof the HAPN system can be chosen in the continuous system and the same marking mis obtained. The following Corollary is straightforwardly obtained from Theorems 18 and 19. Corollary 20 RS(ND,m0)⊆RS(NA,m0)⊆RS(NC,m0) for ordinary nets with µ∈N|T|. 0 1 2 3 4 5 012345 (0,2.5) (2,1.5) (5,0) (5,0) (3,1) (2,1.5) (0,2.5) Figure 4.3: Reachability space and reachability graph of the Petri Net of the Figure 1.1 behaving as HAPN with µ= (1,1). Furthermore, let us show through an example that the RS of the continuous system is, in general, not contained in the RS of the HAPN system, i.e., RS(NC,m0)*RS(NA,m0) with µ∈R|T|. In the 26 HAPN system is necessary and sufficient for deadlock-freeness of the discrete system. As previously defined in Section 2.5, choice free nets are a subnet of PN, such that each place of a choice free PN has at most one output transition: ∀p|p•| ≤ 1. Let us first prove that it is a sufficient condition. Theorem 22 Let hNA,m0ibe an ordinary deadlock-free HAPN system with µ∈N|T|. Then, the discrete system hND,m0iis deadlock-free. Proof Let us assume that the discrete hND,m0ideadlocks at a marking m. According to Theorem 18, marking mcan be reached by hNA,m0i. Given that the net is ordinary, for every transition t, there exists p∈•tsuch that m[p] = 0, i.e., mis a deadlock for hNA,m0i. For the necessary condition, two technical lemmas are introduced before stating the final result. The first one states that if a sequence σis fireable in the adaptive system, its ceil sequence ⌈σ⌉is also fireable in the discrete one. Definition 23 Let σ=α1tγ1α2tγ2. . . αktγkbe a firing sequence of a given HAPN hNA,m0i. The ceil sequence, ⌈σ⌉of σis defined as: ⌈σ⌉=α′ 1tγ1α′ 2tγ2. . . α′ ktγkwhere α′ i=   X 1≤j≤i|tγi=tγj αj    −X 1≤j<i|tγi=tγj α′ j For example, for the sequence σ1= 0.1t10.8t20.1t10.2t10.8t2in the HAPN of Figure 3.2 (a), the ceil sequence ⌈σ1⌉is defined as ⌈σ1⌉= 1 t11t20t10t11t2. Lemma 24 Let hNA,m0ibe an ordinary choice-free HAPN system with µ∈N|T|. If σis a fireable sequence in hNA,m0ithen ⌈σ⌉is fireable in hND,m0i. Proof Let us assume without loss of generality that σ=α1tγ1. . . αktγkand 0< αj≤1for every j∈ {1,...,k}. Induction on the length of σ:|σ|=k. •Base case (|σ|= 1). Let σ=α1tγ1, then ∀p∈•tγ1,m0[p]≥α1and given that m0[p]∈N, it holds that m0[p]≥ ⌈α1⌉. Thus ⌈σ⌉=⌈α1⌉tγ1can be fired in hND,m0i. •Inductive step. Assume that the Lemma holds for |σ|=k. Let us consider the k+ 1 firing, i.e., tγk+1 fires in αk+1. Two cases can occur: a) α′ k+1 = 0. In this case, the Lemma trivially holds. b) α′ k+1 = 1. Let miand σi(m′ iand σ′ i) be the marking and firing count vector obtained just after the firing of tγiin an amount αi(α′ i). If tγk+1 fires in the HAPN system, it means that mk[p]>0for every p∈•t. Notice that, by definition of ceil sequence, after the kth firing the following inequalities are satisfied: σ′ k[t]≥σk[t]and σ′ k[tq]≥σk[tq]for every tq∈•(•t). Given that the net is choice-free, for every place pit holds that |•p|= 0 or |•p| ≥ |p•|= 1. If for p∈•t, it holds that |•p| ≥ |p•|= 1, then the previous inequalities ensure m′ k[p]≥1. If p has no input transitions, then it must hold that σ′ k+1[t]≤m0[p]. Therefore tγk+1 can fire from m′ kan amount of 1. The second lemma states that if a certain sequence σdeadlocks a HAPN, then its firing count vector is in the naturals. 27 Lemma 25 Let hNA,m0ibe an ordinary choice-free HAPN system with µ∈N|T|. If σis a fireable sequence m0 σ −→ m, such that hNA,m0ideadlocks at m, then σ∈(N∪ {0})|T|, where σis the firing count vector of σ. Proof Let us first prove that if mis a deadlock marking then for every transition tthere exists p∈•t such that m[p] = 0. Notice that just after the last firing of tin the sequence σ, which is necessarily discrete firing given that µ∈N|P|, at least one place p∈•tbecomes empty. Assume that after such a firing, a transition t′∈•pfires. If the firing of t′is discrete then twould become enabled again; if it is continuous then t′is sufficiently enabled to fire also as discrete what would enable t. Hence, after the last firing of t, no transition t′∈•pcan fire and premains empty. Assume that σ[t]>0is not a natural number and that m[p] = 0 for a given p∈•t. Then, there exists t′∈•psuch that σ[t′]is not a natural number and σ[t′]≤σ[t]−m0[p]. Notice that there also exists p′∈•t′such that m[p′] = 0, hence t′′ ∈•p′exists such that σ[t′′]is not a natural number and σ[t′′]≤σ[t′]−m0[p′]≤σ[t]−m0[p]−m0[p′]. This reasoning can be repeated until a transition t∗ is found such that it deadlocked with σ[t∗]<1. Contradiction since natural thresholds do not allow σ[t∗]to be less than 1. Therefore, because of Lemmas 24 and 25, if a deadlock marking mis reachable in hNA,m0i when σis fired, the same deadlock marking m′is reachable in hND,m0i, when ⌈σ⌉is fired. Thus, if hND,m0iis deadlock-free, then hNA,m0iis deadlock-free too. Theorem 26 Let hND,m0ibe an ordinary choice-free and deadlock-free discrete system. Then, the HAPN system hNA,m0iis deadlock-free for any µ∈N|T|. The following Corollary is straightforwardly obtained from Theorems 22 and 26. Corollary 27 Let Nbe an ordinary choice-free net. hND,m0iis deadlock-free iff hNA,m0iis deadlock-free with µ∈N|T|. Chapter 6 Conclusions and future work This Chapter puts forward some conclusions obtained in this “Trabajo Fin de M´aster”, and it proposes some future work. 6.1 Conclusions As most formalisms for discrete event systems, Petri nets suffer from the state explosion problem. Such a problem renders enumerative analysis techniques unfeasible for large systems. The hybrid adaptive Petri nets considered here aim at alleviating the state explosion problem by partially relaxing the firing of transitions. More precisely, a transition can fire in real amounts when its load is higher than a given threshold, and it is forced to fire in discrete amounts when its load is lower than that threshold. This partial relaxation offers a chance of preserving important properties of discrete event systems, as deadlock-freeness, that are not always retained by fully continuous approximations. This work focused on the reachability space and the deadlock-freeness property of hybrid adaptive nets. A general algorithm was proposed for the characterization of the reachablity space of any HAPN. Furthermore, an inclusion relationship was proved for the reachability spaces of the discrete, hybrid adaptive and continuous nets; for a rather general class of nets,. With respect to deadlockfreeness, although this property is not preserved in general for arbitrary real thresholds, it was shown that it is necessary and sufficient for deadlock-freeness of choice-free nets with arbitrary natural thresholds. It has been shown that the HAPN is a general formalism that includes the used and known PN formalisms of discrete, continuous and discrete PN. Due to its high generality, HAPN has a very powerful modeling capability. However, developing analysis techniques for such a general formalism can be costly. Hybrid Adaptive analysis techniques involucre discrete, continuous and hybrid PN techniques, maintaining or increasing its complexity. 6.2 Future Work In this TFM, the formalism of HAPN has been defined and some preliminar results about the Reachability Space, the relations among the Reachability Spaces of hybrid adaptive, discrete and continuous PN, and the conditions to preserve the liveness property are presented. However, the liveness property and the reachability space comparison have been done in just two classes of PN, the ordinary PN and the choice-free PN. The future work will be to study the properties of more general classes of HAPN, and the time interpretation of HAPN: •Preserving properties: Given a certain property, for example deadlock-freeness, it would be very useful to obtain a general method to calculate an adequate threshold vector µsuch that it 29 30 the discrete PN was deadlock-free, the HAPN is also deadlock-free. In this case, any discrete PN would be aproximated by a partially fluidified hybrid adaptive PN. •Relations among the Reachability Spaces of the HAPN, discrete, continuous and hybrid Petri nets of more general subclases of Petri nets can be studied in more depth. •Time interpretation: After defining and studying in depth the autonomous HAPN, a certain firing semantics can be defined. The time interpretation allows the study of certain properties such as performance and the simulation of the nets. When simultaing Petri nets, the inconsistencies between continuous and discrete PN are bigger when the workload is low. Therefore, the simulation of HAPN instead of continuous PN could approximate better the behaviour of the discrete one. •Modeling of a real system using the HAPN. Through a real case study, the characteristics and potential of HAPN would be pointed out. Bibliography [1] E. Fraca, J. J´ulvez, C. Mahulea, M. Silva. On reachability and deadlock-freeness of Hybrid Adaptive Petri nets. In Proc. of 18th IFAC World Congress, 2011 [2] H. Yang, C. Lin and Q. Li. Hybrid simulation of biochemical systems using hybrid adaptive Petri nets. VALUETOOLS ’09: Proceedings of the Fourth International ICST Conference on Performance Evaluation Methodologies and Tools. 2009. [3] M. Silva. Las Redes de Petri: en la Autom´atica y la Inform´atica AC, 1985 [4] T. Murata. Petri nets: Properties, analysis and applications. Proceedings of the IEEE,77(4):541– 580, 1989. [5] R. David and H. Alla. Discrete, Continuous and Hybrid Petri Nets. Springer. 2004. (Revised 2nd edition, 2010), Berlin. [6] R. David and H. Alla. Continuous Petri nets. In Proc. of the 8th European Workshop on Application and Theory of Petri Nets, pages 275–294, Zaragoza, Spain, 1987. [7] L. Recalde, E. Teruel, and M. Silva. Autonomous continuous P/T systems. In J. Kleijn S. Donatelli, editor, Application and Theory of Petri Nets 1999, volume 1639 of Lecture Notes in Computer Science, pages 107–126. Springer, 1999. [8] M. Silva and L. Recalde. Petri nets and integrality relaxations: A view of continuous Petri net models. IEEE Trans. on Systems, Man, and Cybernetics, 32(4):314–327, 2002. [9] M. Silva, L. Recalde. On fluidification of Petri net models: from discrete to hybrid and continuous models. Annual Reviews in Control, Vol. 28(2): 253-266. 2004. [10] J. J´ulvez, L. Recalde and M. Silva. On reachability in autonomous continuous Petri net systems. 24th International Conference on Application and Theory of Petri Nets (ICATPN 2003), Lecture Notes in Computer Science, Springer 2003 [11] F. Balduzzi, A. Giua, G. Menga. First-Order Hybrid Petri Nets: a Model for Optimization and Control. IEEE Trans. on Robotics and Automation, Vol. 16 (4):382-399, 2000. 31