Loïc Hélouët
email: loic.helouet@inria.fr

Pranay Agrawal
email: pranay.agrawal@ens-paris-saclay.fr

Waiting Nets (Extended Version)

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. For many systems, one wants to 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 decoupling time measurement and control. Their semantics ignores clocks 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 and show that they are strictly more expressive than TPNs.

Introduction

Time Petri nets (TPNs) are an interesting model to specify cyber-physical systems introduced in [START_REF] Merlin | A Study of the Recoverability of Computing Systems[END_REF]. 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 [α t , β t ] to every transition t. If t has been enabled for at least α t time units it can fire. If t has been enabled for β 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 [START_REF] Esparza | Decidability and complexity of Petri net problems -an introduction[END_REF] (coverability [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF], reachability [START_REF] Mayr | An algorithm for the general Petri net reachability problem[END_REF], boundedness [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF]...) are undecidable for TPNs. Yet, for the class of bounded TPNs, reachability [START_REF] Popova-Zeugmann | On time Petri nets[END_REF] 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 [START_REF] Berthomieu | Modeling and verification of time dependent systems using time Petri nets[END_REF][START_REF] Lime | Model checking of time Petri nets using the state class timed automaton[END_REF].

There are many variants of Petri nets with time. An example is timed Petri nets (TaPN), 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 wellquasi-ordering techniques allow to solve coverability or boundedness problems [START_REF] Abdulla | Timed Petri nets and BQOs[END_REF][START_REF] Reynier | Weak time Petri nets strike back![END_REF]. However, reachability remains undecidable [START_REF] Ruiz | On non-decidability of reachability for timed-arc Petri nets[END_REF]. We refer readers to [START_REF] Jacobsen | Verification of timed-arc Petri nets[END_REF] for Reachability coverability Boundedness Time Petri Nets Undecidable [START_REF] Jones | Complexity of some problems in Petri nets[END_REF] Undecidable [START_REF] Jones | Complexity of some problems in Petri nets[END_REF] Undecidable [START_REF] Jones | Complexity of some problems in Petri nets[END_REF] (bounded) Decidable Decidable -Timed Petri nets Undecidable [START_REF] Ruiz | On non-decidability of reachability for timed-arc Petri nets[END_REF] Decidable [START_REF] De Frutos-Escrig | Decidability of properties of timed-arc Petri nets[END_REF][START_REF] Abdulla | Timed Petri nets and BQOs[END_REF] Decidable [START_REF] De Frutos-Escrig | Decidability of properties of timed-arc Petri nets[END_REF] (bounded) Decidable Decidable -Restricted Urgency

Undecidable [START_REF] Akshay | Decidable classes of unbounded Petri nets with time and urgency[END_REF] Decidable [START_REF] Akshay | Decidable classes of unbounded Petri nets with time and urgency[END_REF] Decidable [START_REF] Akshay | Decidable classes of unbounded Petri nets with time and urgency[END_REF] (bounded) Decidable Decidable -Stopwatch Petri nets Undecidable [START_REF] Berthomieu | Reachability problems and abstract state spaces for time Petri nets with stopwatches[END_REF] Undecidable [START_REF] Berthomieu | Reachability problems and abstract state spaces for time Petri nets with stopwatches[END_REF] Undecidable [START_REF] Berthomieu | Reachability problems and abstract state spaces for time Petri nets with stopwatches[END_REF] (bounded)

Undecidable [START_REF] Berthomieu | Reachability problems and abstract state spaces for time Petri nets with stopwatches[END_REF] Undecidable [START_REF] Berthomieu | Reachability problems and abstract state spaces for time Petri nets with stopwatches[END_REF] -TPNR Undecidable [START_REF] Parrot | Timed Petri nets with reset for pipelined synchronous circuit design[END_REF] Undecidable [START_REF] Parrot | Timed Petri nets with reset for pipelined synchronous circuit design[END_REF] Undecidable [START_REF] Parrot | Timed Petri nets with reset for pipelined synchronous circuit design[END_REF] (bounded)

Decidable [START_REF] Parrot | Timed Petri nets with reset for pipelined synchronous circuit design[END_REF] Decidable [ a survey on TaPN and their verification. Without any notion of urgency, TaPN cannot model delay expiration. In [START_REF] Akshay | Decidable classes of unbounded Petri nets with time and urgency[END_REF], a model mixing TaPN and urgency is proposed, with decidable coverability, even for unbounded 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 resources. To solve this problem, [START_REF] Berthomieu | Reachability problems and abstract state spaces for time Petri nets with stopwatches[END_REF] 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 [START_REF] Cassez | The impressive power of stopwatches[END_REF]. For similar reasons, time Petri nets with preemptable resources [START_REF] Bucci | Timed state space analysis of real-time preemptive systems[END_REF], 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 [α, β] time units when p and q are filled". This model is strictly more expressive than TPN, as TPN are a simple syntactic restriction of waiting nets. Waiting nets allow clocks of enabled transitions to reach their upper bounds, and wait for missing control to fire. A former attempt called Timed Petri nets with Resets (TPNR) distinguishes some delayable transitions that can fire later than their upper bounds [START_REF] Parrot | Timed Petri nets with reset for pipelined synchronous circuit design[END_REF]. 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, 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. Our last contribution is a study of the expressiveness of waiting nets w.r.t timed language equivalence. Interestingly, the expressiveness of bounded waiting nets lays between that of bounded TPNs and timed automata.

Preliminaries

We denote by R ≥0 the set of non-negative real values, and by Q the set of rational numbers. A rational interval [α, β] is the set of values between a lower bound α ∈ Q and an upper bound β ∈ Q. We also consider intervals without upper bounds of the form [α, ∞), to define values that are greater than or equal to α.

A clock is a variable x taking values in R ≥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 → R ≥0 that associates a positive or zero real value v(x) to every variable x ∈ 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 ≤ x, x ≤ b, a ≤ x -y or x -y ≤ b where a, b ∈ Q and x, y ∈ 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 φ, and write v |= φ iff replacing x by v(x) in φ yields a tautology. A constraint φ is satisfiable iff there exists a valuation v for X such that v |= φ. Constraints over real-valued variables can be encoded with Difference bound Matrices (DBMs) and their satisfiability checked in O(n 3 ) [START_REF] Dill | Timing assumptions and verification of finite-state concurrent systems[END_REF]. The domain specified by a constraint φ is the (possibly infinite) set of valuations that satisfy φ.

Given an alphabet Σ, a timed word is an element of (Σ × R + ) * of the form w = (σ 1 , d 1 )(σ 2 , d 2 ) . . . such that d i ≤ d i+1 . A timed language is a set of timed words. Timed automata [START_REF] Alur | A theory of timed automata[END_REF] are frequently used to recognize timed languages.

Definition 1 (timed automaton). A timed automaton A is a tuple A = (L, 0 , X, Σ, Inv, E, F ), where L is a set of locations, 0 ∈ L is the initial location, X is a set of clocks, Σ is an alphabet, Inv : L → Cons(X) is a map associating an invariant to every location. The set of states F ⊆ L is a set of final locations, and E is a set of edges. Every edge is of the form ( , g, σ, R,

) ∈ L × Cons(X) × Σ × 2 X × L.
Intuitively, the semantics of a timed automaton allows elapsing time in a location (in which case clocks valuations grow uniformly), or firing a discrete transition ( , g, σ, R, ) from location with clock valuation v if v satisfies guard g, and the valuation v obtained by resetting all clocks in R to 0 satisfies Inv( ). One can notice that invariants can prevent firing a transition. Every run of a timed automaton starts from ( 0 , v 0 ), where v 0 is the valuation that assigns value 0 to every clock in X. For completeness, we recall the semantics of timed automata in appendix. The timed language recognized by A is denoted L(A).

In the rest of the paper, we will denote by T A the class of timed automata. We will be in particular interested by the subclass T A(≤, ≥) in which guards are conjunctions of atomic constraints of the form x ≥ c and invariants are conjunctions of atomic constraints of the form x ≤ c. Several translations from TPNs to TAs have been proposed, and in particular, the solution of [START_REF] Lime | Model checking of time Petri nets using the state class timed automaton[END_REF] uses the state class graph of a TPN to build a time-bisimilar timed automaton in class T A(≤, ≥). This shows that one needs not the whole expressive power of timed automata to encode timed languages recognized by TPNs.

• p0 • p1 p2 p3 p4 Arrival [25, 28] Order [0, ∞] Departure [30, 32] • p0 • p1 p2 • p3 p4 p5 t0 [0, ∞) t1 [0, 3] t2 [5, 6]

Waiting Nets

TPN are a powerful model: they can be used to encode a two-counter machine, and can hence simulate the semantics of many other formal models. A counterpart to this expressiveness is that most problems (reachability, coverability, 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, in which timing information is symbolically represented by firing domains. For many applications, working with bounded resources is sufficient. However, TPN 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.

Consider the example of Figure 1, that represents 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 beginning of a run of the net. 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. The time constraint attached to Departure is an interval of the form [30,32]. 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". The TPN of Figure 1-a) does not implement this 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 more that 32 minutes in station, if the order is not released first. Similarly, Timed Petri nets, that do not have a notion of urgency, cannot encode this scenario where a transition has to fire after 32 time units.

• p0 Ad [0, ∞] p1 p2 Cp [1, 4] p3 So [0, 3] N o [0, 8] p4 p5 • p0 Ad [0, ∞] p1 p2 Cp [1, 4] p3 p6 So [0, 3] N o [0, 8] T o [3, 3] p4 p5 p7
Fig. 2. a) Decoupled time and control in a waiting net. b) ... with a timeout transition.

We propose an extension of TPNs called Waiting nets (WTPN 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.

Definition 2. A waiting net is a tuple W = P, C, T, • (), () • , α, β, λ, (M 0 • N 0 )
, where -P is a finite set of standard places, C is finite set of control places, such that P ∪C = ∅ and P ∩C = ∅. A marking M.N is a pair of maps M : P → N, N : C → N that associate an integral number of tokens respectively to standard and control places. -T is a finite set of transitions. Every t ∈ T has a label λ(t), -• () ∈ (N P ∪C ) T is the backward incidence function, () • ∈ (N P ∪C ) T is the forward incidence function, -(M 0 • N 0 ) ∈ N P ∪C is the initial marking of the net, α : T → Q + and β : T → Q + ∪ ∞ are functions giving for each transition respectively its earliest and latest firing times (α(t) ≤ β(t)).

Labeling map λ can be injective or not. To differentiate standard and control places in the preset of a transition, we will denote by • (t) the restriction of • (t) to standard places, and by c () the restriction of • () to control places. We will write M (p) = k (resp. N (c) = k) to denote the fact that standard place p ∈ P (resp. control place c ∈ C) contains k tokens. Given two markings M.N and M .N we will say that M.N is greater than M .N and write

M.N ≥ M .N iff ∀p ∈ P, M (p) ≥ M (p) and ∀c ∈ C, N (c) ≥ N (C).
Figure 2-a) is a waiting net modeling 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.

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. (Enabled, fully enabled, waiting transitions)

• A transition t is enabled in marking M.N iff M ≥ • (t) (
) := {t | M.N ≥ • t} • A transition t is waiting in M.N iff t ∈ Enabled(M ) \ FullyEnabled(M.N ) (t
is enabled, but is still waiting for the control part of its preset). We denote by Waiting(M.N ) the set of waiting transitions.

Obviously, FullyEnabled(M.N ) ⊆ 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 ∈ [α(t), β(t)]. We adopt an urgent semantics, i.e. when a transition is fully enabled and x t = β(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 • (t) and produces tokens in all places of (t) • . A consequence of this token movement is that some transitions are disabled, and some other transitions become enabled after firing of t.

Definition 4 (Transition Firing). Firing of a transition t from marking M.N is done in two steps. It first computes an intermediate marking M .N = M.N -• (t) obtained by removing tokens consumed by the transition from its preset. Then, a new marking M .N = M .N + (t) • is computed. We will write M.N t -→ M .N whenever Firing of t from M.N produces marking M .N A transition t i is newly enabled after firing of t from M.N iff it is enabled in M .N , and either it is not enabled in M .N , or it is a new occurrence of t. We denote by ↑ enabled(M.N, t) the set of transitions newly enabled after firing t from marking M.N .

↑ enabled(M.N, t) := {t i ∈ T | • (t i ) ≤ M.N -• (t)+(t) • ∧((t i = t)∨( • (t i ) ≥ M.N -• (t))}
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 | t ∈ T } and write x t = ⊥ if t ∈ enabled(M ). To be consistent, for every value r ∈ R, we set ⊥ + r := ⊥. Definition 5 (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 net is a pair (M 0 .N 0 , v 0 ), where v 0 (x t ) = 0 if t ∈ enabled(M 0 ) and v 0 (x t ) = ⊥ otherwise. A transition t is firable from configuration (M.N, v) iff it is fully enabled, and

v(x t ) ∈ [α(t), β(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.

∀t ∈ Waiting(M.N ), v (x t ) = min(β(t), v(x t ) + d) ∀t ∈ FullyEnabled(M.N ), v(x t ) + d ≤ β(t) and v (x t ) = v(x t ) + d ∀t ∈ T \ enabled(M ), v (x t ) = ⊥ (M.N, v) d -→ (M.N, v ) M • N ≥ • (t) M • N = M • N -• (t) + (t) • α(t) ≤ v(t) ≤ β(t) ∀t i ∈ T, v (t i ) =    0 if t i ∈↑ enabled(M.N, t) ⊥ if t i ∈ enabled(M ) v(t i ) otherwise (M • N, v) t -→ (M • N , v )
Timed moves let d ∈ R ≥0 time units elapse, but leave markings unchanged. We adopt an urgent semantics that considers differently fully enabled transitions and waiting transitions. If t is a fully enabled transitions then, t allows elapsing of d time units from (M.N, v) iff v(t) + d ≤ β(t). The new valuation reached after elapsing d time units is v(t) + d. If we already have v(t) = β(t), then t does not allow time elapsing. We say that firing of t is urgent, that is t has to be fired or disabled by the firing of another transition before elapsing time. If v(t) + d > β(t) then t becomes urgent before d time units, and letting a duration d elapse from (M.N, v) is forbidden. Urgency does not apply to waiting transitions, which can let an arbitrary amount of time elapse when at least one control places 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 increase up to the upper bound allowed by their time interval, and then freeze these clocks. So, for a waiting transition, we have v (t) = min(β(t), v(t) + d). We will write v ⊕ 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 ) is denoted (M • N, v) d -→ (M • N , v ).
M.N, v) to (M .N , v ) via transition t i ∈ T is de- noted (M • N, v) ti -→ (M • N , v ).
Overall, the semantics of a waiting net 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 6. A run of a Waiting net W from a configuration (M.N, v) is a sequence ρ = (M.N, v) e1 -→ (M 1 .N 1 , v 1 ) e2 -→ (M 2 .N 2 , v 2 ) • • • e k -→ (M k .N k , v k ),
where every e i is either a duration d i ∈ R ≥0 , or a transition t i ∈ T , and every

(M i-1 .N i-1 , v i-1 ) ei -→ (M i .N i , v i ) is a legal move of W.
We denote by Runs(W) the set of runs of W. 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 .N ≥ 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 ∈ P and p ∈ C, we have M (p) ≤ K and N (p ) ≤ 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 .N ≥ M.N reachable from (M 0 .N 0 , v 0 ). Remark 1. 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 are undecidable in general for unbounded waiting nets.

Given a run ρ = (M 0 .N 0 , v 0 ) e1 -→ (M 1 .N 1 , v 1 ) e2 -→ (M 2 .N 2 , v 2 ) • • • ,
M k-1 .N k-1 , v k-1 ) e k -→ (M k .N k , v k ), d i
is the sum of all durations in e 1 . . . e k-1 . The sequence t 1 .t 2 . . . is called the untiming of w ρ . The timed language of a waiting net is the set of timed words L(W) = {w ρ | ρ ∈ Runs(W)}. Notice that unlike in timed automata and unlike in the models proposed in [START_REF] Bérard | The expressive power of time Petri nets[END_REF], we do not define accepting conditions for runs of timed words, and hence consider that the timed language of a net is prefix closed. The untimed language of a waiting net W is the language L U (W) = {w ∈ T * | ∃w ρ ∈ L(W), w is the untiming of w ρ }. 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)

(d,t) -→ (M .N , v ) to denote the sequence of moves (M.N, v) d -→ (M.N, v ⊕ d) t -→ (M .N , v ).
Let us illustrate definitions 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, N o, So, Cp}, α(Ad) = α(N o) = α(So) = 0, α(Cp) = 1, β(Ad) = ∞, β(N o) = 8, β(So) = 3, β(Cp) = 4.
We also have • (So) = p 1 and c (So) = p 3 , (So) • = p 4 (we let the reader infer • () and () • for other transitions). The net starts in an initial configuration (M 0 .N 0 , v 0 ) where M 0 (p 0 ) = 1 and M 0 (p i ) = 0 for all other places in P , N 0 (p 3 ) = 0, v 0 (Ad) = 0 and v 0 (t) = ⊥ for all other transitions in T . From this configuration, one can let an arbitrary duration d 0 elapse before firing transition Ad, leading to a configuration M 1 .N 0 with M 1 (p 1 ) = M 1 (p 2 ) = 1, and v 1 (Cp) = v 1 (N o) = v 1 (So) = 0. Then, one can let a duration smaller than 4 elapse and fire N o, or let a duration between 1 and 4 time units elapse and fire Cp. Notice that the net cannot let more than 4 time units elapse before taking a discrete move, as firing of Cp becomes urgent 4 time units after enabling of the transition. Let us assume that Cp is fired after elapsing 2.3 time units. This leads to a new configuration (M 2 .N 2 , v 2 ) where

M 2 (p 1 ) = M 2 (p 2 ) = 1, N 2 (p 3 ) = 1, v 2 (N o) = v 2 (S o ) = 2.3.
In this net, firing of So can only occur after firing of Cp, but yet time measurement starts for So as soon as • (So) 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 , M 1 .N 0 , M 2 .N 2 described above, plus two additional markings M 3 .N 0 where M 3 (p 5 ) = 1 and M 4 .N 0 where M 4 (p4) = 1. 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. We give a more complex example in Appendix E.

Reachability

In a configuration (M.N, v) of a waiting net 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 W is bounded. For TPNs, the set of reachable valuations can be abstracted to get a finite set of domains, to build a state class graph [START_REF] Berthomieu | Modeling and verification of time dependent systems using time Petri nets[END_REF]. In this section, we show how to 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.

Let t be a transition with α(t) = 3 and β(t) = 12, and assume that t has been enabled for 1.6 time units. According to the semantics of WPNs, v(x t ) = 1.6, and t cannot fire yet, as x t < α(t). Transition t can fire only after a certain duration θ t such that 1.4 ≤ θ t ≤ 10.4. Similar constraints hold for all enabled transitions. We will show later that these constraint are not only upper and lower bounds on θ t s, but also constraints of the form θ i -θ j ≤ c ij .

Definition 7 (State Class, Domain).

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

a i ≤ θ i ≤ b i , where a i , b i ∈ Q + and t i ∈ Enabled(M ) θ j -θ k ≤ c jk . where ∀j, k j = k and t j , t k ∈ Enabled(M ).
A variable θ i in a firing domain D over variables θ 1 , . . . , θ 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 β(t i ) if t i is waiting. Hence, if a transition is fully enabled, and a i ≤ θ i ≤ 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. Now, maintaining an interval for values of θ i s is not sufficient. Allowing a transition t i to fire means that no other transition t j becomes urgent before firing of t i , i.e. that adding constraint θ i ≤ θ j for every fully enabled transition t j still allows to find a possible value for θ i . Then, assuming that t i fires, the new firing domain D over variables θ 1 , . . . , θ q will constrain the possible values of θ j s for all transitions t j that remain enabled after firing of t i . As time progresses, we have θ j = θ j -θ i , which gives rise to diagonal constraint of the form θ j -θ k ≤ c jk after elimination of variables appearing in D.

A firing domain D defines a set of possible values for θ i s. We denote by D the set of solutions for a firing domain D. Now, the way to define a set of solutions is not unique. We will say that D 1 , D 2 are equivalent, denoted

D 1 ≡ D 2 iff D 1 = D 2 .
A set of solutions D is hence not uniquely defined, but fortunately, a unique representation called a canonical form exists.

Definition 8 (Canonical Form). The canonical form of a firing domain D is the unique domain

D * = a * i ≤ θ i ≤ b * i θ j -θ k ≤ c * jk .
, where

a * i = Inf (θ i ), b * i = Sup(θ i ), and c * jk = Sup(θ j -θ k )
The canonical form D * is the minimal set of constraints defining D . If two sets of constraints are equivalent then they have the same canonical form. The constraints we consider are of the form

K 1 ≤ x ≤ K 2 and K 1 ≤ x -y ≤ K 2 ,
where K 1 , K 2 are rational values. This type of constraints can be easily encoded by Difference Bound Matrices [START_REF] Dill | Timing assumptions and verification of finite-state concurrent systems[END_REF], or by constraint graph (i.e., a graph where vertices represent variables or the value 0, and an edge from x to y of weight w x,y represents the fact that x -y ≤ w x,y .) A canonical form is obtained by computing the shortest paths from each pair x, y in the constraint graph (or as a closure operation on the DBM). This can be achieved using the Floyd-Warshall algorithm, in O(n 3 ), where n is the number of variables considered (see Appendix C for details and [START_REF] Bengtsson | Timed automata: Semantics, algorithms and tools[END_REF] for a survey on DBMs). The same algorithm can also be used to check satisfiability of a domain (D is satisfiable iff its constraint graph contains no negative cycle).

State classes of waiting nets have the same definition as those of TPNs, and constrain the remaining time before firing of each transition. The fact that transitions can be fully enabled or waiting does not affect representation of constraints, but only forces to stop progress of time for a transition t i when θ i can only take value 0, and to consider t i as non urgent if it is a waiting transition. In some sense, for transitions that have an empty place in c (), variable θ t will represent a time to upper bound of intervals rather than a time to fire.

Following the semantics of section 3, a transition t i can fire from a domain D if one can find a value for θ i that does not violate urgency of other fully enabled transitions. However, the upper bound of waiting transitions should not prevent t i from firing. To get rid of this upper bound, we can use the notion of projection.

Definition 9 (Projection). Let D be a firing domain with variables a i , b i , c jk set as in def. 7. The projection of D on its fully enabled transitions is a domain

D |f ull = {a i ≤ θ i ≤ b i | t i ∈ FullyEnabled(M.N )} ∪ {a i ≤ θ i ≤ ∞, | t i ∈ Waiting(M.N )} ∪ {θ j -θ k ≤ c jk ∈ D | t j , t k ∈ FullyEnabled(M.N )}. A transition t i can fire from a configuration (M.N, v) iff it is fully enabled and v(t i ) ∈ [α(t i ), β(t i )]
. Hence, from configuration (M.N, v), firing of t i is one of the next discrete moves iff there exists a duration θ i such that t i can fire from (M.N, v + θ i ), i.e., after letting duration θ i elapse, and no other transition becomes urgent before θ i time units. We will say that

t i is firable from a state class (M.N, D) iff M.N ≥ • (t i ) and D |f ull ∪ {θ i ≤ θ j | t j ∈ FullyEnabled(M.N )} is satisfiable. So, t i
can be the next transition to fire iff one can find a value θ j greater than or equal to θ i that does not exceed b j for every fully enabled transition t j .

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 = {α(t i ) ≤ θ i ≤ β(t i ) | t i ∈ 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 .N , D ) reachable after firing of t. Note that we only need to consider t ∈ FullyEnabled(M.N ), as t can fire only when N > c (t). Computing M .N follows the usual firing rule of a Petri net: M .N = M.N -• (t) + (t) • and we can hence also compute ↑ enabled(M.N, t), enabled(M .N ) and FullyEnabled(M .N ). 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 will show in the rest of the section that the successor relation for Waiting nets can be effectively computed. It differs from that of TPNs, because it cannot abstract all timing information, and it is not deterministic either. However, it remains finite.

Consider the waiting net of Figure 1-b. This net starts in a configuration

C 0 = (M 0 .N 0 , v 0 ) with M 0 (p 0 ) = M 0 (p 1 ) = M 0 (p 3 ) = 1 M 0 (p) =
0 for every other place, and N 0 (p 2 ) = 0. From this configuration, one can let an arbitrary amount of time δ ∈ R ≥0 elapse. If 0 ≤ δ < 3, then the value of clock x 1 is still smaller than the upper bound β(t 1 ) = 3. Then, if one fires t 0 from

C 0 = (M 0 .N 0 , v 0 + δ), the net reaches a new configuration C 1 = (M 1 .N 1 , v 1 ) where M 1 (p 1 ) = M 1 (p 3 ) = 1, M 1 (p) = 0 for every other place, and N 0 (p 2 ) = 1. We have v 1 (x 0 ) = 0, v 1 (x 1 ) = v 1 (x 2 ) = δ.
One can still wait before firing t 1 in configuration, i.e., t 1 is not urgent and can fire immediately of within a duration 3 -δ. Now, if 3 ≤ δ < 5, then v 1 (x 1 ) = 3, v 1 (x 2 ) < 5 so transition t 1 is urgent and must fire, and transition t 2 still has to wait before firing. Hence, choosing 3 ≤ δ < 5 forces to fire t 1 immediately after t 0 . Conversely, if δ ≥ 5 then after firing t 0 , the net is in configuration [START_REF] Bengtsson | Timed automata: Semantics, algorithms and tools[END_REF][START_REF] Bérard | The expressive power of time Petri nets[END_REF], 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 by domain D.

C 2 = (M 1 .N 1 , v 2 ) where v 2 (x 1 ) = 3 and v 2 (x 2 ) ∈
Definition 10 (Upper Bounds Ordering). Let M.N be a marking, D be a firing domain with constraints of the form

a i ≤ θ i ≤ b i . Let B M.N,D = {b i | t i ∈ 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 = ∞.
Consider a transition t f firable from C = (M.N, D). This means that there is a way to choose a delay θ 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 θ f in a finite set of intervals, and find which transitions reach their upper bound when θ f belongs to an interval. Recall that θ f ≤ θ j for every fully enabled transition t j . This means that when considering that t f fires after a delay θ f such that bnd i ≤ θ f ≤ bnd i+1 , as D also gives a constraint of the form replacing every variable θ i by expression θ i -b eliminating every θ k whose upper bound is b, computing the normal form for the result and renaming all θ i to θ 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 ∈ waiting(M.N ) if x t k ≥ β(t k ), variable θ k , that represents the time needed to reach the upper bound to the interval is not meaningful anymore (as it should remain 0 until t k fires or gets disabled). So the only information to remember is that t k will be urgent as soon as it becomes fully enabled.

a f ≤ θ f ≤ b f , considering an interval such that bnd i is greater than min{b j ∈ B M.N,D | t j ∈ FullyEnabled(M.N )} or smaller than a f leads to inconsistency of constraint D |f ull ∪ tj ∈FullEnabled(M.N ) θ f ≤ θ j ∧bnd i ≤ θ f ≤ bnd i+1 . We denote by B t f M.N,

Definition 12 (Successors).

A successor of a class C = (M.N, D) after firing of a transition t f is a class C = (M .N , D ) such that M .N is the marking obtained after firing t f from M.N , and D is a firing domain reached after firing

t f in some interval [b r , b r+1 ] with b r , b r+1 consecutive in B t f M.N,D .
Given C and a firable transition t f , we can compute the set Post(C, t f ) of successors of C, i.e. Post(C,

t f ) := {(M • N , next r (D, t f )) | b r ∈ B t f M.N,D ∪ {0}}.
The next marking is the same for every successor and is

M •N = M •N -• t f +t •
f . We then compute next r (D, t f ) as follows: 1) Time progress: We successively progress time from D to bounds b 1 < b 2 < • • • < b r to eliminate variables of all enabled transitions reaching their upper bounds, up to bound r. We call D r the domain obtained this way. Every transition t k in Enabled(M.N ) that has no variable θ 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 ≤ θ f ≤ b r+1 ), and for every transition t j ∈ FullyEnabled(M )\{t f }, we add to D r the inequality θ f ≤ θ j . This set of constraints tells that no other transition was urgent when t f has been fired. Let us call D u 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 ≤ θ j ≤ 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 possible value of θ f due to urgency of other transitions.

3) Substitution of variables: As t f fires after elapsing θ 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 = t f that has an associated constraint a j ≤ θ j ≤ b j we do a variable substitution reflecting the fact that the new time to fire θ j decreases w.r.t the former time to fire θ j . We set θ j := θ f +θ j . When this is done, we obtain a domain D u,br over a set of variables θ i1 , . . . θ 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 θ f , it introduced new relationships between remaining firing times of other transitions, i.e other θ i = θ f , that have to be preserved in the next state class. However, as t f is fired, in the next class, it is either newly enabled, or not enabled. We hence need to remove θ f from inequalities, while preserving an equivalent set of constraints. This is achieved by elimination of variable θ f from D u,br . This can be done with the well known Fourier-Motzkin elimination technique (see Appendix B for details). We proceed similarly with variable θ i for every transition t i that is enabled in marking M.N but not in M.N -• (t f ). After elimination, we obtain a domain D E,br 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 ∈↑ enabled(M.N, t f ) we add to D E,br the constraint α(t i ) ≤ θ i ≤ β(t i ). For every timed-out transition t k that becomes fully enabled, we add to D E,br the constraint θ 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 θ i to θ i to get a domain D F,br . Notice that this domain needs not be minimal, so we do a last normalization step (see Definition 8) to obtain a final canonical domain next r (D, t f ) = D F,br * .

As more than one transition can fire from (M.N, D), and as every transition has a different effect on remaining firing times of enabled transitions, it is clear that a state class can have more than one successor, even if a single transition is firable. Note also that these successors can have different sets of constraints. Let C be a state class and Post(C) be the set of successor classes of C. Then |Post(C)| ≤ |enabled(M.N )| 2 . Computing successors can be repeated from each class in P ost(C). For a given net W, and a given marking M 0 .N 0 , we denote by C(W ) the set of classes that can be built inductively. This set need not be finite, but we show next that this comes from markings, and that the set of domains appearing in state classes is finite.

Definition 13. (State Class Graph) The State Class Graph of a waiting net W is a graph SCG(W) = (C(W ), C 0 , →) where C 0 = (M 0 • N 0 , D 0 ), and C → C iff C ∈ P ost(C). Let ρ = (M 0 .N 0 , v 0 ) d1 -→ (M 0 .N 0 , v 0 ⊕ d 1 ) t1 -→ (M 1 .N 1 , v 1 ) . . . (M k .N k , v k ) be a run of W and π = (M 0 .N 0 , D 0 ).(M 1 .N 1 , D 1 ) . . . (M k .N k , D k ) be a path in SCG(W). We will say that ρ and π coincide iff ∀i ∈ 1..k, M i .N i = M i .N i ,
and for every step

(M i .N i , v i ) di -→ (M i .N i , v i ⊕ d i ) ti -→ (M i+1 .N i+1 , v i+1 ), there exists an interval [b r , b r+1 ] such that d i ∈ [b r , b r+1 ] and D i+1 = next r (D i , t i ).
Proposition 1 (Completeness). For every run ρ = (M 0 .N 0 , v 0 ) . . . (M k .N k , v k ) of W there exists a path π of SCG(W) such that ρ and π coincide.

Proof (sketch). The proof is done by induction on the length of runs. The base case considers the first transition firing. One 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 θ i -θ j ≤ c ij . The induction step is similar, and slightly more involved, because domains contain constrains involving pairs of variables. However, we show (Lemma 2) that along run ρ 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 ∈ [a i,f , b i,f ],
where a i,f , b i,f are respectively the lower and upper bounds on variable θ f at step i of the run. Hence, for every run of a waiting net there is a path that visits the same markings and maintains consistent constraints.

Proposition 2 (Soundness). Let π be a path of SCG(W). Then there exists a run ρ of W such that ρ and π coincide.

Proposition 1 shows that every marking reached by a run of a waiting net appears in its state class graph. The proof of Proposition 2 uses a similar induction on runs 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 3. The set of firing domains in SCG(W) is finite.

Proof (sketch). Domains are of the form {a i ≤ θ i ≤ b i } ti⊆T ∪ {θ i -θ j ≤ c i,j } ti,tj ⊆T . We can easily adapt proofs of [START_REF] Berthomieu | Modeling and verification of time dependent systems using time Petri nets[END_REF] (lemma 3 page 9) to show that every domain generated during the construction of the SCG has inequalities of the form This does not yet prove that the set of domains is finite. We define domains that are bounded and linear, i.e. upper and lower bounded by some constants, and where 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) show that variable elimination, reduction to a canonical form, etc. preserve bounds and linearity (a similar result was shown in [START_REF] Berthomieu | Modeling and verification of time dependent systems using time Petri nets[END_REF] 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. This property of waiting nets is essential, as waiting nets allow to stop clocks. Bounded Petri nets with stopwatches do not have a finite state class representation, because clock differences in domains can take any value. WPNs do not have this kind of problem because clocks are stopped at a predetermined instant (when they reach the upper bound of an interval).

a i ≤ θ i ≤ b i and θ i -θ j ≤ c ij , where 0 ≤ a i ≤ α(t i ), 0 ≤ b i ≤ β(t i ) and -α(t i ) ≤ c ij ≤ β(t i ).
Corollary 1. If W is a bounded waiting net then SCG(W) is finite.

Proof. States of SCG(W) are of the form (M.N, D) where M.N is a marking and D a domain for time to fire of enabled transitions. By definition of boundedness, there is a finite number of markings appearing in SCG(W). By Prop. 3, the set of domains appearing in SCG(W) is finite, so SCG(W) is finite.

More precisely, if a net is k P -bounded, there are at most k P P possible markings, and the number of possible domains is bounded by (2

• K W + 1) |T +1| 2 , where K W = max i,j βi αj
is an upper bound on the number of linear combinations of bounds appearing in domains. Hence the size of SCG(W) is in

O(k P P • (2 • K W + 1) |T +1| 2 )
. A direct consequence of Proposition 1, Proposition 2, and Corollary 1 is that many properties of bounded waiting nets are decidable.

Corollary 2 (Reachability and Coverability). The reachability and coverability problems for bounded waiting nets are decidable and PSPACE-complete.

Proof. For membership, given a target marking M t .N t it suffices to explore nondeterministically runs starting from (M 0 .N 0 , D 0 ) of length at most |SCG(W)| to find marking M t .N t , or to find a marking that covers M t .N t . Such reachability questions are known to be 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 [START_REF] Cheng | Complexity results for 1-safe nets[END_REF], and a (bounded) Petri net is a (bounded) waiting net without control places and with [0, ∞) 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 [START_REF] Esparza | Decidability and complexity of Petri net problems -an introduction[END_REF]. This question can be recast as a coverability question for waiting nets, thus establishing the hardness of coverability.

Expressiveness

A natural question is the expressiveness of waiting nets w.r.t other models with time. 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 M 1 and M 2 , we will write M 1 ≤ L M 2 when, for every model

X 1 ∈ M 1 , there exists a model X 2 in M 2 such that L(X 1 ) = L(X 2 ). Similarly, we will write M 1 < L M 2 if M 1 ≤ L M 2 and there exists a model X 2 ∈ M 2 such that for every model X 1 ∈ M 1 , L(X 2 ) = L(X 1 )
. Lastly, we will says that M 1 and M 2 are equally expressive and write

M 1 = L M 2 if M 1 ≤ L M 2 and M 1 ≤ L M 2 .
In the rest of this section, we compare bounded and unbounded waiting nets with injective/non-injective labeling, with or without silent transitions labeled by to timed automata, TPNs, Stopwatch automata, and TPNs with stopwatches.

We first have obvious results. It is worth nothing that every model with noninjective 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 [START_REF] Cassez | Structural translation from time Petri nets to timed automata[END_REF][START_REF] Lime | Model checking of time Petri nets using the state class timed automaton[END_REF]. We show next that one can extend the results of [START_REF] Lime | Model checking of time Petri nets using the state class timed automaton[END_REF], i.e. reuse the state class construction of section 4 to build a finite timed automaton A W that recognizes the same language as a waiting net W. As shown by Proposition 1 and Proposition 2, the state class graph SCG(W) is sound and complete. State class graphs abstract away the exact values of clocks and only remember constraints on remaining time to fire. If we label moves by the name of the transition used to move from a state class to the next one, we obtain an automaton that recognizes the untimed language of W. Further, one can decorate a state class graph with clocks and invariants to recover the timing information lost during abstraction.

Definition 14 (Extended State class

). An extended state class is a tuple C ex = (M.N, D, χ, trans, XP ), where M • N is a marking, D a domain, χ is a set of real-valued clocks, trans ∈ (2 T ) χ maps clocks to sets of transitions and XP ⊆ T is a set of transitions which upper bound have already been reached.

Extended state classes were already proposed in [START_REF] Lime | Model checking of time Petri nets using the state class timed automaton[END_REF] 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 ∈ χ 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 i ). Let C ex denote the set of all state classes. We can now define the state class timed automaton SCT A(W ) by adding guards and resets to the transitions of the state class graph, and invariants to state classes.

Definition 15 (State class timed automaton).

The state class timed automaton of W is a tuple SCT A(W) = (L, l 0 , X, Σ, Inv, E, F ) where:

-L ⊆ 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 ) = Enabled(M 0 .N 0 ) and XP 0 = ∅. -Σ = λ(T ), and X =

trans (x k ) =    trans(x k ) \ Disabled(M.N, t) if trans(x k ) Disabled(M.N, t) ↑ enabled(M.N, t) if x k = x i Undefined otherwise XP = XP ∩Enabled(M -• (t)) \ F ullyEnabled(M .N ) ∪{t k ∈ Enabled(M .N ) | θ k ∈ D } The guard g is set to α(t) ≤ trans -1 (t). Let U rgent(C ex , t, C ex ) = XP ∩ Enabled(M -• (t)) ∩ F ullyEnabled. The set of clocks reset is R = {x i } if some clock
is newly enabled, and R = ∅ otherwise. For the invariant, we have two cases. If U rgent(C ex , t, C ex ) = ∅ i.e. if there is no transition of XP that becomes fully enabled (and hence urgent) after firing t, the invariant Inv is set to

xj ∈ trans -1 (F ullyEnabled(M .N ), t k ∈ trans(xj ) ∩ F ullyEnabled(M .N ) x j ≤ β(t k ) . Conversely, if U rgent(C ex , t, C ex ) = ∅ the invariant is set to t k ∈U rgent(Cex,t,C ex ) trans -1 (t k ) ≤ 0 Proposition 4. Let W be a waiting net. Then L(SCT A(W)) = L(W).
Proof (sketch). Obviously, every sequence of transitions in L(SCT A(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 [α t , β t ] if some time elapses in a state before the firing of t, and at least β 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 SCT A(W) is also a timed word of W. We can reuse the technique of Prop. 1 and prove by induction on the length of runs of W that for every run of W, there exists a run of SCT A(W) with the same sequence of delays and transitions.

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 N of net, we will denote by B -N the bounded subclass of N , add the subscript if transitions with labels are allowed in the model, and a superscript inj if the labeling of transitions is non-injective. For instance B -W T P N inj denotes the class of bounded waiting nets with non-injective labeling and transitions. It is well known that adding moves to automata increases the expressive power of the model [START_REF] Diekert | Removing epsilon-transitions in timed automata[END_REF]. Similarly, allowing non-injective labeling of transitions increases the expressive power of nets. Lastly, adding stopwatches to timed automata or bounded time Petri nets make them Turing powerful [START_REF] Cassez | The impressive power of stopwatches[END_REF].

Theorem 1. BW T P N < L T A(≤, ≥).

Proof. From Proposition 4, we can translate every bounded waiting net W to a finite timed automaton SCT A(W). Notice that SCT A(W) uses only constraints of the form x i ≥ a in guards and of the form x i ≤ b in invariants. Thus, BW T P N ⊆ T A(≤, ≥). This inclusion is strict. Consider the timed automaton A 1 of Figure 3. Action a can occur between date 2 and 3 and b between date 4 and 5.The timed language of 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 A 1 . Remark 2. It was proved in [START_REF] Bérard | The expressive power of time Petri nets[END_REF] that timed automata (with -transitions) have the same expressive power as bounded TPNS with -transitions. These epsilon transitions can be used to "steal tokens" of a waiting transition, and prevent it from firing after a delay. This cannot be done with waiting nets without . Hence, bounded TPN with -transitions are strictly more expressive than waiting nets, and than waiting net with non-injective labeling. Remark 3. 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 with the example in Figure 3-a) that L(A 1 ) cannot be recognized by a waiting net. However, it is easily recognized by the timed Petri net of figure 3-b).

Theorem 2. T P N < L W T P N and BT P N < L BW T P N .

Proof (sketch). TPNS are WTPNS without control places so T P N ≤ L W T P N and BT P N ≤ L BW T P N . We can show that inclusions are strict with the net W of Figure 4, that recognizes language

L(W ) = {(t 0 , d 0 )(t 1 , 20) | 0 ≤ d 0 ≤ 20}.
Assuming that a TPN recognizes this language, it must contain the subnet of figure 4-b), for some values α, β. However, there is no assignment for α, β allowing to consider all values for d 0 in L(W ) (see appendix G for details).

Theorem 3. All injective classes are strictly less expressive than their noninjective counterparts, i.e. BT P N < L BT P N inj , T P N < L T P N inj , BW T P N < L BW T P N inj , and W T P N < L W T P N inj . Proof (sketch). With injective labeling, (W)TPNs can recognize unions of timed language, which is not the case for models with injective labeling. Let N 2 be the TPN of Figure 5. We have

L(N 2 ) = {(a, d 1 ).(b, d 2 ) | d 1 ∈ [0, 1] ∧ d 2 ∈ [d 1 + 4, d 1 + 5]} ∪ {(a, d 1 ).(b, d 2 ) | d 1 ∈ [0, 1] ∧ d 2 ∈ [d 1 + 7, d 1 + 8]}. L(N 2 )
is not recognized by any (waiting) net with injective labeling. Proof. Inclusion BT P N inj ≤ L BW T P N inj is straightforward from definition 2. Take the example of Figure 4-a). The language recognized cannot be encoded with a non-injective TPN, for the reasons detailed in the proof of Thm. 2.

To conclude on the effects of non-injective labeling, we can easily notice that BW T P N inj < L T A(≤, ≥) because the automaton construction of Definition 15 still works (one labels transitions of the automaton with labels attached to transitions and keep the same construction). The last point to consider is whether allowing silent transitions increases the expressive power of the model. It was shown in [START_REF] Diekert | Removing epsilon-transitions in timed automata[END_REF] that timed automata with epsilon transitions are strictly more expressive than without epsilon. We hence have T A(≤, ≥) < L T A (≤, ≥). We can also show that differences between WTPNs, TPN, and automata disappear when silent transitions are allowed. Theorem 4. T A (≤, ≥) = L BT P N = L BW T P N Proof. The equality T A (≤, ≥) = BT P N was already proved in [START_REF] Bérard | The expressive power of time Petri nets[END_REF]. Given BW T P N , one can apply the construction of Definition 15 to obtain a state class timed automaton (with transitions) recognizing the same language.

Figure 6 shows the relations among different classes of nets and automata, including TPNs and automata with stopwatches. An arrow M 1 -→ M 2 means that M 1 is strictly less expressive than M 2 , and this relation is transitively closed. All extensions with clocks and stopwatches allow the considered model to simulate runs of Turing Machines. Actually, it has been shown that these models can encode two-counters machines (and then Turing machines). Obviously, all stopwatch models can simulate one another. Hence, these models are equally expressive in terms of timed languages as soon as they allow transitions. The red dashed line in Figure 6 is the frontier for Turing powerful models, and hence also for decidability of reachability or coverability.

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 diagram 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 [START_REF] Akshay | Combining free choice and time in Petri nets[END_REF]. 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.

A Semantics of timed automata

Let A = (L, 0 , X, Σ, Inv, E, F ) be a timed automaton. A configuration of A is a pair ( , v) where ∈ L is a location, and v a valuation of clocks in X. Let v R:=0 denote a valuation v such that v (x) = 0 if x ∈ R and v (x) = v(x) otherwise. A discrete move via transition e = ( , g e , σ e , R, ) is allowed from ( , v) iff v |= g e (the guard of the transition is satisfied) and v R:=0 |= Inv( ). We will denote such moves by ( , v)

e -→ ( , v ). Let d ∈ R + , and let v + d denote a valuation such that v + d(x) = v(x) + d for every x ∈ X. A timed move of d time units is allowed if v + d |= Inv( ).
We will denote such moves by ( , v)

d -→ ( , v + d) A run of A starts from configuration ( 0 , v 0 )
, where v 0 is the valuation that associates value 0 to every clock. 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 ρ = ( 0 , v 0 )

d0 -→ ( , v 0 + d 0 ) e0 -→ ( 1 , v 1 ) . . .

B Fourier-Motzkin elimination

Fourier-Motzkin Elimination [START_REF] Dantzig | Fourier-Motzkin Elimination and Its Dual[END_REF] is a method to eliminate a set of variables V ⊆ X from a system of linear inequalities over X. Elimination produces another system of linear inequalities over X \ 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 , . . . 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 + • • • + c r .x r ≤ d i
where c j 's and d i are rational values, or equivalently c r .

x r ≤ d i -(c 1 .x 1 + c 2 .x 2 + • • • + c r-1 .x r-1 )
If c r is a negative coefficient, the inequality can be rewritten as x r ≥ b i -(a i,1 .x 1 + a i,2 .x 2 + . . . a i,r-1 .x r-1 ), and if c r is positive, the inequality rewrites as x r ≤ b i -(a i,1 .x 1 + a i,2 .x 2 + . . . a i,r-1 .x r-1 ), where b i = di cr and a i = ci cr . We can partition our set of inequalities as follows.

inequalities of the form x r ≥ b i -r-1 k=1 a ik x k ; denote these by x r ≥ A j (x 1 , . . . , x r-1 ) (or simply x r ≥ 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 ≤ b i -r-1 k=1 a ik x k ; denote these by x r ≤ B j (x 1 , . . . , x r-1 ) (or simply x r ≤ B j for short), for j ranging from 1 to n B where n B is the number of such inequalities; inequalities φ 1 , . . . φ m-(n A +n B ) in which x r plays no role.

The original system is thus equivalent to:

max (A 1 , . . . , A n A ) ≤ x r ≤ min (B 1 , . . . , B n B ) ∧ i∈1..m-(n A +n B ) φ i .
One can find a value for x r in a system of the form a ≤ x ≤ b iff a ≤ b. Hence, the above formula is equivalent to :

max(A 1 , . . . , A n A ) ≤ min(B 1 , . . . , B n B ) ∧ i∈1..m-(n A +n B ) φ i

Now, this inequality can be rewritten as system of n

A × n B + m -(n A + n B ) inequalities {A i ≤ B j | i ∈ 1..n A , j ∈ 1..n B } ∪ {φ i | i ∈ 1..m -(n A + n B )}, that
does not contain x r and is satisfiable iff the original system is satisfiable.

Remark 4. 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

• |T | 2 + 2 • |T | inequalities,

C 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 D , 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 ∈ enabled(M ) we have an inequality of the form

a i ≤ θ i ≤ b i ∀t i ∈ enabled(M ), with a i , b i ∈ Q + , -for every pair of transitions t j = t k ∈ enabled(M ) 2 we have an inequality of the form θ j -θ k ≤ c jk ∀t j = t k ∈ enabled(M ) with c jk ∈ Q +
We then apply the following algorithm:

Algorithm 1: Floyd-Warshall Input: D, E = enabled(M ); for t k ∈ E do for tj ∈ E do for ti ∈ E do r := min(r, b k -a k ) aj := max(aj, a k -c kj ) bi := min(bi, b k + c ik ) cij := min(cij, c ik + c kj ) end end end Output : D *
The system of inequalities input to the algorithm is satisfiable iff at every step of the algorithm r ≥ 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.

D 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 X 0 = X ∪ {0}. Then any domain on variables in X can be rewritten as a conjunction of constraints of the form x -y n for x, y ∈ X 0 , ∈ {<, ≤} and n ∈ Q. For instance, 1 ≤ θ 1 ≤ 2 can be rewritten as 0 -θ 1 ≤ -1 ∧ θ 1 -0 ≤ 2. Naturally, if the encoded domain has two constraints on the same pair of variables, we use their intersection: for a pair of constraints 0 -

θ 1 ≤ -1 ∧ 0 -θ 1 ≤ 0 we only keep 0 -θ 1 ≤ -1
A firing domain D can then be represented by a matrix M D with entries indexed by X 0 :

-For each constraint θ i -θ j n of D, M D [i, j] = (n, ) -For each constraint a i ≤ θ i ≤ b i , that is equivalent to 0 -θ i ≤ -a i and θ i -0 ≤ b i , we set M D [0, i] = (-a i , ) and M D [i, 0] = (b i , ) -For each clock difference θ i -θ j that is unbounded in D, let D ij = ∞ -Implicit constraints 0 -θ i ≤ 0 and θ i -θ i ≤ 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 G(D): Nodes of tha graph are variables 0 and variables θ 1 , θ n . For each entry of the form M D [ij] = (n, ) we have an edge from node θ j to θ i labeled with n. The tightest constraint between two variables θ i and θ j , is the value of the shortest path between the respective nodes in above graph. This can be done using Floyd-Warshall algorithm shown above.

E A complex state class graph example

Let us consider the example in figure 7. Notice that in this particular example, t 0 and t 1 are enabled from beginning, thus we can fire any of them nondeterministically. Suppose we fire t 1 , then we can fire t 7 . But when t 3 is fired, then after 5 seconds, t 5 has reached the upper bound of it interval [START_REF] Akshay | Decidable classes of unbounded Petri nets with time and urgency[END_REF][START_REF] Bengtsson | Timed automata: Semantics, algorithms and tools[END_REF] , and will be urgent as soon as there is a token in c 1 . Similarly, t 4 reaches its upper bound 4 seconds after firing of t 2 , and is urgent as soon as there is a token in c 0 . This does not necessarily means that it will fire, as a token in c 0 can be transferred to c 1 in 0 time by transition t 6 and conversely from c 1 to c 0 with transitions t 7 if it has been enabled for at least one time unit. Now, as soon as one of t 4/5 fires the net reaches a dead state and no further transitions can take place (assuming we fire t 2 and t 3 before firing t 4/5 ). We study the state class graph and untimed language of this example in appendix.

State Class Graph Here, we will show an example where we compute the state class graph of the waiting net given in Figure 7.

We have

C 0 = (M 0 • N 0 , D 0 ) with M 0 • N 0 = {p 0 , p 1 , p 2 }, enabled(M 0 ) = ∅, FullyEnabled(M 0 ) = {t 0 , t 1 , t 2 , t 3 } and D 0 =          θ 0 = 0 θ 1 = 0 0 ≤ θ 2 ≤ ∞ 0 ≤ θ 3 ≤ ∞
We will compute some interesting state classes of the state class graph according to Definition 12. We will not consider labeling of transition to simplify reading. First we will compute C 2 which can be reached as follows : ----------------------- -----------------------

• p0 • p1 • p2 p3 p4 k0 k1 t0 t1 t2 t3 t4 c0 c1 p6 p5 t6 t7 t5 [0, 0] [0, 0] [0, ∞] [0, ∞] [1, 4] [2, 5] [0, ∞] [1, ∞]
C 0 t1,0 --→ C 1 t3, * --→ C 2 We have C 1 = (M 1 •N 1 , D 1 ) with M 1 •N 1 = {p 1 , p 2 , k 1 },N 1 = {c 1 } enabled(M 0 ) = ∅, FullyEnabled(M 0 ) = {t 1 , t 2 , t 7 } and D 1 =      0 ≤ θ 2 ≤ ∞ 0 ≤ θ 3 ≤ ∞ 1 ≤ θ 7 ≤ ∞ Now, we have C 2 = (M 2 •N 2 , D 2 ) with M 2 •N 2 = {p 1 , p 4 , c 1 , k 1 }, enabled(M 2 ) = FullyEnabled(M 2 ) = {t 2 , t 5 , t 7 } and D 2 is computed as follows :      1 ≤ θ 7 ≤ ∞ 0 ≤ θ 2 ≤ ∞ Addition of firing rule : θ3≤θ2,θ7
→ 0 ≤ θ 3 ≤ ∞            θ 3 ≤ θ 7 , θ 2 0 ≤ θ 2 ≤ ∞ Substitution: θj :=θ3+θ j ----------------→ 0 ≤ θ 3 ≤ ∞ 1 ≤ θ 7 ≤ ∞            θ 3 ≤ θ 3 + θ 7 , θ 3 + θ 2 0 ≤ θ 3 + θ 2 ≤ ∞ Elimination ---------→ 0 ≤ θ 3 ≤ ∞ 1 ≤ θ 3 + θ 7 ≤ ∞      0 ≤ θ 7 , θ 2 -∞ ≤ θ 2 ≤ ∞ Addition of new constraints --------------------→ -∞ ≤ θ 7 ≤ ∞            0 ≤ θ 7 , θ 2 -∞ ≤ θ 2 ≤ ∞ Construction of Canonical form
→ -∞ ≤ θ 7 ≤ ∞ 2 ≤ θ 5 ≤ 5 D 2 =      0 ≤ θ 2 ≤ ∞ 0 ≤ θ 7 ≤ ∞ 2 ≤ θ 5 ≤ 5
Let us assume that we want to compute Post(C 2 , t 2 ) the set of successors of C 2 after firing t 2 . One can notice that C 2 has two successors, depending on whether t 5 has reached its upper bound or not. Let C 3 = (M 3 • N 3 , D 3 ) and

C 4 = (M 4 • N 4 , D 4 ) be as follows. We have M 3 .N 3 = M 4 • N 4 = {p 3 , p 4 , c 1 , k 1 }, enabled(M 3 ) = enabled(M 4 ) = {t 4 }, FullyEnabled(M 3 .N 3 ) = FullyEnabled(M 4 .N 4 ) = {t 7 , t 5 }, D 3 = next 0 (D 2 , t 2 ), and D 4 = next 5 (D 2 , t 2 )
We let the reader verify that

D 3 =      1 ≤ θ 4 ≤ 4 5 ≤ θ 5 ≤ 5 0 ≤ θ 7 ≤ ∞
We can compute D 4 as follows :

       0 ≤ θ 2 ≤ ∞ 0 ≤ θ 7 ≤ ∞
Addition of firing rule and condition: θ2≤θ7,θ5 and 5≤θ2≤∞

-------------------------------------------→ 2 ≤ θ 5 ≤ 5                θ 2 ≤ θ 5 , θ 7 0 ≤ θ 2 ≤ ∞ 0 ≤ θ 7 ≤ ∞ Substitution ---------→ 2 ≤ θ 5 ≤ 5 5 ≤ θ 2 ≤ ∞                θ 2 ≤ 5 + θ 5 , θ 2 + θ 7 0 ≤ θ 2 ≤ ∞ 0 ≤ θ 2 + θ 7 ≤ ∞ Elimination ---------→ 2 ≤ 5 + θ 5 ≤ 5 5 ≤ θ 2 ≤ ∞ 0 ≤ θ 7 ≤ ∞ Addition of new constraints --------------------→ θ 5 = 0      1 ≤ θ 4 ≤ 4 0 ≤ θ 7 ≤ ∞ Canonical Form ------------→ θ 5 = 0 D 4 =      1 ≤ θ 4 ≤ 4 0 ≤ θ 7 ≤ ∞ θ 5 = 0
Now, in state class C 4 , t 5 is an urgent transition and t 7 is firable immediately. There are two possible successors for C 4 , reached after firing t 5 or t 7 , but both transitions have to occur immediately.

F Proofs for Section 4

The following lemma shows that if a transition is firable, then one can always find an appropriate timing allowing for the computation of a successor. Lemma 1. Let (M.N, D) be a state class, let t f be a transition firable from that class. Then there exists a bound r ∈ B

t f M.N,D such that next r (D, t f ) is satisfiable. Proof. Let t f be such a firable transition from the state class (M • N, D). This means, θ f satisfies D ∧ tj ∈FullyEnabled(M •N ) θ f ≤ θ j . Now, since t f is firable, this implies t f ∈ E and ∀t j ∈ FullyEnabled(M • N ) a * f ≤ b j (i.e. t f
can be fired before any other transition becomes urgent) . . . [START_REF] Abdulla | Timed Petri nets and BQOs[END_REF].

Let [ bnd k , bnd k+1 ] be the smallest interval between two consecutive bounds of B M.N,D containing a * f . Such an interval exists as bnd 0 ≤ a * f ≤ b * f < ∞. Now, we know that elimination preserves satisfiability. So the successor do-

main next k (D, t f ) is satisfiable, because it is obtained by elimination from D ∧ tj ∈FullyEnabled(M •N ) θ f ≤ θ j ∧ bnd k ≤ θ f ≤ b k+1 which contains at least one solution with θ f = a *
f , and by adding new individually satisfiable constraints associated with newly enabled transitions. These constraints do not change satisfiability of domains obtained after elimination, because each one constrains only a single variable that was not used in the domain D E,b k . Hence, choosing r = k witnesses truth of the lemma.

Proposition 1 For every run ρ = (M 0 .N 0 , v 0 ) . . . (M k .N k , v k ) of W there exists a path π of SCG(W) such that ρ and π coincide.

Proof. Markings in ρ and a path π that coincide with ρ must be the same. It hence remains to show that there exists a consistent sequence of domains

D 1 . . . D k such that path π = (M 0 .N 0 .D 0 ).(M 1 .N 1 , D 1 ) . . . (M k .N k , D k ) is a path of SCG(W)
and coincides with ρ. We show it by induction on the size of runs.

-Base Case :

Let ρ = (M 0 .N 0 , v 0 ) e1=(d1,t1) -------→ (M 1 .N 1 , v 1 ). The corresponding path in SCG is of the form π = (M 0 .N 0 , D 0 ) t1 -→ (M 1 .N 1 , D 1 )
, where D 0 is already known. By definition we have v 0 (t) = 0 for every enabled transition in M 0 .N 0 and v 0 (t) = ⊥ for other transitions. After letting d 1 time units elapse, the net reaches configuration (M 0 .N 0 , v 0 ) where v 0

(t) = v 0 (t) + d 1 if t ∈ FullyEnabled(M 0 .N 0 ), v 0 (t) = min(v(t) + d 1 , β(t)) if t ∈ enabled(M 0 ) \ FullyEnabled(M 0 ) and v 0 (t) = ⊥ otherwise. Now v 1 is computed according to timed moves rules, which means v 1 (t) = 0 if t ∈↑ enabled(M 1 , t 1 ) v 1 (t) = v 0 (t) if t ∈ Enabled(M 0 ) ∩ Enabled(M 1 ), and v 1 (t) = ⊥ otherwise. Now, since ρ = (M 0 .N 0 , v 0 ) (d1,t1) ----→ (M 1 .N 1 , v 1
) is a valid move in W, t 1 as a valid discrete move after the timed move d 1 , which gives us the following condition :

         M 0 • N 0 ≥ • t 1 M 1 • N 1 = M 0 • N 0 -• t 1 + t • 1 α(t 1 ) ≤ v 0 (t 1 ) ≤ β(t 1 ) ∀t, v 1 (t) = 0 if ↑ enabled(t, M 1 , t 1 ) else v 0 (t)
Further, as t 1 can be the first transition to fire, we have v 0 (t i ) ≤ β i for every t i in FullyEnabled(M 0 ). As all clocks attached to fully enabled transitions have the same value d 1 , it means that for every t i we have d 1 ≤ β i . Let us now show that t 1 is firable from class C 0 . Transition t 1 is firable from M 0 .N 0 , D 0 iff there exists a value θ 1 such that α(t 1 ) ≤ v 0 (t 1 ) ≤ β(t 1 ), and iff adding to D 0 the constraint that for every transition fully enabled θ 1 ≤ θ j yields a satisfiable constraints. We can show that setting θ 1 = d 1 allows to find a witness for satisfiability. Clearly, from the semantics, we have α(t 1 ) ≤ θ 1 = d 1 ≤ β(t 1 ), and as no t fully enabled is more urgent than t 1 , we can find θ i , d 1 ≤ θ i ≤ β i , and hence θ i satisfies θ 1 ≤ θ i . As firability from D 0 holds, and M 0 • N 0 ≥ • (t 1 ), there exists D 1 that is a successor of D 0 such that (M 0 .N 0 , D 0 ).(M 1 .N 1 , D 1 ) is a path of SCG(W).

-Induction step:

Suppose that for every run ρ of size at most n of the waiting net, there exists a path π of size n in SCG(W) that coincides with ρ. We have to prove that it implies that a similar property holds for every run of size n + 1. Consider a run ρ from (M 0 .N 0 , v 0 ) to (M n .N n , v n ) of size n and the coinciding run π, of size n too, from (M 0 .N 0 , D 0 ) to (M n .N n , D n ). Assume that some transition t f is firable after a delay d, i.e., (M n .N n , v n )

(d,t f )
-→ (M n+1 .N n+1 , v n+1 ). We just need to show that t f is firable from C n = (M n .N n , D n ). As t f is firable from (M n .N n , v n ) after d time units, we necessarily have α(t f ) ≤ v n (t f ) + d ≤ β(t f ), and for every t j fully enabled v n (t f ) + d ≤ β(t j ) (otherwise t j would become urgent). For every transition t k enabled in (M n .N n , v n ), let us denote by r k the index in the run where t k is last enabled in ρ. We hence have that v n (t k ) = min(β i , i=r k +1..n d i ). In the abstract run π we have b i = β i -Σ k∈ri..n a k,f ) where a k,f is the lower bound of domain D k for the time to fire of the transition used at step k and symmetrically

a i = max(0, α i -Σ k∈ri..n b k,f ).
At every step of path π, at step k of the path, domain D k sets constraints on the possible time to fore of enabled transitions. In every D k , for every enabled transition t i , we have a k,i ≤ θ i ≤ b k,i for some values a k,i ≤ b k,i ≤ β i , and additional constraints on the difference between waiting times. In particular, the set of transitions enabled in M n .N n is not empty, and domain D n imposes that a n,f ≤ θ f ≤ b n,f . Transition t f is firable from D n iff adding one constraint of the form θ f ≤ θ i per fully enabled transitions still yields a satisfiable domain. Now, we can show that the time spent in every configuration of W satisfies the constraints on value for the time to fire allowed for the fired transition at every step. Lemma 2. Let ρ be a run of size n an π be an abstract run (of size n too) that coincide. Then, for every transition

(M i .N i , v i ) di,t i f -→ (M i+1 .N i+1 , v i+1 ) we have d i ∈ [a i,f , b i,f ]. Proof. A transition t i f can fire at date j∈1..i d j iff v i (t f ) ∈ [α i , β i ]. At ev-
ery step i of a run, we have a i,j = max(0, α j -q∈Rj+1..i-1 b q f ) and b i,j = max(0, β j -q∈Rj+1..i-1 a q f ) where b q f (resp. a q f ) is the upper bound (resp. the lower bound) of the interval constraining the value of firing time for the transition fired at step q. At step i if transition t j is newly enabled, then a i+1,j = α j and b i+1,j = β j . Otherwise, a i+1,j = max(0, a i,j -b i f ) and b i+1,j = max(0, b i,j -a i f ). At step i, if t i f was newly enabled at step i-1 then we necessarily have a i+1,j = α j , b i+1,j = β j v i (t f ) = 0, and hence d i+1 ∈ [a i+1,j , b i+1,j ]. Now, let us assume that the property is met up to step i. if transition t f fires at step i + 1, we necessarily have

α f ≤ v i (t f ) + d i+1 ≤ β f . This can be rewritten as α f ≤ q∈R f +1..i d q + d i+1 ≤ β f . Considering step i, we have a i,f i ≤ d i ≤ b i,f i ,and hence α f -b i,f i ≤ q∈R f +1..i-1 d q + d i+1 ≤ β f -a i,f i . we can continue until we get α f -q ∈ R f + 1..ib q,f q ≤ d i+1 ≤ β f -q ∈ R f + 1..ia q,f q , that is d i+1 ∈ [a i+1,f , b i+1,f ].
As one can wait d time units in configuration (M n .N n , v n ), it means that for every fully enabled transition t j , v n (t j ) + d ≤ β j . It now remains to show that setting θ f = d still allows for values for remaining variables in D n . Setting θ f = d and θ f ≤ θ i for every fully enabled transition amount to adding constraint d ≤ θ i to D n . Further, we have a n,f ≤ d ≤ b n,f . We can design a constraint graph for D n , where nodes are of the form {θ i | t i ∈ F ullyEnabled(M n .N n )} ∪ {x 0 } where x 0 represents value 0, and an edge from θ i to θ j has weight w > 0 iff θ i -θ j ≤ w. Conversely, a weight w ≤ 0 represents the fact that w ≤ θ i -θ j . Similarly, and edge of positive weight w from θ i to x 0 represents constraint θ i ≤ w and an edge of negative weight -w from x 0 to θ i represents the fact that w ≤ θ i . It is well known that a system of inequalities such as the constraints defining our firing domains are satisfiable iff there exists no negative cycle in its constraint graph. Let us assume that D n is satisfiable, but -→ θ i for every t i that is fully enabled. Hence, new edges are only edges from/to x 0 . If a negative cycle exists in CG(D n ), as D n is in normal form, this cycle is of size two or three. If it is of size two, it involves a pair of edges θ j bn,j -→ x 0 and x 0 -d -→ θ j . However, following lemma 2, d ≤ b n,i for every fully enabled transition t i , so the weight of the cycle cannot be negative. Let us now assume that we have a negative cycle of size three, i.e. a cycle involving θ i , θ f and x 0 , with edges

D n = D n θ f = 0 ∧ tiF ullyEnabled d ≤ θ i
θ i c -→ θ f d -→ x 0 -d -→ θ i .
This cycle has a negative weight iff c < 0. However, we know that θ i ≥ θ f , this is hence a contradiction. Considering a cycle with a value θ k instead of θ f leads to a similar contradiction, and we need not consider cycles of size more than 3 because D n is in normal form, and hence the constraint graph labels each edge with the weight of the minimal path from a variable to the next one. Last, using lemma 1, as t f is firable from (M n .N n , D n ) there exists D n+1 ∈ P ost(C n , t f ), and hence π.(M n+1 .N n+1 , D n+1 ) is a path of the state class graph of W that coincides with ρ.

(M n .N n , v n ) (d,t f ) -→ (M n+1 .N n+1 , v n+1 )
Proof of Proposition 2 Let π be a path of SCG(W). Then there exists a run ρ of W such that ρ and π coincide.

Proof. Since ρ and π must coincide, if π = (M 0 •N 0 , D 0 ) t1 -→ (M 1 •N 1 , D 1 ) . . . (M k • N k , D k ), then ρ = (M 0 • N 0 , v 0 ) (d1,t1) -→ (M 1 • N 1 , v 1 ) . . . (M k • N k , v k ).
Since successive markings in both π and ρ are computed in the same way from presets and postsets of fired transitions (i.e.

M i •N i = M i-1 •N i-1 -• (t i )+(t i ) •
), we just have to show that for every abstract run π of SCG(W), one can find a sequence of val-

uations v 0 , v 1 , . . . v k such that ρ = (M 0 •N 0 , v 0 ) (d1,t1) -→ (M 1 •N 1 , v 1 ) . . . (M k •N k , v k )
is a run of W and such that firing t i after waiting d i time units is compatible with constraint D i . We proceed by induction on the length of runs. Base Case : Let π = (M 0 .N 0 , D 0 ) t1 -→ (M 1 .N 1 , D 1 ), where D 0 represents the firing domain of transitions from M 0 • N 0 . We have D 0 = {α i ≤ θ i ≤ β i | t i ∈ enabled(M 0 )}. Now, for t 1 to be a valid discrete move, there must be a timed move

d 1 s.t. (M 0 • N 0 , v 0 ) (d1,t1) ----→ (M 1 • N 1 , v 1 )
, which follows the condition :

         M 0 • N 0 ≥ • t 1 M 1 • N 1 = M 0 • N 0 -• t 1 + t • 1 α(t 1 ) ≤ v 0 (t 1 ) ⊕ d 1 ≤ β(t 1 ) ∀t, v 1 (t) = 0 if ↑ enabled(t, M 1 , t 1 ) else v 0 (t) ⊕ d 1
The conditions on markings are met, since t 1 is a transition from

M 0 • N 0 to M 1 • N 1 in the SCG.
Existence of a duration d 1 is also guaranteed, since, adding θ 1 ≤ θ i for every fully enabled transition t i to domain D 0 still allows firing t 1 , i.e. finding a firing delay θ 1 . Hence choosing as value d 1 any witness for the existence of a value θ 1 guarantees that no urgency is violated (valuation v 0 (t i )+d 1 is still smaller than β i for every fully enabled transition t

i ). Let ρ = (M 0 .N 0 , D 0 ) (d1,t1) ----→ (M 1 .N 1 , v 1 )
, where v 1 is obtained from v 0 by elapsing d 1 time units and then resetting clocks of transitions newly enabled by t 1 . Then ρ is compatible with π. General Case : Assume that for every path π n of the state class graph SCG(W) of size up to n ∈ N, there exists a run ρ n of W such that ρ n and π n coincide. We can now show that, given a path

π n = (M 0 • N 0 , D 0 ) t1 -→ (M 1 • N 1 , D 1 ) . . . (M n • N n , D n ) and a run ρ n = (M 0 • N 0 , v 0 ) (d1,t1) -→ (M 1 • N 1 , v 1 ) . . . (M n • N n , v n ) such
that ρ n and π n coincide, and an additional move

(M n .N n , D n ) t f -→ (M n+1 .N n+1 , D n+1 ) via transition t f , we can build a run ρ n+1 such that π n+1 = π n .(M n .N n , D n ) t f -→ (M n+1 .N n+1 , D n+1
) and ρ n+1 coincide. We have D n+1 = next r (D n , t f ) ∈ Post(D n ) for some bound r. As we want ρ n+1 and π n+1 to coincide, we necessarily have

ρ n+1 = ρ n .(M n .N n , v n ) (d,t f ) -→ (M n+1 .N n+1 , v n+1 ), i.e. M n+1 .N n+1 ,
(t i ) = min(β i , j∈ri+1..n d j ), a n,j = α j - q∈rj +1..n b q,t q f , and b n,j = β j - q∈rj +1..n a q,t q f If (M n .N n , D n ) t f -→ (M n+1 .N n+1 , D n+1 ) is enabled, then we necessarily have that D n ∪ θ f ≤ θ i is satisfiable. Let us choose d = θ f = a n,j and show that this fulfills the constraints to fire t f in ρ n+1 v n (t i ) + d ≤ β i iff v n (t i ) + α j - b q∈rj +1.
.n q,t q f ≤ β i , for every fully enabled transition t i . iff q∈rj +1..n d q + α j -q∈rj +1..n b q,t q f ≤ β i As we are looking for a run that coincides with π n+1 , we can assume wlog that we always choose the smallest value for d q , i.e. we choose d q = a q,t q f . Hence, the inequality rewrites as q∈rj +1..n a q,t q f + α j -q∈rj +1..n b q,t q f ≤ β i , or equivalently α j -q∈rj +1..n b q,t q f ≤ β i -q∈rj +1..n a q,t q f . This amount to proving a n,j ≤ b n,i . We can do a similar transformation to transform

v n (t f )+d ∈ [α f , β f ] into an inequality v n (t f )+α j - q∈rj +1..n b q,t q f ≤ β f , then transformed into a n,f ≤ b n,f , and α f ≤ v n (t f ) + d into α f ≤ v n (t f )+α j - q∈rj +1..n b q,t q f , and then α f ≤ q∈rj +1..n a q,t q f +α f - q∈rj +1..n
b q,t q f , which can be rewritten as a q,t q f ≤ b q,t q f . As D n ∪ θ f ≤ θ i is satisfiable, the conjunction of these inequalities holds too. Lemma 3. (Boundedness) For all i, j, k the constants a i , b i and c jk , of a domain of any state class graph have the following bounds :

0 ≤ a i ≤ α(t i ) 0 ≤ b i ≤ β(t i ) -α(t k ) ≤ c jk ≤ β(t j )
Proof. First of all, every variable θ i represents minimal and maximal times to upper bounds of interval, so by definition it can only be a positive value. We hence have 0 ≤ a i , 0 ≤ b i . Now to prove a i ≤ α(t i ) and b i ≤ β(t i ) always hold, we will study the effect of every step to compute next r (D, t f ).

Let us recall how next r (D, t f ) is built. We first add θ f ≤ θ i to D for every fully enabled transition t i , and the inequality b r ≤ θ f ≤ b r+1 . We then do a variable substitution as follows. We write:

θ j :=      b j + θ j if b j ≤ b r and enabled(M ) \ FullyEnabled(M.N ) θ f + θ j if b j > b r and FullyEnabled(M ) 0 otherwise
After variable substitution we have inequalities of the form a

i ≤ θ i + b i ≤ b i , a i ≤ θ i + θ f ≤ b i , b r ≤ θ f ≤ b r+1 , θ f ≤ θ i , θ i -θ j ≤ c ij if t i , t j are both fully enabled, a i ≤ θ i + θ f ≤ b i ,
and θ i = 0 for every enabled transition t i reaching its upper bound b i

We use Fourier-Motzkin elimination to remove variable θ f . This elimination makes new positive values of the form a j = max(0, a j -b i ) or b j = max(0, b j -a i ) appear (See also Lemma 4). Yet, we still have a j ≤ α j and b j ≤ β j .

Then addition new constraints for newly enabled transitions do not change existing constraints, and for every newly enabled transition t i , we have α i ≤ θ i ≤ β i . The last step consist in computing a canonical form. Remember that canonical forms consist in computing a shortest path in a graph. Hence D * also preserves boundedness. (See also Lemma 4) Now, in the canonical form, we can consider bounds for θ j -θ k , knowing that both values are positive.

-a k ≤ θ j -θ k ≤ b j , and hence -α(t k ) ≤ c jk ≤ β(t j ). Definition 16. (linearity) Let Wn be a waiting net, and let K W = max i,j βi αj A domain D is linear (w.r.t. waiting net W) if, for every constraint in D, lower and upper bounds a i , b i of constraints of the form a i ≤ θ i ≤ b i and upper bounds c i,j of difference constraints of the form θ i -θ j ≤ c i,j are linear combination of α i 's and β i 's with integral coefficients in [-K W , K W ].

Obviously, the starting domain D 0 of a waiting net W is bounded and linear. We can now show that the successor domains reached when firing a particular transition from any bounded and linear domain are also bounded and linear. Lemma 4. Elimination of a variable θ i from a firing domain of a waiting net preserves boundedness and linearity.

Proof. Fourier-Motzkin elimination proceeds by reorganization of a domain D, followed by an elimination, and then pairwise combination of expressions (see complete definition of Fourier Motzkin elimination in appendix B). We can prove that each of these steps produces inequalities that are both linear and bounded.

Let D be a firing domain, and D the domain obtained after choosing the fired transition t f and the corresponding variable substitution. An expression in D of the form θ f -θ i ≤ c f,i can be rewritten as θ f ≤ c f,i + θ i . An expression of the form θ i -θ f ≤ c i,f can be rewritten as θ i -c i,f ≤ θ f . We can rewrite all inequalities containing θ f in such a way that they are always of the form exp ≤ θ f or θ f ≤ exp. Then, we can separate inequalities in three sets :

-D + , that contains inequalities of the form exp -≤ θ f , where exp -is either constant a f or an expression of the form θ i -c i,f . Let E -denote expression appearing in inequalities of this form. -D -, that contains inequalities of the form θ f ≤ exp + , where exp + is either constant b f or an expression of the form θ i + c f,i . Let E + denote expression appearing in inequalities of this form. -D θf that contains all other inequalities. The next step is to rewrite D into an equivalent system of the form D θf ∪ max(E -) ≤ θ f ≤ min(E + ),and then eliminate θ f to obtain a system of the form D θf ∪max(E -) ≤ min(E + ). This system can then be rewritten as D θf ∪{exp -≤ exp + | exp -∈ E -∧ exp + ∈ E + }. One can easily see that in this new system, new constants appearing are obtained by addition or substraction of constants in D, and hence the obtained domain is still linear.

At this point, nothing guarantees that the obtained domain is bounded by larger α's and β s. Let us assume that in D, we have 0 ≤ a i ≤ α i , 0 ≤ b i ≤ β i and -α k ≤ c j,k ≤ β j . Then the last step of FME can double the maximal constants appearing in D (for instance when obtaining θ j -c j,f ≤ θ i + c f,i or its equivalent θ j -θ i ≤ +c f,i + c j,f . However, values of a i 's and b i s can only decrease, which, after normalization, guarantees boundedness of θ j -θ i . Lemma 5. Reduction to canonical form preserves linearity.

Proof. It is well known that computing a canonical form from a domain D represented by a DBM Z D amounts to computing the shortest path in a graph representing the constraints. Indeed, a DBM is in canonical form iff, for every pair of indexes 0 ≤ i, j ≤ |T |, and for every index 0 ≤ k ≤ |T | we have Z(i, j) ≤ Z(i, k) + Z(k, j). The Floyd Warshall algorithm computes iteratively updates of shortest distances by executing instructions of the form Z(i, j) := min(Z(i, j), Z(i, k) + Z(k, j)). Hence, after each update, if Z(i, j) is a linear combination of α s and β s, it remains a linear combination. Lemma 6. Fourier Motzkin elimination followed by reduction to canonical form preserves boundedness and linearity.

Proof. From Lemma 4 and Lemma 5, we know that domains generated by FME + canonical reduction are linear. However, after FME, the domain can contain inequalities of the form a i ≤ θ i ≤ b i with a i ≤ a i ≤ α i and b i ≤ b i ≤ β i . However, it may also contain inequalities of the form x ≤ θ i -θ j ≤ y where -2 • max(α i ) ≤ x and y ≤ • max(β i ). Now, using the bounds on values of θ i s, the canonical form calculus will infer a i -b j ≤ θ i -θ j ≤ b i -a j , and we will have -α i ≤ θ i -θ j ≤ β j . Lemma 7. (Bounded Linearity) For all i, j, k the constants a i , b i and c jk , of a domain of any state class graph are linear in α's and β's Proof. Clearly, the constraints in D 0 are linear in α's and β's see Definition [START_REF] Dantzig | Fourier-Motzkin Elimination and Its Dual[END_REF], it remains to prove that, if D is bounded and linear, then for every fired transition t and chosen time bound r, next k (D r , t) is still bounded and linear. We already know that Fourier Motzkin Elimination, followed by canonical form reduction preserves boundedness and linearity (Lemma 6). Addition of new constraints do not change constants of existing constraints, and the constants of new constraints (of the form α i ≤ θ i ≤ β i are already linear. Further, these constraints are completely disjoint from the rest of the domain (there is no constraint of the form θ k -θ i ≤ c k,i for a newly enabled transition t i ). Hence computing a canonical form before or after inserting these variables does not change the canonical domain. So, computing D * after new constraints insertion preserves linearity, and Thus, the constants appearing in the constraints in domain next k (D r , t) are bounded and linear w.r.t. α's and β's.

Proposition 3 The set of firing domains in SCG(W) is finite.

Proof. We know that a domain in a SCG is of form :

a * i ≤ θ i ≤ b * i θ j -θ k ≤ c * jk .
By boundedness ( Lemma 3) we have proved that the constants a * s, b * s and c * s are bounded above and below by α s and β s up to sign, we have also proved that they are linear combinations of α s and β s( Lemma 7). Now, it remains to show that there can only be finitely many such linear combinations, which was shown in [START_REF] Berthomieu | Modeling and verification of time dependent systems using time Petri nets[END_REF]. Hence, the set of domains appearing in SCG(W) is finite.

G Proofs for section 5

Proof of Theorem 2 T P N < L W T P N and BT P N < L BW T P N .

Proof. Clearly, from Def. 2, we have T P N ≤ L W T P N and BT P N ≤ L BW T P N , as TPNS are WTPNS without control places. It remains to show that inclusions are strict. Consider the waiting net W in Figure 4. We have T = {t 0 , t 1 }, P = {p 0 , p 1 }, C = {c 0 } and M 0 .N 0 (p 0 ) = (1 0 0). Hence, from the starting configuration, t 0 is fully enabled and firable (because M 0 ≥ • (t 0 )), but t 1 is enabled and not firable (M 0 ≥ • (t 1 ) and N 0 (c 0 ) = 0). Every valid run of (W ) is of the form (1, 0, 0) t0,d0

---→ (0, 0, 1)

t1,d1

---→ (0, 1, 0) where 0 ≤ d 0 ≤ 20 and d 1 = 20. Thus the timed language of W is L(W ) = {(t 0 , d 0 )(t 1 , 20) | 0 ≤ d 0 ≤ 20}. Let us show that there exists no T P N that recognizes the language L(W ). In TPN, one cannot memorize the time already elapsed using the clocks of newly enabled transitions. A TPN N recognizing L(W ) should satisfy the following properties:

1. The T P N should contain at least two different transitions namely t 0 and t 1 2. t 0 and t 1 are the only transitions which fire in any run of N . 3. t 0 and t 1 are fired only once. 4. t 0 must fire first and should be able to fire at any date in [0, 20] units. 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 L(N ) = L(W). We can now show that it is impossible to build a net N satisfying all these constraints. Since t 1 must fire after t 0 , N must contain a subnet of the form shown in figure 4-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 T P N of Figure 4-b) can not remember the firing date of t 0 , nor let time elapse before t 0 fires. Let [α, β] be the time interval associated to t 1 , and consider the two extreme but legal firing dates of 0 , namely 0 and 20 time units. Allowing these two dates amounts to require that 0 + α(t 1 ) = 0 + β(t 1 ) = 20 + α(t 1 ) = 20 + β(t 1 ) = 20 which is impossible. Hence, there exists no T P N recognizing L(W). This shows that BT P N < L BW T P N . The proof easily extends to T P N < L W T P N , simply by adding an unbounded part of net that becomes active immediately after firing t 1 .

Proof of Theorem 3:

All injective classes are strictly less expressive than their non-injective counterparts, i.e. BT P N < L BT P N inj , T P N < L T P N inj , BW T P N < L BW T P N inj , and W T P N < L W T P N inj .

Proof. 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 σ labeling a transition t σ is constrained by time in a similar way in a word: if t σ is enabled at some date d, then t σ must occur later than date d + α. This remark also holds for distinct words with the same prefix: let w.(σ, d) be a timed word, with w = (σ 1 , d 1 ).(σ 2 , d 2 ) . . . (σ k , d k ). The possible values for d lay in an interval that only depend 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 σ. The union of this set of constraints need not be a single interval. Consider for instance the TPN of Figure 5, that defines the language L(N ) = {(a,

Fig. 1 .

 1 Fig. 1. A simple TPN a) and a simple waiting net b)

  As one can expect, waiting nets enjoy time additivity (i.e. (M.N, v) d1 -→ (M.N, v 1 ) d2 -→ (M.N, v 2 ) implies that (M.N, v) d1+d2 -→ (M.N, v 2 ), and continuity, i.e. if (M.N, v) d -→ (M.N, v ), then for every d < d (M.N, v) d -→ (M.N, v ). Discrete moves fire transitions that meet their time constraints, and reset clocks attached to transitions newly enabled by token moves. A discrete move relation from configuration (

  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 θ f indicates for which waiting transitions t 1 , . . . t k the clocks x t1 , . . . x t k measuring time elapsed since enabling has reached upper bounds β(t 1 ), . . . β(t k ). The values of these clocks become irrelevant, and hence the corresponding θ i 's have to be eliminated from the domains. Definition 11 (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 obtained by:

(

  M.N,D,χ,trans) χ ⊆ {x 1 , . . . x |T | } is a set of clocks -E is a set of transitions of the form (C ex , λ(t), g, R, C ex ). In each transition, C ex = (M.N, D, χ, trans, XP ) and C ex = (M .N , D , χ , trans , XP ) are two extended state classes such that (M .N , D ) -→ (M.N, D) is a move of the STG with D = next r (D

Fig. 3 .

 3 Fig. 3. a) A timed automaton A1 b) an equivalent timed Petri net

Fig. 4 .

 4 Fig. 4. a) A waiting net W b) a part of TPN needed to encode L(W).

Fig. 5 .

 5 Fig. 5. A TPN N2 with non-injective labeling. Corollary 3. BT P N inj < L BW T P N inj

Fig. 6 .

 6 Fig. 6. Relation among net and automata classes, and frontier of decidability.

  . The timed word associated with run ρ is the word w ρ = (σ e0 , dt 0 ) . . . (σ ei , dt i ) . . . where dt i = k=i-1 k=0 d k .

  and then elimination produces a system of at most 2 • |T | 2 + 2 • |T | inequalities once useless inequalities have been removed.

Fig. 7 .

 7 Fig. 7. A complex net with control places and cycles

  is not. It means that CG(D n ) has no cycle of negative weight, but D n has one. Now, the major difference between D n is that there exists an edgeθ f d -→ x 0 , another one x 0 -d -→ θ f ,and an edge x 0 -d

  d 1 ).(b, d 2 ) | d 1 ∈ [0, 1]∧d 2 ∈ [d 1 +4, d 1 +5]}∪{(a, d 1 ).(b, d 2 ) | d 1 ∈ [0, 1]∧d 2 ∈ [d 1 +7, d 1 +8]}.Hence, net variants and their non-injective counterparts do not recognize the same languages.

Table 1 .

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

	23]	-

  for every standard place p in the preset of t, M (p) ≥ • (t)(p)). We denote by Enabled(M ) the set of transitions which are enabled from marking M , i.e. Enabled(M) := {t | M ≥ • (t)}• A transition t is fully enabled in M.N iff, for every place in the preset of t,

M.N (p) ≥ • (t, p). FullyEnabled(M.N ) is the set of transitions which are fully enabled in marking M.N , i.e. FullyEnabled(M.N

  the timed word associated with ρ is the word w ρ = (t 1 , d 1 ) • (t 2 , d 2 ) • • • where the sequence t 1 • t 2 . . . is the projection of e 1 • e 2 • • • on T , and for every (t i , d i ) such that t i appears on move (

  , t). We can compute the set of transitions disabled by the firing of t from M.N , denoted Disabled(M.N, t) and from there, compute a new set of clocks χ .

We have χ = χ \ {x ∈ χ | trans(x) ⊆ Disabled(M.N, t)} if firing t does not enable new transitions. If new transitions are enabled, we have χ = χ \ {x ∈ χ | trans(x) ⊆ Disabled(M.N, t)} ∪ {x i }, where i is the smallest index for a clock in X that is not used. Similarly, we can set

  t f are fixed for both runs, v n+1 is unique once d and t f are set, so we just need to show that there exists a value for d such that ρ n+1 and π n+1 coincide.From (M n .N n , v n ), d time units can elapse iff v n (t i ) + d ≤ β i , for every transition t i fully enabled in M n .N n , andt f can fire from (M n .N n , v n ) iff v n (t f )+ d ∈ [α f , β f ].Let us denote by r i the index in π n , ρ n where transition t i is last newly enabled, and by a i,tj (resp b i,tj ) the lower bound (resp. upper bound) on value θ j in domain D i . Last let t i f be the transition fired at step i We have that v n