Timed Petri Nets

1. Introduction

In the early 60’s a young researcher in Darmstadt looked for a good representation for communicating systems processes that were mathematically sound and had, at the same time, a visual intuitive flavor. This event marked the beginning of a schematic approach that become very important to the modeling of distributed systems in several and distinct areas of knowledge, from Engineering to biologic systems. Carl Adam Petri presented in 1962 his PHD which included the first definition of what is called today a Petri Net. Since its creation Petri Nets evolved from a sound representation to discrete dynamic systems into a general schemata, capable to represent knowledge about processes and (discrete and distributed) systems according to their internal relations and not to their work domain. Among other advantages, that feature opens the possibility to reuse some experiences acquired in the design of known and well tested systems while treating new challenges.

In the conventional approach, the key issue for modeling is the partial ordering among constituent events and the properties that arise from the arrangement of state and transitions once some basic interpretation rules are preserved. Such representation can respond from several systems of practical use where the foundation for analysis is based in reachability and other property analysis. However, there are some cases where such approach is not enough to represent processes completely, for instance, when the assumption that all transitions can fire instantaneously is no longer a good approximation. In such cases a time delay can be associated to firing transitions. This is absolutely equivalent (in a broader sense) to say that firing pre-conditions must hold for a time delay before the firing is completed. The first approach is called T-time Petri Net and the second P-time Petri Nets.

Thus, what we have in conclusion is that even in a hypothesis that we should consider only firing pre-conditions

In many text books and review articles the enabling condition is presented using only firing pre-conditions as a requirement. This can be justified since the use of this week firing condition is sufficient if a complete net, that is, that includes its dual part, is used

[Murata, 1989][Girault et al., 2003] a time delay is associated with a transition location and consequently to its firing. Several applications in manufacturing, business, workflow and other processes can use this approach to represent processes in a more realistic way. It is also true tat even with a simple approach a strong representation power can be derived, including the possibility to make some direct performance analysis [Marsan, 1998][Wang, 1998]. This is called a time slice or a time interval approach. In general, this augmented nets with time delay (P-time, T-time or even both) are called Timed Petri Nets

Some authors also include another possibility where time is associated to the arcs, that is, to a pair (𝑥,𝑦) where 𝑥,𝑦∈𝑋=𝑆⊆𝑇 where 𝑆 and 𝑇 denotes the set of places and transitions, respectively.

.

There are also cases where it is necessary to use more than time delays. In such cases the time is among the variables that describes the state (a set of places in Petri Nets). Notice that raising the number of variables that characterize a state would make untreatable the enumeration of a net state space. Therefore, a more direct approach is adopted, where each transition is associated to a time interval $t_{min}$ and $t_{max}$ where the first would stand for the minimal waiting time since the enabling until a firing can occur. Similarly, $t_{max}$stands for the maximum waiting time allowed since enabling up to a firing.

If the time used in the model is a real number, then we call that a Time Petri Net. It should be also noticed that if $t_{min}=t_{max}$ the situation is reduced to the previous one where a deterministic time interval is associated to a transition. Thus, Time Petri Net is the more general model which can be used to model real time systems in several work domains, from electronic and mechatronic systems to logistic a business domains.

In this chapter we focus in the timed systems and its application which are briefly described in section 2. In section 3 we will present a perspective and demand for a framework to model, analysis and simulation of timed (and time) systems mentioning the open discussion about algorithms and approaches to represent the state space. That discussion will be oriented by the recent advances to establish a standard to Petri Nets in general that includes Timed and Time Petri Nets as a extension. Such standard is presented in ISO/IEC 15.909 proposal launched for the first time in 2004. A short presentation of what could be a general formalization to Time Petri Nets is done in section 4. Concluding remarks are in section 5.

2. A schematic description of time dependent systems

Petri Nets are an abstract formal model for describing and studying information processing systems that are characterized as being concurrent, asynchronous, distributed, parallel, non-deterministic and/or stochastic [Murata, 1989]. Since its creation the formalism has been extended by practitioners and theoreticians for dealing with complex systems attached to many application fields. One of those important extensions were proposed to deal with timed systems.

Among several proposed extensions to deal with time we detach two basic models: Ranchamdani’s Timed Petri nets [Ramchandani, 1973] and Merlin Time Petri nets [Merlin and Faber, 1976]. These two temporal Petri net models are included in t-time nets because time inscriptions are always associated to transitions. Other time extensions have been published including some approaches where time is associated to places or even to both places and arcs (see [Cerone and Maggiolo-Schettini, 1999] for a survey).

Formally, Petri Nets can defined as:

Definition 1. [Petri Net] A Petri net structure is a directed weighted bipartite graph

$$N=(P,T,A,w)$$E1

where

P is the finite set of places, $P\ne \mathrm{\varnothing }$

T is the finite set of transitions, $T\ne \mathrm{\varnothing }$

A (P × T) ∪ (T × P) is the set of arcs from places to transitions and from transitions to places

w : A → {1,2,3,…} is the weight function on the arcs.

We will normally represent the set of places by $P=\{p_1,p_2,\dots ,p_n\}$and the set of transitions $T=\{t_1,t_2,\dots ,t_m\}$where $\left|P\right|=n$and $\left|T\right|=m$are the cardinality of the respective sets. A typical arc is of the form $(p_i,t_j)$ or $(t_j,p_i)$ according to arc direction, where its weight $w$is a positive integer greater than zero.

Definition 2. [Marked Petri Net] A marked Petri net is a five-tuple $(P,T,A,w,M)$ where $(P,T,A,w)$ is a Petri Net and $M$is a marking, defined as a mapping $M:P\to {\mathbb{N}}^{+}$

Thus, a marking is a row vector with $\left|P\right|$ elements. Figure 1 shows a possible marking for a simple Petri Net.

Figure 1.

A marked Petri net and it respective marking vector M

The relational functions $Pre,Pos:P\times T\to \mathbb{N}$are defined to obtain the number of tokens in places $p_i,\mathrm{ }{p}_j$ which are preconditions or postconditions of a transition$t\in T$, that is, there exists arcs $(p_i,t),(p_j,t)\in A$for the $Pre$function or $(t,p_i),(t,p_j)\in A$for the $Pos$function. In Fig. 1 for instance we have $Pre(b1,a3)=1$and$Pos(b3,a3)=3$.

Using Petri nets to model systems imply in associate net elements (places or transitions) to some components and actions of the modeled system, turning out in what is called “labeled” or “interpreted” nets. The evolution of marking in a labeled Petri nets describes the dynamic behavior of the modeled system.

We restrict the definition of Labeled Petri Net to associate labels only to events or actions similarly to the formalism of automata.

Definition 3. [Labeled Petri Net] A labeled Petri net is a seven-tuple

$$N=(P,T,A,w,E,l,M_0)$$E2

where

(P, T, A, w) is a Petri net structure

E  (T), $E\ne \mathrm{\varnothing }$

l : T → E is the transition labeling function

M₀ : P → ⁺ is the initial state of the net

Labeled Petri Nets has been proved to be an efficient tool for the modeling, analysis and control of Discrete Event System (DES). Petri Nets is a good option to model these DES systems for wide set of applications, from manufacturing, traffic, batch chemical processes, to computer, communications, database and software systems [Lafortune and Cassandras, 2008]. From now on we shall refer to “labeled Petri nets” simply as “Petri nets”.

The state transition mechanism in Petri nets is provided by moving tokens through the net and hence changing to a new state. When a transition is enabled, we say that it can fire or that it can occur.

Definition 4. [Enabled Transition] A transition $t_j\in T$in a Petri net is said to be enabled if

$$\forall p\in P,\mathrm{ }\mathrm{ }\mathrm{ }\mathrm{ }M\left(p\right)\ge Pre(p,t_j)$$E3

In other words, a transition $t_j$ in the Petri net is enabled when the number of tokens in $p$is greater then or equal to the weight of the arc connecting $p$to$t_j$, for all places $p$that are input to transition$t_j$.

The set of all enabled transition at some marking $M$is defined as$enb\left(M\right)$. In Fig. 1 only transitions$a2$, $a4$and $a5$are enabled, then$enb\left(M\right)=\{a2,a4,a5\}$.

Definition 5. [State Transition] A Petri net evolves from a marking M to a marking M’ through the firing of a transition $t_f\in T$only if$t_f\in enb\left(M\right)$. The new marking M’ can be obtained by

$$\forall p\in P\left|\right(p,t_f)\vee (t_f,p)\in A,M\mathrm{\text{'}}(p)=M(p)-Pre(p,t_f)+Pos(p,t_f)$$E4

The reachable markings in a Petri net can be computed using an algebraic equation. Two incidence matrices must be defined ($A^{-}$for incoming arcs, and $A^{+}$ for outgoing arcs) and a firing vector $u$which is a (unimodular) row vector containing “$1$” in the corresponding position of the firing transition and “$0$” in all other positions.

The new marking can be obtained using the state equation:

$$M\mathrm{\text{'}}=M+u(A^{+}-A^{-})$$E5

(1)

This formalism is sufficient to represent a great amount of dynamic discrete systems, based only in partial order sequence of transitions. However, “untimed”

A Petri Net where there is no event depending directly or parametrically of the time

Petri nets are not powerful enough to deal with performance evaluations, safety determination, or behavioral properties in systems where time appears as a quantifiable and continuous parameter.

Ramchandani’s timed Petri nets were derived from Petri nets by associating a firing finite duration to each transition in the net. Timed Petri nets and related equivalent models have been used mainly to performance evaluation [Berthomieu and Menasche, 1983].

Definition 6. [Timed Petri Net] A timed Petri net is a six-tuple

$$N=(P,T,A,w,M_0,f)$$E6

where

(P, T, A, w, M₀) is a marked Petri net

f : T → ⁺ is a firing time function that assigns a positive real number to each transition on the net

Therefore, the firing rule has to be modified in order to consider time elapses in the transition firing. If an enabled transition $t_j\in enb\left(M\right)$ then it will fire after $f\left(t_j\right)$times units since it became enabled. The system state is not only determined by the net marking but also by a timer attached to every enabled transition in the net.

Definition 7. [Clock State] The clock state is a pair$(M,V)$, where $M$is a marking and $V$is a clock valuation function, $V:enb\left(M\right)\to {\mathbb{R}}^{+}$

For a clock state $(M,V)$ and$t\in enb\left(M\right)$, $V\left(t\right)$is the value of the clock associated with a transition$t$. The initial clock state is $s_0=(M_0,V_0)$ where$V_0\left(t\right)=f\left(t\right)$,$\forall t\in enb\left(M_0\right)$.

Definition 8. [New Enabled Transition] A transition $t\in T$is said new enabled, after firing transition $t_f$ at marking $M$which leads to marking$M\mathrm{\text{'}}$, if it is enabled at marking $M\mathrm{\text{'}}$and it was not enabled at $M$or, if it was enabled at M, it is the former fired transition$t_f$. Formally:

$$new\left(M\mathrm{\text{'}}\right)=\{t\in enb(M\mathrm{\text{'}}\left)\right|t=t_f\vee \exists p,\mathrm{ }\left(M\mathrm{\text{'}}\right(p)-Pos(p,t_f\left)\right)\le Pre(p,t)\}$$E7

We denote as $new\left(M\mathrm{\text{'}}\right)$the set of transitions new enabled at marking$M\mathrm{\text{'}}$.

The reachability graph of a timed Pedri net can be computed using the definition of firable transition, that is, those transitions that can be fired in a certain marking.

Definition 9. [Firable Transition] A transition $t_f\in T$can fire in a marking $M$yielding a marking $M\mathrm{\text{'}}$if:

t_f ∈ enb(M)

V_M(t_f ) ≤ V_M(t_i) t_i ∈ enb(M)

We denote as $\mathrm{{\rm Y}}\left(M\right)$the set of transitions firable at a marking$M$. Assuming that the firing of transition $t_f$ leads to a new marking$M\mathrm{\text{'}}$, we denote it as $(M,V_M)\stackrel{\tau }{\to }(M\mathrm{\text{'}},V_{M\mathrm{\text{'}}})$ where $\tau =V_M\left(t_f\right)$is the time elapsed in state transition, M’ is computed using equation 1 and $V_{M\mathrm{\text{'}}}$ is computed as follows:

$$V_{M\mathrm{\text{'}}}=\left\{\begin{array}{cc}f\left(t\right)& set\in new\left(M\mathrm{\text{'}}\right);\\ V_M\left(t\right)-\tau & set\in enb\left(M\mathrm{\text{'}}\right)\backslash new\left(M\mathrm{\text{'}}\right)\\ & \end{array}\right.$$E8

The reachability tree can be built including all feasible firing sequences of the timed Petri net. Notice that in $M_0$ all transition are new enabled,$enb\left(M_0\right)=new\left(M_0\right)$. However, finite reachability trees can be built only for bounded Petri nets (see bounded property in [Murata, 1989], and an equivalent result for Time Petri in [Berthomieu and Diaz, 1991]).

Paths or runs in a reachability tree are sequences of state transitions in a timed Petri net. Then, the time elapsed in some path can be computed as the summation of all the elapsed times in the firing schedule. If a path $\omega =s_0\stackrel{{\tau }_1}{\to }{s}_1\stackrel{{\tau }_2}{\to }{s}_2\stackrel{{\tau }_3}{\to }{s}_3$exists, then the time elapsed between states $s_0$ and $s_3$ is$\tau ={\tau }_1+{\tau }_2+{\tau }_3$.

The reachabitity tree approach has been successfully used in communication protocols validation and in performance analyses [Sifakis, 1980, Zuberek, 1980]. Moreover, these tests require known computation times for the tasks (often referred by WCET as “Worst Case Execution Time”) or process durations. Besides the difficulty to measure or estimate such times, taking into consideration a deterministic time (even in the longest path) does not lead necessarily to the worst case [Roux and Déplanche, 2002].

More realistic analysis can be done on communication protocols using Merlin approach, since some network time durations or even software routines cannot be completed always in the same time [Merlin and Faber, 1976, Berthomieu and Diaz, 1991].

Merlin defined Time Petri Nets (TPN) as nets with a time interval associated to each transition. Assuming that a time interval $[a,b]$ ($a,b\in {\mathbb{R}}^{+}$) is associated with a transition$t_i$, and that such transition has been enabled at a marking $M_i$ and is being continuously enabled since then in all successive markings$M_{i+1},\dots ,M_{i+k}$, we define:

• $0\le a$$t_i$
• $0\le b\le \mathrm{\infty }$

Times $a$and $b$for transition $t_i$ are relative to the moment in which transition $t_i$ became last enabled. If transition $t_i$ became enabled at time$\tau$, and remains continuously enabled at $\tau +a$then it can be fired. After time$\tau +a$, transition $t_i$ can remains continuously enabled without fire until$\tau +b$, in which it must be fired. Note that transitions with time intervals $[0,\mathrm{\infty }]$ correspond to the classical "untimed" (no deterministic) Petri net behavior.

The firing semantic described here is called “strong semantic”. There also exists a called “weak semantic” in which transitions must not necessarily be fired at its LFT, and after that time it can no longer be fired [Riviere et~al., 2001]. In this chapter we will used the strong semantic.

Time Petri nets then can model systems in which events has non-deterministic durations. State transitions in that kind of systems may occur not in an exact time but in some time interval. Real-time systems are examples of this kind of system.

Definition 10. [Time Petri Net] A time Petri net is a six-tuple

$$N=(P,T,A,w,M_0,I)$$E9

where

(P, T, A, w, M₀) is a marked Petri net

I : T → {⁺,⁺ ∪ {∞}} associates with each transition t an interval $[\downarrow I(t),\uparrow I(t\left)\right]$ called its static firing interval. The bounds of the time interval are also known as EFT and LFT respectively.

The enabling condition remains the same as in the timed Petri Net but the firing rule must be redefined. The possibility to fire in a time interval rather than an exact time lead to the existence of infinite clock states. Then, even for bounded Petri nets the state space will be infinite, turning intractable any analysis technique based on that model formalism. To overcome this problem, Berthomieu and Menasche [Berthomieu and Menasche, 1983] proposed a new definition for state.

Definition 11. [Interval State] A state in a TPN is a pair $(M,\theta )$ where

M is a marking

$\theta$is a firing interval function$\theta :enb\left(M\right)\to \{{\mathbb{R}}^{+},{\mathbb{R}}^{+}\cup \{\mathrm{\infty }\left\}\right\}$.

The firing interval associated with transition $t\in enb\left(M\right)$is$\theta \left(t\right)=[\downarrow \theta (t),\uparrow \theta (t\left)\right]$.

Using that approach, a bounded TPN yields a finite number of states [Berthomieu and Diaz, 1991]. Note that each Interval state contains infinite clock states, then the new state definition allow us to group infinite clock states into one interval state satisfying the condition:

$$(M,V)\in (M\mathrm{\text{'}},\theta )iff(M=M\mathrm{\text{'}})\wedge \forall t\in enb\left(M\right),\mathrm{ }\downarrow \theta \left(t\right)\le f\left(t\right)-V\left(t\right)\le \uparrow \theta \left(t\right)$$E10

An enumerative analysis technique was introduced in [Berthomieu and Menasche, 1983] based in what is called “state classes”. An algorithm for enumeration of these state classes was proposed for bounded TPNs and then used to the analysis of system. Since then, many algorithm has been proposed to build system state space based on the state class approach [Berthomieu and Diaz, 1991, Boucheneb et~al., 1993, Yoneda and Ryuba, 1998, Berthomieu and Vernadat, 2003, Hadjidj and Boucheneb, 2008, del Foyo and Silva, 2011].

Definition 12. [Firable Transition] Assuming that transition $t_f\in T$becomes enabled at time $\tau$in state$(M,\theta )$, it is firable at time $\tau +\lambda$iff:

t_f ∈ enb(M) : $t_f$is enabled at$(M,\theta )$.

 t_i ∈ enb(M), ↓ t_f ≤ λ ≤ min(↑t_i)

We denote as $\mathrm{{\rm Y}}\left(s\right)$the set of transitions firable at state $s=(M,\theta )$and as $(M,\theta )\stackrel{t_f,\lambda }{\to }(M\mathrm{\text{'}},\theta \mathrm{\text{'}})$ the behavior “transition $t_f$ is firable from state $(M,\theta )$ at time $\lambda$and its firing leads to state$(M\mathrm{\text{'}},\theta \mathrm{\text{'}})$”

The first condition is the usual one for Petri nets and the second results from the necessity of firing transitions according to their firing interval. According to the second condition, a transition$t_f$, enabled by a marking $M$at absolute time$\tau$, could be fired at the firing time $\lambda$iff $\lambda$is not smaller than the EFT of $t_f$ and not greater than the smallest of the LFT’s of all the transitions enabled by marking$M$.

Each firable transition will have its own time interval in which it can be fired. That time depends of its EFT and of the time elapsed since it became last enabled, and of the time in which the rest of the the enabled transitions will reach its LFTs, also according to the time elapsed since each one became last enabled.

Definition 13. [State Class] A state class is a pair $C=(M,D)$where:

M is a marking;

D is the firing domain of the class.

The state class marking is shared by all states in the class and the firing domain is defined as the union of the firing domains of all the states in the class. The domain $D$is a conjunction of atomic constraints of the form$(t-t\mathrm{\text{'}}\prec c)$, $(t\prec c)$or$(-t\prec c)$, where$c\in \mathbb{R}\cup \{\mathbb{\infty },-\mathbb{\infty }\}$, $\prec \in \{=,\le ,\ge \}$and$t,t\mathrm{\text{'}}\in T$.

The domain of $D$is therefore convex and has a unique canonical form defined by:

$$\underset{(t,t\mathrm{\text{'}})\in enb(M{)}^2}{\wedge }\mathrm{ }t-t\mathrm{\text{'}}\le Su{p}_D(t-t\mathrm{\text{'}})\wedge \underset{(t\in enb(M\left)\right)}{\wedge }\mathrm{ }t\le Su{p}_D\left(t\right)\wedge -t\le Su{p}_D(-t)$$E11

where$Su{p}_D(t-t\mathrm{\text{'}})$, $Su{p}_D\left(t\right)$, and $Su{p}_D(-t)$are respectively the supremum of$t-t\mathrm{\text{'}}$, $t$, and $-t$in the domain of$D$.

In [Boucheneb and Mullins, 2003] was proposed an implementation for the firing rule, which directly computes the canonical form of each reachable state class in$O\left(n^2\right)$. The firing sequences beginning at some state $s_i$ has the form:

$$\omega =s_i\stackrel{t_1,[l_{i+1},u_{i+1}]}{\to }{s}_{i+1}\stackrel{t_2,[l_{i+2},u_{i+2}]}{\to }{s}_{i+2}\dots s_{i+n-1}\stackrel{t_j,[l_{i+n},u_{i+n}]}{\to }{s}_{i+n}$$E12

(2)

where the intervals $[l_n,u_n]$ for each $t_n$ are respectively the minimum and maximum time in which the transition can fire.

Once the state space is built, different verifications can be done, including model-checking techniques which determine if some temporal formulas are true or false over the state space. There are severals tools that use such approach [Berthomieu et~al, 2004, Hadjidj and Boucheneb, 2006, Gardey et~al., 2005, Yoneda and Ryuba, 1998, del Foyo and Silva, 2011].

In the special case where EFT and LFT has the same value, the behavior of the TPN reproduce the one of timed Petri Nets. Note that in paths over the graph which is built using the timed Petri net firing rule, the elapsed time in state transitions is fixed while in the TPN it is a time interval. In timed Petri nets states are clock states while in TPN they are interval states or state classes that contain infinite clock states.

The Timed Automaton (TA) with guards [Alur and Dill, 1990] is an automaton to which is adjoined a set of continuous variables whose dynamical evolution is time-driven. This formalism has been used to modeling and to a formal verification of real-time systems with success. Some tools as KRONOS [Daws et~al., 1995] and UPPAAL [Larsen et~al., 2000] are available for such purposes. The state space yielded using Timed Automaton with guards is quite similar of that of TPN regarding the differences on their constructions.

3. Towards a unified PN system framework

In spite of the great theoretical importance and applicability of Time (or Timed) Petri Nets the PN theory was develop since the early 60’s in different directions, always seeking for a way to face combinatorial explosion or to approximate to Fuzzy Logic or object-oriented systems. Several extensions were developed to fit practical applications or to attend the need to treat a new class of distributed systems, such as real-time systems. The new century started with a good amount of work published in this area but also with some confusion about concepts and representations. On the other hand, the raising complexity of distributed systems demanded a unified approach that could handle from abstract models down to the split of these general schemas in programs addressed to specific devices. In fact, integrated and flexible systems depend on that capacity.

A ISO/IEC project were launched in the beginning of this century to provide a standard to Petri Nets: the ISO/IEC 15909. Briefly, this project consists of three phases, where the first one defined P/T nets and High Level Nets in a complementary view, that is, taken P/T nets as a reduced set of the High Level Nets (HLPNs) when we reduce the color set to only one type. That is equivalent to unfold the net. Therefore, the proposed standard provides a comprehensive documentation of the terminology, the semantical model and graphic notations for High-level Petri nets. It also describes different conformance levels. Technically, the part 1 of the standard provides mathematical definitions of High-level Petri Nets, called semantic model, and a graphical form, known as High-level Petri Net Graphs (HLPNGs), as well as its mapping to the semantic model [ISO/IEC, 2002, ISO/IEC, 2005].

Similarly to other situations where advances in technology and engineering demands a standardization, the introduction of a Petri Net standard also put in check the capacity of exchanging models among different modeling environments and tools. Thus, a Petri Net Markup Language (PNML) was introduced as an interchange format for the Petri nets defined in part 1 of the standard [Kindler, 2006]. That composes the Part 2 of the standard and was published in February 2011, after a great amount of discussion, defining a transfer format to support the exchange of High-level Petri Nets among different tool environments [ISO/IEC, 2005]. The standard defined also a transfer syntax for High-level Petri Net Graphs and its subclasses defined in the first part of the standard, capturing the essence of all kinds of colored, high-level and classic Petri nets.

Part 3 is of the standard is devoted to Petri nets extensions, including hierarchies, time and stochastic nets, and is still being discussed, with a estimated time to be launched in 2013. The main requirement is that extensions be built upon developments over the core model, providing a structured and sound description. That also would allow user defined extensions based on built-in extensions and would reduce the profusion of nets attached to application domains. At least two main advantages would come out from that:

• a simple, comprehensive and structured definition of PN which would make it easier the modeling and design of distributed systems;

• a wide range of possible applications will be using the same representation which facilitate the re-use of modeling inside work domains;

• the expansion of reusability to cases among different work domains, reinforcing the use of PNs as a general schema;

• the extension of the use of Petri Nets beyond the modeling phase of design, including requirements analysis and validation.

Thus, it is very important to insert Timed Petri Nets in the proper context of the net standard, and in the context of PN extensions. During the last years a design environment has been built, in parallel with our study of Timed nets and its application to the design of automated and real time systems: the General Hierarchical Enhanced Net System (GHENeSys), where timed Petri Nets were included in a complementary way. That is, the time definition - which could be a proposal to part 3 of the standard - is made associating to each transition (place) a time interval, as proposed by Merlin [Merlin and Faber, 1976] to model dense time. In the special case of deterministic transition (place) time it suffices to make the interval collapse by making the extremes equal to the same constant. For the case of a deterministic time PN, this imply in modifying Definition 6 to have the mapping$f:T\to \{{\mathbb{R}}^{+}\times {\mathbb{R}}^{+}\cup \{\mathrm{\infty }\left\}\right\}$.

Besides the time extension, GHENeSys is also a hierarchical, object-oriented net which has also the following extended elements:

• Gates: which stands for elements propagating only information and preserving the marking in its original place. It could be an enabling gate, that is, one that send information if is marked or an inhibitor gate, if propagates information when is not marked. Of course GHENeSys does not allow internal gates. Thus gates should have always an original place, a special place called pseudo-box.

• Pseudo-boxes: denotes an observable condition that is not controlled by the modeled system. During the course of the modeling pseudo-boxes could also stand for control information external to the hierarchical components and could be collapsed when components are put together. Thus, pseudo-boxes must be considered in the structure of the net but should not affect its properties or the rank of the incidence matrix.

The graphic representation of the elements followed the schema shown in the Fig. 2 bellow,

Figure 2.

Graphic representation GHENeSys graphic elements.

Since our focus in this work is time extensions we illustrate hierarchy with a simple example net shown in the Fig. 3 Notice that hierarchical elements are such that the border is composed of only place or transition elements and has a unique entrance element and a unique output element. Besides, we require that each hierarchical element be simply live, that is, there is at least one live path from the entrance to the output. This is called a proper element in the theory of structured systems.

Figure 3.

Example of hierarchical proper elements or macro-boxes and macro-transitions.

Definition 14.[GHENeSys] GHENeSys is tuple $G=(L,A,F,K,\mathrm{\Pi },C_0,\tau )$where $(L,A,F,K,\mathrm{\Pi })$ represents a net structure, $C_0$is a set of multisets representing the initial marking, and $\tau$is a function that maps time intervals to each element of the net.

• $L=B\cup P$Boxespseudo-boxes
• $A$
• $F\subseteq (L\times A\to N)\cup (A\times L\to N)$
• $K:L\to N^{+}$
• $\mathrm{\Pi }:(B\cup A)\to \left\{\mathrm{0,1}\right\}$
• $C_0=\left\{\right(l,{\sigma }_j\left)\right|l\in L,{\sigma }_j\in R^{+}\mathrm{ }\mathrm{ }\left|l\right|\le K\left(l\right)\}$
• $\tau :(B\cup A)\to \{{\mathbb{R}}^{+},{\mathbb{R}}^{+}\cup \{\mathrm{\infty }\left\}\right\}$

3.1. A simple example of verification with GHENeSys

As mentioned before the main advantage of GHENeSys is to facilitate the verification of requirements and restrictions in the modeling and design of distributed systems. Therefore the environment should be able to related the elements and verify the interpretation of formulas that could involve deterministic time (explicitly or not). In the simple example that follow we show how this verification is performed in the GHENeSys system.

Besides the illustration of the use of deterministic time and the GHENeSys net, the example also shows a method adopted to the modeling with Petri Nets, which is based on eliciting requirements in UML and then (if the target is a dynamic system) transforming the semantic diagrams of UML in classic Petri Nets

It would also be possible to synthesize a high level net, but this is not in the scope of the present work

. A Petri Net with some extensions is created in the GHENeSys which also allows the insertion of formulas in CTL that can be verified. Figure 4 [Baresi et al., 2001] shows the UML class diagram to this problem. In a cycle time three drives come to the station which has only two independent pumps.

Figure 4.

Class diagram to the problem of gas station.

In the gas station problem three different agents are identified: i) the gas station management who is responsible for charging the users, ii) the pumps that are supposed to serve gasoline to the costumers, and iii) the costumers, that is, drivers who are supposed to pay for a proper amount of gasoline and them help themselves. In this simple event we follow the model proposed in Baresi [Baresi et al., 2001] where three drivers depends of only one cashier to pay for the gas and can use two different pumps to fill their cars. First of all we can guarantee that the proper process is followed and them we could insert a characteristic time in the basic operations. We used GHENeSys to provide the model using a classic P/T net. The resulting model is shown in the Fig. 5. This problem is to simple to use extensions but even in that case it would be possible to simply verify if the payment was done (using a gate) to enable the pump with the proper amount of gas instead or carrying the mark. For this problem it would be no significant difference in the size of the graph or in the resulting model.

Figure 5.

Classic model to the gas problem.

The important feature here is to follow a modeling approach, which is implied in the steps described so far. Before modeling, requirements should be modeled in UML by semantic diagrams. There is a good discussion in the academy about the choice of the diagrams to each class of problem. Some authors prefer to go directly to SysML [Andrade et al, 2011] while others just leave open the question about which diagrams should be used and invest in the analysis of this diagrams using Petri Nets [del Foyo et al., 2011, Vaquero et al, 2009, Tierry-Mieg et al, 2008, Baresi et al., 2001, Bodbar et al, 2000].

Proceeding with our example let us suppose that we desire to verify some properties of the model such as

$$getMoney\to \forall \diamond Pumping$$E13

(3)

$$\forall \mathrm{∎}(getMoney\to \forall \diamond Pumping)$$E14

(4)

Using GHENeSys, formulas 3 and 4 can be evaluated by the Timed Petri Net modeling as we can see in the following.

Figure 6.

Sanpshot of the GHENeSys verifier for property 4.

The introduction of deterministic time (transition) would add more detail about the process, with the characteristic time for processing the payment or to fill a car. An organized queue would fail (even if works quite fine in the model) since this time can be modified depending of the user or to unpredictable events during the payment or during the supply process. However if specific (and deterministic)intervals such as 3 min for the payment and 5 min for the filling of gas are stablished, the system could handle 9 drivers in 25 min with a waiting time of at most 2 min for some drivers.

More convincing examples can be found in business, manufacturing or computer networks. More challenge problems emerged in the spatial applications or satellite control, but what is important is that even deterministic time approach can be used to solve a diversified set of problems. However, it could be stressed that the timed approach should be supported for tools and environments that rely in a sound and complementary approach to Timed Nets including Time Petri Nets. The approach shown here, inserted in the GHENeSys environment is exactly one of this cases. Besides, GHENeSys is an implementation of a unified net, that follows the specifications in ISO/IEC 15909 standard.

In the next section we go further in the discussion of using Petri Nets and specifically Timed Petri Nets to fit requirements that come in the new version of UML, which includes time diagrams and timelines.

4. PN as a general system representation framework

As pointed in the beginning of this work, Petri Nets has developed for the last fifty years to become a general schema for systems modeling.

In the previous section, we showed that a modeling discipline should be followed to achieve good results with Petri Nets formal representation, specially when time is an important variable to consider, either by deterministic time or using continuous dense time intervals. However, in the example above time does not appear explicitly at the beginning, since we started with the class diagram where there was no reference to duration time of the processes (supplying or payment). The problem them begins with a demand to a proper representation of time duration in UML that could later be transformed in a timed net.

To fit this demand UML 2.0 specification inserted an interaction diagram derived from the sequence diagram where time intervals or time duration are very important issues. Thus, once identified the actors and sub-systems in the model, their interaction could be viewed and modeled taking in account that it occurs during a running time where specific events can cause a change in the status of that interaction. Thus, the full relation can be described in what is called a state lifetime where several timelines show the evolution of the interacting components.

OMG (www.omg.org) shows a very appealing example of time diagram to model

Figure 7.

Time diagram for the web user latency.

In Figure 7 we can see a hierarchical superposition of levels and the action derived from the interaction between a user and a web system. Sub-systems invoked by this action and the time they spent to provide a proper action are explicitly depicted. As in the previous problem of the gas station, the total time interval spent to serve one or nine users is the summation of the not superposed time intervals required for each dependent action.

Thus, the complete process would be to elicit the requirements using UML diagrams - including time diagrams - synthesize a Timed Petri Net from this model, and them perform the requirement analysis and final synthesis of a model for the problem. In fact, the final results for the example of the gas station were obtained following this approach.

Formally, the timelines are drawn according the behavior of state variables, defined in the following.

Definition 15.[State Variables] A state variable is a triple $(V,T,D)$ where:

V = v_i is a finite set of state values;

T : V → V specify each atomic transition or change in value.

D : V →  ×  is the time duration for each state value.

A timeline is the tracking of all changes in state value in a interval $[0,\tau )$ where $\tau$is the observed time horizon. A timeline is said to be completely closed if the union of its not superposed values is exactly$\tau$. In that case the transitions occur in deterministic time.

If the transitions occur in a time interval $[t_{min},t_{max}]$ the timeline is said to be flexible. In this case we can represent the transition in a Timed Petri Net by an interval, as proposed in the first section. If we want to deal with deterministic time transition it is enough to make $t_{min}=t_{max}$ and the same net framework could be used.

Timeline models can be very useful in some critical problem applications such as intelligent planning and scheduling. Some of those applications could be used in spatial projects [Cesta et al, 2010]

See also the Mexar 2 Project and the use of intelligent software application in the link mexar.istc.cnr.it/mexar2.

. In other applications Petri Nets were used to perform requirements analysis including deterministic time, as in the one proposed by Vaquero et al.[Vaquero et al, 2009][Vaquero et al, 2011]. In that case the idea of solving real life planning problems starts with the elicitation and specification of requirements using UML, goes through the analysis of this requirements using Timed Petri Nets, synthesizes a model also in Petri Nets and finally uses a specific language, PDDL, to transfer the model to software planners which will provide the final result. Also, a modeling design environment were developed to perform this process[Vaquero et al, 2011][Vaquero et al, 2009].

Figure 8.

Language structure in itSIMPLE 3.1

Figure 9.

Time diagram in the itSIMPLE system.

A specific state lifetime were developed to model and analyze the timelines for the agents and objects that would compose the plan, as shown in Figure 8.

Based on this time diagram Petri Nets could be synthesized to make the proper validation of the model. It is important to notice that there are a large number of approaches and tools that claim to perform a good analysis of models directly associated to a planer software with good results. However, most of this systems address only model problems which are well behaved and/or have a limited size and complexity. When the challenge is to model a large system, such as the space project mentioned before or a port to get and deliver petroleum, the challenge could be too big to be faced by these proposals.

Therefore the combination UML/Timed Petri Nets could be successful in the modeling of large and complex problems also in the planning area, with the possibility to be applied in practice to real systems.

5. Conclusions

In conclusion it is important to remark that the evolution of Petri Nets towards a formal representation, capable to treat complex systems should be based in two basis: the extension to model timed systems; and the development of a unified net that includes all extensions besides the timed approach - hierarchy, gates, not controled elements, always respecting the recent published ISO/IEC standard and its next release to appear in 2013. This is the fundamental concepts to have new environments that could support a complementary treatment of timed systems, that is, that could deal with deterministic timed net as well as with time PN in the same environment. That is the focus of the present work.

Besides, it would be advisable that the same environment could deal, also in a complementary way, with classic P/T nets as well as with high level (HLPN) nets or even with simetric nets, which is also part of the ISO/IEC standard. The novelty would be to use a unified net system as a platform to reach the further challenge which would be the introduction of abstract nets.

In what concerns the unified net to treat time intervals and dense time, we achieve a good point with the system GHENeSys where the present work focus most in the first part. However, in [del Foyo and Silva, 2011] a more detailed description of the state class algorithm is given and the basic concepts that lead to a modeling and simulation approach to dense time nets. Therefore the unification with timed PN is a promising result in the near future. Also the system GHENeSys is being developed to implement a unified net as we described above, dealing with P/T and HLPN in the same environment. That is a good combination, capable to model and simulate timed and time nets (in that case using model checking) in the same environment, with the advantage to have a sound and formal representation supporting all process.

Thus, it would be possible to have performance analysis that really fits the complexity of the problem addressed, adapting very easily to discrete or dense time approach.

Acknowledgement

The authors acknowledge to all members of the Design Lab in Mechatronic Department for their work who are present in every part of this article be in the background, in the implementation of tools, in the search for new applications in the analysis of the problems already solved. Particularly we thank the work of Gustavo Costa, Arianna Salmon and Jose Armando S. P. Miralles.