In this paper we use partial order semantics to express the truly concurrent behaviour of interval-timed Petri nets (ITPNs) in their most general setting, i.e. with autoconcurrency and zero duration, as studied with its standard maximal step semantics in [8]. First we introduce the notion of timed processes for ITPNs inductively. Then we investigate if the equivalence of inductive and axiomatic process semantics - true for classical Petri nets - could hold for ITPNs too. We will see that the notions of independence and immediate ring obligation seem to be antagonistic ones, and that local axioms, adequate to de ne processes of classical Petri nets, are not su cient to caracterize timed Processes of IITPNs. We propose several original "global" axioms which reveal to be an e ective solution. Thus we yield nally a full axiomatic de nition of timed processes for ITPNs.
Petri nets are an algebraic and graphical formalism, proposed by Carl Adam
Petri [
Several time extensions of Petri nets have been proposed in the literature,
[
Let us state precisely the concepts which lead to the describtion of the
behaviour of ITPNs under maximal step semantics, cf. [
By convention, we only consider ITPNs with zero duration which are
wellformed, as in [
Partial order semantics allow to describe the behaviour of concurrent systems
by expressing explicitly concurrency, seen as independency. Processes are the
usual partial order semantics for classical Petri nets [
Inspired by this approach, we de ne in this paper timed processes for ITPNs,
inductively using ring step sequences. To our knowledge processes have never
been introduced for this class. Our de nitions will be coherent with the approach
in [
But when trying to de ne timed processes axiomatically, some antagonism appears. Let us remind that the axiomatic de nition (for classical Petri Nets) states local properties which are true for all events in the process, independently of all other events and independently of any particular cut (or marking). Now, for ITPNs, events have to satisfy global contraints too, they are no longer independent but inter-dependent and cuts (before ticks) will play the role of synchronisation barriers. In particular, each tick event depends on the set of events which precede it. We will see the limits of an axiomatization where only local properties are de ned and illustrate them with an example. Then gradually the global constraints are discussed and formulated in "global" axioms. Such global axioms are something original in Petri Net semantics. We succeed to give them in rst order logic without quanti cation on sets (or cuts). Finally we are able to present a group of local and global axioms which form a total axiomatization of timed processes.
The remaining of the paper is organized as follows: Section 2 contains formal de nitions about Interval-Timed Petri Nets. In Section 3 basic de nitions around partial order structures can be found. Section 4 gives an inductive de nition of timed processes and Section 5 details the discussion and formulation of an axiomatic one. Section 6 presents some concluding remarks. 2
A Petri net is a 3-tuple N = (P; T; v) such that - P and T are nite sets of places and transitions respectively with P \ T = ; - v : (P T ) [ (T P ) ! N is its valuation function.
The states of Petri nets are described by markings M : P ! N which are represented by vectors of dimension jP j.
Let x be a node such that, x 2 P [ T . The preset of x is denoted by x, with x = fy 2 P [ T j v(y; x) > 0g. Similarly, x denotes the postset of x, with x = fy 2 P [ T j v(x; y) > 0g. In the same manner, the preset of a net N is de ned by N = fx 2 P [ T j x = ;g, the postset of a net N is de ned by N = fx 2 P [ T j x = ;g.
Formally, a multiset U of events E is a mapping U : E ! N, such that, for e 2 E the natural number U (e) is called the multiplicity of e. The multiset U can be written in the extended set notation U = feU(e) j e 2 E and U (e) 6= 0g.
Several time extensions of classical Petri nets have been proposed to integrate
temporal modeling properties, time Petri nets [
In this paper, Interval-Timed Petri Nets (ITPNs) are considered in their most
general setting, i.e. allowing zero duration and autoconcurrency. ITPNs are an
extension of Timed Petri Nets in which the ring duration of each transition is
given within an interval. We recall shortly the de nitions of [
An Interval-Timed Petri Net is a 5-tuple N = (P; T; v; M0; I) such that - (P; T; v) is a Petri net, called skeleton of the net N - M0 : P ! N is its initial marking - I : T ! N; N is its interval function.
We suppose that the set of transitions is enumerated: T = ft1; t2; ::; tjT jg. The time interval associated with a transition t is given by I(t) = sfd(t); lfd(t) , where sfd(t) is called the shortest ring duration and lfd(t) sfd(t) the longest ring duration.
Only ITPNs are considered whose transitions have a non empty preset and postset i.e., for each transition t 2 T holds that j tj > 0 and jt j > 0.
In Interval-Timed Petri Nets a marking is not su cient to describe completely the state of a net. The state must also include temporal informations. This is given by a matrix which codes the transitions clocks.
D e nition 3 State A state of an ITPN N = (P; T; v; Mo; I) is a pair S = (M; h) such that - M is a marking. - h is a clock matrix which has jT j rows and d columns s.t. d = max lfd(ti) + 1 . ti2T The value hi;j+1 represents the number of active transitions ti with age j (i.e. red since j time ticks).
The set of all possible states of N is denoted by States(N ). The initial state of N is denoted S0 = (M0; h0) where M0 is the initial marking of the skeleton and h0 is a zero matrix, i.e. no transition is active. 2.1 Firing rules for ITPNs
Let N be an ITPN and S = (M; h) its current state. Then a transition t is enabled at the marking M n times autoconcurrently if 8p 2 P; n v(p; t) 6 M (p). If n = 1 this is the usual de nition of (single) enabling.
For each transition the value Ei(M ) tells how many times (at most) transition ti can be red autoconcurrently at marking M . Thus Ei(M ) = ni if 8p 2WPh;en(tnrianvsi(tpi;otnis) 6maMy (pr)e,anrdin9gps2taPrt;s i(mnmi+ed1ia)tevly(p;;tthii)s>isMdo(npe) b.y removing input tokens from the preplaces of the chosen transitions. A start red transition t stays active for some time delay in between its associated time interval sfd(t); lfd(t) , until it may or must end re by delivering the output tokens to its postplaces.
Three types of events are distinguished : start re, end re and tick events. The e ect of each of these events on the state of an ITPN is given below.
Let N be an ITPN and (M; h) its current state. 1. Start re events : A start re event, denoted by [ti, may occur immediately, even up to n times, if ti is enabled at M , resp. if Ei(M ) = n. For each occurrence of [ti the needed input tokens of ti are removed from their preplaces, the clock associated with ti will count this occurrence by incrementing the number hi;1. (M; h) [t!i (M 0; h0) with M 0 = M P v(p; ti) and h0i;1 = hi;1 + 1.
p2 ti There may be con icts between enabled transitions, and the way they are solved is arbitrary. Tick events may not occur when there are still enabled transitions, i.e., if for some i, Ei(M ) > 0. 2. End re events : An end re event, denoted by tii must occur (even n times) if the clock associated with some ti reach the upper bound of its associated interval i.e. hi;j+1 1 with j = lfd(ti). An end re event tii may occur if there is an active transition ti with age in [sfd(ti); lfd(ti)[ . The corresponding hi;j+1 is then decremented. (M; h) t!ii (M 0; h0) if
P sfd(ti)6j6lfd(ti) M 0 = M + P v(ti; p) and h0i;j+1 = hi;j+1 p2ti hi;j+1 > 1 with 1 for some j with hi;j+1 > 0.
If this new state enables some transitions, one or more start re events must then occur, and if end re events(of zero duration) must occur in the sequel, they have to be handled, and so on. 3. Tick events : A tick event, denoted by X, is enabled once neither a start re event nor a must end re event have to occur. The tick event increments the clocks for all active transitions and models the passing of time. (M; h) X! (M 0; h0) with M 0 = M and for all i holds if ( Ei(M ) = 0 and hi;lfd(ti)+1 = 0 then h0i;j =
The ITPN N presented in Fig.1. is used as a running example.
p1 5 2
The condition of the occurrence of a tick event ensures that what have occurred since the previous tick event (i.e. in between two ticks) is maximal. In the case of transitions which may late zero time, which is allowed in the net class considered here, the notion of start ring event which need to occur "immediately", means "before the next tick". There is no time scale within zero time. The following de nition will precise the notion of global step which happens in between two ticks and where multisets of start re and end re events will alternate until nothing more need to occur.
We only consider wellformed ITPNs in this article. They ensure to have always only a nite number of events which appear between two ticks. If there is no ring sequence of transitions of possible zero duration which increases a marking, the ITPN is wellformed. This property is decidable on the subnet restricted to transitions whose sfd is zero.
All results given here could be easily extended to ITPNs which are not
necessarily wellformed: they allow in nite global steps where no tick event can follow.
Thus such an in nite global step would be the "end" of a step ring sequence.
We just like to limite the considerations here to the standard wellformed case.
The executions of wellformed ITPNs with zero duration and autoconcurrency
under maximal step semantics are given by the so called ring step sequence as
de ned in [
A globalstep is a multiset of ring events of an ITPN in between two tick events, it consists on two principal multisets, the rst one is called Endstep and the second one is called Iteratedstep. So a ring step is a triplet (Endstep; Iteratedstep; tick), or a couple (globalstep; tick).
An Endstep at state S contains all end re events which must occur at S and an arbitrary multiset of end re events which may occur at S. At the beginning, at initial state S0, it is always empty as no transition has start red. In the following steps, it can be empty; then the whole global step can be empty and one tick event follows immediately the previous one. An Iteratedstep is an alternating sequence of multisets of start re events (not necessarily maximal) and multisets of end re events with zero duration (containing all must end re ones). The alternation ends if neither a transition is enabled nor an end re event with zero duration must occur, thus the iterated step is maximal and nite. This situation happens because of the wellformedness.
Thus a ring step sequence of length n is given by
globalstep1 ~ X globalstep2 ~ X globalstepn ~ X = S0 ! S0 ! S1 ! S1 ! S2 Sn 1 ! Sn 1 ! Sn. If in S~n 1 = (M~ n 1; h~n 1) no transition is active, i.e. if h~n 1 is the Zero-matrix, then we have a deadlock , and the last tick and Sn do not exist.
The following example illustrates ring steps.
E xample 1 Consider the ITPN N , one possible initial ring step from its initial state S0 is given in the sequel.
The rst Endstep is necessarily empty (Endstep1 = ;). Then, suppose that we re two times t1 and one time t2, i.e. f[t12; [t2g then we choose to end re t1 at zero duration, i.e. ft1ig, after that we re f[t4g, no further start re event is possible now, so a tick event is executed. The rst iterated step is the union of all these multisets : Iteratedstep1 = f[t12; [t2g ] ft1ig ] f[t4g = f[t12; [t2; t1i; [t4g.
Thus a possible rst ring step of N is fg; f[t12; [t2; t1i; [t4g; X . 3
In this paper we plan to study the behaviour of ITPNs without
sequentializing the observation. Thus we will use partial order semantics to express true
concurrency and in particular, nonsequential processes [
Processes have been de ned and investigated for classical Petri nets and for
some other net classes like time Petri Nets [
Partial order structures Concurrent runs or executions of an ITPN are usually represented by condition/event nets where all arcs have an arc weight 1.
N 0 = (B; E; G) is a condition/event net if B \ E = ; and G (B E) [ (E B). The places of B are called conditions and the transitions of E are called events.
A causal net is a condition/event net N 0 = (B; E; G) such that { for every b 2 B; j bj 6 1 and jb j 6 1, { G , the transitive closure of G is acyclic, { N 0 is nitly preceded, i.e., for every x 2 B [ E the set fy j (y; x) 2 G g is nite.
Causal nets do not allow any branching at conditions. In a causal net N 0 = (B; E; G), the transitive closure of the ow relation G is acyclic and therefore a partial order. We call it the precedence relation and denote it by . The symbol denotes the re exive and transitive closure of G.
A homomorphism is a mapping that preserves the nature of nodes and the environment of events. A homomorphism is used to connect conditions and events of a causal net to places and transitions of the executed net whose behaviour is observed.
A chain c of a causal net is a set of totally ordered events, i.e., c E and 8e 2 c 8e0 2 c (e0 e) _ (e e0) : It can be seen as a sequence of events that occurred during the run of the system.
A set AC of nodes of a causal net is an antichain if 8x 2 AC 8x0 2 AC (:(x x0) ^ :(x0 x)): An antichain AC is a maximal antichain or a cut if 8x 2= AC the union AC [ fxg is not an antichain.
Note that usually, cuts are considered restricted to conditions or restricted to events. In particular, a cut restricted to conditions is called cut of conditions or B-cut. Note that each B-cut of a process of a classical Petri Net represent a possible marking that may occur during the concurrent execution for some observer. 4
A timed process of an ITPN N will be de ned as a pair (N 0; ) where N 0 is a causal net and a homomorphism which labels the causal net with information from the ITPN N . The set of clock labels is introduced to capture information about time elapsed since a transition is active. It is de ned by
CL = f(t; j) j t 2 T and j 6 lfd(ti)g and P \ CL = ;:
The following set of ring events denoted by F E will label the events:
F E = f[t j t 2 T g [ fti j t 2 T g [ fXg and P \ F E = ;:
Thus in a causal net where conditions are labeled in P [ CL a B-cut is able to represent a time-state (M,h). Note that for any set B0 B the image (B0) de nes a multi-set of labels. 4.1
Inductive de nition Let N = (P; T; v; M0; I) be an ITPN. A timed process of N is constructed along a possible ring step sequence of N , whose length is no, as follows.
We construct successively labeled causal nets i = (Ni0; i) = (Bi; Ei; Gi; i) where i : Bi [ Ei ! (P [ CL) [ F E by induction on i by using three Addprocedures given below for the creation of events. The i th induction step corresponds to the i th ring step of a . We stop if = (N 0; ) = no .
The sets BCL and BP will be the sets of conditions whose postset is currently empty and which are labeled by clock labels and by places respectively.
Base of induction i = 0: 0 = B0 will be a set of conditions with 0 : B0 ! P representing the initial marking such that 8p 2 P j 0 1(p) \ B0j = M0(p). We set E0 = G0 = ;, BP = B0 and BCL = ;.
Hypothesis: Let n > 1. We suppose that 8i < n, i = (Bi; Ei; Gi; i) has been constructed and the current BCL and BP are known.
Induction step i = n: We start by setting Bi = Bi 1; Ei = Ei 1; Gi = Gi 1 and i = i 1. Then i is constructed as follows: a) (Treatment of the rst Endstep of the current globalstep)
For each condition b 2 BCL: - If i(b) = (t; j) for some t with j = lfd(t) then Add b; ti; i . - If i(b) = (t; j) for some t with sfd(t) 6 j < lfd(t) then Add b; ti; i or do nothing. b) (Treatment of the Iteratedstep of the current globalstep) b.1) (Treatment of Start rings )
If there exists a set B0 BP with i(B0) = t for some t 2 T , then Add B0; [t; i .
Repeat b.1) or goto to b.2) . b.2) (Treatment of an Endstep)
For each condition b 2 BCL: - If i(b) = (t; 0) for some t with lfd(t) = 0, then Add b; ti; i . - If i(b) = (t; 0) for some t with sfd(t) = 0 and lfd(t) 6= 0, then Add b; ti; i or do nothing. ( Maximality of the globalstep) Repeat step b) until 8t 2 T : t * (BP )) (i.e. until no start re event is possible) , then go to c). c) (Treatment of a Tickevent )
If BCL 6= ; then Add X; i .
End (If i = no)
The start re event creation Add B0; [t; i : { We add an event e with i(e) = [t: Ei = Ei [ feg . { We add arcs Gi = Gi [ f(b; e)jb 2 B0g. { We add a condition b0 with i(b0) = (t; 0): Bi = Bi [ fb0g; BCL = BCL [ fb0g. { We add an arc Gi = Gi [ (e; b0) and reset BP = BP n B0.
The end re event creation Add b; ti; i : { We add an event e with i(e) = ti: Ei = Ei [ feg . { We add an arc Gi = Gi [ (b; e) and rede ne BCL = BCL n fbg. { For each p 2 t , we add v(t; p) conditions B0 = fb01; ::; b0v(t;p)g with i(b0) = p for all b0 2 B0: Bi = Bi [ B0 and BP = BP [ B0.
{ We add arcs Gi = Gi [ f((e; b0)jb0 2 B0g.
{ We add an event e with i(e) = X: Ei = Ei [ feg. { We add arcs Gi = Gi [ f(b; e)jb 2 BCLg. { For each b 2 BCL, if i(b) = (t; j) for some t and j, then we add a condition b0 with i(b0) = (t; j + 1): Bi = Bi [ fb0g and an arc Gi = Gi [ (e; b0). { We rede ne BCL = e .
We observe that c) happens at each step because of the wellformedness of the executed ITPN. If BCL = ; then a deadlock appeared; otherwise a tick is added. A process construction stops after the creation of some tick event, except for deadlock. Thus global steps are fully included. It is easy to see, that for each i the cut i is a B-cut and represents the time-state Si+1 reached after the execution of the considered ring step sequence of length i, respectively S~n0 1 in the case of a deadlock after n0 global steps. (t1; 0)
8 (t2; 0)
7
We start by proposing an axiomatization by local properties of events as
processes of a classical Petri Nets have been axiomatized, for instance in [
Case 1 : If (e) = [t for some t 2 T then
8p 2 P j 1(p) \ ej = v(p; t) and je j = 1 with (e ) = f(t; 0)g Case 2: If (e) = ti for some t 2 T then j ej = 1 and ( e) = f(t; j)g for some j 2 [sfd(t); lfd(t)] and 8b 2 e (b) 2 P and 8p 2 P j 1(p) \ e j = v(t; p).
Case 3: If (e) = X then 8b 2 e [ e (b) 2 CL and 8b 2 e (b) = (t; j)) for some t and some j < lfd(t) and 8t 2 T 8j 2 [0; d] j 1((t; j)) \ ej = j 1((t; j + 1)) \ e j
These axioms de ne especially local properties of events in the same way as axioms of processes for classical Petri Nets, i.e., they ensure that each event has a correct pre- and postset of conditions with respect to the ring rule. Only the initial cut and the nal one are evoked. It is evident that each event of an inductively de ned process satis es clearly the corresponding axiom.
First let us state the following sentence.
P roposition 1 There are evolutions which are not processes.
Proof. An evolution of the net N of Fig.1 is given in Fig.3. It respects all points of the axiomatic de nition but does not correspond to any ring step sequence of N . We can see in this example that tick event e2 is not global as it should be, and may only occur when neither a start re event nor a must end re event is possible. In particular, e3 and e4 are independent from e2, thus conditions b8 and b9 are also independent from e2 instead of entering it. These axioms also allow in nite evolutions, and we could have added an axiom like [ 6= ; and 8b 2 B 9x 2 b x] to ensure that is nite. But as niteness will be a consequence of the axioms adjoined in the sequel, we omit it here. p1 5
Therefore, with the given axiomatic de nition we are unable to avoid some partial orders that violate important properties like the fact that tick events have to be global and have to form a chain. Let us try to formulate supplementary axioms about non local properties for tick events: Globality axioms: { (a) 8e 8e0 ( (e) = X ^ (e0) = X) ) (e = e0 _ e0 e _ e e0) { (b) 8e 8e0 ( (e) = X ^ (e0) = X ^ e0 e)) ) (8b 2 e e0 b) X 2 X 5 [t2 4 [t1 3
The axiom (a) ensures that all tick events form a chain in the partial order, and (b) that all conditions entering later tick events are necessarily greater than other preceding tick events, thus in particular greater than its potential direct predecessor tick. In particular, for the running example, point (b) makes impossible to creat a "partial" tick event like e2 in Fig.3, as b9 and b8 entering e5 are not comparable to (and not greater than) e2.
Finally global axioms about maximality and concerning the nal cut have to be de ned.
Final cut axioms: { (d) 8t 2 T 9p 2 t j 1(p) \ j < v(p; t) { (e) 8t 2 T 8b ( (b) = (t; lf d(t)) ) jb j = 1) { (f) 8x 2 (x) 2 P _ 9e ( (e) = X ^ 8x (e x ) (x) 2 CL) ^ 8b 2= e ( (b) 2 CL) ) b 6= ;) As by (d) no start re event is possible at the nal cut , availible tokens (P labeled conditions) are maximally used for start re events and thus the obligation of start ring, up to some choice, is satis ed.
By axiom (e) must end re events must occur.
Axiom (f) ensures that either (case 1) all elements in the nal cut are place labeled, which together with (d) means that the process ends by an deadlock; or (case 2) there is a last tick event whose postset are clock labeled conditons in the nal cut and all other clock labeled conditons have a successor; i.e., they enter in an end ring event, or they enter in a tick event which is by axiom (b) the appropriate one and not a later one.
We may conclude that what happens between two tick events is a global step and axioms (d) and (e) together ensure its maximality. Axiom (f) also implies the niteness of the process. Finally the nite cut correspond to the time state reached after the execution of all events of the evolution.
The initial cut and the nal cut are the only sets of nodes evoked in the given axioms; they are just used like constant sets. Thus we have successfully avoided to use second order quanti cation over sets - representing intermediate B-cuts - in all proposed axioms.
As consequence of these observations we obtain the desired result. P roposition 2 Let N be a wellformed ITPN. Then the class of timed evolutions of N which also satisfy the axioms (a) to (f ) is the same as that of timed processes of N de ned inductively.
In this paper we investigate ITPNs in their most general setting, i.e., with
autoconcurrency and with zero duration. In a previous paper their usual maximal
step semantics were introduced [
The goal of the present article is to present their truly concurrent behaviour. Thus rst, timed processes of ITPNs have been de ned inductively along ring step sequences. Then the possibility of de ning these processes in an axiomatic way too are studied. Our rst attempt was to propose local axioms, similar to the way processes of classical Petri Nets are de ned axiomatically, obtaining the so called timed evolutions. Then we stated and illustrated the fact that some timed evolutions do not correspond to any ring step sequence and therefore they cannot be timed processes.
Several supplementary "global" axioms are gradually formulated and discussed. They are a novelty when de ning processes, but the price to pay to capture global timing and ring constraints.
We succeed to give a full axiomatization of timed processes totally compatible with the ring step semantics. 6
My thanks go to Raymond Devillers for his attentive reading of divers versions and a lot of pertinent remarks and suggestions.