=Paper=
{{Paper
|id=Vol-1698/CS&P2016_02_Pelz_Timed-Processes-of-Interval-Timed-Petri-Nets
|storemode=property
|title=Timed Processes of Interval-Timed Petri Nets
|pdfUrl=https://ceur-ws.org/Vol-1698/CS&P2016_02_Pelz_Timed-Processes-of-Interval-Timed-Petri-Nets.pdf
|volume=Vol-1698
|authors=Elisabeth Pelz
|dblpUrl=https://dblp.org/rec/conf/csp/Pelz16
}}
==Timed Processes of Interval-Timed Petri Nets==
https://ceur-ws.org/Vol-1698/CS&P2016_02_Pelz_Timed-Processes-of-Interval-Timed-Petri-Nets.pdf
Timed Processes of Interval-Timed Petri Nets
Elisabeth Pelz
LACL, Université Paris-Est Créteil, France
pelz@u-pec.fr
Abstract. 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 in-
troduce the notion of timed processes for ITPNs inductively. Then we
investigate if the equivalence of inductive and axiomatic process seman-
tics - true for classical Petri nets - could hold for ITPNs too. We will see
that the notions of independence and immediate firing obligation seem to
be antagonistic ones, and that local axioms, adequate to define processes
of classical Petri nets, are not sufficient to caracterize timed Processes of
IITPNs. We propose several original ”global” axioms which reveal to be
an effective solution. Thus we yield finally a full axiomatic definition of
timed processes for ITPNs.
1 Introduction
Petri nets are an algebraic and graphical formalism, proposed by Carl Adam
Petri [9], used to represent complex interactions and activities in a system, they
model situations like synchronisation, sequentiality, concurrency and conflict.
Classical Petri nets do not carry any time information and so they are not
suitable for quantitative analysis of the performance and reliability of systems
with respect to time.
Several time extensions of Petri nets have been proposed in the literature,
[7,10]. In this paper, we consider Interval-Timed Petri Nets (ITPNs) with auto-
concurrency which are a generalisation of Timed Petri Nets. The main feature
of Interval-Timed Petri Nets is that transitions which are enabled need to start
immediately their firing, and the firing lasts some time within an (integer) in-
terval. Thus in the observation the startfiring and the endfiring of a transition
are considered as two distinct events. Furthermore, in the class of ITPNs we
consider here, we allow transitions to take no time (i.e. to have zero duration).
This obligation of immediate firing led to the standard execution of Timed Petri
Nets in (simultanous) maximal steps.
Let us state precisely the concepts which lead to the describtion of the be-
haviour of ITPNs under maximal step semantics, cf. [8]. Each transition has its
own clock. The progress of time is managed by a global clock by means of (dis-
crete) ticks which increment all local clocks. Inbetween two ticks, we must fire as
many transitions as possible, i.e., for a maximal number of enabled transitions
there are startfiring events; but also, we have to endfire every fired transition
which reach its maximal duration (i.e., which must endfire) plus an arbitrary
multiset of fired transitions which may endfire. The maximal multiset of events
which occur between two time ticks is called a global step. In [8] such standard
semantics of ITPNs in terms of firing step sequences are exhaustively defined.
By convention, we only consider ITPNs with zero duration which are well-
formed, as in [8], i.e. where no infinite global step is possible.
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 [11,2]. They are also defined
for time Petri nets [1,13,12] as well as for high level Timed Petri nets (with one-
safe markings) [5]. Processes of classical Petri Nets can be defined by axiomatic
definitions or by inductive ones using firing sequences, as discussed in [4].
Inspired by this approach, we define in this paper timed processes for ITPNs,
inductively using firing step sequences. To our knowledge processes have never
been introduced for this class. Our definitions will be coherent with the approach
in [5], albeit arbitrary markings and auto-concurrency introduce new challenges.
We propose a way to respect also the above quoted concepts of immediate firing
obligation and global tick in the inductive definition.
But when trying to define timed processes axiomatically, some antagonism
appears. Let us remind that the axiomatic definition (for classical Petri Nets)
states local properties which are true for all events in the process, indepen-
dently 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 syn-
chronisation 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 defined 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 first order logic without quantification 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
definitions about Interval-Timed Petri Nets. In Section 3 basic definitions around
partial order structures can be found. Section 4 gives an inductive definition
of timed processes and Section 5 details the discussion and formulation of an
axiomatic one. Section 6 presents some concluding remarks.
2 Some Definitions
Let us start to define classical Petri nets.
Definition 1 Petri Nets
A Petri net is a 3-tuple N = (P, T, v) such that
- P and T are finite 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 |P |.
Let x be a node such that, x ∈ P ∪ T . The preset of x is denoted by • x,
with • x = {y ∈ P ∪ T | v(y, x) > 0}. Similarly, x• denotes the postset of x,
with x• = {y ∈ P ∪ T | v(x, y) > 0}. In the same manner, the preset of a net N
is defined by • N = {x ∈ P ∪ T | • x = ∅}, the postset of a net N is defined by
N • = {x ∈ P ∪ T | x• = ∅}.
Formally, a multiset U of events E is a mapping U : E → N, such that, for
e ∈ E the natural number U (e) is called the multiplicity of e. The multiset U
can be written in the extended set notation U = {eU (e) | e ∈ E and U (e) 6= 0}.
Several time extensions of classical Petri nets have been proposed to integrate
temporal modeling properties, time Petri nets [7], timed Petri nets [10] and causal
time Petri nets [3].
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 firing duration of each transition is
given within an interval. We recall shortly the definitions of [8], which contains
much more details and examples.
Definition 2 Interval-Timed Petri Nets
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 = {t1 , t2 , .., t|T | }.
The time interval associated
with a transition t is given by
I(t) = sfd(t), lfd(t) , where sfd(t) is called the shortest firing duration and
lfd(t) ≥ sfd(t) the longest firing duration.
Only ITPNs are considered whose transitions have a non empty preset and
postset i.e., for each transition t ∈ T holds that | • t| > 0 and |t• | > 0.
In Interval-Timed Petri Nets a marking is not sufficient to describe com-
pletely the state of a net. The state must also include temporal informations.
This is given by a matrix which codes the transitions clocks.
Definition 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 |T | rows and d columns s.t. d = max lfd(ti ) + 1 .
ti ∈T
The value hi,j+1 represents the number of active transitions ti with age j (i.e.
fired 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
Definition 4 Autoconcurrently enabled transitions
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 ∀p ∈ P, n · v(p, t) 6 M (p). If
n = 1 this is the usual definition of (single) enabling.
For each transition the value Ei (M ) tells how many times (at most) transition
ti can be fired autoconcurrently at marking M . Thus Ei (M ) = ni if
∀p ∈ P, (ni · v(p, ti ) 6 M (p) and ∃p ∈ P, (ni + 1) · v(p, ti ) > M (p) .
When transitions may fire, firing starts immediately; this is done by remov-
ing input tokens from the preplaces of the chosen transitions. A startfired tran-
sition t stays active for some time delay in between its associated time interval
sfd(t), lfd(t) , until it may or must endfire by delivering the output tokens to
its postplaces.
Three types of events are distinguished : startfire, endfire and tick events. The
effect of each of these events on the state of an ITPN is given below.
Definition 5 State change rules
Let N be an ITPN and (M, h) its current state.
1. Startfire events : A startfire 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 occur-
rence 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 .
[ti
(M, h) −→ (M 0 , h0 ) with M 0 = M − v(p, ti ) and h0i,1 = hi,1 + 1.
P
p∈ • ti
There may be conflicts 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. Endfire events : An endfire event, denoted by ti i 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 endfire event ti i may occur if
there is an active transition ti with age in [sfd(ti ), lfd(ti )[ . The corresponding
hi,j+1 is then decremented.
ti i
(M, h) −→ (M 0 , h0 ) if
P
hi,j+1 > 1 with
sfd(ti )6j6lfd(ti )
M0 = M + v(ti , p) and h0i,j+1 = hi,j+1 − 1 for some j with hi,j+1 > 0.
P
p∈t•
i
If this new state enables some transitions, one or more startfire events must
then occur, and if endfire 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 startfire
event nor a must endfire event have to occur. The tick event increments the
clocks for all active transitions and models the passing of time.
X
(M, h) −→ (M 0 , h0 ) with M 0 = M and for all(i holds if
hi,j−1 if 1 < j 6 d
Ei (M ) = 0 and hi,lfd(ti )+1 = 0 then h0i,j = .
0 if j = 1
The ITPN N presented in Fig.1. is used as a running example.
[0, 2] p2 [1, 3] p4
t1 t4
p1 2 [1, 2]
5 t5
[1, 1] p3 [0, 0]
t2 t3
Fig. 1: ITPN N
The condition of the occurrence of a tick event ensures that what have oc-
curred 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 firing event which need to occur ”im-
mediately”, means ”before the next tick”. There is no time scale within zero
time. The following definition will precise the notion of global step which hap-
pens in between two ticks and where multisets of startfire and endfire events will
alternate until nothing more need to occur.
We only consider wellformed ITPNs in this article. They ensure to have
always only a finite number of events which appear between two ticks. If there
is no firing 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 neces-
sarily wellformed: they allow infinite global steps where no tick event can follow.
Thus such an infinite global step would be the ”end” of a step firing sequence.
We just like to limite the considerations here to the standard wellformed case.
2.2 Maximal Step Semantics for ITPNs
The executions of wellformed ITPNs with zero duration and autoconcurrency
under maximal step semantics are given by the so called firing step sequence as
defined in [8], where a firing step sequence is an alternating sequence of global-
steps and ticks.
A globalstep is a multiset of firing events of an ITPN in between two tick
events, it consists on two principal multisets, the first one is called Endstep and
the second one is called Iteratedstep. So a firing step is a triplet
(Endstep, Iteratedstep, tick), or a couple (globalstep, tick).
An Endstep at state S contains all endfire events which must occur at S and
an arbitrary multiset of endfire events which may occur at S. At the beginning, at
initial state S0 , it is always empty as no transition has startfired. 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 startfire events (not necessarily maximal) and multisets
of endfire events with zero duration (containing all must endfire ones). The
alternation ends if neither a transition is enabled nor an endfire event with zero
duration must occur, thus the iterated step is maximal and finite. This situation
happens because of the wellformedness.
Thus a firing step sequence σ of length n is given by
globalstep1 X globalstep2 X globalstepn X
σ = S0 −−−−−→ S̃0 −→ S1 −−−−−→ S̃1 −→ S2 · · · Sn−1 −−−−−→ S̃n−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 firing steps.
E xample 1 Consider the ITPN N , one possible initial firing step from its ini-
tial state S0 is given in the sequel.
The first Endstep is necessarily empty (Endstep1 = ∅). Then, suppose that
2
we fire two times t1 and one time t2 , i.e. {[t1 , [t2 } then we choose to endfire t1
at zero duration, i.e. {t1 i}, after that we fire {[t4 }, no further startfire event is
possible now, so a tick event is executed. The first iterated step is the union of
all these multisets :
2 2
Iteratedstep1 = {[t1 , [t2 } ] {t1 i} ] {[t4 } = {[t1 , [t2 , t1 i, [t4 }.
Thus a possible first firing step of N is {}, {[t21 , [t2 , t1 i, [t4 }, X .
3 True concurrent semantics
In this paper we plan to study the behaviour of ITPNs without sequentializ-
ing the observation. Thus we will use partial order semantics to express true
concurrency and in particular, nonsequential processes [6,2,11].
Processes have been defined and investigated for classical Petri nets and for
some other net classes like time Petri Nets [13,1,12]. The only known contri-
bution on process semantics of a timed Petri Net class is [5], but in a context
of high level nets with one-safe markings. Arbitrary markings, zero durations of
events and auto-concurrency give us new challenges. Also, no axiomatic approach
exists until now for time or timed Petri nets.
3.1 Partial order structures
Concurrent runs or executions of an ITPN are usually represented by condi-
tion/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 ∈ B, | • b| 6 1 and |b• | 6 1,
– G∗ , the transitive closure of G is acyclic,
– N 0 is finitly preceded, i.e., for every x ∈ B ∪ E the set {y | (y, x) ∈ G∗ } is
finite.
Causal nets do not allow any branching at conditions. In a causal net N 0 =
(B, E, G), the transitive closure of the flow relation G is acyclic and therefore a
partial order. We call it the precedence relation and denote it by ≺. The symbol
denotes the reflexive 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 be-
haviour is observed.
A chain c of a causal net is a set of totally ordered events, i.e.,
c ⊂ E and ∀e ∈ c ∀e0 ∈ 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
∀x ∈ AC ∀x0 ∈ AC (¬(x ≺ x0 ) ∧ ¬(x0 ≺ x)). An antichain AC is a maximal
antichain or a cut if ∀x ∈ / AC the union AC ∪ {x} 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 Process semantics for ITPNs
A timed process of an ITPN N will be defined 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 defined by
CL = {(t, j) | t ∈ T and j 6 lfd(ti )} and P ∩ CL = ∅.
A clock label (t, j) means that t is active and has age j.
The following set of firing events denoted by FE will label the events:
FE = {[t | t ∈ T } ∪ {ti | t ∈ T } ∪ {X} 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 B 0 ⊆ B the image φ(B 0 )
defines a multi-set of labels.
4.1 Inductive definition
Let N = (P, T, v, M0 , I) be an ITPN. A timed process π of N is constructed
along a possible firing 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 Add-
procedures given below for the creation of events. The i−th induction step cor-
responds to the i−th firing 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
∀p ∈ P |φ0 −1 (p) ∩ B0 | = M0 (p). We set E0 = G0 = ∅, BP = B0 and BCL = ∅.
Hypothesis: Let n > 1. We suppose that ∀i < 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 first Endstep of the current globalstep)
For each condition b ∈ 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 Startfirings)
0 0 •
If there exists
0
a set B ⊆ BP with φi (B ) = t for some t ∈ T , then
Add B , [t, i .
Repeat b.1) or goto to b.2) .
b.2) (Treatment of an Endstep)
For each condition b ∈ 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 ∀t ∈ T : • t * φ(BP )) (i.e. until no startfire event is
possible) , then go to c).
c) (Treatment of a Tickevent)
If BCL 6= ∅ then Add X, i .
End (If i = no )
The three Add-procedures are as follows:
The startfire event creation Add B 0 , [t, i :
– We add an event e with φi (e) = [t: Ei = Ei ∪ {e} .
– We add arcs Gi = Gi ∪ {(b, e)|b ∈ B 0 }.
– We add a condition b0 with φi (b0 ) = (t, 0): Bi = Bi ∪ {b0 }; BCL = BCL ∪ {b0 }.
– We add an arc Gi = Gi ∪ (e, b0 ) and reset BP = BP \ B 0 .
The endfire event creation Add b, ti, i :
– We add an event e with φi (e) = ti: Ei = Ei ∪ {e} .
– We add an arc Gi = Gi ∪ (b, e) and redefine BCL = BCL \ {b}.
– For each p ∈ t• , we add v(t, p) conditions B 0 = {b01 , .., b0v(t,p) } with φi (b0 ) = p
for all b0 ∈ B 0 : Bi = Bi ∪ B 0 and BP = BP ∪ B 0 .
– We add arcs Gi = Gi ∪ {((e, b0 )|b0 ∈ B 0 }.
The tick event creation Add X, i :
– We add an event e with φi (e) = X: Ei = Ei ∪ {e}.
– We add arcs Gi = Gi ∪ {(b, e)|b ∈ BCL }.
– For each b ∈ 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 ∪ {b0 } and an arc Gi = Gi ∪ (e, b0 ).
– We redefine 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 firing step sequence of length i, respectively S̃n0 −1
in the case of a deadlock after n0 global steps.
p1 p2
5
[t1 (t1 , 0) t1 i 9
[t4 (t4 , 0)
3 8 4 5 11
p1 p2
4 10
p1 [t2 (t2 , 0) (t2 , 1) t2 i p3 [t3 (t3 , 0) t3 i p2
3 2 7 12 7 15 8 16 9 17
X
p1 6
(t1 , 1) (t1 , 2)
2 13 18
[t1 (t1 , 0) X
p1 1 6
(t4 , 1) 10
(t4 , 2)
1 14 19
Fig. 2: An arbitrary process of the ITPN N of Fig.1.
We use abreviation as follows: i Denotes condition bi and j denotes event ej .
4.2 Axiomatic definition and how to overcome its limits
We start by proposing an axiomatization by local properties of events as pro-
cesses of a classical Petri Nets have been axiomatized, for instance in [4].
The causal net π = (N 0 , φ) is an timed evolution of N if
φ : B ∪ E → (P ∪ CL) ∪ F E is a homomorphism verifying
– ∀b ∈ B, φ(b) ∈ P ∪ CL and ∀e ∈ E, φ(e) ∈ FE (coherence of labeling).
– • π ⊆ B and ∀p ∈ P, |φ−1 (p) ∩ • π| = M0 (p) (the initial marking).
– For each event e of the causal net N 0 it holds :
• Case 1 : If φ(e) = [t for some t ∈ T then
∗ ∀p ∈ P |φ−1 (p) ∩ • e| = v(p, t) and |e• | = 1 with φ(e• ) = {(t, 0)}
• Case 2: If φ(e) = ti for some t ∈ T then
∗ | • e| = 1 and φ( • e) = {(t, j)} for some j ∈ [sfd(t), lfd(t)] and
∗ ∀b ∈ e• φ(b) ∈ P and ∀p ∈ P |φ−1 (p) ∩ e• | = v(t, p).
• Case 3: If φ(e) = X then
∗ ∀b ∈ • e ∪ e• φ(b) ∈ CL and
∗ ∀b ∈ • e φ(b) = (t, j)) for some t and some j < lfd(t) and
∗ ∀t ∈ T ∀j ∈ [0, d] |φ−1 ((t, j)) ∩ • e| = |φ−1 ((t, j + 1)) ∩ e• |
These axioms define 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 firing rule. Only
the initial cut and the final one are evoked. It is evident that each event of an
inductively defined process satisfies clearly the corresponding axiom.
First let us state the following sentence.
Proposition 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 definition but does not correspond to any firing 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 startfire event nor a must endfire 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 infinite evolutions, and we could have added an axiom like
[π • 6= ∅ and ∀b ∈ B ∃x ∈ π • b ≤ x] to ensure that π is finite. But as finiteness
will be a consequence of the axioms adjoined in the sequel, we omit it here.
p1
5
[t1 (t1 , 0) X (t1 , 1) (t4 , 1)
1 6 2 7 16
p1
4
(t2 , 1) X (t2 , 2)
11 8 17
p1 [t2 (t2 , 0)
3 4 9
X (t1 , 1) (t1 , 2)
5 10 18
p1 p2
2
[t1 (t1 , 0) (t1 , 2) t1 i 13
p1 3 8 12 6
p3 [t4 (t4 , 0)
1 14 7 15
Fig. 3: An evolution which is not a process of running example.
Therefore, with the given axiomatic definition 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) ∀e ∀e0 (φ(e) = X ∧ φ(e0 ) = X) ⇒ (e = e0 ∨ e0 ≺ e ∨ e ≺ e0 )
– (b) ∀e ∀e0 (φ(e) = X ∧ φ(e0 ) = X ∧ e0 ≺ e)) ⇒ (∀b ∈ • e e0 ≺ b)
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 impos-
sible 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 final cut have to
be defined.
Final cut axioms:
– (d) ∀t ∈ T ∃p ∈ • t |φ−1 (p) ∩ π • | < v(p, t)
– (e) ∀t ∈ T ∀b (φ(b) = (t, lf d(t)) ⇒ |b• | = 1)
– (f) ∀x ∈ π • φ(x) ∈ P ∨ ∃e (φ(e) = X ∧ ∀x (e ≺ x ⇒ φ(x) ∈ CL) ∧
/ e• (φ(b) ∈ CL) ⇒ b• 6= ∅)
∀b ∈
As by (d) no startfire event is possible at the final cut π • , availible tokens (P la-
beled conditions) are maximally used for startfire events and thus the obligation
of startfiring, up to some choice, is satisfied.
By axiom (e) must endfire events must occur.
Axiom (f) ensures that either (case 1) all elements in the final 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 final cut π • and all other clock labeled conditons have a successor; i.e., they
enter in an endfiring 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 finiteness of the process. Finally the finite cut correspond to the time state
reached after the execution of all events of the evolution.
The initial cut • π and the final 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 quantification over sets - representing intermediate
B-cuts - in all proposed axioms.
As consequence of these observations we obtain the desired result.
Proposition 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 defined inductively.
5 Conclusion
In this paper we investigate ITPNs in their most general setting, i.e., with auto-
concurrency and with zero duration. In a previous paper their usual maximal
step semantics were introduced [8], in terms of firing step sequences.
The goal of the present article is to present their truly concurrent behaviour.
Thus first, timed processes of ITPNs have been defined inductively along firing
step sequences. Then the possibility of defining these processes in an axiomatic
way too are studied. Our first attempt was to propose local axioms, similar to
the way processes of classical Petri Nets are defined axiomatically, obtaining the
so called timed evolutions. Then we stated and illustrated the fact that some
timed evolutions do not correspond to any firing step sequence and therefore
they cannot be timed processes.
Several supplementary ”global” axioms are gradually formulated and dis-
cussed. They are a novelty when defining processes, but the price to pay to
capture global timing and firing constraints.
We succeed to give a full axiomatization of timed processes totally compatible
with the firing step semantics.
6 Acknowlegment
My thanks go to Raymond Devillers for his attentive reading of divers versions
and a lot of pertinent remarks and suggestions.
References
1. T. Aura and J. Lilius. Time processes for time petri-nets. In Proc. of 18th Inter-
national Conference ICATPN ’97, LNCS, volume 1248, pages 136–155. Springer,
1997.
2. E. Best and C. Fernández. Nonsequential Processes - A Petri Net View, volume 13
of EATCS Monographs on Theoretical Computer Science. Springer, 1988.
3. C. Bui Thanh, H. Klaudel, and F. Pommereau. Petri nets with causal time for
system verification. Electr. Notes Theor. Comput. Sci., 68(5):85–100, 2002.
4. E.Best and R.Devillers. Sequential and concurrent behaviour in petri net theory.
Theoretical Computer Science, 55(1):87–136, 1987.
5. H. Fleischhack and E. Pelz. Hierarchical Timed High Level Nets and their Branch-
ing Processes. In Proc. of 26th International Conference ICATPN’03, LNCS ,
volume 2679, pages 397–416. Springer, 2003.
6. U. Goltz and W. Reisig. The non-sequential behavior of petri nets. Information
and Control, 57(2/3):125–147, 1983.
7. P. Merlin. A Study of the Recoverability of Communication Protocols. PhD thesis,
Irvine, 1974.
8. E. Pelz, A. Kabouche, and L. Popova-Zeugmanm. Interval-timed petri nets with
auto-concurrent semantics and their state equation. In Proc. of International
Workshop on Petri Nets and Software Engineering (PNSE’15), CEUR Workshop,
http://ceur-ws.org/Vol-1372, pages 245–265, 2015.
9. C. A. Petri. Fundamentals of a Theory of Asynchronous Information Flow. In
IFIP Congress, 1962.
10. C. Ramchandani. Analysis of Asynchronous Concurrent Systems by Timed Petri
Nets. Project MAC-TR 120, MIT, February 1974.
11. P. H. Starke. Processes in petri nets. Elektronische Informationsverarbeitung und
Kybernetik, 17(8/9):389–416, 1981.
12. V. Valero Ruiz, D. de Frutos-Escrig, and F. Cuartero. Timed processes of timed
petri nets. In Proc. of 16th International Conference, ICATPN ’95, LNCS, volume
616, pages 490–509. Springer, 1995.
13. J. Winkowski. Algebras of processes of timed petri nets. In Proc. of 5th Inter-
national Conference CONCUR ’94, LNCS, volume 836, pages 194–209. Springer,
1994.