22 XXXX

# Waiting Nets: State Classes and Taxonomy

Loïc Hélouët
University Rennes  Inria  CNRS  IRISA  France
<EMAIL_ADDRESS>Pranay Agrawal
ENS-Paris-Saclay  France
<EMAIL_ADDRESS>
###### Abstract

In time Petri nets (TPNs), time and control are tightly connected: time
measurement for a transition starts only when all resources needed to fire it
are available. Further, upper bounds on duration of enabledness can force
transitions to fire (this is called urgency). For many systems, one wants to
decouple control and time, i.e. start measuring time as soon as a part of the
preset of a transition is filled, and fire it after some delay and when all
needed resources are available. This paper considers an extension of TPN
called waiting nets that dissociates time measurement and control. Their
semantics allows time measurement to start with incomplete presets, and can
ignore urgency when upper bounds of intervals are reached but all resources
needed to fire are not yet available. Firing of a transition is then allowed
as soon as missing resources are available. It is known that extending bounded
TPNs with stopwatches leads to undecidability. Our extension is weaker, and we
show how to compute a finite state class graph for bounded waiting nets,
yielding decidability of reachability and coverability. We then compare
expressiveness of waiting nets with that of other models w.r.t. timed language
equivalence, and show that they are strictly more expressive than TPNs.

###### keywords:

Time, Petri nets, State Classes.

††volume: VVV††issue: II

Waiting Nets: State Classes and Taxonomy

##  1 Introduction

Time Petri nets (TPNs) [26] are an interesting model to specify cyber-physical
systems. They allow for the specification of concurrent or sequential events
(modeled as transitions occurrences), resources, time measurement, and
urgency. In TPNs, time constraints are modeled by attaching an interval
$[\alpha_{t},\beta_{t}]$ to every transition $t$. If $t$ has been enabled for
at least $\alpha_{t}$ time units it can fire. If $t$ has been enabled for
$\beta_{t}$ time units, it is urgent: time cannot elapse, and $t$ must either
fire or be disabled. Urgency is an important feature of TPNs, as it allows for
the modeling of strict deadlines, but gives them a huge expressive power. In
their full generality, TPNs are Turing powerful. A consequence is that most
properties that are decidable for Petri Nets [17] (coverability [29],
reachability [23], boundedness [29]…) are undecidable for TPNs. Yet, for the
class of bounded TPNs, reachability [28] and coverability are decidable. The
decision procedure relies on a symbolic representation of states with state
classes and then on the definition of abstract runs as paths in a so-called
state class graph [7, 22].

There are many variants of Petri nets with time. An example is timed Petri
nets (TaPN) [30], where tokens have an age, and time constraints are attached
to arcs of the net. In TaPNs, a token whose age reaches the upper bound of
constraints becomes useless. The semantics of TaPNs enjoys some monotonicity,
and well-quasi-ordering techniques allow to solve coverability or boundedness
problems [1, 31]. However, reachability of a given marking remains undecidable
for TaPNs [32]. Without any notion of urgency, TaPN cannot model delay
expiration. In [2], a model mixing TaPN and urgency is proposed, with
decidable coverability, even for unbounded nets. We refer readers to [20] for
a survey on TaPNs and their verification, and to [9] for a survey on different
ways to introduce time in Petri nets.

| Reachability | coverability | Boundedness
---|---|---|---
Time Petri Nets | Undecidable [21] | Undecidable [21] | Undecidable [21]
(bounded) | Decidable | Decidable | –
Timed Petri nets | Undecidable [32] | Decidable [18, 1] | Decidable [18]
(bounded) | Decidable | Decidable | –
Restricted Urgency | Undecidable [2] | Decidable [2] | Decidable [2]
(bounded) | Decidable | Decidable | –
Stopwatch Petri nets | Undecidable [8] | Undecidable [8] | Undecidable [8]
(bounded) | Undecidable [8] | Undecidable [8] | –
TPNR | Undecidable [27] | Undecidable [27] | Undecidable [27]
(bounded) | Decidable [27] | Decidable [27] | –
Waiting Nets | Undecidable (Rmk. 3.6) | Undecidable (Rmk. 3.6) | Undecidable (Rmk. 3.6)
(bounded) | PSPACE-Complete (Thm. 4.16) | PSPACE-Complete (Thm. 4.16) | –

Table 1: Decidability and complexity results for time(d) variants of Petri
nets.

Working with bounded models is enough for many cyber-physical systems.
However, bounded TPNs suffer another drawback: time measurement and control
are too tightly connected. In TPNs, time is measured by starting a new clock
for every transition that becomes enabled. By doing so, measuring a duration
for a transition $t$ starts only when all resources needed to fire $t$ are
available. Hence, one cannot stop and restart a clock, nor start measuring
time while waiting for missing resources. To solve this problem, [8] equips
bounded TPNs with stopwatches. Nets are extended with read arcs, and the
understanding of a read arc from a place $p$ to a transition $t$ is that when
$p$ is filled, the clock attached to $t$ is frozen. Extending bounded TPNs
with stopwatches leads to undecidability of coverability, boundedness and
reachability. This is not a surprise, as timed automata with stopwatches are
already a highly undecidable model [11]. For similar reasons, time Petri nets
with preemptable resources [10], where time progress depends on the
availability of resources cannot be formally verified.

This paper considers waiting nets, a new extension of TPN that decouples time
measurement and control. Waiting nets distinguish between enabling of a
transition and enabling of its firing, which allows rules of the form ”start
measuring time for $t$ as soon as $p$ is filled, and fire $t$ within
$[\alpha,\beta]$ time units when $p$ and $q$ are filled”. Syntactically, this
model is a simple extension of TPNs: the model is built by adding a particular
type of control place to TPNs. Waiting nets allow clocks of enabled
transitions to reach their upper bounds, and wait for missing control to fire.
A first contribution of this paper is a formal definition of the semantics of
this new model. An immediate result is that waiting nets are more expressive
than TPNs, as TPNs are a simple syntactic restriction of waiting nets. A
former attempt called Timed Petri nets with Resets (TPNR) distinguishes some
delayable transitions that can fire later than their upper bounds [27]. For
bounded TPNR, reachability and TCTL model checking are decidable. However,
delayable transitions are never urgent, and once delayed can only fire during
a maximal step with another transition fired on time. Further, delayable
transitions start measuring time as soon as their preset is filled, and hence
do not allow decoupling of time and control as in waiting nets.

As a second contribution of this paper, we define state class graphs for
waiting nets. We build on the work of [7] to define domains, i.e. symbolic
representations for the values of clocks that measure time elapsed since
enabling of transitions. We then define a successor relation via transition
firing among domains. This allows for the construction of a state class graph
depicting reachable markings and domains of a waiting net. We show that the
state class graphs of bounded waiting nets are finite, yielding decidability
of reachability and coverability (which are PSPACE-complete). This is a
particularly interesting result, as these properties are undecidable for
stopwatch Petri nets, even in the bounded case. The table 1 summarizes known
decidability results for reachability, coverability and boundedness problems
for time variants of Petri nets, including the new results for waiting nets
proved in this paper. Another interesting result shown in this paper is that a
state class may have more that one successor via a transition. This shows that
state class graphs of waiting nets are not deterministic, and that TPNs and
waiting nets are hence different models.

Our last contribution is a study of the expressiveness of waiting nets w.r.t.
timed language equivalence. We compare the timed languages generated by timed
automata, TPNs, waiting nets. We consider variants of these models with
injective or non-injective labelings, and with $\epsilon-$transitions.
Interestingly, the expressiveness of bounded waiting nets lays between that of
bounded TPNs and timed automata.

This paper is an extended version of an article originally published in [19].
The rest of the paper is organized as follows: we recall the formal background
needed later in the paper in Section 2. We recall in particular definitions of
clock constraints, timed automata and timed languages. We define the syntax
and semantics of waiting nets in Section 3. Section 4 shows a state class
graph construction for waiting nets and proves finiteness of the set of
domains of waiting nets. Finiteness of the obtained state class graph is then
used to show PSPACE completeness of reachability and coverability for bounded
waiting nets. Section 5 compares the expressive power of waiting nets with
that of other models and with other timed variants of Petri nets before
conclusion. For readability, several technical proofs of Section 4 are only
sketched, but are provided in Appendix.

##  2 Preliminaries

We denote by $\mathbb{R}^{\geq 0}$ the set of non-negative real values, and by
$\mathbb{Q}$ the set of rational numbers. A rational interval $[\alpha,\beta]$
is the set of values between a lower bound $\alpha\in\mathbb{Q}$ and an upper
bound $\beta\in\mathbb{Q}$. We also consider intervals without upper bounds of
the form $[\alpha,\infty)$, to define values that are greater than or equal to
$\alpha$.

A clock is a variable $x$ taking values in $\mathbb{R}^{\geq 0}$. A variable
$x_{t}$ will be used to measure the time elapsed since transition $t$ of a net
was last newly enabled. Let $X$ be a set of clocks. A valuation for $X$ is a
map $v:X\to\mathbb{R}^{\geq 0}$ that associates a positive or zero real value
$v(x)$ to every variable $x\in X$. Intervals alone are not sufficient to
define the domains of clock valuations met with TPNs and timed automata. An
atomic constraint on $X$ is an inequality of the form $a\leq x$, $x\leq b$,
$a\leq x-y$ or $x-y\leq b$ where $a,b\in\mathbb{Q}$ and $x,y\in X$. A
constraint is a conjunction of atomic constraints. We denote by $Cons(X)$ the
set of constraints over clocks in $X$. We will say that a valuation $v$
satisfies a constraint $\phi$, and write $v\models\phi$ iff replacing $x$ by
$v(x)$ in $\phi$ yields a tautology. A constraint $\phi$ is satisfiable iff
there exists a valuation $v$ for $X$ such that $v\models\phi$. Constraints
over real-valued variables can be efficiently encoded with Difference Bound
Matrices (DBMs) and their satisfiability checked in $O(n^{3})$ [16]. For
completeness, we give a formal definition of DBMs in Appendix C. We also show
in Appendix B that checking satisfiability of a constraint amounts to
detecting negative cycles in a weighted graph, which can be checked using a
variant of the Floyd-Warshall algorithm. The domain specified by a constraint
$\phi$ is the (possibly infinite) set of valuations that satisfy $\phi$.

Given an alphabet $\Sigma$, a timed word is an element of
$(\Sigma\times\mathbb{R}^{+})^{*}$ of the form
$w=(\sigma_{1},d_{1})(\sigma_{2},d_{2})\dots$ such that $d_{i}\leq d_{i+1}$. A
timed language is a set of timed words. Timed automata [4] are frequently used
to recognize timed languages. In the last section of this paper, we compare
expressiveness of several variants of time(d) Petri nets and timed automata.
For completeness, we recall the definition and semantics of timed automata.

######  Definition 2.1 (Timed Automaton)

A Timed Automaton $\mathcal{A}$ is a tuple
$\mathcal{A}=(L,\ell_{0},X,\Sigma,Inv,E,F)$, where $L$ is a set of locations,
$\ell_{0}\in L$ is the initial location, $X$ is a set of clocks, $\Sigma$ is
an alphabet, $Inv:L\to Cons(X)$ is a map associating an invariant to every
location. The set of states $F\subseteq L$ is a set of final locations, and
$E$ is a set of edges. Every edge is of the form
$(\ell,g,\sigma,R,\ell^{\prime})\in L\times Cons(X)\times\Sigma\times
2^{X}\times L$.

Intuitively, the semantics of a timed automaton allows elapsing time in a
location $\ell$ (in which case clocks valuations grow uniformly) if this does
not result in a valuation that violates $Inv(\ell)$, or firing a discrete
transition $(\ell,g,\sigma,R,\ell^{\prime})$ from location $\ell$ with clock
valuation $v$ if $v$ satisfies guard $g$, and the valuation $v^{\prime}$
obtained by resetting all clocks in $R$ to $0$ satisfies $Inv(\ell^{\prime})$.
One can notice that invariants can prevent firing a transition. Every run of a
timed automaton starts from $(\ell_{0},v_{0})$, where $v_{0}$ is the valuation
that assigns value $0$ to every clock in $X$.

Let $\mathcal{A}=(L,\ell_{0},X,\Sigma,Inv,E,F)$ be a timed automaton. A
configuration of $\mathcal{A}$ is a pair $(\ell,v)$ where $\ell\in L$ is a
location, and $v$ a valuation of clocks in $X$. Let $v_{R:=0}$ denote a
valuation $v^{\prime}$ such that $v^{\prime}(x)=0$ if $x\in R$ and
$v^{\prime}(x)=v(x)$ otherwise. A discrete move via transition
$e=(\ell,g_{e},\sigma_{e},R,\ell^{\prime})$ is allowed from $(\ell,v)$ iff
$v\models g_{e}$ (the guard of the transition is satisfied) and
$v_{R:=0}\models Inv(\ell^{\prime})$. We will denote such moves by
$(\ell,v)\overset{e}{\longrightarrow}(\ell^{\prime},v^{\prime})$. Let
$d\in\mathbb{R}^{+}$, and let $v+d$ denote a valuation such that
$v+d(x)=v(x)+d$ for every $x\in X$. A timed move of $d$ time units is allowed
if $v+d^{\prime}\models Inv(\ell)$ for every real value $d^{\prime}\leq d$. We
will denote such moves by
$(\ell,v)\overset{d}{\longrightarrow}(\ell^{\prime},v+d)$.

A run of $\mathcal{A}$ is a sequence of discrete and timed moves that starts
from configuration $(\ell_{0},v_{0})$, where $v_{0}$ is the valuation that
associates value $0$ to every clock in $X$. A run is accepting if it ends in a
final location. Without loss of generality, we will assume that runs of timed
automata alternate timed and discrete moves (possibly of duration $0$). A run
is hence a sequence of the form
$\rho=(\ell_{0},v_{0})\overset{d_{0}}{\longrightarrow}(\ell,v_{0}+d_{0})\overset{e_{0}}{\longrightarrow}(\ell_{1},v_{1})\dots$,
where each $d_{i}\in\mathbb{R}$ is a duration, and each $e_{i}$ is a
transition. The timed word associated with run $\rho$ is the word
$w_{\rho}=(\sigma_{e_{0}},dt_{0})\dots(\sigma_{e_{i}},dt_{i})\dots$ where
$dt_{i}=\sum_{k=0}^{k=i-1}d_{k}$. The (timed) language recognized by
$\mathcal{A}$ is denoted $\mathcal{L}(\mathcal{A})$, and is the set of timed
words associated with accepting runs of $\mathcal{A}$. The definition of timed
automata can be easily extended to include silent transitions. Timed automata
then contain transitions of the form
$e=(\ell,g_{e},\epsilon,R_{e},\ell^{\prime})$ labeled by an unobservable
letter denoted $\epsilon$, and are hence automata over an alphabet
$\Sigma\cup\epsilon$. In this case, the word recognized along a run $\rho$ is
the projection of $w_{\rho}$ on pairs $(\sigma_{e_{i}},dt_{i})$ such that
$\sigma_{e_{i}}\neq\epsilon$.

In the rest of the paper, we will denote by $TA$ the class of timed automata.
We will be in particular interested by the subclass $TA(\leq,\geq)$ in which
guards are conjunctions of atomic constraints of the form $x\geq c$ and
invariants are conjunctions of atomic constraints of the form $x\leq c$.
Several translations from TPNs to TAs have been proposed (see for instance
[12, 22]). In particular, the solution of [22] uses the state class graph of a
TPN to build a time-bisimilar timed automaton in class $TA(\leq,\geq)$. This
shows that one needs not the whole expressive power of timed automata to
encode timed languages recognized by TPNs.

##  3 Waiting Nets

TPNs are a powerful model: they can be used to encode a two-counter machine
(see for instance [31] for an encoding of counter machines), and can hence
simulate the semantics of many other formal models. A counterpart to this
expressiveness is that most problems (reachability, coverability, boundedness,
verification of temporal logics…) are undecidable. Decidability is easily
recovered when considering the class of bounded TPNs. Indeed, for bounded
TPNs, one can compute a finite symbolic model called a state class graph [7],
in which timing information is symbolically represented by firing domains. For
many applications, working with bounded resources is sufficient. However, TPNs
do not distinguish between places that represent control (the ”state” of a
system), and those that represent resources: transitions are enabled when all
places in their preset are filled. A consequence is that one cannot measure
time spent in a control state, when some resources are missing.

$\bullet$$p_{0}$$\bullet$$p_{1}$$p_{2}$$p_{3}$$p_{4}$$Arrival$$[25,28]$$Order$$[0,\infty]$$Departure$$[30,32]$$\bullet$$p_{0}$$\bullet$$p_{1}$$p_{2}$$p_{3}$$p_{4}$$Arrival$$[25,28]$$Order$$[0,\infty]$$Departure$$[30,32]$$[30,32]$$\bullet$$p_{0}$$\bullet$$p_{1}$$p_{2}$$p_{3}$$p_{4}$$Arrival$$[25,28]$$Order$$[0,\infty]$$Departure$$[30,32]$

Figure 1: A TPN $a)$ a Timed Petri net $b)$, and a Waiting net $c)$

Consider the examples of Figure 1, that are designed to represent an arrival
of a train followed by a departure. The arrival in a station is modeled by
transition $Arrival$, that should occur between $25$ and $28$ minutes after
the beginning of a run. The station is modeled by place $p_{2}$, and the
departure of the train by transition $Departure$. A train can leave a station
only if a departure order has been sent, which is modeled by transition
$Order$. Assume that one wants to implement a scenario of the form ”the train
leaves the station between 30 and 32 minutes after its arrival if it has
received a departure order”.

Consider the TPN of Figure 1-a). The time constraint attached to $Departure$
is an interval of the form $[30,32]$, which is the only way to impose a
precise timing in TPNs. This TPN does not implement our scenario, but rather
behaviors in which the train leaves the station between 30 and 32 minutes
after the instant when it is in station and a departure order is received.
This means that a train may spend $32+d$ minutes in station, if the order is
released $d$ minutes after its arrival. Now, consider the second net in Figure
1-b). It is a timed Petri net, i.e. a variant of nets where tokens are given
an age (the durations that have elapsed since they were created in a place)
and flow relations constrain the age of consumed tokens. In a nutshell, the
semantics of timed Petri nets allow consumption of tokens which age satisfy
the timing constraints of flow relations. Tokens that become too old to
satisfy a constraint are never consumed and can be ignored. In the net of
Figure 1-b), a token can move from place $p_{1}$ to place $p_{3}$ at any time
(i.e. a departure order can be issued at any instant), and a second token can
move from place $p_{0}$ to place $p_{2}$ when its age is between $25$ and $28$
minutes, representing arrival of a train within a delay ranging from 25 to 28
minutes. Following the semantics of timed Petri nets, one can simply ”forget”
the token in place $p_{2}$ if the delay to produce a token in place $p_{3}$
exceeds $28+32$. In other words, in this model, one can forget a train arrived
in station if the departure order arrives more than 32 minutes after its
$Arrival$. This is not the scenario we want to model. Further, there is no
timed Petri net that can specify this example, because timed Petri nets do not
have a notion of urgency, and hence cannot enforce occurrence of an action
after a predetermined delay (in our case a departure of a train at latest
after 32 minutes).

We propose an extension of TPNs called waiting nets (WTPNs for short), that
decouples control and resources during time measurement. We consider two types
of places: standard places, and control places, with the following functions:
Time measurement for a transition $t$ starts as soon as $t$ has enough tokens
in the standard places of its preset. Then, $t$ can fire if its clock value
lays in its timing interval, and if it has enough tokens in the control places
of its preset. To illustrate this extension, consider the example of Figure
1-c). This example is similar to the net of Figure 1-a), but with $p_{3}$
replaced by a control place (symbolized by a dashed circle). Let us detail the
changes brought by control places. Let transition $Arrival$ fire at a date $d$
between $25$ and $28$ minutes, filling place $p_{2}$. This immediately enables
transition $Departure$, that is forced to fire at latest $32$ time units later
if transition $Order$ is fired at a date smaller than $d+32$, or exactly at
the date of firing of transition $Order$ if this transition is fired more than
$32$ minutes after date $d$. This net models a situation where a train can
arrive at date $d\in[25,28]$ minutes, and leave as soon as at least 30 minutes
have elapsed since arrival, and a departure order was given. If the departure
order is received at a date smaller than $d+32$, then the train can leave at
latest at date $d+32$. If the departure order is given at a date
$d^{\prime}>d+32$, then the train leaves at date $d^{\prime}$, i.e. when the
departure order is given. This is exactly the scenario described above. We can
now define waiting nets formally as follows :

###### Definition 3.1

A waiting net is a tuple
$\mathcal{W}\\!=\\!\\!\big{(}P,C,T,{{}^{\bullet}}\\!(),()^{\bullet}\\!,\alpha,\beta,\lambda,(M_{0}.N_{0})\big{)}$,
where

  * •

$P$ is a finite set of standard places, $C$ is finite set of control places,
such that $P\cup C\neq\emptyset$ and $P\cap C=\emptyset$. A marking $M.N$ is a
pair of maps $M:P\to\mathbb{N}$, $N:C\to\mathbb{N}$ that associate an integral
number of tokens respectively to standard and control places.

  * •

$T$ is a finite set of transitions. Every $t\in T$ has a label
$\lambda(t)\in\Sigma\cup\epsilon$,

  * •

${{}^{\bullet}}\\!()\in(\mathbb{N}^{P\cup C})^{T}$ is the backward incidence
function, $()^{\bullet}\in(\mathbb{N}^{P\cup C})^{T}$ is the forward incidence
function,

  * •

$(M_{0}.N_{0})\in\mathbb{N}^{P\cup C}$ is the initial marking of the net,

  * •

$\alpha:T\to\mathbb{Q}^{+}$ and $\beta:T\to\mathbb{Q}^{+}\cup{\infty}$ are
functions giving for each transition respectively its earliest and latest
firing times. For every transition $t$, we have $\alpha(t)\leq\beta(t)$.

The labeling map $\lambda$ is injective if
$\lambda(t)=\lambda(t^{\prime})\Leftrightarrow t=t^{\prime}$, and may allow
labeling transitions with a silent action label denoted $\epsilon$. To
differentiate standard and control places in the preset of a transition, we
will denote by ${{}^{\circ}}\\!(t)$ the restriction of ${{}^{\bullet}}\\!(t)$
to standard places, and by ${{}^{c\>}}\\!()$ the restriction of
${{}^{\bullet}}\\!()$ to control places. We will write $M(p)=k$ (resp.
$N(c)=k$) to denote the fact that standard place $p\in P$ (resp. control place
$c\in C$) contains $k$ tokens. Given two markings $M.N$ and
$M^{\prime}.N^{\prime}$ we will say that $M.N$ is greater than
$M^{\prime}.N^{\prime}$ and write $M.N\geq M^{\prime}.N^{\prime}$ iff $\forall
p\in P,M(p)\geq M^{\prime}(p)$ and $\forall c\in C,N(c)\geq N^{\prime}(C)$.

$\bullet$$p_{0}$$Ad$$[0,\infty]$$p_{1}$$p_{2}$$Cp$$[1,4]$$p_{3}$$So$$[0,3]$$No$$[0,8]$$p_{4}$$p_{5}$$\bullet$$p_{0}$$Ad$$[0,\infty]$$p_{1}$$p_{2}$$Cp$$[1,4]$$p_{3}$$p_{6}$$So$$[0,3]$$No$$[0,8]$$To$$[3,3]$$p_{4}$$p_{5}$$p_{7}$

Figure 2: $a)$ Decoupled time and control in a waiting net. $b)$ … with a
timeout transition.

Figure 2-a) is a waiting net modelling an online sale offer, with limited
duration. Control places are represented with dashed lines. A client receives
an ad, and can then buy a product up to 8 days after reception of the offer,
or wait to receive a coupon offered to frequent buyers to benefit from a
special offer at reduced price. However, this special offer is valid only for
3 days. In this model, a token in control place $p_{3}$ represents a coupon
allowing the special offer. However, time measure for the deal at special
price starts as soon as the ad is sent. Hence, if the coupon is sent 2 days
after the ad, the customer still has 1 day to benefit from this offer. If the
coupon arrives more than 3 days after the ad, he has to use it immediately.
Figure 2-b) enhances this example to model expiration of the coupon after 3
days with a transition. Transition $T_{O}$ consumes urgently a token from
place $p_{6}$ exactly $3$ time units after firing of transition $Ad$ if it is
still enabled, which means that the special offer expires within 3 days, and
coupon arriving later than $3$ days after the add cannot be used.

The semantics of waiting nets associates clocks to transitions, and lets time
elapse if their standard preset is filled. It allows firing of a transition
$t$ if the standard and the control preset of $t$ is filled.

######  Definition 3.2 (Enabled, Fully Enabled, Waiting transitions)

  * $\bullet$

A transition $t$ is enabled in marking $M.N$ iff $M\geq{{}^{\circ}}\\!(t)$
(for every standard place $p$ in the preset of $t$,
$M(p)\geq{{}^{\circ}}\\!(t)(p)$). We denote by $\mathsf{Enabled}(M)$ the set
of transitions which are enabled from marking $M$, i.e.
$\mathsf{Enabled}(M):=\\{t\,|\,M\geq{{}^{\circ}}\\!(t)\\}$.

  * $\bullet$

A transition $t$ is fully enabled in $M.N$ iff, for every place in the preset
of $t$, $M.N(p)\geq{{}^{\bullet}}\\!(t)(p)$. $\mathsf{FullyEnabled}(M.N)$ is
the set of transitions which are fully enabled in marking $M.N$, i.e.
$\mathsf{FullyEnabled}(M.N):=\\{t\,|\,M.N\geq{{}^{\bullet}}\\!(t)\\}$.

  * $\bullet$

A transition $t$ is waiting in $M.N$ iff
$t\in\mathsf{Enabled}(M)\setminus\mathsf{FullyEnabled}(M.N)$ ($t$ is enabled,
but is still waiting for the control part of its preset). We denote by
$\mathsf{Waiting}(M.N)$ the set of waiting transitions.

Obviously, $\mathsf{FullyEnabled}(M.N)\subseteq\mathsf{Enabled}(M)$. For every
enabled transition $t$, there is a clock $x_{t}$ that measures for how long
$t$ has been enabled. For every fully enabled transition $t$, $t$ can fire
when $x_{t}\in[\alpha(t),\beta(t)]$. We adopt an urgent semantics, i.e. when a
transition is fully enabled and $x_{t}=\beta(t)$, then this transition, or
another one enabled at this precise instant has to fire without letting time
elapse. Firing of a transition $t$ from marking $M.N$ consumes tokens from all
places in ${{}^{\bullet}}\\!(t)$ and produces tokens in all places of
$(t)^{\bullet}$. A consequence of this token movement is that some transitions
are disabled, and some other transitions become enabled after firing of $t$.

######  Definition 3.3 (Transition Firing)

Firing of a transition $t$ from marking $M.N$ is done in two steps. The first
step computes an intermediate marking
$M^{\prime\prime}.N^{\prime\prime}=M.N-{{}^{\bullet}}\\!(t)$ obtained by
removing tokens consumed by the transition from its preset. Then, a new
marking
$M^{\prime}.N^{\prime}=M^{\prime\prime}.N^{\prime\prime}+(t)^{\bullet}$ is
computed. We will write $M.N\overset{t}{\longrightarrow}M^{\prime}.N^{\prime}$
whenever firing of $t$ from $M.N$ produces marking $M^{\prime}.N^{\prime}$. A
transition $t_{i}$ is newly enabled after firing of $t$ from $M.N$ iff it is
enabled in $M^{\prime}.N^{\prime}$, and either it is not enabled in
$M^{\prime\prime}.N^{\prime\prime}$, or $t_{i}$ is a new occurrence of $t$. We
denote by $\uparrow\mathsf{enabled}(M.N,t)$ the set of transitions newly
enabled after firing $t$ from marking $M.N$.

$\uparrow\mathsf{enabled}(M.N,t):=\\{t_{i}\in
T\mid{{}^{\bullet}}\\!(t_{i})\leq
M.N-{{}^{\bullet}}\\!(t)+(t)^{\bullet}\land\big{(}(t_{i}=t)\lor({{}^{\bullet}}\\!(t_{i})\geq
M.N-{{}^{\bullet}}\\!(t))\big{)}\\}$

As explained informally with the examples of Figure 2, the semantics of
waiting nets allows transitions firing when some time constraints on the
duration of enabling are met. Hence, a proper notion of state for a waiting
net has to consider both place contents and time elapsed. This is captured by
the notion of configuration. In configurations, time is measured by attaching
a clock to every enabled transition. To simplify notations, we define
valuations of clocks on a set $X_{T}=\\{x_{t}\mid t\in T\\}$ and write
$x_{t}=\bot$ if $t\not\in enabled(M)$. To be consistent, for every value
$r\in\mathbb{R}$, we set $\bot+r:=\bot$.

######  Definition 3.4 (Configuration)

A Configuration of a waiting net is a pair $(M.N,v)$ where $M.N$ is a marking
and $v$ is a valuation of clocks in $X_{T}$. The initial configuration of a
waiting net is a pair $(M_{0}.N_{0},v_{0})$, where $v_{0}(x_{t})=0$ if
$t\in\mathsf{enabled(M_{0})}$ and $v_{0}(x_{t})=\bot$ otherwise. A transition
$t$ is firable from configuration $(M.N,v)$ iff it is fully enabled, and
$v(x_{t})\in[\alpha(t),\beta(t)]$.

Slightly abusing our notation, we will write $v(t)$ instead of $v(x_{t})$. The
semantics of waiting nets is defined in terms of timed or discrete moves from
one configuration to the next one. Timed moves increase the value of clocks
attached to enabled transitions (when time elapsing is allowed) while discrete
moves are transitions firings that reset clocks of newly enabled transitions.
We give the formal operation definition of timed and discrete moves in Figure
3 and then detail these operational rules.

$\begin{array}[]{l}\\\ \forall t\in\mathsf{Waiting}(M.N),\\\ \qquad
v^{\prime}(t)=\min(\beta(t),v(t)+d)\\\ \forall
t\in\mathsf{FullyEnabled}(M.N),\\\ \qquad v(t)+d\leq\beta(t)\\\ \hskip
28.45274pt\mbox{~{}and~{}}v^{\prime}(t)=v(t)+d\\\ \forall t\in
T\setminus\mathsf{Enabled}(M),v^{\prime}(t)=\bot\\\
\hline\cr\qquad(M.N,v)\overset{d}{\longrightarrow}(M.N,v^{\prime})\end{array}$

$\begin{array}[]{c}M.N\geq{{}^{\bullet}}\\!(t)\\\
M^{\prime}.N^{\prime}=M.N-{{}^{\bullet}}\\!(t)+(t)^{\bullet}\\\ \alpha(t)\leq
v(t)\leq\beta(t)\\\ \forall t_{i}\in
T,v^{\prime}(t_{i})=\left\\{\begin{array}[]{l}0\mbox{~{}if~{}}t_{i}\in\uparrow\mathsf{enabled}(M.N,t)\\\
\bot\mbox{~{}if~{}}t_{i}\not\in\mathsf{enabled}(M)\\\
v(t_{i})\mbox{~{}otherwise}\end{array}\right.\\\
\hline\cr(M.N,v)\overset{t}{\longrightarrow}(M^{\prime}.N^{\prime},v^{\prime})\end{array}$

Figure 3: Operational semantics of Waiting Nets

A timed move from a configuration $(M.N,v)$ lets $d\in\mathbb{R}^{\geq 0}$
time units elapse, but leaves the marking unchanged. We adopt an urgent
semantics that considers differently fully enabled transitions and waiting
transitions. First of all, elapsing of $d$ time units from $(M.N,v)$ is
allowed only if, for every fully enabled transition $t$, $v(t)+d\leq\beta(t)$.
If $v(t)+d>\beta(t)$ then $t$ becomes urgent before $d$ time units, and
letting a duration $d$ elapse from $(M.N,v)$ is forbidden. If we already have
$v(t)=\beta(t)$, then no timed move is allowed, and firing of $t$ is urgent:
$t$ has to be fired or disabled by the firing of another transition before
elapsing time. On the other hand, if elapsing $d$ time units does not violate
urgency of any fully enabled transition, the new valuation for the clock
$x_{t}$ attached to a fully enabled transition after elapsing $d$ time units
is $v^{\prime}(t)=v(t)+d$. Urgency does not apply to waiting transitions,
which can let an arbitrary amount of time elapse when at least one control
place in their preset is not filled. Now, as we model the fact that an event
has been enabled for a sufficient duration, we let the value of clocks
attached to waiting transitions increase up to the upper bound allowed by
their time interval, and then freeze these clocks. So, for a waiting
transition, we have $v^{\prime}(t)=\min(\beta(t),v(t)+d)$. We will write
$v\oplus d$ to denote the valuation of clocks reached after elapsing $d$ time
units from valuation $v$. A timed move of duration $d$ from configuration
$(M.N,v)$ to $(M.N,v^{\prime})$ is denoted
$(M.N,v)\overset{d}{\longrightarrow}(M.N,v^{\prime})$. As one can expect,
waiting nets enjoy time additivity (i.e.
$(M.N,v)\overset{d_{1}}{\longrightarrow}(M.N,v_{1})\overset{d_{2}}{\longrightarrow}(M.N,v_{2})$
implies that $(M.N,v)\overset{d_{1}+d_{2}}{\longrightarrow}(M.N,v_{2})$, and
continuity, i.e. if $(M.N,v)\overset{d}{\longrightarrow}(M.N,v^{\prime})$,
then for every $d^{\prime}<d$
$(M.N,v)\overset{d^{\prime}}{\longrightarrow}(M.N,v^{\prime\prime})$.

A discrete move fires a fully enabled transition $t$ whose clock $x_{t}$ meets
the time constraint of $t$ (i.e., $\alpha(t)\leq x_{t}\leq\beta[t]$), and
resets clocks attached to transitions newly enabled by token moves. A discrete
move relation from configuration $(M.N,v)$ to
$(M^{\prime}.N^{\prime},v^{\prime})$ via transition
$t_{i}\in\mathsf{FullyEnabled}(M.N)$ is denoted
$(M.N,v)\overset{t_{i}}{\longrightarrow}(M^{\prime}.N^{\prime},v^{\prime})$.
Overall, the semantics of a waiting net $\mathcal{W}$ is a timed transition
system (TTS) with initial state $q_{0}=(M_{0}.N_{0},v_{0})$ and which
transition relation follows the time and discrete move semantics rules.

###### Definition 3.5

A run of a waiting net $\mathcal{W}$ from a configuration $(M.N,v)$ is a
sequence

$\rho=(M.N,v)\overset{e_{1}}{\longrightarrow}(M_{1}.N_{1},v_{1})\overset{e_{2}}{\longrightarrow}(M_{2}.N_{2},v_{2})\cdots\overset{e_{k}}{\longrightarrow}(M_{k}.N_{k},v_{k})$

where every $e_{i}$ is either a duration $d_{i}\in\mathbb{R}^{\geq 0}$, or a
transition $t_{i}\in T$, and every
$(M_{i-1}.N_{i-1},v_{i-1})\overset{e_{i}}{\longrightarrow}(M_{i}.N_{i},v_{i})$
is a legal move of $\mathcal{W}$.

We denote by $\mathsf{Runs(\mathcal{W})}$ the set of runs of $\mathcal{W}$
starting from $(M_{0}.N_{0},v_{0})$. A marking $M.N$ is reachable iff there
exists a run from $(M_{0}.N_{0},v_{0})$ to a configuration $(M.N,v)$ for some
$v$. $M.N$ is coverable iff there exists a reachable marking
$M^{\prime}.N^{\prime}\geq M.N$. We will say that a waiting net is bounded iff
there exists an integer $K$ such that, for every reachable marking $M.N$ and
every place $p\in P$ and $p^{\prime}\in C$, we have $M(p)\leq K$ and
$N(p^{\prime})\leq K$. Given two markings $M_{0}.N_{0}$ and $M.N$ the
reachability problem asks whether $M.N$ is reachable from
$(M_{0}.N_{0},v_{0})$, and the coverability problem whether there exists a
marking $M^{\prime}.N^{\prime}\geq M.N$ reachable from $(M_{0}.N_{0},v_{0})$.

###### Remark 3.6

A waiting net with an empty set of control places is a TPN. Hence, waiting
nets inherit all undecidability results of TPNs: reachability, coverability
and boundeness [21] are undecidable in general for unbounded waiting nets.

Given a run
$\rho=(M_{0}.N_{0},v_{0})\overset{e_{1}}{\longrightarrow}(M_{1}.N_{1},v_{1})\overset{e_{2}}{\longrightarrow}(M_{2}.N_{2},v_{2})\cdots$,
the timed word associated with $\rho$ is the word
$w_{\rho}=(t_{1},d_{1})\cdot(t_{2},d_{2})\cdots$ where the sequence
$t_{1}\cdot t_{2}\dots$ is the projection of $e_{1}\cdot e_{2}\cdots$ on $T$,
and for every $(t_{i},d_{i})$ such that $t_{i}$ appears on move
$(M_{k-1}.N_{k-1},v_{k-1})\overset{e_{k}}{\longrightarrow}(M_{k}.N_{k},v_{k})$,
$d_{i}$ is the sum of all durations in $e_{1}\dots e_{k-1}$. The sequence
$t_{1}.t_{2}\dots$ is called the untiming of $w_{\rho}$. The timed language of
a waiting net is the set of timed words
$\mathcal{L}(\mathcal{W})=\\{w_{\rho}\mid\rho\in\mathsf{Runs(\mathcal{W})}\\}$.
Notice that unlike in timed automata and unlike in the models proposed in [6],
we do not define accepting conditions for runs or timed words, and hence
consider that the timed language of a net is prefix closed. The untimed
language of a waiting net $\mathcal{W}$ is the language
$\mathcal{L}^{U}(\mathcal{W})=\\{w\in T^{*}\mid\exists
w_{\rho}\in\mathcal{L}(\mathcal{W}),w\mbox{~{}is the untiming
of~{}}w_{\rho}\\}$. These definitions can be adapted the obvious way to
consider labels of transitions instead of transition themselves (i.e. timed
words are sequences of pairs of the form $(\lambda(t_{i}),d_{i})$ , and
labeling of transitions by $\epsilon$. To simplify notations, we will consider
runs alternating timed and discrete moves. This results in no loss of
generality, since durations of consecutive timed moves can be summed up, and a
sequence of two discrete move can be seen as a sequence of transitions with 0
delays between discrete moves. In the rest of the paper, we will write
$(M.N,v)\overset{(d,t)}{\longrightarrow}(M^{\prime}.N^{\prime},v^{\prime})$ to
denote the sequence of moves $(M.N,v)\overset{d}{\longrightarrow}(M.N,v\oplus
d)\overset{t}{\longrightarrow}(M^{\prime}.N^{\prime},v^{\prime})$.

Let us illustrate the semantics of waiting nets with the example in Figure
2-a). In this net, we have $P=\\{p_{0},p_{1},p_{2},p_{4},p_{5}\\}$,
$C=\\{p_{3}\\}$, $T=\\{Ad,No,So,Cp\\}$, $\alpha(Ad)=\alpha(No)=\alpha(So)=0$,
$\alpha(Cp)=1$, $\beta(Ad)=\infty$, $\beta(No)=8$, $\beta(So)=3$,
$\beta(Cp)=4$. We also have ${{}^{\circ}}\\!(So)=p_{1}$ and
${{}^{c\>}}\\!(So)=p_{3}$, $(So)^{\bullet}=p_{4}$ (we let the reader infer
${{}^{\bullet}}\\!()$ and $()^{\bullet}$ for other transitions). For
conciseness, we will denote by $\\{p_{i},p_{j},..\\}.\\{p_{k},p_{r},...\\}$ a
marking where standard places $p_{i},p_{j},...$ and control places
$p_{k},p_{r},...$ are marked. The net starts in an initial configuration
$(M_{0}.N_{0},v_{0})$ where $M_{0}.N_{0}=\\{p_{0}\\}.\\{\\}$, $v_{0}(Ad)=0$
and $v_{0}(t)=\bot$ for all other transitions in $T$.

A possible run of the net of Figure 2-a) is :

$(\\{p_{0}\\}.\\{\\},v_{0})\overset{(d_{0},Ad)}{\longrightarrow}(\\{p_{1},p_{2}\\}.\\{\\},v_{1})\overset{(2,Cp)}{\longrightarrow}(\\{p_{1}\\}.\\{p_{3}\\},v_{2})\overset{(1,No)}{\longrightarrow}(\\{p_{5}\\}.\\{p_{3}\\},v_{3})$

where $d_{0}$ is any arbitrary positive real value $v_{1}(ad)=\bot$ and
$v_{1}(No)=v_{1}(So)=v_{1}(Cp)=0$, $v_{2}(ad)=v_{2}(Cp)=\bot$ and
$v_{2}(No)=v_{2}(So)=2$. This run represents a situation where a advertisement
is sent at some date $d$, a coupon 2 days later, and the customer decides to
take the normal offer. Another possible run is :

$(\\{p_{0}\\}.\\{\\},v_{0})\overset{(d_{0},Ad)}{\longrightarrow}(\\{p_{1},p_{2}\\}.\\{\\},v_{1})\overset{(3,Cp)}{\longrightarrow}(\\{p_{1}\\}.\\{p_{3}\\},v^{\prime}_{2})\overset{(1,So)}{\longrightarrow}(\\{p_{4}\\}.\\{\\},v^{\prime}_{3})$

with $v^{\prime}_{2}(ad)=v^{\prime}_{2}(Cp)=\bot$ and
$v^{\prime}_{2}(No)=v^{\prime}_{2}(So)=3$. This run represents a scenario
where a customer decides to use the coupon sent. Notice that from
$(\\{p_{1}\\}.\\{p_{3}\\},v^{\prime}_{2})$, time cannot elapse, because
transition $So$ is fully enabled, $v^{\prime}_{2}(So)=3$, and $\beta(So)=3$.
Notice also that firing of $So$ can only occur after firing of $Cp$, but yet
time measurement starts for $So$ as soon as ${{}^{\circ}}\\!(So)=\\{p_{1}\\}$
is filled, i.e. immediately after firing of $Ad$. This example is rather
simple: the net is acyclic, and each transition is enabled/disabled only once.
One can rapidly see that the only markings reachable are
$M_{0}.N_{0}=\\{p_{0}\\}.\\{\\}$, $M_{1}.N_{0}=\\{p_{1},p_{2}\\}.\\{\\}$,
$M_{2}.N_{2}=\\{p_{1}\\}.\\{p_{3}\\}$, $M_{3}.N_{3}=\\{p_{5}\\}.\\{p_{3}\\}$
and $M^{\prime}_{3}.N^{\prime}_{3}=\\{p_{4}\\}.\\{\\}$ visited in the runs
above, and two additional markings $M_{4}.N_{4}=\\{p_{2},p_{5}\\}.\\{\\}$
(reached when transition $No$ is fired before transition $Cp$ and
$M_{5}.N_{5}=\\{p_{5}\\}.\\{p_{3}\\}$ reachable immediately from $M_{4}.N_{4}$
by firing $Cp$. A normal order can be sent at most 8 time units after
advertising, a special order must be sent at most 3 time units after
advertising if a coupon was received, etc.

##  4 Reachability

In a configuration $(M.N,v)$ of a waiting net $\mathcal{W}$, $v$ assigns real
values to clocks. The timed transition system giving the semantics of a
waiting net is hence in general infinite, even when $\mathcal{W}$ is bounded.
In timed automata, clock valuations can be partitioned into equivalence
classes called regions [4] to get a finite abstraction. For TPNs, these
equivalence classes are called domains, and can be used to define an untimed
transition systems called a state class graph [7], that recognizes firable
sequences of transitions. In this section, we build similar graphs for waiting
nets. We also prove that the set of domains in these graphs is always finite,
and use this result to show that reachability and coverability are decidable
for bounded waiting nets. The type of domain built for waiting nets is
identical to that of TPNs, and the construction of successors is based on the
same operations, namely verification of the emptiness of domains, variable
substitution, variable elimination, and calculus of a normal form. The main
change is that one has to consider time elapsed when computing a successor
domain to take into account waiting transitions that have reached their upper
bound. A consequence is that a domain can have several successors via the same
transition firing. Yet, verification of coverability and reachability remain
similar to that of TPNs, i.e. yield an exponential time complexity w.r.t. the
number of transitions.

Let $t_{i}$ be a fully enabled transition with $\alpha(t_{i})=3$ and
$\beta(t_{i})=12$, and assume that $t_{i}$ has been enabled for $1.6$ time
units. According to the semantics of WPNs, $v(t_{i})=1.6$, and $t_{i}$ cannot
fire yet, as $x_{t_{i}}<\alpha(t_{i})$. Transition $t_{i}$ can fire only after
a certain duration $\theta_{i}$ such that $1.4\leq\theta_{i}\leq 10.4$.
Similar constraints hold for all enabled transitions. We will show later that
they are not only upper and lower bounds on $\theta_{i}$’s of the form
$a_{i}\leq\theta_{i}\leq b_{i}$, but can include dependencies of the form
$\theta_{i}-\theta_{j}\leq c_{ij}$ on pairs of variables. These constraints
form a domain of legal real values defining the time that can elapse before
firing an enabled transition or reaching the upper bound of the interval
attached to it.

######  Definition 4.1 (State Class, Domain)

A state class of a waiting net $\mathcal{W}$ is a pair $(M.N,D)$, where $M.N$
is a marking of $\mathcal{W}$ and $D$ is a set of inequalities called firing
domain. The inequalities in $D$ are of two types:

$\begin{cases}a_{i}\leq\theta_{i}\leq b_{i},&\text{ where
}a_{i},b_{i}\in\mathbb{Q}^{+}\text{ and }t_{i}\in\mathsf{Enabled}(M)\\\
\theta_{j}-\theta_{k}\leq c_{jk}.&\text{ where }c_{jk}\in\mathbb{Q}\text{ and
}t_{j},t_{k}\in\mathsf{Enabled}(M).\end{cases}$

A variable $\theta_{i}$ in a firing domain $D$ over variables
$\theta_{1},\dots,\theta_{m}$ represents the time that can elapse before
firing transition $t_{i}$ if $t_{i}$ is fully enabled, and the time that can
elapse before the clock attached to $t_{i}$ reaches the upper bound
$\beta(t_{i})$ if $t_{i}$ is waiting. Hence, if a transition is fully enabled,
and $a_{i}\leq\theta_{i}\leq b_{i}$, then $t_{i}$ cannot fire before $a_{i}$
time units, and cannot let more than $b_{i}$ time units elapse, because it
becomes urgent and has to fire or be disabled before $b_{i}$ time units.
Inequalities in $D$ define an infinite set of possible values for
$\theta_{i}^{\prime}s$. We denote by $\llbracket D\rrbracket$ the set of
solutions for a firing domain $D$. Domains give upper and lower bounds on
$\theta_{i}^{\prime}s$ with inequalities of the form $a_{i}\leq\theta_{i}\leq
b_{i}$, but also contain diagonal constraint of the form
$\theta^{\prime}_{j}-\theta^{\prime}_{k}\leq c_{jk}$. These constraints appear
when two transitions $t_{i},t_{j}$ are enabled in a state class, and one has
to add inequalities of the form $\theta_{i}\leq\theta_{j}$ to check firability
of $t_{i}$. We will say that $t_{i}$ is firable from $(M.N,D)$ if there exists
$v\in\llbracket D\rrbracket$ such that
$(M.N,v)\overset{t_{i}}{\longrightarrow}(M^{\prime}.N^{\prime},v^{\prime})$.
We will say that $(M^{\prime}.N^{\prime},D^{\prime})$ is a successor of
$(M.N,D)$ via transition $t_{i}$ iff $t_{i}$ is firable from $(M.N,D)$ and
$D^{\prime}$ is a domain describing the set of values for
$\theta_{k}^{\prime}s$ that are reachable when elapsing time and firing
$t_{i}$ from a valuation in $D$. The initial state class for a waiting net is
the state class $(M_{0}.N_{0},D_{0})$ where $M_{0}.N_{0}$ is the usual initial
marking of a waiting net, and $D_{0}$ is the domain

$D_{0}=\\{\alpha(t_{i})\leq\theta_{i}\leq\beta(t_{i})\mid
t_{i}\in\mathsf{enabled}(M_{0})\\}$

The main reason to work with domains is to abstract time and bring back
decidability issues for reachability or coverability on an infinite timed
transition system to a similar problem on a finite untimed structure. This
calls for three properties of the abstraction: first, one has to be able to
compute effectively a successor relation $\mathsf{Succ()}$ among state
classes. Second, the closure $\mathsf{Succ^{*}(M_{0}.N_{0},D_{0})}$ of the
initial state class through this successor relation has to be finite. Last,
the construction has to be sound and complete. These three properties hold for
time Petri nets [25, 7]. In the rest of this paper, we will show that a sound,
complete and effective construction of state class graphs for waiting nets
exists, but that it slightly differs from existing constructions defined for
TPNs.

The way to define a set of solutions $\llbracket D\rrbracket$ is not unique.
We will say that $D_{1}$, $D_{2}$ are equivalent, denoted $D_{1}\equiv D_{2}$
iff $\llbracket D_{1}\rrbracket=\llbracket D_{2}\rrbracket$. A set of
solutions $\llbracket D\rrbracket$ is hence not uniquely defined, but
fortunately, a unique representation called a canonical form exists [24].

######  Definition 4.2 (Canonical Form)

The canonical form of a firing domain $D$ is the unique domain

$D^{*}=\left\\{\begin{array}[]{l}a_{i}^{*}\leq\theta_{i}\leq b_{i}^{*}\\\
\theta_{j}-\theta_{k}\leq c_{jk}^{*}\end{array}\right.$

where $a^{*}_{i}=Inf(\theta_{i})$, $b^{*}_{i}=Sup(\theta_{i})$, and
$c^{*}_{jk}=Sup(\theta_{j}-\theta_{k})$

The canonical form $D^{*}$ is the minimal set of constraints defining the set
of solutions $\llbracket D\rrbracket$. If two sets of constraints are
equivalent then they have the same canonical form. The constraints we consider
are of the form $a_{i}\leq\theta_{i}\leq b_{i}$ and $\theta_{i}-\theta_{j}\leq
c_{ij}$, where $a_{i},b_{i},c_{ij}$ are rational values. This type of
constraint can be easily encoded by Difference Bound Matrices [16], or by
constraint graphs (i.e., graphs where vertices represent variables or the
value 0, and an edge from $\theta_{i}$ to $\theta_{j}$ of weight $w_{x,y}$
represents the fact that $\theta_{i}-\theta_{j}\leq w_{x,y}$). The canonical
form for a domain is obtained as a closure operation, that amounts to
computing the shortest paths for each pair $\theta_{i},\theta_{j}$ in the
constraint graph. This can be achieved using the Floyd-Warshall algorithm, in
$O(n^{3})$, where $n$ is the number of variables in the domain. We refer
interested readers to [5] for a survey on operations on constraints, specified
using DBMs. Note that the set of constraints in a domain $D$ may not be
satisfiable, i.e. $\llbracket D\rrbracket$ can be empty. In particular, for
TPNs and waiting nets, unsatisfiable domains may appear when checking whether
a particular transition can be the first one to fire in a domain $D$.
Satisfiability of a domain is decidable, and amounts to checking existence of
negative cycles in the constraint graph of $D$, wich can again be achieved in
polynomial time with Floyd-Warshall.

$\bullet$$p_{0}$$\bullet$$c_{0}$$\bullet$$p_{1}$$p_{2}$$p_{3}$$t_{0}$$[2,3]$$t_{1}$$[4,5]$$D_{0}=\left\\{\begin{array}[]{l}2\leq\theta_{0}\leq
3\\\ 4\leq\theta_{1}\leq 5\\\
\end{array}\right.$$\begin{array}[]{l|ccc}&0&\theta_{0}&\theta_{1}\\\
\hline\cr 0&(\leq,0)&(\leq,-2)&(\leq,-4)\\\
\theta_{0}&(\leq,3)&(\leq,0)&(\leq,\infty)\\\
\theta_{1}&(\leq,5)&(\leq,\infty)&(\leq,0)\\\
\end{array}$$0$$\theta_{0}$$\theta_{1}$$-2$$3$$-4$$5$$0$

Figure 4: A Waiting net, its initial domain, an equivalent DBM representation,
and its constraint graph.

Consider for instance the example of Figure 4. This simple waiting net has two
enabled transitions in its initial marking
$M_{0}.N_{0}=\\{p_{0},p_{1}\\}.\\{c_{0}\\}$, and its initial domain is the
pair of inequalities $D_{0}$ represented in the Figure. These constraint can
alternatively be represented by a DBM (also shown in the Figure), or a
constraint graph ( restricted to plain edges) represented on the left of the
Figure. Clearly, $D_{0}$ has a solution. For instance
$\theta_{0}=2.2,\theta_{1}=4.5$ is a solution for the system of inequalities
in $D_{0}$. Let us test if transition $t_{1}$ can fire before $t_{0}$. This
amounts to adding the constraint $\theta_{1}\leq\theta_{0}$ to domain $D_{0}$,
or equivalently the dashed edge with weight 0 in the constraint graph. As
expected, $D_{0}\cup\\{\theta_{1}\leq\theta_{0}\\}$ is not satisfiable, and
one can verify that adding the dashed edge creates a negative cycle in the
constraint graph.

Syntactically, state classes, domains and their canonical forms are identical
for TPNs and waiting nets. Indeed, the fact that a transition is waiting or
fully enabled does not affect the representation of constraints, as each
$\theta_{i}$ represents a time remaining until the upper bound $\beta(t_{i})$
is reached by clock $x_{t_{i}}$. However, there is a major difference in the
construction of successors for state classes of TPNs and those of waiting
nets. In TPNs, the maximal duration that can elapse in a state class is
constrained by all enabled transitions. For waiting nets, the maximal duration
that can elapse in a state class is constrained by fully enabled transitions
only: elapsing $\delta$ time units before firing some transition $t_{i}$ can
be allowed even if a waiting transition $t_{j}$ reaches its upper bound after
$\delta^{\prime}<\delta$ time units, because variable $\theta_{j}$ represents
a time to upper bound of interval $[\alpha(t_{j}),\beta(t_{j})]$ rather than a
time to fire. On the other hand, when elapsing time, one has to consider which
clocks attached to waiting transitions have reached their upper bound. A
consequence is that a state class has several successors via the same
transition, and hence state class graphs of waiting nets are not
deterministic.

In state classes of TPNs, verifying that $t_{i}$ can fire from $(M.N,D)$ is
checked by verifying that
$D^{+\theta_{i}}::=D\cup\\{\theta_{i}\leq\theta_{j}\mid
t_{j}\in\mathsf{Enabled}(M.N)\\}$ is satisfiable. Intuitively, satisfiability
of $D^{+\theta_{i}}$ means that it is possible to fire $t_{i}$ witout
violating urgency of other transitions. Following the semantics of section 3,
a transition $t_{i}$ can fire from a configuration $(M.N,v)$ iff it is fully
enabled and $v(t_{i})\in[\alpha(t_{i}),\beta(t_{i})]$. Hence, from
configuration $(M.N,v)$, firing of $t_{i}$ is one of the next discrete moves
iff there exists a duration $\theta_{i}$ such that $t_{i}$ can fire from
$(M.N,v+\theta_{i})$, i.e., after letting duration $\theta_{i}$ elapse, and no
other transition becomes urgent before $\theta_{i}$ time units. One can check
firability of a transition $t_{i}$ as in TPNs through satisfiability of
$D^{+\theta_{i}}$, but considering only fully enabled transitions. Note
however that if there is a waiting transition $t_{j}$, $D$ contains a pair of
constraints of the form $\theta_{j}\leq b_{j}$, and $\theta_{i}-\theta_{j}\leq
0$, then the constraint on $\theta_{j}$ may over-constrain the possible values
for $\theta_{i}$. To avoid any conflict between fully enabled transitions and
waiting transitions, we define a notion of projection of a domain on its fully
enabled transitions, that erases all upper bounds of waiting transitions, and
diagonal constraints involving variables associated with waiting transitions.

######  Definition 4.3 (Projection)

Let $D$ be a firing domain with variables $a_{i},b_{i},c_{jk}$ set as in def.
4.1. The projection of $D$ on its fully enabled transitions is a domain

$\begin{array}[]{lcll}&&\\{a_{i}\leq\theta_{i}\leq b_{i}\mid
t_{i}\in\mathsf{FullyEnabled}(M.N)\\}\\\
D_{|full}=&\cup&\\{a_{i}\leq\theta_{i}\leq\infty,\mid
t_{i}\in\mathsf{Waiting}(M.N)\\}\\\ &\cup&\\{\theta_{j}-\theta_{k}\leq
c_{jk}\in D\mid t_{j},t_{k}\in\mathsf{FullyEnabled}(M.N)\\}.\end{array}$

In waiting nets, $t_{i}$ is firable from a state class $(M.N,D)$ iff
$M.N\geq{{}^{\bullet}}\\!(t_{i})$ and
$D_{|full}\cup\\{\theta_{i}\leq\theta_{j}\mid
t_{j}\in\mathsf{FullyEnabled}(M.N)\\}$ is satisfiable, i.e. there exists a
value for $\theta_{i}$ and for every $\theta_{j}$ attached to a fully enabled
transition $t_{j}$ that does not violate the constraint that $\theta_{j}$ is
greater than or equal to $\theta_{i}$ and does not exceed the upper bound
$b_{j}$ appearing in $D$.

The construction of the set of reachable state classes of a waiting net is an
inductive procedure. Originally, a waiting net starts in a configuration
$(M_{0}.N_{0},v_{0})$, so the initial state class of our system is
$(M_{0},D_{0})$, where
$D_{0}=\\{\alpha(t_{i})\leq\theta_{i}\leq\beta(t_{i})\mid
t_{i}\in\mathsf{Enabled}(M_{0}.N_{0})\\}$. Then, for every state class
$(M.N,D)$, and every transition $t$ firable from $(M.N,D)$, we compute all
possible successors $(M^{\prime}.N^{\prime},D^{\prime})$ reachable after
firing of $t$. Note that we only need to consider
$t\in\mathsf{FullyEnabled}(M.N)$, as $t$ can fire only when
$N>{{}^{c\>}}\\!(t)$. Computing $M^{\prime}.N^{\prime}$ follows the usual
firing rule of a Petri net:
$M^{\prime}.N^{\prime}=M.N-{{}^{\bullet}}\\!(t)+(t)^{\bullet}$ and we can
hence also compute $\uparrow\mathsf{enabled}(M.N,t)$,
$\mathsf{enabled}(M^{\prime}.N^{\prime})$ and
$\mathsf{FullyEnabled}(M^{\prime}.N^{\prime})$. It remains to show the effect
of transitions firing on domains to compute all possible successors of a
class. Firing a transition $t$ from $(M.N,D)$ propagates constraints of the
firing domain $D$ on variables attached to transitions that remain enabled.
Variables associated to newly enabled transitions only have to meet lower and
upper bounds on their firing times. We can now show that for waiting nets, the
set of successors of a state class is finite and can be effectively computed
despite waiting transitions and non-determinism.

$\bullet$$p_{0}$$\bullet$$p_{1}$$p_{2}$$\bullet$$p_{3}$$p_{4}$$p_{5}$$t_{0}$$[0,\infty)$$t_{1}$$[0,3]$$t_{2}$$[5,6]$
Figure 5: Upper bounds of transitions influence state classes of waiting Nets

Let us illustrate the influence of control places on the construction of state
classes with the waiting net of Figure 5. This net starts in a configuration
$C_{0}=(M_{0}.N_{0},v_{0})$ with $M_{0}.N_{0}=\\{p_{0},p_{1},p_{3}\\}.\\{\\}$.
Transitions $t_{0},t_{1},t_{2}$ are enabled in this marking, but $t_{0}$ is
the only fully enabled transition. From configuration $C_{0}$, one can let an
arbitrary amount of time $\delta\in\mathbb{R}^{\geq 0}$ elapse, and then fire
transition $t_{0}$. If $t_{0}$ fires from
$C_{0}^{\prime}=(M_{0}.N_{0},v_{0}+\delta)$, the net reaches a new
configuration $(M^{\prime}.N^{\prime},v^{\prime})$ where
$M^{\prime}.N^{\prime}=\\{p_{1},p_{3}\\}.\\{p_{2}\\}$, and
$v^{\prime}(t_{0})=\bot,v^{\prime}(t_{1})=v^{\prime}(t_{2})=\delta$.

Let $C_{1}=(M^{\prime}.N^{\prime},v_{1})$ be a configuration reached when
$0\leq\delta<3$. The value of clock $x_{t_{1}}$ is still smaller than the
upper bound $\beta(t_{1})=3$. Then, from $C_{1}$, one can still wait before
firing $t_{1}$, i.e., $t_{1}$ is not urgent and can fire immediately or within
a duration $3-\delta$, and transition $t_{2}$ is not firable, and cannot
become firable before the urgent firing of $t_{1}$. Now, let
$C_{2}=(M^{\prime}.N^{\prime},v_{2})$ be a configuration reached after
elapsing $\delta$ with $3\leq\delta<5$. In $C_{2}$, we have $v_{2}(t_{2})<5$
and $v_{2}(t_{1})=3$, as the value of clock $x_{t_{1}}$ was frozen when
reaching the upper bound $\beta(t_{3})=3$. Hence, in $C_{2}$, transition
$t_{1}$ is urgent and must fire, and transition $t_{2}$ still has to wait
before firing. Hence, choosing $3\leq\delta<5$ forces to fire $t_{1}$
immediately after $t_{0}$. As this firing consumes the token in control place
$p_{2}$, it will prevent $t_{2}$ from firing. In a similar way, let us call
$C_{3}=(M^{\prime}.N^{\prime},v_{3})$ a configuration reached after elapsing
$\delta\geq 5$ time units and then firing $t_{0}$. In this configuration, we
have $v_{3}(t_{1})=3$ and $v_{3}(t_{2})\in[5,6]$, forcing $t_{1}$ or $t_{2}$
to fire immediately without elapsing time. This example shows that the time
elapsed in a configuration has to be considered when computing successors of a
state class. We have to consider whether the upper bound of a waiting
transition has been reached or not, and hence to differentiate several cases
when firing a single transition $t$. Fortunately, these cases are finite, and
depend only on upper bounds attached to waiting transitions in domain $D$.

######  Definition 4.4 (Upper Bounds Ordering)

Let $M.N$ be a marking, $D$ be a firing domain with constraints of the form
$a_{i}\leq\theta_{i}\leq b_{i}$. Let $B_{M.N,D}=\\{b_{i}\mid
t_{i}\in\mathsf{enabled}(M)\\}$. We can order bounds in $B_{M.N,D}$, and
define $bnd_{i}$ as the $i^{th}$ bound in $B_{M.N,D}$. We also define
$bnd_{0}=0$ and $bnd_{|B_{M.N,D}|+1}=\infty$.

In the example of Figure 5, the initial domain $D_{0}$ is

$D_{0}=\left\\{\begin{array}[]{l}0\leq\theta_{0}\leq\infty\\\
0\leq\theta_{1}\leq 3\\\ 5\leq\theta_{2}\leq 6\\\ \end{array}\right.$

The bounds appearing in $D_{0}$ are hence $0,3,6,\infty$. Consider a
transition $t_{f}$ firable from $C=(M.N,D)$. This means that there is a way to
choose a delay $\theta_{f}$ that does not violate urgency of all other
transitions. We use $B_{M.N,D}$ to partition the set of possible values for
delay $\theta_{f}$ in a finite set of intervals, and find which transitions
reach their upper bound when $\theta_{f}$ belongs to an interval. Recall that
$t_{f}$ can fire only if adding constraint $\theta_{f}\leq\theta_{j}$ for
every fully enabled transition $t_{j}$ to domain $D$ still yields a
satisfiable set of constraints. This means that when considering that $t_{f}$
fires after a delay $\theta_{f}$ such that $bnd_{i}\leq\theta_{f}\leq
bnd_{i+1}$, as $D$ also contains a constraint of the form
$a_{f}\leq\theta_{f}\leq b_{f}$, considering an interval such that $bnd_{i}$
is greater than $\min\\{b_{j}\in B_{M.N,D}\mid
t_{j}\in\mathsf{FullyEnabled}(M.N)\\}$ or smaller than $a_{f}$ immediately
leads to inconsistency of constraint
$D_{|full}\cup\underset{t_{j}\in\mathsf{FullEnabled}(M.N)}{\bigwedge}\theta_{f}\leq\theta_{j}\wedge
bnd_{i}\leq\theta_{f}\leq bnd_{i+1}$. We denote by $B^{t_{f}}_{M.N,D}$ the set
of bounds $B_{M.N,D}$ pruned out from these inconsistent bound values. Now,
choosing a particular interval $[bnd_{i},bnd_{i+1}]$ for the possible values
in $\theta_{f}$ indicates for which waiting transitions $t_{1},\dots t_{k}$
the clocks $x_{t_{1}},\dots x_{t_{k}}$ measuring time elapsed since enabling
has reached upper bounds $\beta(t_{1}),\dots\beta(t_{k})$. The values of these
clocks become irrelevant, and hence the corresponding $\theta_{i}$’s have to
be eliminated from the domains.

######  Definition 4.5 (Time progress (to the next bound))

Let $M.N$ be a marking, $D$ be a firing domain, and $b=\min B_{M.N,D}$ be the
smallest upper bound for enabled transitions. The domain reached after
progressing time to bound $b$ is the domain $D^{\prime}$ obtained by:

  * •

replacing every variable $\theta_{i}$ by expression $\theta_{i}^{\prime}-b$

  * •

eliminating every $\theta^{\prime}_{k}$ whose upper bound is $b$,

  * •

computing the normal form for the result and renaming all
$\theta_{i}^{\prime}$ to $\theta_{i}$

Progressing time to the next upper bound allows to remove variables related to
waiting transitions whose clocks have reached their upper bounds from a firing
domain. We call these transitions timed-out transitions. For a transition
$t_{k}\in waiting(M.N)$ if $v(x_{t_{k}})=\beta(t_{k})$, variable $\theta_{k}$,
that represents the time needed to reach the upper bound of the interval is
not meaningful any more: either $t_{k}$ gets disabled in the future, or is
fired urgently as soon as it becomes fully enabled, because $\theta_{k}=0$. So
the only information to remember is that $t_{k}$ will be urgent as soon as it
becomes fully enabled.

######  Definition 4.6 (Successors)

A successor of a class $C=(M.N,D)$ after firing of a transition $t_{f}$ is a
class $C^{\prime}=(M^{\prime}.N^{\prime},D^{\prime})$ such that
$M^{\prime}.N^{\prime}$ is the marking obtained after firing $t_{f}$ from
$M.N$, and $D^{\prime}$ is a firing domain reached after firing $t_{f}$ in
some interval $[b_{r},b_{r+1}]$ where $b_{r},b_{r+1}$ are consecutive values
in $B^{t_{f}}_{M.N,D}$.

Given $C$ and a firable transition $t_{f}$, we can compute the set
$\mathsf{Post}(C,t_{f})$ of successors of $C$, i.e.
$\mathsf{Post}(C,t_{f}):=\\{(M^{\prime}.N^{\prime},\mathsf{next}_{r}(D,t_{f}))\,|\,b_{r}\in
B^{t_{f}}_{M.N,D}\cup\\{0\\}\\}$. The next marking is the same for every
successor and is
$M^{\prime}.N^{\prime}=M.N-{{}^{\bullet}}\\!t_{f}+t_{f}^{\bullet}$. We then
compute $\mathsf{next}_{r}(D,t_{f})$ as follows:

### 1) Time progress:

We successively progress time from $D$ to bounds $b_{1}<b_{2}<\dots<b_{r}$ to
eliminate variables of all enabled transitions reaching their upper bounds, up
to bound $b_{r}$. We call $D^{r}$ the domain obtained this way. Every
transition $t_{k}$ in $Enabled(M.N)$ that has no variable $\theta_{k}$ in
$D^{r}$ is hence a waiting transition whose upper bound has been reached.

### 2) Firing condition:

We add to $D^{r}$ the following constraints: we add the inequality
$(b_{r}\leq\theta_{f}\leq b_{r+1})$, and for every transition
$t_{j}\in\mathsf{FullyEnabled}(M)\setminus\\{t_{f}\\}$, we add to $D^{r}$ the
inequality $\theta_{f}\leq\theta_{j}$. This means that no other transition was
urgent when $t_{f}$ has been fired. Let $D^{u}$ be the new firing domain
obtained this way. If any fully enabled transition $t_{j}$ has to fire before
$t_{f}$, then we have a constraint of the form $a_{j}\leq\theta_{j}\leq b_{j}$
with $b_{j}<a_{f}$, and $D^{u}$ is not satisfiable. As we know that $t_{f}$ is
firable, this cannot be the case, and $D^{u}$ has a solution, but yet, we have
to include in the computation of the next firing domains reached after firing
of $t_{f}$ the constraints on $\theta_{f}$ due to urgency of other
transitions.

### 3) Substitution of variables:

As $t_{f}$ fires after elapsing $\theta_{f}$ time units, the time to fire of
other transitions whose clocks did not yet exceed their upper bounds decreases
by the same amount of time. Variables of timed-out transitions have already
been eliminated in $D^{u}$. So for every $t_{j}\neq t_{f}$ that has an
associated constraint $a_{j}\leq\theta_{j}\leq b_{j}$ we do a variable
substitution reflecting the fact that the new time to fire
$\theta^{\prime}_{j}$ decreases w.r.t. the former time to fire $\theta_{j}$.
We set $\theta_{j}:=\theta_{f}+\theta^{\prime}_{j}$. When this is done, we
obtain a domain $D^{\prime u,b_{r}}$ over a set of variables
$\theta^{\prime}_{i_{1}},\dots\theta^{\prime}_{i_{k}}$, reflecting constraints
on the possible remaining times to upper bounds of all enabled transitions
that did not timeout yet.

### 4) Variable Elimination:

As $t_{f}$ fired at time $\theta_{f}$, it introduced new relationships between
remaining firing times of other transitions, i.e other
$\theta_{i}^{\prime}\neq\theta_{f}$, that must be preserved in the next state
class. However, as $t_{f}$ is fired and changed the marking of the waiting
net, in the next class, either $t_{f}$ is a newly enabled transition, or it is
not enabled. In the first case, the new domain will contain a fresh variable
attached to the new occurrence of $t_{f}$ enabled by the firing. In the second
case, variable $\theta_{f}$ should not appear in the new domain. We hence need
to remove the ”old” variable $\theta_{f}$ from inequalities, while preserving
an equivalent set of constraints, before introduction of constraints
associated with newly enabled transitions. This is achieved by elimination of
variable $\theta_{f}$ from $D^{\prime u,b_{r}}$, for instance with the well
known Fourier-Motzkin technique (see Appendix A for details). We proceed
similarly with variable $\theta^{\prime}_{i}$ for every transition $t_{i}$
that is enabled in marking $M.N$ but not in $M.N-{{}^{\bullet}}\\!(t_{f})$.
After elimination, we obtain a domain $D^{\prime E,b_{r}}$ over remaining
variables.

### 5) Addition of new constraints :

The last step to compute the next state classes is to introduce fresh
constraints for firing times of newly enabled transitions. For every
$t_{i}\in\uparrow\mathsf{enabled}(M.N,t_{f})$ we add to $D^{\prime E,b_{r}}$
the constraint $\alpha(t_{i})\leq\theta^{\prime}_{i}\leq\beta(t_{i})$. For
every timed-out transition $t_{k}$ that becomes fully enabled, we add to
$D^{\prime E,b_{r}}$ the constraint $\theta_{k}=0$. Timed-out transitions that
become fully enabled are hence urgent in the next class. After adding all
constraints associated to newly enabled transitions, we obtain a domain, in
which we can rename every $\theta^{\prime}_{i}$ to $\theta_{i}$ to get a
domain $D^{\prime F,b_{r}}$. Notice that this domain needs not be minimal, so
we do a last normalization step (see Definition 4.2) to obtain a final
canonical domain $\mathsf{next}_{r}(D,t_{f})=D^{\prime F,b_{r}\>*}$.

Let us compare the state class construction in TPNs and in waiting nets. In
TPNs (see [7, 22]), for a domain $D$ and a transition $t_{f}$, there is a
single successor domain in $\mathsf{Post}(D,t_{f})$, and hence a state class
can have up to $|T|$ successors. In waiting nets, for a given firable
transition $t_{f}$, $\mathsf{Post}(D,t_{f})$ contains one domain per bound in
$B^{t_{f}}_{M.N,D}$, i.e. $\mathsf{Post}(D,t_{f})$ is not a singleton anymore.
Now, if a waiting net has no control place, there is no bound on waiting
transitions to consider, as enabled transitions are fully enabled in every
configuration. Step 1 of successor construction leaves the starting domain $D$
unchanged, and consequently the state class construction shown above is
exactly the standard construction for TPNs. The number of successors for a
state class in TPNs is exactly the number of enabled transitions. Let
$\mathsf{Post}(C)$ be the set of successors of a class $C$. Then
$|\mathsf{Post}(C)|\leq|\mathsf{enabled}(M.N)|^{2}$, as the number of bounds
to consider for a transition cannot exceed the number of enabled transitions.
Computing successors can be repeated from each class in $Post(C)$. For a given
net $\mathcal{W}$, and a given marking $M_{0}.N_{0}$, we denote by
$\mathcal{C}({W})$ the set of classes that can be built inductively. This set
need not be finite, but we show next that this is due to markings, and that
the set of domains appearing in state classes is finite.

###### Definition 4.7

(State Class Graph) The State Class Graph of a waiting net $\mathcal{W}$ is a
graph $SCG(\mathcal{W})=(\mathcal{C}({W}),C_{0},\longrightarrow)$ where
$C_{0}=(M_{0}.N_{0},D_{0})$, and $C\overset{t}{\longrightarrow}C^{\prime}$ iff
$C^{\prime}\in Post(C,t)$.

Let
$\rho=(M_{0}.N_{0},v_{0})\overset{d_{1}}{\longrightarrow}(M_{0}.N_{0},v_{0}\oplus
d_{1})\overset{t_{1}}{\longrightarrow}(M_{1}.N_{1},v_{1})\dots(M_{k}.N_{k},v_{k})$
be a run of $\mathcal{W}$ and
$\pi=(M^{\prime}_{0}.N^{\prime}_{0},D_{0}).(M^{\prime}_{1}.N^{\prime}_{1},D_{1})\dots(M^{\prime}_{k}.N^{\prime}_{k},D_{k})$
be a path in $SCG(\mathcal{W})$. We will say that $\rho$ and $\pi$ coincide
iff $\forall i\in 1..k,M_{i}.N_{i}=M^{\prime}_{i}.N^{\prime}_{i}$, and for
every step
$(M_{i}.N_{i},v_{i})\overset{d_{i}}{\longrightarrow}(M_{i}.N_{i},v_{i}\oplus
d_{i})\overset{t_{i}}{\longrightarrow}(M_{i+1}.N_{i+1},v_{i+1})$, there exists
an interval $[b_{r},b_{r+1}]$ such that $d_{i}\in[b_{r},b_{r+1}]$ and
$D_{i+1}=\mathsf{next}_{r}(D_{i},t_{i})$.

$\\{p_{0},p_{1},p_{3}\\}.\\{~{}\\}$
$\begin{array}[]{l}\theta_{0}\in[0,\infty)\\\ \theta_{1}\in[0,3]\\\
\theta_{2}\in[5,6]\end{array}$$Cl_{0}$$\\{p_{1},p_{3}\\}.\\{p_{2}\\}$
$\begin{array}[]{l}\theta_{1}\in[0,3],\theta_{2}\in[2,6]\\\
\theta_{1}-\theta_{2}\leq-2\\\ \theta_{2}-\theta_{1}\leq 6\end{array}$
$Cl_{1}$$\\{p_{1},p_{3}\\}.\\{p_{2}\\}$ $\begin{array}[]{l}\theta_{1}=0\\\
\theta_{2}\in[2,3]\end{array}$$Cl_{2}$$\\{p_{1},p_{3}\\}.\\{p_{2}\\}$
$\begin{array}[]{l}\theta_{1}=0\\\
\theta_{2}=0\end{array}$$Cl_{3}$$\\{p_{3},p_{4}\\}.\\{~{}\\}$
$\theta_{2}\in[5,6]$$Cl_{4}$$\\{p_{3},p_{4}\\}.\\{~{}\\}$
$\theta_{2}\in[2,3]$$Cl_{5}$$\\{p_{3},p_{4}\\}.\\{~{}\\}$
$\theta_{2}=0$$Cl_{6}$$\\{p_{1},p_{5}\\}.\\{~{}\\}$
$\theta_{1}=0$$Cl_{7}$$t_{0}$$\theta_{0}\in[0,3]$$t_{0}$$\theta_{0}\in[3,6]$$t_{0}$$\theta_{0}\in[6,\infty)$$t_{1}$$\theta_{1}\in[0,3]$$t_{1}$$\theta_{1}=0$$t_{1}$$\theta_{1}=0$$t_{2}$$\theta_{2}=0$
Figure 6: A non-deterministic state class graph for the waiting net of Figure
5.

Let us illustrate the construction of state classes with the example of Figure
5. We start from an inital state class $Cl_{0}=(M_{0}.N_{0},D_{0})$ with
$M_{0}.N_{0}=\\{p_{0},p_{1},p_{3}\\}\\{\\}$ and $D_{0}$ is given by the set of
constraints $0\leq\theta_{0},0\leq\theta_{1}\leq 3,5\leq\theta_{2}\leq 6$.
From the initial configuration $(M_{0}.N_{0},v_{0})$ one can only fire
transition $t_{0}$, that is, wait for some duration $\theta_{0}$ and then
perform a discrete move with transition $t_{0}$. So $t_{0}$ is also the only
firable transition from state class $Cl_{0}$. Here, we have two important
bounds, $3$ and $6$ which are the upper bounds attached to $t_{1}$ and $t_{2}$
respectively. Let us assume that $t_{0}$ fires after a duration in $[0,3]$. We
hence fire from a domain that satisfies the following constraints:

$D^{\prime}_{0}=\left\\{\begin{array}[]{l}0\leq\theta_{0}\leq 3\\\
0\leq\theta_{1}\leq 3\\\ 5\leq\theta_{2}\leq 6\\\ \end{array}\right.$

One can easily find values for $\theta_{0},\theta_{1},\theta_{2}$ satisfying
$D^{\prime}_{0}$ and such that $\theta_{0}\leq\theta_{1}$ and
$\theta_{0}\leq\theta_{2}$. So $t_{0}$ is firable from $Cl_{0}$. Let
$\theta^{\prime}_{1},\theta^{\prime}_{2}$ be variables describing the
remaining times to fire after firing $t_{0}$. As $t_{0}$ is the fired
transition, all remaining (positive) times are decreased by $\theta_{0}$, i.e.
$\theta_{1}^{\prime}=\theta_{1}-\theta_{0}$ and
$\theta_{2}^{\prime}=\theta_{2}-\theta_{0}$. This gives a variable change
allowing to obtain the following domain:

$\left\\{\begin{array}[]{l}0\leq\theta_{0}\leq 3\\\
0\leq\theta_{1}^{\prime},0\leq\theta_{2}^{\prime}\\\
0\leq\theta_{1}^{\prime}+\theta_{0}\leq 3\\\
5\leq\theta_{2}^{\prime}+\theta_{0}\leq 6\\\ \end{array}\right.\mbox{~{}or
equivalently~{}}\left\\{\begin{array}[]{l}0\leq\theta_{0}\leq 3\\\
0\leq\theta_{1}^{\prime},0\leq\theta_{2}^{\prime}\\\
0-\theta_{1}^{\prime}\leq\theta_{0}\leq 3-\theta_{1}^{\prime}\\\
5-\theta_{2}^{\prime}\leq\theta_{0}\leq 6-\theta_{2}^{\prime}\\\
\end{array}\right.$

The variable to eliminate is now $\theta_{0}$, we can hence reorganize lines
containing $\theta_{0}$ in this domain as

$\max(0,0-\theta_{1}^{\prime},5-\theta_{2}^{\prime})\leq\theta_{0}\leq\min(3,3-\theta_{1}^{\prime},6-\theta_{2}^{\prime})$

We hence obtain, after elimination of $\theta_{0}$

$\left\\{\begin{array}[]{lcl}0\leq 3&(tautology)\\\
0\leq\theta_{1}^{\prime},0\leq\theta_{2}^{\prime}\\\ 0\leq
3-\theta_{1}^{\prime}&\Longleftrightarrow&\theta_{1}^{\prime}\leq 3\\\ 0\leq
6-\theta_{2}^{\prime}&\Longleftrightarrow&\theta_{2}^{\prime}\leq 6\\\
0-\theta_{1}^{\prime}\leq 3&\Longleftrightarrow&-3\leq\theta_{1}^{\prime}\\\
0-\theta_{1}^{\prime}\leq 3-\theta_{1}^{\prime}&(tautology)\\\
0-\theta_{1}^{\prime}\leq 6-\theta_{2}^{\prime}\\\ 5-\theta_{2}^{\prime}\leq
3&\Longleftrightarrow&2\leq\theta_{2}^{\prime}\\\ 5-\theta_{2}^{\prime}\leq
3-\theta_{1}^{\prime}\\\ 5-\theta_{2}^{\prime}\leq
6-\theta_{2}^{\prime}&(tautology)\\\ \end{array}\right.$

After elimination of redundancies and tautologies, and renaming
$\theta^{\prime}_{1},\theta^{\prime}_{2}$ into $\theta_{1},\theta_{2}$ we
obtain a domain $D_{1}$ with the following constraints:

$D_{1}=\left\\{\begin{array}[]{l}0\leq\theta_{1}\leq 3\\\ 2\leq\theta_{2}\leq
6\\\ \theta_{2}-\theta_{1}\leq 6\\\ \theta_{1}-\theta_{2}\leq-2\\\
\end{array}\right.$

The state class reached by firing $t_{0}$ after elapsing $0$ to $3$ time units
is $Cl_{1}=(M_{1}.N_{1},D_{1})$ with $M_{1}=\\{p_{1},p_{3}\\}$ and
$N_{1}=\\{p_{2}\\}$. One can notice that, as transitions $t_{1},t_{2}$ remain
enabled after firing of $t_{0}$, variable elimination adds diagonal
constraints of the form $\theta_{2}-\theta_{1}\leq 6$ and
$\theta_{1}-\theta_{2}\leq-2$. This is the case in general for all pairs of
transitions that remain enabled. Domains are hence not limited to interval
contraints of the form $a_{i}\leq\theta_{i}\leq b_{i}$. Similarly, starting
from $Cl_{0}$ one can let between $3$ and $6$ time units elapse and reach
ctate class $Cl_{2}=(M_{2}.N_{2},D_{2})$. $D_{2}$ is easily obtained by
progressing $D_{0}$ of $3$ time units (this is a variable change replacing
$\theta_{i}$ by $\theta^{\prime}_{i}+3$), and projecting away constraints
containing $\theta^{\prime}_{1}$. Then, firing $t_{0}$ gives a pair of
constraints $0\leq\theta_{0}^{\prime}\leq 3$ and
$2\leq\theta_{2}^{\prime}+\theta_{0}^{\prime}\leq 3$. We let the reader check
that this reduces to $2\leq\theta_{2}\leq 3$ after elimination of
$\theta_{0}$. Then by adding constraints on $\theta_{1}$ arising from the fact
that after firing of $t_{0}$, $t_{1}$ becomes fully enabled, we obtain :

$D_{2}=\left\\{\begin{array}[]{l}\theta_{1}=0\\\ 2\leq\theta_{2}\leq 3\\\
\end{array}\right.$

One can immediately notice that from any configuration in class $Cl_{2}$,
transition $t_{1}$ is urgent, and is the the only transition that can fire. We
let the readers build the remaining classes, and give the complete state class
graph for the waiting net of figure 5 in Figure 6. One can observe that this
state class graph is not deterministic.

######  Proposition 4.8 (Completeness)

For every run $\rho=(M_{0}.N_{0},v_{0})\dots(M_{k}.N_{k},v_{k})$ of
$\mathcal{W}$ there exists a path $\pi$ of $SCG(\mathcal{W})$ such that $\rho$
and $\pi$ coincide.

###### Proof 4.9

We only give a proof sketch, a complete proof of this proposition is provided
in Appendix D. We proceed by induction on the length of runs. For the base
case, we can easily prove that any transition firing from the initial
configuration after some delay $d$ gives a possible solution for $D_{0}$ and a
successor class, as $D_{0}$ does not contain constraints of the form
$\theta_{i}-\theta_{j}\leq c_{ij}$ . The induction step is similar, and
slightly more involved, because domains contain constraints involving pairs of
variables. However, we can show (Lemma D.4 in Appendix D) that along run
$\rho$ for every pair of steps composed of a time elapsing of duration $d_{i}$
followed by the firing of a transition $t_{f}$, we have
$d_{i}\in[a_{i,f},b_{i,f}]$, where $a_{i,f}$ is the lower and $b_{i,f}$ the
upper bound on variable $\theta_{f}$ at step $i$ of the run. Hence, for every
run of $\mathcal{W}$ there is a path that visits the same markings and
maintains consistent constraints.

######  Proposition 4.10 (Soundness)

Let $\pi$ be a path of $SCG(\mathcal{W})$. Then there exists a run $\rho$ of
$\mathcal{W}$ such that $\rho$ and $\pi$ coincide.

###### Proof 4.11

As for Proposition 4.8, we can prove this property by induction on the length
of paths in $SCG(\mathcal{W})$. A complete proof of this proposition is
provided in Appendix D.

Proposition 4.8 shows by induction on runs length that every marking reached
by a run of a waiting net appears in its state class graph. The proof of
Proposition 4.10 uses a similar induction on paths length, and shows that we
do not introduce new markings. These propositions show that the state class
graph is a sound and complete abstraction, even for unbounded nets. We can
show a stronger property, which is that the set of domains appearing in a
state class graph is finite.

###### Proposition 4.12

The set of firing domains in $SCG(\mathcal{W})$ is finite.

###### Proof 4.13

We only give a proof sketch, and provide a complete proof in Appendix D.
Domains are of the form $\\{a_{i}\leq\theta_{i}\leq b_{i}\\}_{t_{i}\subseteq
T}\cup\\{\theta_{i}-\theta_{j}\leq c_{i,j}\\}_{t_{i},t_{j}\subseteq T}$. We
can easily adapt proofs of [7] (lemma 3 page 9) to show that every domain
generated during the construction of the SCG has inequalities of the form
$a_{i}\leq\theta_{i}\leq b_{i}$ and $\theta_{i}-\theta_{j}\leq c_{ij}$, where
$0\leq a_{i}\leq\alpha(t_{i})$, $0\leq b_{i}\leq\beta(t_{i})$ and
$-\alpha(t_{i})\leq c_{ij}\leq\beta(t_{i})$ and $\alpha_{i},\beta(t_{i})$ are
the constant bounds of interval attached to $t_{i}$. This does not yet prove
that the set of domains is finite. We then show that domains are bounded, i.e.
that $\theta_{i}$’s and their differences have rational upper and lower bounds
(see Lemma D.7 in Appendix). We then show that domains are also linear, i.e.
that constants appearing in inequalities are linear combinations of a finite
set of constant values. Domain $D_{0}$ is bounded and linear, and a series of
technical lemmas (given in Appendix D) show that variable elimination,
reduction to a canonical form, etc. preserve bounds and linearity (a similar
result was shown in [7] for domains of TPNs). The set of bounded linear
domains between fixed bounds is finite, so the set of domains of a waiting net
is finite.

Finiteness of the set of domains of waiting nets is an important property,
that is not a straightforward consequence of the syntactic proximity with TPNs
nor of the effectiveness of successors construction. Indeed, waiting nets
allow to stop time measurement for waiting transitions reaching their upper
bounds. Petri nets with stopwatches, where time measurement can also be
stopped, do not have a finite state class representation, even for bounded
nets. The reason is that clock differences in domains of stopwatch Petri nets
can take any value. Waiting nets avoid this issue because clocks are always
stopped at a predetermined instant (when they reach the upper bound of an
interval).

###### Corollary 4.14

If $\mathcal{W}$ is a bounded waiting net then $SCG(\mathcal{W})$ is finite.

###### Proof 4.15

States of $SCG(\mathcal{W})$ are of the form $(M.N,D)$ where $M.N$ is a
marking and $D$ a domain for times to fire of enabled transitions. By
definition of boundedness, the number of markings in $SCG(\mathcal{W})$ is
finite. By Prop. 4.12, the set of domains appearing in $SCG(\mathcal{W})$ is
finite, so $SCG(\mathcal{W})$ is finite.

More precisely, if a net is $k_{M}$-bounded, there are at most $k_{M}^{|P|}$
possible markings, and the number of possible domains is bounded by $(2\cdot
K_{\mathcal{W}}+1)^{|T+1|^{2}}$, where
$K_{\mathcal{W}}=\max_{i,j}\lfloor\frac{\beta_{i}}{\alpha_{j}}\rfloor$ is an
upper bound on the number of linear combinations of bounds appearing in
domains. Hence the size of $SCG(\mathcal{W})$ is in $O(k_{M}^{|P|}\cdot(2\cdot
K_{\mathcal{W}}+1)^{|T+1|^{2}})$. A direct consequence of Proposition 4.8,
Proposition 4.10, and Corollary 4.14 is that many properties of bounded
waiting nets are decidable.

######  Corollary 4.16 (Reachability and Coverability)

The reachability and coverability problems for bounded waiting nets are
decidable and PSPACE-complete.

###### Proof 4.17

For PSPACE membership, given a target marking $M_{t}.N_{t}$ it suffices to
explore non-deterministically all runs starting from $(M_{0}.N_{0},D_{0})$ of
length at most $|SCG(\mathcal{W})|$ to find marking $M_{t}.N_{t}$ and prove
reachability, or a marking that covers $M_{t}.N_{t}$ witnessing coverability.
Random walks of bounded length are feasible in NLOGSPACE w.r.t. the size of
the explored graph, whence the NPSPACE=PSPACE complexity. For hardness, we
already know that reachability for $1$-safe Petri nets is PSPACE-Complete
[13], and a (bounded) Petri net is a (bounded) waiting net without control
places and with $[0,\infty)$ constraints. Similarly, given $1$-safe Petri net
and a place $p$, deciding if a marking with $M(p)=1$ (which is a coverability
question) is reachable is PSPACE-complete [17]. This question can be recast as
a coverability question for waiting nets, thus proving the hardness of
coverability.

Let us illustrate the advantages and expressive power of waiting nets with the
example of Figure 7 containing a cyclic behavior. This net contains a control
part (in Gray), composed of standard places $p_{2},p_{3}$, of control places
$c_{3},c_{4}$, and of two transitions $tc_{3}$ and $tc_{4}$ with respective
time intervals $[2,2]$ and $[1,1]$. The main idea in this control part is to
move a token from place $c_{3}$ to place $c_{4}$ after 2 time units, and then
move the token from $c_{4}$ to $c_{3}$ after 1 time unit. Control places
$c_{3}$ and $c_{4}$ are used to allow/forbid firing of transitions $t_{1}$ and
$t_{2}$ in the right part of the net. Transitions $t_{1}$ and $t_{2}$ are
independent transitions with respective time intervals $[1,2]$ and $[2,3]$ and
which firings are respectively allowed when place $c_{3}$ and $c_{4}$ are
filled. Note that allowing or forbidding firings of transitions does not
affect their enabledness: while transition $t_{2}$ is waiting for a token in
$c_{4}$ to fire, one measures the time elapsed since it was last enabled (and
similarly when transition $t_{1}$ is waiting for a token in $c_{3}$).

$\bullet$$p_{2}$$tc_{3}$$[2,2]$$p_{3}$$\bullet$$c_{3}$$tc_{4}$$[1,1]$$c_{4}$$\bullet$$p_{0}$$t_{1}$$[1,2]$$\bullet$$p_{1}$$t_{2}$$[2,3]$

Figure 7: A cyclic Waiting net

The main idea of this example is to give control alternatively to transition
$t_{1}$ and $t_{2}$, but measure enabled time for $t_{2}$ when control allows
firing of $t_{1}$ and enabled time for $t_{1}$ when control allows firing of
$t_{2}$. The timed word $(t_{1},1)(t_{1},2)(tc_{3},3)(t_{2},3.2)$ is a
possible behavior of this net. Notice that transition $t_{2}$ becomes fully
enabled after firing of $t_{3}$, but was enabled from the beginning of the
run. In a symmetric way, the timed word
$(t_{1},1)(t_{1},2)(tc_{3},3)(tc_{4},4)(t_{1},4)(t_{1},5)(t_{1},6)$ is a legal
behavior of the model. Indeed, after firing of $tc_{3}$ time still elapses for
$t_{1}$, which can fire immediately after firing of $tc_{4}$. These two
example behaviors show that one can design controllers that decouple control
and time measurement with waiting nets. The state class computed for this
example contains 44 state classes, and show that one can fire up to 5
occurrences of $t_{1}$ before an occurrence of $t_{2}$ fires urgently. Notice
that if one replaces control places by standard places in this example to
obtain a TPN, then transition $t_{2}$ never fires, as it is disabled at most 1
time unit after its enabling by firing of $t_{4}$. This example shows that
waiting nets can be a tool to design easily fair controllers.

##  5 Expressiveness

The next natural question for waiting nets is their expressiveness w.r.t.
other timed models. There are several ways to compare expressiveness of timed
models: One can build on relations between models such as isomorphism of their
underlying timed transition systems, timed similarity, or bisimilarity. In the
rest of this section, we compare models w.r.t. the timed languages they
generate. For two particular types of model $\mathcal{M}_{1}$ and
$\mathcal{M}_{2}$, we will write
$\mathcal{M}_{1}\leq_{\mathcal{L}}\mathcal{M}_{2}$ when, for every model
$X_{1}\in\mathcal{M}_{1}$, there exists a model $X_{2}$ in $\mathcal{M}_{2}$
such that $\mathcal{L}(X_{1})=\mathcal{L}(X_{2})$. Similarly, we will write
$\mathcal{M}_{1}<_{\mathcal{L}}\mathcal{M}_{2}$ if
$\mathcal{M}_{1}\leq_{\mathcal{L}}\mathcal{M}_{2}$ and there exists a model
$X_{2}\in\mathcal{M}_{2}$ such that for every model $X_{1}\in\mathcal{M}_{1}$,
$\mathcal{L}(X_{2})\neq\mathcal{L}(X_{1})$. Lastly, we will say that
$\mathcal{M}_{1}$ and $\mathcal{M}_{2}$ are equally expressive and write
$\mathcal{M}_{1}=_{\mathcal{L}}\mathcal{M}_{2}$ if
$\mathcal{M}_{1}\\!\leq_{\mathcal{L}}\\!\mathcal{M}_{2}$ and
$\mathcal{M}_{1}\\!\leq_{\mathcal{L}}\\!\mathcal{M}_{2}$. In the rest of this
section, we compare bounded and unbounded waiting nets with injective/non-
injective labelling, with or without silent transitions labelled by $\epsilon$
to timed automata, TPNs, Stopwatch automata, and TPNs with stopwatches.

We first have obvious results. It is worth nothing that every model with non-
injective labeling is more expressive than its injective counterpart.
Similarly, every unbounded model is strictly more expressive than its bounded
subclass. Waiting nets can express any behavior specified with TPNs. Indeed, a
WTPN without control place is a TPN. One can also remark that (unbounded)
TPNs, and hence WTPNs are not regular. It is also well known that the timed
language of a bounded TPN can be encoded by a time bisimilar timed automaton
[12, 22, 6]. We show next that one can extend the results of [22] to waiting
nets, i.e. reuse the state class construction of section 4 to build a finite
timed automaton $\mathcal{A}_{\mathcal{W}}$ that recognizes the same language
as a waiting net $\mathcal{W}$. As shown by Proposition 4.8 and Proposition
4.10, the state class graph $SCG(\mathcal{W})$ is sound and complete. State
class graphs abstract away the exact values of clocks and only remember
constraints on remaining times to fire of fully enabled transitions, and times
to upper bounds for enabled transitions. If we label moves of
$SCG(\mathcal{W})$ by the label of the transition used to move from a state
class to the next one, the state class graph becomes an automaton that
recognizes the untimed language of $\mathcal{W}$. Further, one can add guards
on clock values to moves and clock invariants to states of a state class graph
to recover the timing information lost during abstraction.

######  Definition 5.1 (Extended State Class)

An extended state class is a tuple $C_{ex}=(M.N,D,\chi,trans,XP)$, where $M.N$
is a marking, $D$ a domain, $\chi$ is a set of real-valued clocks,
$trans\in(2^{T})^{\chi}$ maps clocks to sets of transitions and $XP\subseteq
T$ is a set of transitions which upper bound have already been reached.

Extended state classes were already proposed in [22] as a building step for
state class timed automata recognizing languages of bounded TPNs. Here, we add
information on transitions that have been enabled for a duration that is at
least their upper bound. This is needed to enforce urgency when such
transitions become firable. In extended state classes, every clock $x\in\chi$
represents the time since enabling of several transitions in $trans(x)$, that
were enabled at the same instant. So, for a given transition $t$, the clock
representing the valuation $v(x_{t})$ is $trans^{-1}(t)$111An alternative is
to associate a clock to every enabled transition, but using a map $trans$ as
proposed in [22] allows to build automata with a reduced number of clocks..
Let $\mathbb{C}^{ex}$denote the set of all state classes. We can now define
the state class timed automaton $SCTA(\mathcal{W})$ by adding guards and
resets to the transitions of the state class graph, and invariants to state
classes.

######  Definition 5.2 (State Class Timed Automaton)

The state class timed automaton of $\mathcal{W}$ is a tuple
$SCTA(\mathcal{W})=(L,l_{0},X,\Sigma,Inv,E,F)$ where:

  * •

$L\subseteq\mathbb{C}^{ex}$ is a set of extended state classes.
$l_{0}=(M_{0}.N_{0},D_{0},\\{x_{0}\\},trans_{0},XP_{0})$, where
$trans_{0}(x_{0})=\mathsf{Enabled}(M_{0}.N_{0})$ and $XP_{0}=\emptyset$.

  * •

$F=L$, i.e. every run is accepting,

  * •

$\Sigma=\lambda(T)$, and $X=\underset{(M.N,D,\chi,trans,XP)\in
L}{\bigcup}\chi\subseteq\\{x_{1},\dots x_{|T|}\\}$ is a set of clocks

  * •

$E$ is a set of transitions of the form
$(C_{ex},\lambda(t),g,R,C^{\prime}_{ex})$. In each transition, the locations
$C_{ex}=(M.N,D,\chi,trans,XP)$ and
$C^{\prime}_{ex}=(M^{\prime}.N^{\prime},D^{\prime},\chi^{\prime},trans^{\prime},XP^{\prime})$
are two extended state classes such that
$(M^{\prime}.N^{\prime},D^{\prime})\longrightarrow(M.N,D)$ is a move of the
STG with $D^{\prime}=next_{r}(D,t)$ for some index $r$ chosen among the upper
bounds ordering computed from domain $D$.

We can compute the set of transitions disabled by the firing of $t$ from
$M.N$, denoted
$\mathsf{Disabled}(M.N,t)$ and from there, compute a new set of clocks
$\chi^{\prime}$. We have $\chi^{\prime}=\chi\setminus\\{x\in\chi\mid
trans(x)\subseteq\mathsf{Disabled}(M.N,t)\\}$ if firing $t$ does not enable
new transitions. If new transitions are enabled or become fully enabled after
reaching their upper bound, we have
$\chi^{\prime}=\chi\setminus\\{x\in\chi\mid
trans(x)\subseteq\mathsf{Disabled}(M.N,t)\\}\cup\\{x_{i}\\}$, where $i$ is the
smallest index for a clock in $X$ that is not used. Intuitively, $x_{i}$ will
memorize the time elapsed since the firing of $t$, and hence the time elapsed
since new enabling of all transitions enabled by this firing instead of
memorizing the same value for every transition.

Similarly, we can set

$trans^{\prime}(x_{k})=\left\\{\begin{array}[]{l}\uparrow\mathsf{enabled}(M.N,t)\cup\\{t\in
XP\cap\mathsf{FullyEnabled}(M^{\prime}.N^{\prime})\\}\mbox{~{}if~{}}x_{k}=x_{i}\\\
trans(x_{k})\setminus\mathsf{Disabled}(M.N,t)\mbox{~{}if~{}}x_{k}\neq
x_{i}\mbox{~{}and~{}}trans(x_{k})\nsubseteq\mathsf{Disabled}(M.N,t)\\\
\mbox{Undefined otherwise}\end{array}\right.$

The set $XP$ lists the waiting transitions that have reached their upper
bounds and were not fully enabled.

$\begin{array}[]{ll}XP^{\prime}=XP&\cap\>\>\mathsf{Enabled}(M-{{}^{\bullet}}\\!(t))\setminus\mathsf{FullyEnabled}(M^{\prime}.N^{\prime})\\\
&\cup\>\>\\{t_{k}\in\mathsf{Enabled}(M^{\prime}.N^{\prime})\mid\theta_{k}\not\in
D^{\prime}\\}\\\ \end{array}$

In words, $XP^{\prime}$ contains the transitions already in $XP$ that are
still enabled, and did not receive a token in the control places of their
preset, plus enabled waiting transitions that reached their upper bound, and
for which no constraint is kept in domain $D^{\prime}$.

The set of clocks reset in a transition is $R=\\{x_{i}\\}$, where $x_{i}$ is
the first unused clock, if some transition is newly enabled, or was in $XP$
and becomes fully enabled. $R=\emptyset$ otherwise.

The guard $g$ is set to $\alpha(t)\leq trans^{-1}(t)$ if there is no
constraint of the form $trans^{-1}(t)\leq 0$ in the invariant of $C_{ex}$,
that is if $t$ is not a transition that became urgent after timing out, and
$g$ is set to true otherwise.

  * •

Let us now consider invariants attached to states. Let
$\mathsf{Urgent}(C_{ex})$ denote the set of fully enabled transitions of $M.N$
that are urgent. One can compute this set by looking at fully enabled
transitions with a constraint of the form $\theta_{k}=0$ in domain $D$. We
distinguish two cases. The first one is when no transition is urgent, i.e.,
$\mathsf{Urgent}(C_{ex})=\emptyset$. In this situation, we can let some time
elapse in location $C_{ex}$ until the upper bound for some clock attached to a
transition is reached. The invariant $Inv(C_{ex})$ is hence:

$Inv(C_{ex})=\underset{\scriptsize\begin{array}[]{l}x_{j}\in
trans^{-1}(\mathsf{FullyEnabled}(M^{\prime}.N^{\prime}),\\\ t_{k}\in
trans(x_{j})\cap\mathsf{FullyEnabled}(M^{\prime}.N^{\prime})\end{array}}{\bigwedge}x_{j}\leq\beta(t_{k})$

If $\mathsf{Urgent}(C_{ex}^{\prime})\neq\emptyset$ the invariant $Inv(C_{ex})$
is set to:

$Inv(C_{ex})=\underset{x_{k}\in
trans^{-1}\big{(}\mathsf{Urgent}(C_{ex})\big{)}}{\bigwedge}x_{k}\leq 0$

The invariant in location $C_{ex}$ then guarantees that if $t$ is urgent in
$C_{ex}$, then it is fired immediately without elapsing time, or another
urgent transition is fired immediately.

###### Proposition 5.3

Let $\mathcal{W}$ be a waiting net. Then
$\mathcal{L}(SCTA(\mathcal{W}))=\mathcal{L}(\mathcal{W})$.

###### Proof 5.4

Obviously, every sequence of transitions in $\mathcal{L}(SCTA(\mathcal{W}))$
is a sequence of transitions of the STG, and hence there exists a timed word
that corresponds to this sequence of transitions. Furthermore, in this
sequence, every urgent transition is fired in priority before elapsing time,
and the delay between enabling and firing of a transition $t$ lays between the
upper and lower bound of the time interval $[\alpha_{t},\beta_{t}]$ if some
time elapses in a state before the firing of $t$, and at least $\beta_{t}$
time units if $t$ fires immediately after reaching some state in the sequence
(it is an urgent transition, so the upper bound of its interval has been
reached, possibly some time before full enabling). Hence, every timed word of
$SCTA(\mathcal{W})$ is also a timed word of $\mathcal{W}$. We can reuse the
technique of Prop. 4.8 and prove by induction on the length of runs of
$\mathcal{W}$ that for every run of $\mathcal{W}$, there exists a run of
$SCTA(\mathcal{W})$ with the same sequence of delays and transitions. Let us
first consider a run of size 1, that is of the form
$(M_{0}.N_{0},v_{0})\overset{d_{0},t_{0}}{\longrightarrow}(M_{1}.N_{1},v_{1})$.
The domain $D_{0}$ is a conjunction of constraints of the form
$\alpha_{i}\leq\theta_{i}\leq b_{i}$ for every enabled transition, and
firability of $t_{0}$ after a delay $d_{0}$ is checked on the projection of
$D_{0}$ on transitions that are not timed-out in the bound interval
$[b_{r},b_{r+1}]$ that contains $d_{0}$, i.e. on a subset of the original set
of constraint $D_{0}$. We have associated to location $l_{0}$ the invariant
$Inv(l_{0})=x_{0}\leq\min_{t_{k}\in\mathsf{FullyEnabled}(M_{0}.N_{0})}(\beta_{k})$
(there is a single clock $x_{0}$ as all enabled transitions are enabled at
date $0$). All transition labeled by $t_{0}$ leaving $l_{0}$ are attached a
guard of the form $g=\alpha(t_{0})\leq x_{0}$. The move of $\mathcal{W}$ via
transition $t_{0}$ after $d_{0}$ time units is allowed, so we necessarily have
$v(x_{t_{0}})=d_{0}\geq b_{r}\geq\alpha(t_{0})$. As we have
$b_{r}\leq\beta(t_{0})$, and as $t_{0}$ is firable from $D_{0}$, we can also
claim that $v_{0}+d_{0}\models Inv(l_{0})$ and $v_{0}+d_{0}\models g$. Hence
$(d_{0},t_{0})$ is a timed word of $\mathcal{L}(SCTA(\mathcal{W}))$.

Let us now consider a sequence of moves of the form
$(M_{0}.N_{0},v_{0})\overset{d_{0},t_{0}}{\longrightarrow}\dots\overset{d_{k-1},t_{k-1}}{\longrightarrow}(M_{k}.N_{k},v_{k})$.
As the state class graph is complete, there exists a sequence of abstract
moves
$(M_{0}.N_{0},D_{0})\overset{t_{0}}{\longrightarrow}\dots\overset{t_{k-1}}{\longrightarrow}(M_{k}.N_{k},D_{k})$.
By induction hypothesis, there exists a sequence of delays and transitions in
$SCTA(\mathcal{W})$ that leads to a configuration $(l_{k},\mu_{k})$ where
$l_{k}=(M_{k}.N_{k},D_{k},\xi_{k},trans_{k})$ is an extended state class with
invariant $inv_{k}$ and $\mu_{k}$ is a valuation of clocks. Assume that a
fully enabled transition $t_{k}$ is firable from $(M_{k}.N_{k},v_{k})$, and
let $h$ be the index of move at which $t_{k}$ was enabled. Still using the
completeness argument, this means that $t_{k}$ is firable from
$(M_{k}.N_{k},D_{k})$. Hence, there exists a transition from
$l_{k}=(M_{k}.N_{k},D_{k},\xi_{k},trans_{k})$ to some
$l_{k+1}=(M_{k+1}.N_{k+1},D_{k+1},\xi_{k+1},trans_{k+1})$ labeled by
transition $t_{k}$. Assume that $t_{k}$ is not a transition that has timeout.
Then the move is attached with guard $g::=\alpha(t_{k})\leq
trans^{-1}(t_{k})$. We know that in configuration $(M_{k}.N_{k},v_{k})$ of
$\mathcal{W}$, $v_{k}(x_{t_{k}})=d_{k}+\underset{i\in
h..k-1}{\sum}d_{i}\geq\alpha(t_{k})$. As $t_{k}$ did not timeout, the clock
$x_{h}=trans_{k}^{-1}(t_{k})$ was never reset since the $h^{th}$ transition.
So, $\mu_{k}=v_{k}(x_{t_{k}})$, and $t_{k}$ can fire from $(l_{k},\mu_{k})$
after $d_{k}$ time units. Now assume that $t_{k}$ is an urgent transition that
became urgent after a timeout. Then, we have $d_{k}=0$, and the invariant
$Inv(l_{k})=trans_{k}^{-1}(t_{k})\leq 0$ attached to $l_{k}$ does not let time
elapse, and $t_{k}$ can fire, and cannot let a duration of more than $d_{k}$
time units elapse.

We are now ready to compare expressiveness of waiting nets and their variants
w.r.t. other types of time Petri nets, and with timed automata. For a given
class $\mathcal{N}$ of net, we will denote by $B$-$\mathcal{N}$ the bounded
subclass of $\mathcal{N}$, add the subscript $\epsilon$ if transitions with
$\epsilon$ labels are allowed in the model, and a superscript $\overline{inj}$
if the labeling of transitions is non-injective. For instance
$B$-$WTPN_{\epsilon}^{\overline{inj}}$ denotes the class of bounded waiting
nets with non-injective labeling and $\epsilon$ transitions. It is well known
that adding $\epsilon$ moves to timed automata increases the expressive power
of the model [15]. Similarly, allowing non-injective labeling of transitions
or adding $\epsilon$ transitions increases the expressive power of nets [6].
Lastly, adding stopwatches to timed automata or bounded time Petri nets makes
them Turing powerful [11].

###### Theorem 5.5

$BWTPN<_{\mathcal{L}}TA(\leq,\geq)$.

###### Proof 5.6

From Proposition 5.3, we can translate every bounded waiting net $\mathcal{W}$
to a finite timed automaton $SCTA(\mathcal{W})$. Notice that
$SCTA(\mathcal{W})$ uses only constraints of the form $x_{i}\geq a$ in guards
and of the form $x_{i}\leq b$ in invariants. Thus, $BWTPN\subseteq
TA(\leq,\geq)$. This inclusion is strict. Consider the timed automaton
$\mathcal{A}_{1}$ of Figure 8$-a)$. Action $a$ can occur between date 2 and 3
and $b$ between date $4$ and $5$. The timed language of $\mathcal{A}_{1}$
cannot be recognized by a BWTPN with only two transitions $t_{a}$ and $t_{b}$,
because $t_{a}$ must be firable and then must fire between dates 2 (to satisfy
the guard) and $3$ (to satisfy the invariant in $s_{1}$). However, in TPNs and
WTPNs, transitions that become urgent do not let time elapse, and cannot be
disabled without making a discrete move. As $t_{b}$ is the only other possible
move, but is not yet allowed, no WTPN with injective labeling can encode the
same behavior as $\mathcal{A}_{1}$.

$s_{0}$$s_{1}$$s_{2}$$a,x\geq 2$$b,x\geq 4$$x\leq 3$$x\leq
5$$\bullet$$p_{0}$$p_{1}$$p_{2}$$a$$[2,3]$$b$$[4,5]$$\bullet$$p_{0}$$p_{1}$$p_{2}$$p_{3}$$p_{4}$$\epsilon$$[0,0]$$b$$[4,5]$$\epsilon$$[0,0]$$a$$[2,3]$
Figure 8: a) A timed automaton $\mathcal{A}_{1}$ b) An equivalent timed Petri
net c) An equivalent TPN in $TPN_{\epsilon}$

###### Remark 5.7

It was proved in [6] that timed automata (with $\epsilon-$transitions) have
the same expressive power as bounded TPNs with $\epsilon-$transitions. These
epsilon transitions can be used to ”steal tokens” of an enabled transition,
and prevent it from firing urgently after a delay. This cannot be done with
TPNs nor waiting nets without $\epsilon$, because a transition that is fully
enabled can be disabled only by a discrete move, and not by elapsing time.
Hence, bounded TPN with $\epsilon-$transitions are strictly more expressive
than waiting nets, and than waiting net with non-injective labeling.

$\bullet$$p_{0}$$t_{0}$$[0,20]$$c_{0}$$t_{1}$$[20,20]$$p_{1}$$\bullet$$p_{0}$$t_{0}$$[0,20]$$p$$t_{1}$$[\alpha,\beta]$$\bullet$$p_{0}$$t_{0}$$[0,20]$$c_{0}$$t_{1}$$[20,20]$$p_{1}$$t_{2}$$[0,1]$$p_{2}$
Figure 9: $a)$ A waiting net $\mathcal{W}$ $b)$ a part of TPN needed to encode
$\mathcal{L}(\mathcal{W})$ $c)$ An unbounded waiting net

###### Remark 5.8

Another easy result is that timed Petri nets and waiting nets are
incomparable. Indeed, timed Petri nets cannot encode urgency of TPNs, and as a
consequence some (W)TPNs have no timed Petri net counterpart, even in the
bounded case. Similarly, one can design a timed Petri net in which a
transition is firable only in a bounded time interval and is then disabled
when time elapses. We have seen in Figure 8-a) that
$\mathcal{L}(\mathcal{A}_{1})$ cannot be recognized by a waiting net. However,
it is easily recognized by the timed Petri net of figure 8-b).

###### Theorem 5.9

$TPN<_{\mathcal{L}}WTPN$ and $BTPN<_{\mathcal{L}}BWTPN$.

###### Proof 5.10

Clearly, from Definition 3.1, we have $TPN\leq_{\mathcal{L}}WTPN$ and
$BTPN\leq_{\mathcal{L}}BWTPN$, as TPNs are WTPNs without control places. It
remains to show that inclusions are strict. Consider the waiting net
$\mathcal{W}$ in Figure 9-a. We have $T=\\{t_{0},t_{1}\\}$,
$P=\\{p_{0},p_{1}\\},C=\\{c_{0}\\}$ and $M_{0}.N_{0}=\\{p_{0}\\}\\{\\}$.
Hence, from the starting configuration, $t_{0}$ is fully enabled and firable
(because $M_{0}\geq{{}^{\bullet}}\\!(t_{0})$), but $t_{1}$ is enabled and not
firable ($M_{0}\geq{{}^{\bullet}}\\!(t_{1})$ and $N_{0}(c_{0})=0$). Every
valid run of $\mathcal{W}$ is of the form
$\\{p_{0}\\}\\{\\}\xrightarrow[]{(d_{0},t_{0})}\\{\\}\\{c_{0}\\}\xrightarrow[]{(d_{1},t_{1})}\\{p_{1}\\}\\{\\}\text{
where }0\leq d_{0}\leq 20\text{ and }d_{0}+d_{1}=20$.

Thus the timed language of $\mathcal{W}$ is
$\mathcal{L}(\mathcal{W})=\\{(t_{0},d_{0})(t_{1},20)\,|\,0\leq d_{0}\leq
20\\}$. Let us show that there exists no $TPN$ that recognizes the language
$\mathcal{L}(\mathcal{W})$. In TPN, one cannot memorize the time already
elapsed using the clocks of newly enabled transitions. A TPN $\mathcal{N}$
recognizing $\mathcal{L}(\mathcal{W})$ should satisfy the following
properties:

  1. 1.

The $TPN$ should contain at least two different transitions namely $t_{0}$ and
$t_{1}$

  2. 2.

$t_{0}$ and $t_{1}$ are the only transitions which fire in any run of
$\mathcal{N}$.

  3. 3.

$t_{0}$ and $t_{1}$ are fired only once.

  4. 4.

$t_{0}$ must fire first and should be able to fire at any date in $[0,20]$
units.

  5. 5.

$t_{1}$ must fire second at time 20 units, regardless of the firing date of
$t_{0}$

The above conditions are needed to ensure that
$\mathcal{L}(\mathcal{N})=\mathcal{L}(\mathcal{W})$. We can now show that it
is impossible to build a net $\mathcal{N}$ satisfying all these constraints.
Since $t_{1}$ must fire after $t_{0}$ , $\mathcal{N}$ must contain a subnet of
the form shown in figure 9-b, where $p$ is an empty place preventing firing
$t_{1}$ before $t_{0}$. Notice however that $p$ forbids enabling $t_{1}$ (and
hence measuring time) from the beginning of a run. We can force $t_{0}$ to
fire between 0 and 20 units with the appropriate time interval $[0,20]$, but
the $TPN$ of Figure 9-$b)$ can not remember the firing date of $t_{0}$, nor
associate to $t_{1}$ a clock which value increases before $t_{0}$ fires. Let
$[\alpha,\beta]$ be the time interval associated to $t_{1}$, and consider the
two extreme but legal firing dates of $t_{0}$, namely 0 and 20 time units.
Allowing these two dates amounts to requiring that
$0+\alpha(t_{1})=0+\beta(t_{1})=20+\alpha(t_{1})=20+\beta(t_{1})=20$ which is
impossible. Hence, there exists no $TPN$ recognizing
$\mathcal{L}(\mathcal{W})$. This shows that $BTPN<_{\mathcal{L}}BWTPN$. The
proof easily extends to show that $TPN<_{\mathcal{L}}WTPN$, simply by adding
an unbounded part of net that becomes active immediately after firing $t_{1}$,
as depicted in the waiting net of Figure 9-c.

As mentioned earlier in the paper, one can consider that in a run of waiting
net, a transition with an empty control place in its preset can let its clock
reach the upper bound of its interval, and then freeze it, waiting for the
control place to be filled. A stopwatch time Petri net (SwTPN for short) is a
TPN with an additional relation $sw:P\to T$, defining stopwatch arcs. An
enabled transition $t$ such that $M\geq sw(t)$ is said active, and its clock
evolves during timed moves. An enabled transition such that $M<sw(t)$ is said
suspended and it clock does not change during timed move until it becomes
active again. A natural question is hence to compare waiting nets and SwTPNs.
The first thing to notice is that bounded SwTPNs (BSwTPNs) are already Turing
powerful [8] while bounded waiting nets are not. So we immediately obtain the
following proposition.

###### Proposition 5.11

There exists bounded SwTPNs that cannot be simulated by bounded waiting nets.

One interesting point to remark is that expressiveness of waiting nets and
SwTPNs have different origins. Waiting nets (and TPNs) can encode instructions
of a Counter Machine only if they are unbounded. For stopwatch Petri nets,
counter values in a Minsky Machine can be encoded by differences between upper
and lower bounds on clock constraints in domains [8], and this encoding works
even whith bounded SwTPNs. We can go further and prove that bounded waiting
nets and BSwTPNS are incomparable. Consider again the example of Figure 9-a.
We already know that the language of this bounded waiting net cannot be
encoded by a bounded TPN with only two transitions and an injective labeling.
Now, allowing stopwatch arcs still does not alllow for the encoding of a SwTPN
recognizing the same timed language as the waiting net of Figure 9-a.

###### Proposition 5.12

Bounded waiting nets and bounded stopwatch Petri nets are uncomparable.

###### Proof 5.13

We already know from Proposition 5.11 that some BSwTPNs cannot be simulated by
waiting nets. It remains to show the converse direction. Assume that there
exists a BSwTPN that can encode the same language as the waiting net of Figure
9-a. We know from the proof of Theorem 5.9 that, to encode this example with a
TPN that has only two transitions $t_{0}$ and $t_{1}$, if
$(t_{0})^{\bullet}\cap{{}^{\bullet}}\\!(t_{1})\neq\emptyset$, then, one has to
enforce occurrence of $t_{1}$ at date $20-d_{0}$ for every possible date
$d_{0}$ for the firing of $t_{0}$. We also proved that this is impossible for
any time interval $[\alpha,\beta]$ attached to $t_{1}$. Let us assume that
$(t_{0})^{\bullet}\cap{{}^{\bullet}}\\!(t_{1})\neq\emptyset$, and that there
exists $p_{sw}\in sw(t_{1})$, i.e. that a stopwatch arc from $p_{sw}$ to
$t_{1}$ controls clock and firing of $t_{1}$. If $p_{sw}\in(t_{0})^{\bullet}$
then $t_{1}$ is suspended until $t_{0}$ fires, and we are still in a situation
where we cannot enforce firing of $t_{1}$ exactly $20-d_{0}$ time units after
firing of $t_{0}$. If $p_{sw}\in{{}^{\bullet}}\\!(t_{0})$, then after firing
of $t_{0}$, $t_{1}$ cannot fire. Let us now assume that
$(t_{0})^{\bullet}\cap{{}^{\bullet}}\\!(t_{1})=\emptyset$. We already know
from Theorem 5.9 that without a stopwatch arc restricting firing of $t_{1}$,
one cannot prevent $t_{1}$ from firing at date $20$ before $t_{0}$. As in the
preceding case, if we attach interval $[\alpha,\beta]$ to transition $t_{1}$
and require $p_{sw}\in(t_{0})^{\bullet}$, then $t_{1}$ is initially suspended,
and we mush have $[\alpha,\beta]=[20-d_{0},20-d_{0}]$ for all values of
$d_{0}$, which is impossible. Now assume that
$p_{sw}\in{{}^{\bullet}}\\!(t_{0})$. Then $t_{1}$ is suspended after firing of
$t_{0}$ and hence we cannot fire it. We hence have
$p_{sw}\not\in{{}^{\bullet}}\\!(t_{0})\cup(t_{0})^{\bullet}$, and as the
contents of $p_{sw}$ is unchanged by firing of $t_{0}$, then $t_{1}$ is either
never firable if $M_{0}(p_{sw})=0$, or can fire before $t_{0}$ if
$M_{0}(p_{sw})>0$ and we set $[\alpha,\beta]=[20,20]$ , or at an unwanted
dates if we attach another arbitrary interval $[\alpha,\beta]$ to $t_{1}$.

###### Theorem 5.14

Injective TPNs and WTPNS are strictly less expressive than their non-injective
counterparts, i.e.

$\begin{array}[]{ll}BTPN<_{\mathcal{L}}BTPN^{\overline{inj}},&TPN<_{\mathcal{L}}TPN^{\overline{inj}},\\\
BWTPN<_{\mathcal{L}}BWTPN^{\overline{inj}},&WTPN<_{\mathcal{L}}WTPN^{\overline{inj}}\\\
\end{array}$

###### Proof 5.15

With non-injective labeling, (W)TPNs can recognize unions of timed language,
which is not the case for models with injective labeling. In every timed word
of the language of a model with injective labeling, a letter represents an
occurrence of a transition. That is, every occurrence of some letter $\sigma$
labeling a transition $t_{\sigma}$ is constrained by time in a similar way in
a word: if $t_{\sigma}$ is enabled at some date $d$, then $t_{\sigma}$ must
occur later at some date $d^{\prime}$ with $d+\alpha(t_{\sigma})\leq
d^{\prime}\leq\beta(t_{\sigma})$ at every position in the considered word.
This remark also holds for distinct words with the same prefix: let
$w.(\sigma,d)$ be a timed word, with
$w=(\sigma_{1},d_{1}).(\sigma_{2},d_{2})\dots(\sigma_{k},d_{k})$. The possible
values for $d$ lay in an interval that only depends on the unique sequence of
transitions followed to recognize $w$. With non-injective labeling, one can
recognize a word $w$ via several sequences of transitions, and associate
different constraints to the firing date of $\sigma$. The union of this set of
constraints need not be a single interval. Consider for instance the TPN of
Figure 10, that defines the language
$\mathcal{L}(\mathcal{N})=\\{(a,d_{1}).(b,d_{2})\mid d_{1}\in[0,1]\wedge
d_{2}\in[d_{1}+4,d_{1}+5]\\}\cup\\{(a,d_{1}).(b,d_{2})\mid d_{1}\in[0,1]\wedge
d_{2}\in[d_{1}+7,d_{1}+8]\\}$. Hence, TPNs and WTPNs variants are strictly
less expressive than their non-injective counterparts.

$\bullet$$p_{0}$$p_{1}$$p_{2}$$p_{3}$$p_{4}$$a$$[0,1]$$b$$[4,5]$$a$$[0,1]$$b$$[7,8]$
Figure 10: A TPN $\mathcal{N}_{2}$ with non-injective labeling.

###### Corollary 5.16

$BTPN^{\overline{inj}}<_{\mathcal{L}}BWTPN^{\overline{inj}}$

###### Proof 5.17

Inclusion $BTPN^{\overline{inj}}\leq_{\mathcal{L}}BWTPN^{\overline{inj}}$ is
straightforward from Definition 3.1. Now this inclusion is strict. Take the
example of Figure 9-a), and attach distinct labels to $t_{0}$ and $t_{1}$. The
language recognized cannot be encoded with a non-injective TPN, for the
reasons detailed in the proof of Theorem. 5.9.

To conclude on the effects of non-injective labeling, we can easily notice
that $BWTPN^{\overline{inj}}\leq_{\mathcal{L}}TA(\leq,\geq)$ because the
automaton construction of Definition 5.2 still works. Indeed, the automaton
construction depends on transitions fired in extended state classes, and not
on their labels. Hence, starting from a non-injective BWTPN, the construction
of Definition 5.2 gives a timed automaton that recognizes the same language.
As in the injective case, this relation is strict, because the example
$\mathcal{A}_{1}$ of Figure 8-a cannot be implemented by a waiting net in
$BWTPN^{\overline{inj}}$.

The last point to consider is whether allowing silent transitions increases
the expressive power of the model. Consider again the automaton
$\mathcal{A}_{1}$ of Figure 8-a. If transitions labeled by $\epsilon$ are
allowed, then the timed language $\mathcal{L}(\mathcal{A}_{1})$ can be encoded
by the TPN of Figure 8-c. It was shown in [15] that timed automata with
epsilon transitions are strictly more expressive than timed automata without
epsilon. We hence have $TA(\leq,\geq)<_{\mathcal{L}}TA_{\epsilon}(\leq,\geq)$.
We can also show that differences between WTPNs, TPN, and automata disappear
when silent transitions are allowed.

###### Theorem 5.18

$TA_{\epsilon}(\leq,\geq)=_{\mathcal{L}}BTPN_{\epsilon}=_{\mathcal{L}}BWTPN_{\epsilon}$

###### Proof 5.19

The equality $TA_{\epsilon}(\leq,\geq)=BTPN_{\epsilon}$ was already proved in
[6]. From Definition 3.1, we have
$BTPN_{\epsilon}\leq_{\mathcal{L}}WBTPN_{\epsilon}$. Further, for any waiting
net $\mathcal{W}\in BWTPN_{\epsilon}$, one can apply the construction of
Definition 5.2 to obtain a state class timed automaton $SCTA(\mathcal{W})$
(with $\epsilon$ transitions) recognizing the same language as $\mathcal{W}$.
We hence have
$BWTPN_{\epsilon}\leq_{\mathcal{L}}TA_{\epsilon}(\leq,\geq)=_{\mathcal{L}}BTPN_{\epsilon}$,
which allows to conclude that $TA_{\epsilon}(\leq,\geq),BTPN_{\epsilon}$, and
$BWTPN_{\epsilon}$ have the same expressive power.

Figure 11 summarizes the relations among different classes of nets and
automata, including TPNs and automata with stopwatches. An arrow
$\mathcal{M}_{1}\longrightarrow\mathcal{M}_{2}$ means that $\mathcal{M}_{1}$
is strictly less expressive than $\mathcal{M}_{2}$, and this relation is
transitively closed. Extensions of timed automata with stopwatches allow the
obtained model to simulate two-counters machines (and then Turing machines)
[11]. It is well known that unbounded TPNs can simulate Turing Machines too.
More surprisingly, adding stopwatches to bounded TPNs already gives them the
power of Turing Machines [8]. Obviously, all stopwatch models can simulate one
another. Hence, these models are equally expressive in terms of timed
languages as soon as they allow $\epsilon$ transitions. The thick dashed line
in Figure 11 is the frontier for Turing powerful models, and hence also for
decidability of reachability or coverability.

$BTPN$$TPN$$SwTPN$$BSwTPN$$BWTPN$$WTPN$$TA(\leq,\geq)$$TA$$SwTA$$\begin{array}[]{l}TA_{\epsilon}(\leq,\geq)\\\
=BTPN_{\epsilon}\\\
=BWTPN_{\epsilon}\end{array}$$TA_{\epsilon}$$BTPN^{\overline{inj}}$$BWTPN^{\overline{inj}}$$TPN^{\overline{inj}}$$WTPN^{\overline{inj}}$$\begin{array}[]{l}SwTPN_{\epsilon}=BSwTPN_{\epsilon}\\\
=TPN_{\epsilon}=WTPN_{\epsilon}\\\ =SwTA_{\epsilon}\end{array}$

Figure 11: Relation among net and automata classes, and frontier of
decidability.

##  6 Conclusion

We have proposed waiting nets, a new variant of time Petri nets, that measure
time elapsed since enabling of a transition while waiting for additional
control allowing its firing. This class obviously subsumes time Petri nets.
More interestingly, expressiveness of bounded waiting nets lays between that
of bounded TPNs and timed automata. Waiting nets allow for a finite
abstraction of the firing domains of transitions. A consequence is that one
can compute a finite state class graph for bounded WTPNs, and decide
reachability and coverability.

As future work, we will investigate properties of classes of WTPN outside the
bounded cases. In particular, we should investigate if being free-choice
allows for the decidability of more properties in unbounded WTPNs [3]. A
second interesting topic is control. Waiting nets are tailored to be guided by
a timed controller, filling control places in due time to allow transitions
firing. A challenge is to study in which conditions one can synthesize a
controller to guide a waiting net in order to meet a given objective.

## References

  * [1] P.A. Abdulla and A. Nylén.  Timed Petri nets and BQOs.  In ICATPN, LNCS 2075, p.53-70, 2001.
  * [2] S. Akshay, B. Genest, and L. Hélouët.  Decidable classes of unbounded Petri nets with time and urgency.  In F. Kordon and D. Moldt, editors, Application and Theory of Petri Nets and Concurrency - 37th International Conference, Petri Nets 2016, Toruń, Poland, June 19-24, 2016. Proceedings, volume 9698 of Lecture Notes in Computer Science, pages 301–322. Springer, 2016.
  * [3] S. Akshay, L. Hélouët, and R. Phawade.  Combining free choice and time in Petri nets.  J. Log. Algebraic Methods Program., 110, 2020.
  * [4] R. Alur and D.L. Dill.  A theory of timed automata.  Theor. Comput. Sci., 126(2):183–235, 1994.
  * [5] J. Bengtsson and W. Yi.  Timed automata: Semantics, algorithms and tools.  In Jörg Desel, Wolfgang Reisig, and Grzegorz Rozenberg, editors, Lectures on Concurrency and Petri Nets, Advances in Petri Nets, volume 3098 of Lecture Notes in Computer Science, pages 87–124. Springer, 2003.
  * [6] B. Bérard, F. Cassez, S. Haddad, D. Lime, and O. H. Roux.  The expressive power of time Petri nets.  TCS, 474:1–20, 2013.
  * [7] B. Berthomieu and M. Diaz.  Modeling and verification of time dependent systems using time Petri nets.  IEEE Trans. Software Eng., 17(3):259–273, 1991.
  * [8] B. Berthomieu, D. Lime, O.H. Roux, and F. Vernadat.  Reachability problems and abstract state spaces for time Petri nets with stopwatches.  Discret. Event Dyn. Syst., 17(2):133–158, 2007.
  * [9] F.D.J. Bowden.  Modelling time in petri nets.  In Proc. Second Australia-Japan Workshop on Stochastic Models, 1996\.
  * [10] G. Bucci, A. Fedeli, L. Sassoli, and E. Vicario.  Timed state space analysis of real-time preemptive systems.  IEEE Trans. Software Eng., 30(2):97–111, 2004.
  * [11] F. Cassez and K.G. Larsen.  The impressive power of stopwatches.  In C. Palamidessi, editor, CONCUR 2000 - Concurrency Theory, 11th International Conference, University Park, PA, USA, August 22-25, 2000, Proceedings, volume 1877 of Lecture Notes in Computer Science, pages 138–152. Springer, 2000.
  * [12] F. Cassez and O.H. Roux.  Structural translation from time Petri nets to timed automata.  Journal of Systems and Software, 79(10):1456–1468, 2006.
  * [13] A. Cheng, J. Esparza, and J. Palsberg.  Complexity results for 1-safe nets.  Theor. Comput. Sci., 147(1&2):117–136, 1995.
  * [14] G. Dantzig and B. C. Eaves.  Fourier-Motzkin Elimination and Its Dual.  J. Comb. Theory, Ser. A, 14(3):288–297, 1973.
  * [15] V. Diekert, P. Gastin, and A. Petit.  Removing epsilon-transitions in timed automata.  In R. Reischuk and M. Morvan, editors, STACS 97, 14th Annual Symposium on Theoretical Aspects of Computer Science, Lübeck, Germany, February 27 - March 1, 1997, Proceedings, volume 1200 of Lecture Notes in Computer Science, pages 583–594. Springer, 1997.
  * [16] D.L. Dill.  Timing assumptions and verification of finite-state concurrent systems.  In J. Sifakis, editor, Automatic Verification Methods for Finite State Systems, International Workshop, Grenoble, France, June 12-14, 1989, Proceedings, volume 407 of Lecture Notes in Computer Science, pages 197–212. Springer, 1989.
  * [17] J. Esparza.  Decidability and complexity of Petri net problems - an introduction.  In Proc. of Petri Nets, volume 1491 of LNCS, pages 374–428, 1998.
  * [18] D. de Frutos-Escrig, V.V. Ruiz, and O. Marroquín Alonso.  Decidability of properties of timed-arc Petri nets.  In M. Nielsen and D. Simpson, editors, Application and Theory of Petri Nets 2000, 21st International Conference, ICATPN 2000, Aarhus, Denmark, June 26-30, 2000, Proceeding, volume 1825 of Lecture Notes in Computer Science, pages 187–206. Springer, 2000.
  * [19] L. Hélouët and P. Agrawal.  Waiting nets.  In Luca Bernardinello and Laure Petrucci, editors, Proc. of PETRI NETS 2022, volume 13288 of LNCS, pages 67–89, 2022.
  * [20] L. Jacobsen, M. Jacobsen, M. H. Møller, and J. Srba.  Verification of timed-arc Petri nets.  In SOFSEM’11. LNCS 6543, p.46-72, 2011.
  * [21] N.D. Jones, L. H. Landweber, and Y. E. Lien.  Complexity of some problems in Petri nets.  Theor. Comput. Sci., 4(3):277–299, 1977.
  * [22] D. Lime and O.H. Roux.  Model checking of time Petri nets using the state class timed automaton.  Discret. Event Dyn. Syst., 16(2):179–205, 2006.
  * [23] E.W. Mayr.  An algorithm for the general Petri net reachability problem.  In Proceedings of the 13th Annual ACM Symposium on Theory of Computing, May 11-13, 1981, Milwaukee, Wisconsin, USA, pages 238–246. ACM, 1981.
  * [24] M. Menasche.  Analyse des réseaux de Petri temporisés et Application aux systèmes distribués.  PhD thesis, Univ. Paul Sabatier, Toulouse, 1982.
  * [25] M. Menasche and B. Berthomieu.  Time petri nets for analyzing and verifying time dependent communication protocols.  In Harry Rudin and Colin H. West, editors, Protocol Specification, Testing, and Verification, III, Proceedings of the IFIP WG 6.1 Third International Workshop on Protocol Specification, Testing and Verification, organized by IBM Research, Rüschlikon, Switzerland, 31 May - 2 June, 1983, pages 161–172. North-Holland, 1983.
  * [26] P. M. Merlin.  A Study of the Recoverability of Computing Systems.  PhD thesis, University of California, Irvine, CA, USA, 1974.
  * [27] R. Parrot, M. Briday, and O.H. Roux.  Timed Petri nets with reset for pipelined synchronous circuit design.  In D. Buchs and J. Carmona, editors, Application and Theory of Petri Nets and Concurrency - 42nd International Conference, Petri Nets 2021, Virtual Event, June 23-25, 2021, Proceedings, volume 12734 of Lecture Notes in Computer Science, pages 55–75. Springer, 2021.
  * [28] L. Popova-Zeugmann.  On time Petri nets.  J. Inf. Process. Cybern., 27(4):227–244, 1991.
  * [29] C. Rackoff.  The covering and boundedness problems for vector addition systems.  Theor. Comput. Sci., 6:223–231, 1978.
  * [30] C. Ramchandani.  Analysis of asynchronous concurrent systems by timed Petri nets.  PhD thesis, Massachusetts Institute of Technology, 1974.
  * [31] P.-A. Reynier and A. Sangnier.  Weak time Petri nets strike back!  In Proc. of CONCUR 2009, volume 5710 of LNCS, pages 557–571, 2009.
  * [32] V. V. Ruiz, F. C. Gomez, and D. de Frutos-Escrig.  On non-decidability of reachability for timed-arc Petri nets.  In PNPM, pages 188–. IEEE Computer Society, 1999.

##  Appendix A Fourier-Motzkin elimination

Fourier-Motzkin Elimination [14] is a method to eliminate a set of variables
$V\subseteq X$ from a system of linear inequalities over $X$. Elimination
produces another system of linear inequalities over $X\setminus V$, such that
both systems have the same solutions over the remaining variables. Elimination
can be done by removing one variable from $V$ after another.

Let $X=\\{x_{1},\dots x_{r}\\}$ be a set of variables, and w.l.o.g., let us
assume that $x_{r}$ is the variable to eliminate in $m$ inequalities. All
inequalities are of the form

$c_{1}.x_{1}+c_{2}.x_{2}+\dots+c_{r}.x_{r}\leq d_{i}$

where $c_{j}$’s and $d_{i}$ are rational values, or equivalently
$c_{r}.x_{r}\leq d_{i}-(c_{1}.x_{1}+c_{2}.x_{2}+\dots+c_{r-1}.x_{r-1})$

If $c_{r}$ is a negative coefficient, the inequality can be rewritten as
$x_{r}\geq b_{i}-(a_{i,1}.x_{1}+a_{i,2}.x_{2}+\dots a_{i,r-1}.x_{r-1})$, and
if $c_{r}$ is positive, the inequality rewrites as $x_{r}\leq
b_{i}-(a_{i,1}.x_{1}+a_{i,2}.x_{2}+\dots a_{i,r-1}.x_{r-1})$, where
$b_{i}=\frac{d_{i}}{c_{r}}$ and $a_{i}=\frac{c_{i}}{c_{r}}$.

We can partition our set of inequalities as follows.

  * •

inequalities of the form $x_{r}\geq b_{i}-\sum_{k=1}^{r-1}a_{ik}x_{k};$ denote
these by
$x_{r}\geq A_{j}(x_{1},\dots,x_{r-1})$ (or simply $x_{r}\geq A_{j}$ for
short), for $j$ ranging from $1$ to $n_{A}$ where $n_{A}$ is the number of
such inequalities;

  * •

inequalities of the form $x_{r}\leq b_{i}-\sum_{k=1}^{r-1}a_{ik}x_{k};$ denote
these by
$x_{r}\leq B_{j}(x_{1},\dots,x_{r-1})$ (or simply $x_{r}\leq B_{j}$ for
short), for $j$ ranging from $1$ to $n_{B}$ where $n_{B}$ is the number of
such inequalities;

  * •

inequalities $\phi_{1},\dots\phi_{m-(n_{A}+n_{B})}$ in which $x_{r}$ plays no
role.

The original system is thus equivalent to:
$\max\left(A_{1},\ldots,A_{n_{A}}\right)\leq
x_{r}\leq\min\left(B_{1},\ldots,B_{n_{B}}\right)\land\underset{i\in
1..m-(n_{A}+n_{B})}{\bigwedge}\phi_{i}$.

One can find a value for $x_{r}$ in a system of the form $a\leq x\leq b$ iff
$a\leq b$. Hence, the above formula is equivalent to :
$\max(A_{1},\ldots,A_{n_{A}})\leq\min(B_{1},\ldots,B_{n_{B}})\land\underset{i\in
1..m-(n_{A}+n_{B})}{\bigwedge}\phi_{i}$

Now, this inequality can be rewritten as system of $n_{A}\times
n_{B}+m-(n_{A}+n_{B})$ inequalities $\\{A_{i}\leq B_{j}\mid i\in 1..n_{A},j\in
1..n_{B}\\}\cup\\{\phi_{i}\mid i\in 1..m-(n_{A}+n_{B})\\}$, that does not
contain $x_{r}$ and is satisfiable iff the original system is satisfiable.

###### Remark A.1

The Fourier-Motzkin elimination preserves finiteness and satisfiability of a
system of constraints. In general, the number of inequalities can grow in a
quadratic way at each variable elimination. However, when systems describe
firing domains of transitions and are in canonical form, they always contain
less than $2\cdot|T|^{2}+2\cdot|T|$ inequalities, and then elimination
produces a system of at most $2\cdot|T|^{2}+2\cdot|T|$ inequalities once
useless inequalities have been removed.

##  Appendix B Canonical forms : the Floyd-Warshall algorithm

A way to compute the canonical form for a firing domain $D$ (i.e. the minimal
set of constraints defining $\llbracket D\rrbracket$, the possible delays
before firing of transitions) is to consider this domain as constraints on
distances from variable’s value to value $0$, or to the value of another
variable. The minimal set of constraints can then be computed using a slightly
modified version of the Floyd-Warshall algorithm. Given a marking $M.N$, a
firing domain $D$ is defined with inequalities of the form:

  * •

for every transition $t_{i}\in\mathsf{enabled}(M)$ we have an inequality of
the form $a_{i}\leq\theta_{i}\leq b_{i}\,\forall t_{i}\in\mathsf{enabled}(M)$,
with $a_{i},b_{i}\in\mathbb{Q}^{+}$,

  * •

for every pair of transitions $t_{j}\not=t_{k}\in\mathsf{enabled}(M)^{2}$ we
have an inequality of the form $\theta_{j}-\theta_{k}\leq c_{jk}\,\forall
t_{j}\not=t_{k}\in\mathsf{enabled}(M)$ with $c_{jk}\in\mathbb{Q}^{+}$

We then apply the following algorithm:

Input: $D$, $E=\mathsf{enabled}(M)$;

for  _$t_{k}\in E$_ do

for  _$t_{j}\in E$_ do

for  _$t_{i}\in E$_ do

$r:=\min(r,b_{k}-a_{k})$

$a_{j}:=\max(a_{j},a_{k}-c_{kj})$

$b_{i}:=\min(b_{i},b_{k}+c_{ik})$

$c_{ij}:=\min(c_{ij},c_{ik}+c_{kj})$

end for

end for

end for

Output : $D^{*}$

Algorithm 1 Floyd-Warshall

The system of inequalities input to the algorithm is satisfiable iff at every
step of the algorithm $r\geq 0$. One can easily see that computing a canonical
form, or checking satisfiability of a firing domain can be done in cubic time
w.r.t. the number of enabled transitions.

##  Appendix C Difference Bound Matrices

An interesting property of firing domains is that they can can be represented
with Difference Bound Matrices (DBMs). To have a unified form for constraints
we introduce a reference value 0 with the constant value 0. Let
$\mathcal{X}_{0}=\mathcal{X}\cup\\{0\\}$. Then any domain on variables in
$\mathcal{X}$ can be rewritten as a conjunction of constraints of the form
$x-y\preceq n$ for $x,y\in\mathcal{X}_{0}$, $\preceq\in\\{<,\leq\\}$ and
$n\in\mathbb{Q}$.
For instance, $1\leq\theta_{1}\leq 2$ can be rewritten as
$\textbf{0}-\theta_{1}\leq-1\land\theta_{1}-\textbf{0}\leq 2$. Naturally, if
the encoded domain has two constraints on the same pair of variables, we use
their intersection: for a pair of constraints
$\textbf{0}-\theta_{1}\leq-1\land\textbf{0}-\theta_{1}\leq 0$ we only keep
$\textbf{0}-\theta_{1}\leq-1$

A firing domain $D$ can then be represented by a matrix $M_{D}$ with entries
indexed by $\mathcal{X}_{0}$:

  * •

For each constraint $\theta_{i}-\theta_{j}\preceq n$ of $D$,
$M_{D}[i,j]=(n,\preceq)$

  * •

For each constraint $a_{i}\leq\theta_{i}\leq b_{i}$, that is equivalent to
$\textbf{0}-\theta_{i}\leq-a_{i}$ and $\theta_{i}-\textbf{0}\leq b_{i}$, we
set $M_{D}[0,i]=(-a_{i},\preceq)$ and $M_{D}[i,0]=(b_{i},\preceq)$

  * •

For each clock difference $\theta_{i}-\theta_{j}$ that is unbounded in $D$,
let $D_{ij}=\infty$

  * •

Implicit constraints $\textbf{0}-\theta_{i}\leq 0$ and
$\theta_{i}-\theta_{i}\leq 0$ are added for all clocks.

### Canonical DBM

There can be infinite number of DBMs to represent a single set of solutions
for a domain $D$, but each domain has a unique canonical representation, that
can be computed as a closure of $M_{D}$ or equivalently as a closure on a
constraint graph. From matrix $M_{D}$, we create a directed graph
$\mathcal{G}(D)$: Nodes of the graph are variables 0 and variables
$\theta_{1},\theta_{n}$. For each entry of the form $M_{D}[ij]=(n,\preceq)$ we
have an edge from node $\theta_{j}$ to $\theta_{i}$ labeled with $n$. The