B Bérard

F Cassez

S Haddad
email: serge.haddad@lsv.ens-cachan.fr

D Lime

O H Roux

When are Timed Automata weakly timed bisimilar to Time Petri Nets?

Keywords: Time Petri Nets, Timed Automata, Weak Timed Bisimilarity

In this paper 4 , we compare Timed Automata (TA) and Time Petri Nets (TPN) with respect to weak timed bisimilarity. It is already known that the class of bounded TPNs is strictly included in the class of TA. It is thus natural to try and identify the subclass T A wtb of TA equivalent to some TPN for the weak timed bisimulation relation. We give a characterization of this subclass and we show that the membership problem and the reachability problem for T A wtb are P SP ACEcomplete. Furthermore we show that for a TA in T A wtb with integer constants, an equivalent TPN can be built with integer bounds but with a size exponential w.r.t. the original model. Surprisingly, using rational bounds yields a TPN whose size is linear.

Introduction

Time in Petri nets. Adding explicit time to classical models of dynamic systems was first done in the seventies for Petri nets [START_REF] Merlin | A study of the recoverability of computing systems[END_REF][START_REF] Ramchandani | Analysis of asynchronous concurrent systems by timed Petri nets[END_REF], with the aim to verify quantitative properties of systems. Since then, various timed models based on Petri nets were proposed. Among them, the two most prominent ones are Time Petri Nets (TPN) [START_REF] Merlin | A study of the recoverability of computing systems[END_REF][START_REF] Berthomieu | Modeling and verification of time dependent systems using time Petri nets[END_REF] and Timed Petri Nets (TdPN) [START_REF] Ramchandani | Analysis of asynchronous concurrent systems by timed Petri nets[END_REF][START_REF] Abdulla | Timed Petri Nets and BQOs[END_REF]. In TPNs, a time interval is associated with each transition and a transition can fire if its enabling duration belongs to its interval. Since time elapsing must not disable transitions, TPNs naturally model urgency requirements. Efficient verification methods have been designed for bounded TPNs (e.g. [START_REF] Berthomieu | Time Petri Nets Analysis with TINA[END_REF]) implemented in several tools [START_REF] Gardey | Roméo: A Tool for Analyzing Time Petri Nets[END_REF][START_REF] Berthomieu | Time Petri Nets Analysis with TINA[END_REF]. Roughly speaking, in TdPNs a time interval is associated with each arc, a token can be consumed along an input arc if its age belongs to the corresponding interval and the initial age of token produced along an output arc is non deterministically selected inside the corresponding interval. Contrary to TPNs, there is no urgency mechanism and tokens may become useless due to time elapsing. However the lazy behaviour of such nets has led to the design of verification methods for unbounded nets [START_REF] Abdulla | Decidability of Zenoness, Syntactic Boundedness and Token-Liveness for Dense-Timed Petri Nets[END_REF]. Time in finite automata. Timed Automata (TA), introduced in the seminal paper [START_REF] Alur | A theory of timed automata[END_REF] have yielded a significant breakthrough in the theory of modelling and analysis of timed systems. The most commonly used variant of TA, called Safety TA has been defined in [START_REF] Henzinger | Symbolic model checking for real-time systems[END_REF] and this is the one we study here. A TA is a finite automaton equipped with a set of clocks which evolve synchronously with time. Elementary constraints on clock values restrict the sojourn in a location and the firing of transitions. In addition, transitions may involve some clock reset. Extensions of this model have been subsequently proposed (e.g. diagonal or linear constraints, silent transitions, non deterministic updates, etc. [START_REF] Bouyer | Updatable Timed Automata[END_REF]). In these models, verification is based on a finite partition of clock values and is supported by various tools [START_REF] Yovine | Kronos: A Verification Tool for real-Time Systems[END_REF][START_REF] Pettersson | Uppaal2k[END_REF]. Expressiveness of timed models. Due to the diversity of time mechanisms involved in these models, their relative expressiveness is a natural issue. More precisely, given two different formalisms, some questions must be considered:

-Are they equally expressive? Otherwise is one formalism more powerful than the other? -Given a model of the first kind can we decide whether it is equivalent to a model of the second kind (membership problem)? In this case, can we build such an equivalent model?

Two standard equivalence criteria are the family of timed languages generated and the weak timed bisimilarity of the models. For instance, in the framework of TdPNs w.r.t. the language criterion, it has been shown that read arcs add expressive power and that TdPNs and TA are incomparable [START_REF] Bouyer | Timed Petri Nets and Timed Automata: On the Discriminating Power of Zeno Sequences[END_REF]. In the framework of TA w.r.t. the language criterion, it has been shown that silent transitions add expressive power [START_REF] Bérard | Characterization of the expressive power of silent transitions in timed automata[END_REF] and (very recently) that the corresponding membership problem is undecidable [START_REF] Bouyer | Undecidability Results for Timed Automata with Silent Transitions[END_REF].

Comparison of TA and TPNs. In [START_REF] Haar | Equivalence of Timed State Machines and safe Time Petri Nets[END_REF], the authors compare Timed State Machines (TSM, a restricted version of TA) and TPNs, giving a translation from TSM to TPN that preserves timed languages. In [START_REF] Bérard | Comparison of the Expressiveness of Timed Automata and Time Petri Nets[END_REF], we have designed a more general translation between TA and TPNs with better complexity. In [START_REF] Bérard | Comparison of Different Semantics for Time Petri Nets. Automated Technology for Verification and Analysis: Third International Symposium[END_REF], we studied the effect of different semantics for TPNs on expressiveness w.r.t. weak timed bisimilarity. Here, we are interested in comparing the expressive power of TA and TPN for weak timed bisimilarity. Recall that there are unbounded TPNs for which no bisimilar TA exists. This is a direct consequence of the following observation: the untimed language of a TA is regular which is not necessarily the case for TPNs. It was proved in [START_REF] Cassez | Structural Translation of Time Petri Nets into Timed Automata[END_REF] that bounded TPNs form a strict subclass of the class of timed automata, in the sense that for each bounded TPN N , there exists a TA which is weakly timed bisimilar to N but the converse is false. A similar result can be found in [START_REF] Lime | State class timed automaton of a time Petri net[END_REF], where it is obtained by a completely different approach. However given a TA, deciding whether there exists a bisimilar TPN remained an open question.

Our Contribution. In this work, we give a characterization of the maximal subclass T A wtb of timed automata which admit a weakly timed bisimilar TPN. This condition is not intuitive and relates to the topological properties of the so-called region automaton associated with a TA. To prove that the condition is necessary, we introduce the notion of uniform bisimilarity, which is stronger than weak timed bisimilarity. Conversely, when the condition holds for a TA, we provide two effective constructions of bisimilar TPNs: the first one with rational constants has a size linear w.r.t. the TA, while the other one, which uses only integer constants has an exponential size. From this characterization, we deduce that given a TA, the problem of deciding whether there is a TPN bisimilar to it, is P SP ACE-complete. Thus, we obtain that the membership problem is P SP ACE-complete. Finally we also prove that the reachability problem is P SP ACE-complete.

Outline of the paper. In section 2, we recall the definitions for Timed Transition Systems which are used to describe the semantics of TPNs and TA, and for timed bisimilarity relations. We also describe Timed Automata (TA) and the associated notions of zones and regions. Section 3 presents Time Petri Nets (TPNs) and explains the characterization of TA bisimilar to TPNs. The following sections are devoted to the proof for this characterization: section 4 defines the notion of uniform bisimulation and gives the proof that the condition is necessary, while sections 5 and 6 show that the condition is sufficient by exhibiting two constructions which differ by their complexity. We give complexity results in section 7 and we conclude in section 8.

Timed Transition Systems and Timed Automata

Notations. Let Σ be a finite alphabet, Σ * (resp. Σ ω ) the set of finite (resp. infinite) words of Σ and Σ ∞ = Σ * ∪ Σ ω . We also use Σ ε = Σ ∪ {ε} with ε (the empty word) not in Σ.

The sets N, Q ≥0 and R ≥0 are respectively the sets of natural, non-negative rational and non-negative real numbers. We denote by 0 the tuple v ∈ N n such that v(k) = 0 for all 1 ≤ k ≤ n. For a natural number K and a tuple

v ∈ R n ≥0 , we write v ≤ -→ K if v(k) ≤ K for all 1 ≤ k ≤ n.
For a non negative real number z, we denote by z the integral part of z (the greatest natural number which is less than or equal to z) and, similarly, by z the smallest natural number greater than or equal to z. We also denote by f ract(z) the fractional part of z.

Let g > 0 in N, we write N g = { i g | i ∈ N}. A tuple v ∈ Q n belongs to the g-grid if v(k) ∈ N g for all 1 ≤ k ≤ n.
An interval I of R ≥0 is a Q ≥0 -interval iff its left endpoint belongs to Q ≥0 and its right endpoint belongs to Q ≥0 ∪{∞}. We set I ↓ = {x | x ≤ y for some y ∈ I}, the downward closure of I and I ↑ = {x | x ≥ y for some y ∈ I}, the upward closure of I. We denote by I(Q ≥0 ) the set of Q ≥0 -intervals of R ≥0 .

Timed Transition Systems and Equivalence Relations

Timed transition systems describe systems which combine discrete and continuous evolutions. They are used to define and compare the semantics of time Petri nets and timed automata.

A Timed Transition System (TTS) is a transition system S = (Q, q 0 , →), where Q is the set of configurations, q 0 ∈ Q is the initial configuration and the relation → consists of either delay moves q d -→ q , with d ∈ R ≥0 , or discrete moves q a -→ q , with a ∈ Σ ε . Moreover, we require standard properties for the relation →: Time-Determinism: if q d --→ q and q d --→ q with d ∈ R ≥0 , then q = q 0-delay:

q 0 --→ q Additivity: if q d --→ q and q d --→ q with d, d ∈ R ≥0 , then q d+d ----→ q Continuity: if q d --→ q , then for every d and d in R ≥0 such that d = d + d ,
there exists q such that q d --→ q d ---→ q . These properties have been formally introduced in the framework of Algebra of Timed Processes [START_REF] Nicollin | An Overview and Synthesis on Timed Process Algebras In CAV'91, Aalborg, invited talk[END_REF] but are also satisfied in TTS studied here. With these properties, a run of S can be defined as a finite or infinite sequence of moves ρ = q 0

d 0 -→ q 0 a 0 -→ q 1 d 1 -→ q 1 a 1 -→ • • • q n d n
-→ q n . . . where discrete actions alternate with durations. For a finite run, we also write q d 0 a 0 ...d n ...

-------→ q . The word Untimed(ρ) in Σ ∞ is obtained by the concatenation a 0 a 1 . . . of labels in Σ ε (so empty labels disappear), and Duration(ρ) = |ρ| i=0 d i , where |ρ| is the length of ρ. From a TTS, we define the relation =

⇒⊆ Q × (Σ ∪ R ≥0 ) × Q for a ∈ Σ and d ∈ R ≥0 by: -q d = ⇒ q iff ∃ ρ = q w -→ q with Untimed(ρ) = ε and Duration(ρ) = d, -q a = ⇒ q iff ∃ ρ = q w -→ q with Untimed(ρ) = a and Duration(ρ) = 0.
Definition 1 (Weak Timed Bisimilarity). Let S 1 = (Q 1 , q 1 0 , → 1 ) and S 2 = (Q 2 , q 2 0 , → 2 ) be two TTS and let ≈ be a binary relation over

Q 1 × Q 2 .
We write q ≈ q for (q, q ) ∈ ≈. The relation ≈ is a weak timed bisimulation between S 1 and S 2 iff q 1 0 ≈ q 2 0 and for all a ∈ Σ ∪ R ≥0 : -if q 1 a = ⇒ 1 q 1 and q 1 ≈ q 2 then ∃q 2 a = ⇒ 2 q 2 such that q 1 ≈ q 2 ; -conversely, if q 2 a = ⇒ 2 q 2 and q 1 ≈ q 2 then ∃q 1 a = ⇒ 1 q 1 such that q 1 ≈ q 2 . Two TTS S 1 and S 2 are weakly timed bisimilar, written S 1 ≈ W S 2 , if there exists a weak timed bisimulation relation between them.

Strong timed bisimilarity would require similar properties for transitions labeled by a ∈ Σ ∪ R ≥0 , but with a -→ instead of a = ⇒. Thus it forbids the possibility of simulating a move by a sequence. On the other hand, weak timed bisimilarity is more precise than language equivalence and it is well-known to be central among equivalence relations between timed systems. In the rest of the paper, we abbreviate weak timed bisimilarity by bisimilarity and we explicitly name other equivalences when needed.

Timed Automata

First defined in [START_REF] Alur | A theory of timed automata[END_REF], the model of timed automata (TA) associates with a finite automaton a set of non negative real-valued variables called clocks. Let X be a finite set of clocks. A constraint over X is a conjunction of atomic formulas of the form x h for x ∈ X, h ∈ N and ∈ {<, ≤, ≥, >} and we write C(X) for the set of constraints.

Definition 2 (Timed Automaton). A Timed Automaton

A over alphabet Σ ε is a tuple (L, 0 , X, Σ ε , E, Inv) where -L is a finite set of locations with 0 ∈ L is the initial location, -X is a finite set of clocks, -E ⊆ L × C(X) × Σ ε × 2 X × L is a finite set of edges and -Inv ∈ C(X) L assigns an invariant to each location.
An edge e = , γ, a, R, ∈ E, also written γ,a,R ---→ , represents a transition from location to location with guard γ and reset set R ⊆ X. We restrict the invariants to conjunctions of terms of the form x h for x ∈ X, h ∈ N and ∈ {<, ≤}.

We consider injectively-labelled automata i.e., where two different edges have different labels (and no label is ε). Figure 1 shows two injectively-labelled timed automata that will be used to illustrate the constructions throughout the paper.

0 x ≤ 1 1 x ≤ 1 l 2 x ≤ 1, a, ∅ x = 1, b, {y} x ≥ 1 ∧ y ≤ 0, c, ∅ A 0 : 0 x ≤ 1 1 x ≤ 1 l 2 x ≤ 1, a, {y} x ≥ 1 ∧ y ≤ 0, c, ∅ A 1 : Fig. 1. Two timed automata A valuation v is a mapping in R X ≥0 .
The effect of reset operations and time elapsing on valuations are described as follows. For R ⊆ X, the valuation v[R → 0] maps each variable in R to the value 0 and agrees with v over X \ R. For valuation v and d ∈ R ≥0 , valuation v+d is defined by: ∀x ∈ X, (v+d)(x) = v(x)+ d. Constraints of C(X) are interpreted over valuations: we write v |= γ when the constraint γ is satisfied by v. The set of valuations satisfying a constraint γ is denoted by [[γ]].

Definition 3 (Semantics of TA). The semantics of a timed automaton A = (L, 0 , X, Σ ε , E, Inv) is a timed transition system S A = (Q, q 0 , →) where Q = L × (R ≤0 ) X , q 0 = ( 0 , 0) and → is defined by: -either a delay move ( , v)

d --→ ( , v + d) iff v + d |= Inv( ), -or a discrete move ( , v) e -→ ( , v ) iff there exists some e = ( , γ, a, R, ) in E such that v |= γ, v = v[R → 0] and v |= Inv( ).
In order to ensure in a syntactic way that a move associated with a discrete transition e always leads to a configuration ( , v ) such that v |= Inv( ), we may modify the initial timed automaton in the following way : any atomic constraint related to a clock x occurring in the invariant of is added to the guard of each transition arriving in which does not reset x. This transformation does not change the resulting transition system but makes some proofs simpler and in the sequel, we always assume that the timed automaton has this property.

Since our results are mainly based on the region automaton and some of its variants, we now recall the material needed.

Elementary zones of a timed automaton

Notations. A zone is a subset of (R ≥0 ) X defined by a conjunction of atomic clock constraints of the form x h or xy h, where x and y are clocks in X, h ∈ N and ∈ {<, ≤, ≥, >}. In particular, if γ is a clock constraint in C(X), then the set [[γ]] is a zone. Constraints of the form xy h are usually called diagonal constraints. The future of a zone Z is defined by

f ut(Z) = {v + d | v ∈ Z, d ∈ R ≥0 }. A zone Z satisfies a constraint γ ∈ C(X), written Z |= γ, if
all valuations in Z satisfy γ. For k ∈ N, a k-zone is a zone for which no atomic clock constraint in its definition involves a constant greater than k.

Elementary zones. Recall [START_REF] Alur | A theory of timed automata[END_REF] that, if m is the maximal constant appearing in atomic formulas x h of A, an equivalence relation with finite index can be defined on clock valuations, leading to a partition of (R ≥0 ) X , with the following property: two equivalent valuations have the same behaviour under progress of time and reset operations, with respect to the constraints. In the original definition, an element of the partition is specified by a pair ({I x } x∈X , ∝) where I x is an interval in the set {{0}, ]0, 1[, {1}, . . . , {m}, ]m, +∞[} and ∝ is a relation on the subset of clocks x such that I x =]m, +∞[ defined by x ∝ y ≡ f ract(x) ≤ f ract(y).

Note that the property related to the behaviour of the systems holds for any partition which refines the above partition. In this paper, we define a family of refining partitions P K,g for K ≥ m + 1 and g ∈ N \ {0}. whose elements are called elementary zones. The constant g is called the granularity and P K,g is called a g-grid. For such a partition the interval I x belongs to the set

{{0}, ]0, 1 g [, { 1 g }, ] 1 g , 2 g [. . . , {K -1 g }, ]K -1 g , K[, [K, +∞[} (instead of keeping {K} separately).
As before, we also specify the ordering on the fractional parts w.r.t. g for all clocks x (i.e. the value δ ∈ [0, 1 g [ such that ∃i, x = i g + δ) with valuation less than K. We include the case K = +∞.

When K is finite, reachability can be decided by the usual method applied on these partitions; however we consider [K, ∞[ (rather than the usual ]K, ∞[) as the last interval for topological reasons explained later. The partition K = +∞ is used here as a tool for our expressiveness results. Figure 2 is associated with g = 1 and K = 3. For this example, elementary zones Z 1 and Z 2 are described as follows: If Z and Z are elementary zones, Z is a time successor of Z, written Z ≤ Z , if for each valuation v ∈ Z, there is some d ∈ R ≥0 such that v + d ∈ Z . For each elementary zone Z, there is at most one elementary zone such that (i) Z is a time successor of Z, (ii) Z = Z and (iii) there is no time successor Z different from Z and Z such that Z ≤ Z ≤ Z . When it exists, this elementary zone is called the immediate time successor of Z and denoted by succ(Z). From the definition of elementary zones as equivalent classes consistent with reset operations, the reset can be extended to elementary zones, so that

Z 1 : (2 < x < 3) ∧ (1 < y < 2) ∧ (0 < f rac(y) < f rac(x)) or equivalently, (2 < x < 3) ∧ (1 < y < 2) ∧ (x -y > 1) and Z 2 : (x ≥ 3) ∧ (1 < y < 2).
Z[R → 0] is the elementary zone containing any v[R → 0], for v ∈ Z.
Standard topological notions on (R ≥0 ) n apply to zones. Moreover, due to the particular form of the constraints, the topological closure of any elementary zone has a minimal element.

For a timed automaton A, a constant K and a granularity g, we call region a pair ( , Z), where is a location of A and Z an elementary zone of (R ≥0 ) X . We now give a description for regions, which distinguishes time-closed and timeopen descriptions. It is equivalent to the original one but more convenient for our proofs and it fits both cases, whether K is finite or infinite.

Definition 4 (Region description w.r.t. constant K and granularity g). A time-closed description of a region r is given by: r the location of r, -min r ∈ N X g with ∀x, min r (x) ≤ K, the minimal vector of the topological closure of r, -ActX r = {x ∈ X | min r (x) < K} the subset of relevant clocks, -the number size r of different fractional parts for the values of relevant clocks in the N ActX r g grid, with 1 ≤ size r ≤ M ax(|ActX r |, 1) and the onto mapping ord r : X → {1, . . . , size r } giving the ordering of the fractional parts.

By convention, ∀x ∈

X \ ActX r , ord r (x) = 1. Then r = {( r , min r + δ) | δ ∈ R X ≥0 and ∀x, y ∈ ActX r [ord r (x) = 1 ⇔ δ(x) = 0] ∧ δ(x) < 1/g ∧ [ord r (x) < ord r (y) ⇔ δ(x) < δ(y)]}
A time-open description of a region r is defined with the same attributes (and conditions) as the time-closed one with:

r = {( r , min r + δ + d) | ∃ d ∈ R >0 ∧ ∀x ∈ ActX r , d(x) = d ∧ δ(x) + d < 1/g ∧ ∀x / ∈ ActX r , d(x) = 0}.
The set [X] r is the set of equivalence classes of clocks w.r.t. their fractional parts, i.e. x and y are equivalent iff ord r (x) = ord r (y).

Thus, a time-open region corresponds to an immediate time successor of a timeclosed region and the decomposition of a valuation in a time-open region as

min r + δ + d is unique if min r + δ belongs to the previous time-closed region.
This property is used in the sequel. Also remark that min r / ∈ r except if there is a single class of clocks relative to r (for instance if the corresponding zone is a singleton). Of course, when K = +∞, the part about relevant clocks, for which the value is less than K, can be omitted (since ActX r = X). The hypothesis K = +∞ makes some proofs simpler, because the extremal case where a clock value is greater than K is avoided, and it can be lifted afterward. Furthermore when K is finite, some regions admit both time-open and time-closed descriptions (for instance a region associated with zone Z 2 in fig. 3), whereas when K = +∞, a region admits a single description, so that time elapsing leads to an alternation of time-open regions (where time can elapse) and time-closed ones (where no time can elapse). Furthermore in this case, the representation of a valuation in a time-open region can be written min r + δ + d with d a (scalar) duration.

Region automaton and class automaton of a TA.

For a timed automaton A, a constant K and a granularity g, the region automaton R(A) g,K is a finite automaton, the states of which are regions. These regions are built inductively from the initial one ( 0 , 0) by the following transitions over the set of labels {succ} ∪ Σ ε :

-( , Z) succ ---→ ( , succ(Z)) if succ(Z) |= Inv( ) and -( , Z) a -→ ( , Z ) if there is a transition ( , γ, a, R, ) ∈ E such that Z |= γ and Z = Z[R → 0], with Z |= Inv( ).
A region r = ( , Z) is said to be maximal in R(A) g,K with respect to if no succ-transition is possible from r. In the sequel, the topological properties of r are implicitly derived from those of Z. We write r for the topological closure of r, and recall that min r denotes the minimal vector of r.

We also consider another automaton, called the class automaton, in which the states, called classes, are of the form ( , Z), where Z is a zone. In this case, the automaton is built from the initial class ( 0 , f ut(0) ∩ Inv( 0 )) by the following transitions:

( , Z 1 ) a -→ ( , Z 2 ) if there exists ( , γ, a, R, ) ∈ E such that Z 1 ∩ [[γ ]] = ∅, and Z 2 = f ut((Z 1 ∩ [[γ]])[R → 0]) ∩ Inv( ).
While this construction does not always yield a finite number of classes, it is now well known [START_REF] Bouyer | Forward Analysis of Updatable Timed Automata[END_REF] that for a timed automaton without diagonal constraints (as is our case), replacing each zone Z from the previous construction by its K-approximation (Approx K (Z), the smallest K-zone containing Z), we obtain a finite automaton such that any configuration belonging to a zone is strongly timed bisimilar to a reachable configuration (see also the discussion of the next paragraph). This method is usually implemented in tools like Uppaal [START_REF] Pettersson | Uppaal2k[END_REF] or Kronos [START_REF] Yovine | Kronos: A Verification Tool for real-Time Systems[END_REF] for on-the-fly verification, with each zone represented by a Difference Bounded Matrix [START_REF] Dill | Timing assumptions and verification of finite-state concurrent systems[END_REF].

Reachability

For a region r of R(A) g,K , not all configurations of r are reachable. Nevertheless, by induction on the reachability relation, the following property can be shown: for any region r of R(A) g,K , there is a region reach(r) with respect to the g-grid and constant K = ∞ such that

-(i) reach(r) ⊂ r, - (ii
) each configuration of reach(r) is reachable and -(iii) if reach(r) admits a time-open description then this is also the case for r, else r admits a time-closed description.

As a consequence, we have: ∀x ∈ ActX r , min reach(r) (x) = min r (x) and ∀x ∈ X \ ActX r , min reach(r) (x) ≥ K and ord r restricted to ActX r is identical to ord reach(r) . Consider now the relation R defined by

( , v) R ( , v ) iff ∀x ∈ X, v (x) = v(x) ∨ (v(x) ≥ K ∧ v (x) ≥ K).
It is a strong timed bisimulation relation. From the previous observations, we note that each configuration of a region is strongly timed bisimilar to a reachable configuration of this region. Thus speaking about reachability of regions is a slight abuse of notations. Note that the same property holds for the classes of the class automaton.

3 Characterizing TA bisimilar to Time Petri Nets

Time Petri Nets

Introduced in [START_REF] Merlin | A study of the recoverability of computing systems[END_REF], Time Petri Nets (TPNs) extend Petri nets by associating a (topological) closed time interval with each transition (see figure 4). The meaning of this interval is detailed after the definition. Definition 5 (Labeled Time Petri Net). A Labeled Time Petri Net N over Σ ε is a tuple (P, T, Σ ε , • (.), (.)

• , M 0 , Λ, I) where:

-P is a finite set of places, -T is a finite set of transitions with

P ∩ T = ∅, -• (.) ∈ (N P ) T is the backward incidence mapping, -(.) • ∈ (N P ) T is the forward incidence mapping, -M 0 ∈ N P is the initial marking, -Λ : T → Σ ε is the labeling function, -I : T → I(Q ≥0 )
associates with each transition a closed firing interval.

A TPN N is a g-TPN if for all t ∈ T , the interval I(t) has its bounds in N g . We also use

• t (resp. t • ) to denote the set of places • t = {p ∈ P | • t(p) > 0} (resp. t • = {p ∈ P | t • (p) > 0})
as is common in the literature. The intended meaning of these notations will be clear from the context.

As usual, a marking M is a mapping in N P , with M (p) the number of tokens in place p. A transition t is enabled in a marking M iff M ≥ • t. We denote by En(M ) the set of enabled transitions in M . A configuration of a TPN is a pair (M, ν) where M is a marking and the valuation ν is a mapping in (R ≥0 ) En(M ) , which describes the values of clocks implicitely associated with transitions enabled in M . Roughly speaking, such a clock measures the time elapsed since the enabling of the corresponding transition as explained more precisely below.

An enabled transition t can be fired if ν(t) belongs to the interval I(t). The result of this firing is as usual the new marking M = M -• t + t • . Moreover, some valuations are reset and we say that the corresponding transitions are newly enabled. Different semantics are possible for this operation. In this paper, we choose persistent atomic semantics, which is different from the classical semantics [START_REF] Berthomieu | Modeling and verification of time dependent systems using time Petri nets[END_REF][START_REF] Aura | A causal semantics for time Petri nets[END_REF], but equivalent when the net is bounded [START_REF] Bérard | Comparison of Different Semantics for Time Petri Nets. Automated Technology for Verification and Analysis: Third International Symposium[END_REF]. The predicate describing when a transition t is newly enabled by the firing of transition t is defined by:

↑enabled(t , M, t) = t ∈ En(M -• t + t • ) ∧ (t ∈ En(M )).
Thus, firing a transition is considered as an atomic step and the transition currently fired behaves like the other transitions (ν(t) need not be reset when t is fired). In classical semantics, when firing a transition, disabling of the other transitions is checked after the consumption of tokens from input places and before the production of tokens to output places. Furthermore the clock associated with the fired transition is always reset. Observe that our results also hold for the classical semantics but we have chosen this one as it leads to more elegant constructions in sections 5 and 6. More precisely, the sufficient condition is obtained by construction of a bounded TPN and it has been proven that for bounded nets, both semantics are equivalent [START_REF] Bérard | Comparison of Different Semantics for Time Petri Nets. Automated Technology for Verification and Analysis: Third International Symposium[END_REF]. The necessary condition is based on lemmas 1 and 2 which do not depend on the triggering of clock reset in TPNs.

The set ADM(N ) of admissible configurations consists of the pairs (M, ν) such that ν(t) ∈ I(t) ↓ for each transition t ∈ En(M ). Thus time can progress in a marking only until it reaches the first right endpoint of the intervals for all enabled transitions. For d ∈ R ≥0 , the valuation ν + d is defined by

(ν + d)(t) = ν(t) + d for each t ∈ En(M ).
Definition 6 (Semantics of TPN). The semantics of a TPN N = (P, T, Σ ε , • (.), (.)

• , M 0 , Λ, I) is a TTS S N = (Q, q 0 , →) where Q = ADM(N ), q 0 = (M 0 , 0)
and → is defined by:

-either a delay move (M, ν)

d --→ (M, ν + d) iff ∀t ∈ En(M ), ν(t) + d ∈ I(t) ↓ , -or a discrete move (M, ν) Λ(t) ---→ (M -• t+t • , ν ) where ∀t ∈ En(M -• t+t • ), ν (t ) = 0 if ↑enabled(t , M, t) and ν (t ) = ν(t ) otherwise, iff t ∈ En(M ) and ν(t) ∈ I(t).
We simply write (M, ν) w -→ to emphasise that a sequence of transitions w can be fired. If Duration(w) = 0, we say that w is an instantaneous firing sequence. A net is said to be k-bounded if for each reachable configuration (M, ν) and for each place p, M (p) ≤ k.

Denoting ((M 0 (p 1 ), M 0 (p 2 )), (ν 0 (t 1 ), ν 0 (t 2 ))) by ((2, 1), (0, 0)), the sequence ((2, 1), (0, 0))

2 -→ ((2, 1), (2, 2)) t 1 -→ ((1, 1), (2, 2)) t 1
-→ ((0, 1), (-, 2)) is a firing sequence of the net of figure 4. Note that, due to the semantics, the first firing of t 1 does not reset its clock even if the token in p 2 is consumed and produced again. Note also that time cannot progress beyond time 2 as long as t 1 remains fireable. Afterwards time can progress for at most 2 t.u. at which point t 2 must fire (it could also fire before). This temporal feature is sometimes called an urgent behaviour in contrast to a lazy behaviour.

A characterization of TA bisimilar to TPNs

We aim at characterizing TA bisimilar to some TPN whatever the labelling of the TA. In fact to check this property is equivalent to test whether an associated injectively-labelled TA is bisimilar to some TPN. This is why we only consider injectively-labelled TA in the sequel.

TA include both lazy mechanisms since time elapsing can falsify the guard of an edge and urgent mechanisms since invariants may forbid time elapsing in some configurations. Hence a characterization of TA bisimilar to some TPN seems to be closely related to the absence of laziness features. In this paragraph, we first present two intuitive conditions for a TA to be bisimilar to a TPN which do not characterize this property before introducing the exact characterization.

The first condition is obtained by observing that a transition (and more generally an instantaneous firing sequence) of a TPN cannot be disabled by time elapsing. Consequently, our first attempt to characterize this property is: "A TA is bisimilar to some TPN if time elapsing cannot falsify the guard of an edge starting from the current location". By virtue of the observation this condition is necessary. However it is not sufficient and the automaton A 1 of figure 1 does not admit a bisimilar TPN whereas it fulfills this condition as can be checked on its region automaton represented in figure 6. The three parts of this figure (from left to right) represent respectively the reachable regions associated with locations 0 , 1 and 2 . Thin arrows represent time elapsing (thus staying in the same location) while thick (labelled) arrows represent discrete transitions from some ( , Z) to another region ( , Z ). For instance, ( 0 , 0 < x = y < 1)

a -→ ( 1 , 0 < x < 1 ∧ y = 0) Fig. 6. The region automaton of A 1 (K = 2, g = 1)
The previous observation about the behaviour of a TPN may be sharpened and yields the following lemma useful for subsequent developments. . Let w be an instantaneous firing sequence, then:

(i) (M, ν) w -→ implies (M, ν + δ) w -→ (ii) If ν ∈ N g En(M ) and δ ∈ [0, 1/g[ En(M ) then (M, ν + δ) w -→ implies (M, ν) w -→
Proof. There are two kinds of transitions firing in w: those corresponding to a firing of a transition (say t) still enabled from the beginning of the firing sequence and those corresponding to a newly enabled transition (say t ).

Proof of (i) Since t is firable from (M, ν), ν(t) ∈ I(t) ⊂ I(t) ↑ , so ν(t) + δ(t) ≥ ν(t) also belongs to I(t) ↑ . Since t ∈ En(M ) and (M, ν + δ) is reachable, ν(t) + δ(t) ∈ I(t) ↓ . Thus ν(t) + δ(t) ∈ I(t) and t is also firable from (M, ν + δ).

Since t is newly enabled, 0 ∈ I(t ) and t is also firable when it occurs starting from (M, ν + δ).

Proof of (ii) The case of newly enabled transitions in w is handled as before. Now let t be firable in (M, ν + δ). Taking into account this lemma, one can elaborate a slightly modified version of the first condition: "A TA is bisimilar to some TPN if given any two reachable configurations (l, v) and (l, v ) with v ≥ v and an edge e, then (l, v) e -→⇒ (l, v ) e -→". For instance, A 1 does not fulfill this condition (take (l 1 , (1, 0)),(l 1 , (1, 1)) and the edge labelled by c in figure 6). Unfortunately this condition is not necessary. The TA A 0 of figure 1 does not fulfill this condition whereas there exists a TPN bisimilar to it (see figure 13 in section 5). Indeed take (l 1 , (1, 0)),(l 1 , (1, 1)) and the edge labelled by c and see its region automaton presented in figure 7 (with the same conventions as in figure 6). The difference between the two automata w.r.t. the property to be checked is the existence of the reachable region (l 1 , x = 1 ∧ 0 < y < 1) whose topological closure includes the configuration (l 1 , (1, 0)). In fact, the exact characterization takes into account topological considerations as stated by the following theorem which also contains effectiveness and complexity results.

Theorem 1. Let A be a injectively-labelled timed automaton and R(A) 1,K its region automaton with a constant K strictly greater than any constant occurring in the automaton, then A is weakly timed bisimilar to a time Petri net iff for each region r of R(A) 1,K and for each edge e from A, (a) Every region r such that r ∩ r = ∅ is reachable

(b) ∀( r , v) ∈ r, if ( r , v) e -→ then ( r , min r ) e -→ (c) ∀( r , v) ∈ r, if ( r , min r ) e -→ then ( r , v) e -→.
Furthermore, if these conditions are satisfied then we can build a 1-bounded 2-TPN bisimilar to A whose size is linear w.r.t. the size of A and a 1-bounded 1-TPN bisimilar to A whose size is exponential w.r.t. the size of A. We denote by T A wtb the corresponding subclass of timed automata.

Thus T A wtb is the maximal subclass of TA that are weakly timed bisimilar to a TPN. In [START_REF] Bérard | Comparison of the Expressiveness of Timed Automata and Time Petri Nets[END_REF], we have proposed a "syntactical" (proper) subclass of T A wtb which avoids to check this characterization.

The characterization of Theorem 1 is closely related to the topological closure of reachable regions: it states that any region intersecting the topological closure of a reachable region is also reachable and that a discrete step either from a region or from the minimal vector of its topological closure is possible in the whole topological closure. Consider again the two TA A 0 and A 1 in Figure 1. The automaton A 0 admits a bisimilar TPN whereas A 1 does not. Indeed, the region r = ( 1 , x = 1 ∧ 0 < y < 1) is reachable. The guard of edge c is true in min r = ( 1 , (1, 0)) whereas it is false in r.

The next sections are devoted to the proof of Theorem 1.

4 Proof of necessary condition for Theorem 1

From bisimulation to uniform bisimulation

As a first step, we prove that when a g-TPN and a TA are bisimilar, this relation can in fact be strengthened in what we call uniform bisimulation. Lemma 2 is the central point for the proof of necessity. It shows that bisimulation implies uniform bisimulation for the g-grid with K = ∞. Roughly speaking, uniform bisimulation means that a unique mechanism is used for every configuration of the topological closure of the region to obtain a bisimilar configuration of the net.

Lemma 2 (From bisimulation to uniform bisimulation). Let A be a timed automaton bisimilar to some g-TPN N via some relation R and let R(A) g,∞ be a region automaton of A. Then:

-if a region r belongs to R(A) g,∞ then any region included in r also belongs to R(A) g,∞ ; -for each region r, there exist a configuration of the net (M r , ν r ) with ν r ∈ N En(M r ) g and a mapping φ r : En(M r ) → [X] r such that:

• If r is time-closed, then for each δ ∈ R X ≥0 such that ( r , min r + δ) ∈ r, ( r , min r + δ) R (M r , ν r + proj r (δ)), • If r is time-open, then for each δ ∈ R X ≥0 , d ∈ R ≥0 such that ( r , min r + δ + d) ∈ r, ( r , min r + δ + d) R (M r , ν r + proj r (δ) + d),
where proj r (δ)(t) = δ(φ r (t)).

Proof. First note that the choice of a particular clock x in the class φ r (t) is irrelevant when considering the value δ(x). Thus the definition of proj r is sound. The proof is an induction on the transition relation in the region automaton. The basis case is straightforward with {(l 0 , 0)} and {(M 0 , 0)}. The induction part relies on lemma 1, with 4 cases, according to the incoming or target region and to the nature of the step: 1. A time step from a time-closed region (see figure 8(1)). Let r be a time-closed region in R(A) g,∞ and let us denote r = succ(r) the immediate Fig. 8. The different cases of the proof as follows. Let t be a transition newly enabled during the firing sequence, then φ r (t) is associated to the class of index 1. Let t be a transition always enabled during the firing sequence. There are two cases to consider for φ r (t): if there is a x ∈ φ r (t) not reset, then φ r (t) = |x] r otherwise φ r (t) is the class of maximal index which precedes φ r (t) and contains a clock not reset or else the class of index 1. The two last affectations are sound since, it means that whatever, before the firing of w, the fractional value of the implicit clock associated with t between the fractional value of the new clock corresponding to t and the fractional value of a clock of φ r (t), the firing sequence w leads to bisimilar configurations (as being bisimilar to the same configuration of the automaton). Case b. The case where r is a time-open region is handled in a similar way.

Let ( r , min r +δ 0 + d 0 ) be some element of r. Suppose that ( r , min r +δ 0 + d 0 ) e -→ ( , v + δ 0 ) with ∀x ∈ R(e), v (x) = δ 0 (x) = 0, ∀x / ∈ R(e), v (x) = min r (x) ∧ δ 0 (x) = δ 0 (x) + d 0 . Then in N there is an instantaneous firing sequence (M r , ν r + proj r (δ 0 ) + d 0 ) w -→ labelled by e. Due to lemma 1, this firing sequence is also fireable from any (M r , ν r + proj r (δ) + d) bisimilar to ( r , min r + δ + d) ∈ r. By bisimilarity, ( r , min r +δ + d) e -→ for any ( r , min r + δ + d) ∈ r. Let r be the region including (l , v + δ 0 ), then any configuration of r is reachable by this discrete step. Note that l r = l and min r = v . From (M r , ν r +proj r (δ)+d), the sequence w leads to some (M , ν ) bisimilar to (l r , min r + δ )). We now show how to define M r , ν r and φ r . First M r = M . Second, ν r (t) = ν r (t) for transitions t always enabled during the firing sequence and ν r = 0 otherwise. At last, φ r is obtained from φ r as follows. Let t be a transition newly enabled during the firing sequence, then φ r (t) is associated to the class of index 1. There are two cases to consider for φ r (t): if there is a x ∈ φ r (t) not reset, then φ r (t) = |x] r otherwise φ r (t) is the class of maximal index which precedes φ r (t) and contains a clock not reset or else the class of index 1. The two last affectations are sound since, it means that whatever, before the firing of w, the fractional value of the implicit clock associated with t between the fractional value of the new clock corresponding to t and the fractional value of a clock of φ r (t), the firing sequence w leads to bisimilar configurations (as being bisimilar to the same configuration of the automaton). Then this region can be reached via a discrete step into a time-closed region followed by a time step. So we do not need to examine this case.

Proof of Necessity

The fact that conditions In order to complete the proof, we successively show that if the conditions are satisfied in R(A) g,∞ for some g, they also hold for R(A) 1,∞ (lemma 3), and finally that they are satisfied in the standard region automaton R(A) 1,K , with a finite constant K, sufficiently large (lemma 4). Recall (section 2.2) that any atomic constraint related to a clock x occurring in the invariant of a location is added to the guard of each incoming transition which does not reset x.

Lemma 3 (about the conditions and the grid). Let A be a timed automaton and g > 0 in N. If conditions (a),(b),(c) are satisfied in the region automaton R(A) g,∞ , then they are satisfied in R(A) 1,∞ .

Sufficient condition: first construction

Starting from a timed automaton A satisfying the conditions of Theorem 1, we build a 2-TPN bisimilar to A. We describe the construction and give the proof of correctness.

For the figures corresponding to all constructions, all edges are weighted by 1. Omitted labels for transitions stand for ε. A firing interval [0, 0] is indicated by a blackened transition and intervals [0, ∞[ are omitted. A double arrow between a place p and a transition t indicates that p is both an input and an output place for t.

Construction

First remark that any constraint of the form x < c occurring in an invariant of A may be safely omitted. If it would forbid the progress of time in some configuration, then the associated region would be a maximal time-open region r. Due to condition (a), r is reachable but since r is time-open, r ∩ succ(r) = ∅, so that succ(r) is reachable which contradicts the maximality of r.

• T x<h F x<h change x<h [h -1 2 , h -1 2 ] Rnext x i Rnext x i+1 Rinit reset 1 x<h reset 2 x<h init x<h • T x≤h F x≤h change x≤h [h + 1 2 , h + 1 2 ] Rnext x i Rnext x i+1 Rinit reset 1 x≤h reset 2 x≤h init x≤h
Fig. 9. Subnets for x < h (with h > 0) and x ≤ h in guards Clock constraints. The atomic constraints associated with a clock x are arbitrarily numbered from 1 to n(x) where n(x) is the number of such conditions. When x ≤ h occurs in at least one transition and in at least one invariant, we consider it as two different conditions. Then we add places Rinit and (Rnext x i ) i≤n(x)+1 for the reset operations. We build a subnet for each atomic constraint x h occurring in a transition of the TA, and one for each condition x ≤ h occurring in an invariant. Figure 9 shows the subnets corresponding to x < h (with h > 0) on the left and x ≤ h on the right, while Figure 10 shows the subnets for x > h on the left and x ≥ h (with h > 0) on the right, in the case where the constraint has number i. Figure 11 shows the subnet for invariant x ≤ h. Since constant 1 2 appears in interval bounds, the resulting TPN is a 2-TPN.

• Locations and edges. With each location of the automaton, we associate an eponymous place . The place is initially marked iff the location is the initial one. The invariant Inv( ) is tested with the subnets corresponding to its atomic constraints:

F x>h T x>h change x>h [h + 1, h + 1] Rnext x i Rnext x i+1 Rinit reset 1 x>h reset 2 x>h init x>h • F x≥h T x≥h change x≥h [h, h] Rnext x i Rnext x i+1 Rinit reset 1 x≥h reset 2 x≥h init x≥h
-if condition x ≤ h (with h > 0) occurs in the invariant, then we add a transition stop x≤h , with both and T Reach x≤h as input and output places, and interval [0, 0], -if condition x ≤ 0 occurs in the invariant, we simply add a transition stop with as only input and output place, and also interval [0, 0].

To simulate an edge e = ( , γ, a, R, ), we must test the atomic constraints from γ = γ 1 ∧ . . . ∧ γ m(e) , using the places corresponding to true in the associated subnets, and reset successively all the clocks in R = {x 1 , . . . , x k(e) } by instantaneous transitions. This is done by the subnet in Figure 12, which must be connected to some subnets like those of Figure 9, 10 or 11.

T γ 1 T γ 2 T γ m (e) . . . . . . . . . . . . W 1 e W 2 e W k(e) e Rnext x 1 1 Rnext x 1 n(x 1 )+1 Rnext x 2 n(x 2 )+1 Rnext x 2 1 Rnext x k(e) 1
Rnext

x k(e) n(x k(e) )+1
f ire e , a This construction is illustrated in figure 13 for the timed automaton A 0 from figure 1 with some simplifications related to this particular timed automaton. More precisely, places F Reach x≤1 and F x≥1 (resp. T Reach x≤1 and T x≥1 ) have been merged. Moreover since x is never reset in A 0 the corresponding parts in the TPN are omitted.

First note that the subnet associated to the constraint y ≤ 0 switches the condition to false (marking F y≤0 ) when the implicit value of y maintained in the net reaches 1/2. This translation thus seems less constrained than the original condition, so we explain how we prove that it is nevertheless sound. Let r be the region corresponding to the current configuration ( , v) of the automaton simulated by the net. If the net is able to simulate a discrete step of the automaton, we prove that in the configuration ( , min r ) of the automaton, this step is also possible. Thus by condition (c), the step is also possible from ( , v). On the other hand, if a discrete step is possible for ( , v) in the automaton, we show that this step can also be simulated in the net using both conditions (b) and (c) and the following fact: ∀x ∈ X, ∃( r , v ), ( r , v ) ∈ r such that v (x) = v(x) and v (x) = v(x) . The subnet associated to the atomic constraint x ≤ 1 occuring in the invariant of 0 leads to transition inv 0 (not modifying the marking) 13. A 2-TPN bisimilar to A 0 which is fireable as soon as the simulated value of x reaches 1 and the place 0 is marked. Thus time cannot progress except if the location is left.

• • • Rnext [1/2, 1/2] Rinit init y≤0 c, [0, +∞[ l 2 1 F x≥1 T y≤0 F y≤0 0 a, [0, +∞[ b, [0, +∞[ T x≥1 [1, 1] stop x≤1 0 Fig.

Correctness proof

We decompose the reachable configurations (and markings) into intermediate ones (some W i e is marked) and permanent ones (some is marked). An easy induction shows that in permanent configurations (M, ν) the enabled timed transitions relative to a clock are "synchronized": ν(change c ) = ν(change c ) = ν(reach c ) as soon as c, c , c relates to the same clock x. We define ν(x) as this common value if at least one such transition is enabled and otherwise ν(x) = K(x) where K(x) is the maximal value relative to clock x occuring in the net N . Furthermore from any intermediate configuration (M, ν), the behaviour of the net is quasi-deterministic until it reaches a permanent configuration: there are only instantaneous firing sequences (i.e. no time step) and the finite maximal ones lead to permanent configurations. These permanent configurations (say (M next , ν next )) have the same marked place and the same values ν next (x). They may only differ depending on whether some transitions related to a condition switch have been fired.

It is also obvious that once some f ire e is fired, the construction ensures the existence of a "resetting" sequence which reinitializes the subnets associated to the clocks to be reset.

Bisimulation relation. We now define the relation R between reachable configurations of the automaton A and the net N . Let us define ( , v)R(M, ν) iff:

-either M is a permanent marking and M ( ) is marked and if ν(x) < K(x)

then v(x) = ν(x) else v(x) ≥ K(x).
-or M is an intermediate marking leading to some permanent (M next , ν next ) and ( , v)R(M next , ν next ). This definition is sound due to the common features of the different (M next , ν next ).

It remains to prove that R is a bisimulation, which is done in the next lemma.

Lemma 5. The relation R defined above is a weak timed bisimulation.

Proof. We first consider moves from A. Case 1: ( , v) e -→ ( , v ). We prove that (M, ν) σ -→ with σ labelled by e. At first, σ begins by σ which consists to fire all the change c fireable leading to some (M , ν ) (with ( , v)R(M , ν )).

Now we prove that (M , ν )

f ire e ---→. By definition of R, M ( ) is marked. Let c be a condition occuring in the guard of e. If c = [x ≥ a] then v(x) ≥ a which implies ν(x) ≥ a and that T x≥a is marked (possibly with the help of σ ). If c = [x > a] then let r be the region to which ( , v) belongs. min r (x) = v(x) . Using condition (b), (l, min r ) e -→. Thus v(x) ≥ min r (x) ≥ a + 1 which implies ν(x) ≥ a + 1 and that T x>a is marked (possibly with the help of σ ). If c = [x ≤ a] then v(x) ≤ a which implies ν(x) ≤ a and that T x≤a is marked (remember that change x≤a fires when ν(x) = a + 1/2). If c = [x < a] then let r be the region to which ( , v) belongs. Then there exists ( , v 1 ) ∈ r with v 1 (x) = v(x) . Using condition (b) and then (c), (l, v 1 ) e -→. Thus v(x) ≤ v 1 (x) ≤ a -1 which implies ν(x) ≤ a -1 and that T x<a is marked (remember that change x<a fires when ν(x) = a -1/2). Thus f ire e is fireable from (M , ν ). We complete σ by the "resetting" sequence leading to a configuration bisimilar to ( , v ) If M is an intermediate marking, we have to fire a sequence leading to some (M next , ν next ) and perform the previous simulation.

Case 2: ( , v) d -→ ( , v + d)
If M is an intermediate marking, again we fire an instantaneous sequence leading to some (M next , ν next ) still bisimilar to ( , v) and perform the following simulation for the case when M is permanent.

We must determine which transitions could prevent d time units to elapse: either change or stop transitions. When after d < d time units, a change transition prevents time elapsing, it is fired leading to another permanent marking bisimilar to ( , v + d ). The only possible stop transitions that could prevent time elapsing correspond to conjuncts of the form x ≤ a belonging to the invariant of . This means that v(x) + d ≤ a. Thus from (M, ν), we let a time d elapse interleaved with possible firings of change transitions. The stop transitions associated with will be possibly firable but only at the end of this step sequence.

Conversely, we consider moves from N . Case 3: (M, ν) t -→ (M , ν ) If t is labelled by , then by construction ( , v)R(M , ν ).

Thus we only to need to examine the case of f ire e (M is then a permanent marking). Let r be the region to which ( , v) belongs. We will show that ( , min r ) e -→. Then by condition (c), we will obtain that ( , v) 6 Sufficient condition: second construction When the conditions on the injectively-labelled timed automaton A are satisfied, we now build a 1-TPN N which is weakly timed bisimilar to A.

Construction

The construction of the TPN contains a partial replication of both the region automaton of A and its class automaton. Recall that we consider K = m + 1, where m is the maximal constant for A. There is first a subnet for each clock x, in which only the integral parts of x appear in the places (but with a fractional part that can reach 1).

• . . . h x 0 h x 1 t x 0 [1, 1] t x 1 [1, 1] t x K-1 [1, 1] h x K Fig. 14. Subnet for clock x
Then we add one place C for each class C = ( , Z) of the class automaton, with the initial class marked. Now let e = ( , g, a, R, ) be a transition of A. For each pair (v, v ) of clock valuations in N X , with v, v ≤ -→ K , we build a subnet (see figure 15) which simulates the transition ( , v) e -→ ( , v ), where we have v

(x) = 0 if x ∈ R and v (x) = v(x) otherwise. Let C 1 = ( , Z 1 ), . . . , C k = ( , Z k ) be the subset of classes such that ∃v ∈ Z i ∧ ∀x ∈ X, v (x) = v(x) ∨ (v (x) ≥ K ∧ v(x) = K)) for 1 ≤ i ≤ k.
Otherwise stated, there is a configuration in every Z i which is strongly time bisimilar to v. Let C 1 , . . . , C k the classes obtained by applying transition e to C 1 , . . . , C k respectively. We have a transition with label e for each C i (with k = 2 in figure 15), all with interval [0, +∞[. Note that all reset operations for clocks in R are executed successively with instantaneous transitions. Moreover, the upper part of the net ensures that the invariant conditions of location l are satisfied (this part has been omitted for in the figure). For instance, for the automaton A 0 from Figure 1, we have four classes: and C 1 are marked and t x 0 and t y 0 have been enabled for 1 t.u. Suppose that the transition t x 0 is fired, marking the place t x 1 , then without the input place C 2 the transition labelled c could be erroneously fired. Since C 2 is unmarked this firing is disabled.

. . . l h z c , z ≤ c ∈ Inv( ) [0, +∞[ e h x v(x) , x ∈ R h x v(x) , x / ∈ R reset x e h x 0 , x ∈ R
C 0 = {l 0 , 0 ≤ x = y ≤ 1}, C 1 = {l 1 , 0 ≤ x = y ≤ 1}, C 2 = {l 1 , x = 1 ∧ y = 0} and C 3 = {l 2 , 0 ≤ y = x -1}.

Correctness proof

Like in the previous proof, we say that a configuration (and the corresponding marking) (M, ν) of the TPN is permanent if M ( ) = 1 for some l. Otherwise, it is an intermediate configuration (and marking), where M (reset x e ) = 1 for some (exactly one of each) x and e, meaning that some reset operations are in progress. Here again, a permanent configuration is reached instantaneously from such an intermediate configuration, with only firing sequences completing the reset operations for transition e (interleaved with possibly transitions firings of some t x c ). Furthermore, for a configuration (M, ν), there is exactly one non empty place h x c for each clock x. Writing c x for the constant such that M (h x c x ) = 1, we have either c x = K or 0 ≤ ν(t x c x ) ≤ 1, where ν(t x c ) is the time elapsed since arrival of the token in the place h x c x . This means that the value of clock x is either v(x) ≥ K or v(x) = c x + ν(t x c x ) with v(x) equal to either c x or c x + 1. In the latter case, transition t x c x can be fired instantaneously, leading to the configuration (M , ν ) with one token in place h x c x +1 and either c x + 1 = K or ν (t x c x +1 ) = 0. We can thus reach a configuration where its associated c = (c x ) x∈X is maximal, i.e. for every x, either c x = K or ν(t x c x ) < 1.

Bisimulation relation. The relation R is defined as the set of pairs ((M, ν), ( , v)) such that:

-either (M, ν) is a permanent configuration with M ( ) = 1, the relation between v and ν is the one described above, and there exists exactly one class C = ( , Z) such that M (C) = 1 and v ∈ Z; -or (M, ν) is an intermediate configuration leading to some permanent configuration (M , ν ) such that ((M , ν ), ( , v)) ∈ R.

Case 2: If ( , v) e -→ ( , v ) for some e = ( , g, a, R, l ) then condition (b) implies that a transition ( , v ) e -→ ( , v ) is also possible in A. Here again we may have to apply from (M, ν) a sequence of instantaneous transitions, leading to (M 1 , ν 1 ) where place l is marked, and from there we can reach an equivalent configuration (M 2 , ν 2 ) with its associated c = (c x ) x∈X maximal. Let C = ( , Z) be the class for which M (C) = 1, with v ∈ Z. From lemma 6, ( , v ) also belongs to C, and ∀x ∈ X, v (x) = c x ∨ ( v (x) ≥ K ∧ c x = K) so that the transition e (corresponding to this vector and this class) can be fired in N , immediately followed by the corresponding reset sequence, leading to (M , ν ). Since exactly one class C is marked after e, we have (M , ν )R( , v ) by the definition of R.

For the converse, we consider a move in N . Case 3: (M, ν) d -→ (M, ν + d) (with d = 0). Then, neither reset transitions nor transitions of the form t x c can be fired in N . Thus, the places h x c which contain a token are such that ν(t x c ) < 1 and ν(t x c ) + d ≤ 1. For the state ( , v), we have

M ( ) = 1 and v(x) = c + ν(t x c ). The move ( , v) d -→ ( , v + d) is possible in A since ( , v +
d) belongs either to the region of ( , v) or to its time successor which is reachable by condition (a). Therefore ( , v)

d -→ ( , v + d) in A with (M, ν + d)R( , v + d). Case 4: (M, ν) t -→ (M , ν ).
For any transition t of N which is not associated with some transition e = ( , g, a, R, l ) in A, no time can elapse so there is no need for a move in A because (M , ν ) is still equivalent to ( , v). Suppose now that t is associated with an edge e, we have M

( ) = 1, M (C) = 1 for some class C = ( , Z) with v ∈ Z. Since t is fireable, considering the valuation c = (c x ) x∈X associated with (M, ν) the construction implies that ∃v ∈ Z s.t. ∀x ∈ X, v (x) = c x ∨ (v (x) ≥ K ∧ c x = K), which implies that the segment [v , v] ⊆ Z, from the convexity of Z, with 0 ≤ v(x) -v (x) = v(x) -c x ≤ 1 for each x s.t. c x < K. Thus, [( , v ), ( ,

Complexity results

This characterization leads to the the following complexity results. Proposition 1. Given a (injectively-labelled) timed automaton A, deciding whether there is a TPN weakly timed bisimilar to A is P SP ACE-complete. The reachability problem for the class T A wtb is P SP ACE-complete.

Proof. The reachability problem for regions is in P SP ACE. In order to check whether the condition (a) is false we non deterministically pick a region r and a region r which intersects r and check whether r is reachable and r is not reachable. In order to check whether the condition (b) is false we non deterministically pick a region r and a edge e and check whether r is reachable and e is firable from r and not fireable from (l r , min r ). In order to check whether the condition (c) is false we non deterministically pick a region r, a region r which intersects r and a edge e and check whether r is reachable and e is not firable from r or r and fireable from (l r , min r ). By Savitch construction, we obtain a deterministic algorithm in P SP ACE. In order to show the P SP ACE-hardness, we adapt the construction given in [START_REF] Aceto | Is Your Model Checker on Time? On the Complexity of Model Checking for Timed Modal Logics[END_REF] (appendix D) which reduces the acceptation problem for linear bounded Turing machines (LBTM) to the reachability problem for TA with restricted guards. In order to be self-content, we develop the complete proof.

The Turing machine M = Q, Σ, q 0 , q F , T r is defined by Q its finite set of states, Σ = {a, b} its alphabet, q 0 (resp. q F ) its initial (resp. final) state and T r the transitions of the machine. Each transition θ = (q, α, alpha , δ, q ) is defined by its current state q, the character to be read α, the character to be written α , the move to be performed δ ∈ {L, R} and the next state q . Let w 0 be a word of length n. We first build a TA A M,w 0 bisimilar to a TPN which reaches location end iff w 0 is accepted by M.

The set of clocks of A M,w 0 is {x i } 0≤i≤n . Clock x 0 rules the behaviour of the simulation by letting exactly 1 time unit elapse before performing instantaneously the simulation of a machine transition. For 1 ≤ i, at the time of transition execution, the value of clock x i is related to the value of the i th cell: x i = 1 iff the cell contains an a and x i ≥ 2 iff the cell contains an b.

The set of locations of A M,w 0 is:

{(q, i) | q ∈ Q, 1 ≤ i ≤ n} ∪ {init, end} ∪ {(i, θ, l) | 1 ≤ i ≤ n, θ ∈ T r, 1 ≤ l ≤ n}
When the machine is in state q reading the i th cell, the location of an automaton is (q, i). When the machine changes its configuration to state q reading the i th cell by transition θ = (q, α, alpha , δ, q ), the automaton will first let 1 time unit elapse and then will successively visit (i, θ, 1), . . . , (i, θ, n), (q , i ) in zero time.

Thus the invariant associated with every (q, i) is x 0 ≤ 1 and the one associated with every (i, θ, l) is x 0 ≤ 0. Let us describe the automaton transitions related to such a transition (we do not give the labels as the TA is injectively-labelled). We define s(i, δ) by: if δ = L then s(i, δ) = i -1 else s(i, δ) = i + 1.

-(q, i) g,{x 0 } ----→ (i, θ, 1) with g = (x 0 ≥ 1) ∧ (x i ≤ 1) (resp. g = (x 0 ≥ 1) ∧ (x i ≥ 2)) if α = a (resp. α = b) -(i, θ, i) true,r ----→ (i, θ, i + 1) if i < n and (n, θ, n) true,r ----→ (q , s(n, δ)) with r = {x i } (resp. r = ∅) if α = a (resp. α = b) -(i, θ, l)

x l ≤1,{x l } ------→ (i, θ, l +1) if l < n∧i = l and (i, θ, n)

x n ≤1,{x n } -------→ (q , s(i, δ)) if i = n (in this case δ must be L).

-(i, θ, l)

x l ≥2,∅ ----→ (i, θ, l + 1) if l < n ∧ i = l and (i, θ, n)

x n ≥2,∅ -----→ (q , s(i, δ)

) if i = n
The first step of the simulation consists in checking whether the i th cell contains α whereas the other steps consists in resetting the clocks corresponding to a cell containing an a. By this way, such clocks will have value 1 at the next stage of the simulation whereas the other ones will have a value at least 2. In the last step, the new location (q , s(i, δ)) is reached.

It remains to "initialize" the clocks according to w 0 . This is performed through the transition init

x 0 ≥1,{x 0 }∪r w 0 ----------→ (q 0 , 1) with r w 0 being the positions of a in w 0 . Once again, the invariant associated with init is x 0 ≤ 1. At last, we add transitions in order to reach end: (q F , i) true,{x 0 } ------→ end. From the details of the contruction, it is clear that the size of A M,w 0 is polynomial w.r.t. n. Furthermore it satisfies the conditions (a), (b) and (c). This is mainly due to the fact that in a configuration with x 0 ∈ {0, 1} all the other clocks have integral values.

We build another TA A M,w 0 by adding an edge end x 0 =0,∅ ----→ end.

If the LBTM M does not accept the word w 0 , then the state end is not reachable and A M,w 0 which behaves as A M,w 0 , satisfies the conditions (a),(b),(c).

If the LBTM M accepts the word w 0 , then the state end is reachable and A M,w 0 does not satisfy the condition (c) (the additional edge is fireable when entering end but not after letting the time elapse). The fact that the reachability problem for the class T A wtb is P SP ACE-complete was proved implicitely within the proof above.

Conclusion

In this paper, we considered the subclass T A wtb of injectively-labelled TA such that a timed automaton A is in T A wtb if and only if there is a TPN N weakly timed bisimilar to A. We obtained a characterization of this class, based on the region automaton associated with A. To prove that our condition is necessary, we introduced the notion of uniform bisimulation between TA and TPNs. For the sufficiency, we proposed two constructions. From this characterization, we have proved that for the class T A wtb , the membership problem and the reachability problem are P SP ACE-complete. Of course, checking this condition is therefore expensive but it should be noted that the syntactic subclass of TA proposed in [START_REF] Bérard | Comparison of the Expressiveness of Timed Automata and Time Petri Nets[END_REF] fulfills the condition. Hence there is a simpler (even if coarser) way to check a sufficient condition avoiding the complexity. Furthermore translation of a TA into a TPN provides an alternative method for verification with tools like TINA [START_REF] Berthomieu | Time Petri Nets Analysis with TINA[END_REF] or ROMEO [START_REF] Gardey | Roméo: A Tool for Analyzing Time Petri Nets[END_REF] in case UPPAAL [START_REF] Pettersson | Uppaal2k[END_REF] or KRONOS [START_REF] Yovine | Kronos: A Verification Tool for real-Time Systems[END_REF] are inefficient. Besides the techniques introduced in this paper give some insight for use of the region automaton in order to obtain expressivity results.

Fig. 2 .

 2 Fig. 2. Partition of (R + ) 2 with granularity g = 1 and K = 3

Figures 2 and 3

 3 Figures 2 and 3 represent different partitions for the set of two clocks X = {x, y}. The horizontal and vertical lines correspond to the possible intervals I x and I y whereas the diagonal lines specify the ordering of fractional parts.Figure2is associated with g = 1 and K = 3. For this example, elementary zones Z 1 and Z 2 are described as follows:Z 1 : (2 < x < 3) ∧ (1 < y < 2) ∧ (0 < f rac(y) < f rac(x)) or equivalently, (2 < x < 3) ∧ (1 < y < 2) ∧ (xy > 1) and Z 2 : (x ≥ 3) ∧ (1 < y < 2).Figure 3 (left) is associated with g = 2 and K = 2 while figure 3 (right) is associated with g = 2 and K = +∞. The dotted lines of this figure mean that the pattern is infinitely repeated.

Figure 3 (

 3 Figures 2 and 3 represent different partitions for the set of two clocks X = {x, y}. The horizontal and vertical lines correspond to the possible intervals I x and I y whereas the diagonal lines specify the ordering of fractional parts.Figure2is associated with g = 1 and K = 3. For this example, elementary zones Z 1 and Z 2 are described as follows:Z 1 : (2 < x < 3) ∧ (1 < y < 2) ∧ (0 < f rac(y) < f rac(x)) or equivalently, (2 < x < 3) ∧ (1 < y < 2) ∧ (xy > 1) and Z 2 : (x ≥ 3) ∧ (1 < y < 2).Figure 3 (left) is associated with g = 2 and K = 2 while figure 3 (right) is associated with g = 2 and K = +∞. The dotted lines of this figure mean that the pattern is infinitely repeated.

1 Fig. 3 .

 13 Fig. 3. Partitions of (R + ) 2 with granularity g = 2, for K = 2 and K = +∞

Fig. 4 .

 4 Fig. 4. A labelled time Petri net

Fig. 5 .

 5 Fig. 5. An execution in a time Petri net

Lemma 1 .

 1 Let (M, ν) and (M, ν + δ) be two admissible configurations of a g-TPN with ν, δ ∈ R En(M ) ≥0

Fig. 7 .

 7 Fig. 7. The region automaton of A 0 (K = 2, g = 1)

  1. a time step from a time-closed region, 2. a time step from a time-open region, 3. a discrete step into a time-closed region, and 4. a discrete step into a time-open region.

4 .

 4 A discrete step into a time-open region (see figure 8(4)). In order to reach a time-open region by a discrete step, the corresponding transition must start from a time-open region and must not reset any clock. Let ( r , min r + δ + d) ∈ r and ( r , min r + δ + d) e -→ (l , min r + δ + d). Here we have used the hypothesis that no clock is reset. Then there is a firing sequence (M r , ν r + proj r (δ) + d) w -→ labelled by e. Due to the lemma 1, (M r , ν r +proj r (δ)) w -→. ( r , v r +δ) is bisimilar to (M r , ν r + proj r (δ)). Thus ( r , min r + δ) e -→ (l , min r + δ) d -→ (l , min r + δ + d).

  (a), (b) and (c) of Theorem 1 hold for R(A) g,∞ is now straightforward: (a) This assertion is included in the inductive assertions. (b) Let r be a region, let ( r , min r + δ) ∈ r be a configuration with δ ∈ [0, 1/g[ X , then ∃(M, ν) ν ∈ N En(M ) g bisimilar to ( r , min r ) and (M, ν + δ ) with δ ∈ [0, 1/g[ En(M ) bisimilar to ( r , v + δ). Suppose that ( r , min r + δ) e -→, then (M, ν + δ ) w -→ with w an instantaneous firing sequence and label(w) = e. Now by lemma 1-(ii), (M, ν) w -→, thus ( r , min r ) e -→. (c) Let r be a region, and ( r , min r + δ) ∈ r with δ ∈ [0, 1/g] X thus ∃(M, ν) bisimilar to ( r , min r ) and (M, ν + δ ) with δ ∈ [0, 1/g] En(M ) bisimilar to ( r , min r + δ). Suppose that ( r , min r ) e -→, then (M, ν) w -→ with w an instantaneous firing sequence and label(w) = e. By lemma 1-(i), we have (M, ν + δ ) w -→, thus ( r , min r + δ) e -→.

Fig. 10 .Fig. 11 .

 1011 Fig. 10. Subnets for x > h and x ≥ h (with h > 0) in guards

Fig. 12 .

 12 Fig. 12. The subnet for edge e = ( , γ = γ 1 ∧ . . . ∧ γ m(e) , a, R = {x 1 , . . . , x k(e) }, )

  Let c be a condition occuring in the guard of e. If c = [x ≥ a] then T x≥a is marked which implies that ν(x) ≥ a and then v(x) ≥ a, thus min r(x) = v(x) ≥ a. If c = [x > a] then then T x>a is marked which implies that ν(x) ≥ a + 1 and then v(x) ≥ a + 1 thus min r (x) = v(x) ≥ a + 1 > a If c = [x ≤ a] then T x≤a is marked which implies that ν(x) ≤ a + 1/2 and then v(x) ≤ a + 1/2 thus min r (x) = v(x) ≤ a If c = [x < a] then T x<a is marked which implies that ν(x) ≤ a -1/2 and then v(x) ≤ a -1/2 thus min r (x) = v(x) ≤ a -1 < a So ( , v) e -→ ( , v) for some ( , v ). By construction of N and definition of R, ( , v )R(M , ν ). Case 4: (M, ν) d -→ (M, ν + d) An intermediate marking cannot let time elapse. Thus M is a permanent marking. Let x ≤ a belonging to the invariant of . Then a = 0, otherwise from (M, ν), transition stop must be fired and time may not elapse. Similarly since stop x≤a is only possibly fireable from (M, ν + d), it follows that ν(x) + d ≤ a, thus v(x) + d ≤ a. Consequently ( , v) d -→ ( , v + d) and obviously ( , v + d)R(M, ν + d).

1 C 2 Fig. 15 .

 1215 Fig. 15. Simulation of a transition

1 -→ (l 1 , 3 Fig. 16 .

 11316 Fig. 16. Subnet of transition c

  v)] is contained in the topological closure r of some reachable region such that min r = c and l = l r . Since ( , c) e -→ ( , c ) is possible in A, condition (c) implies that a move ( , v) e -→ ( , v ) is also possible in A. From the definition, (M , ν )R( , v ).

A preliminary version of this work has been published in[START_REF] Bérard | When are timed automata weakly timed bisimilar to time Petri nets ? 25[END_REF].

time successor of r. Let ( r , min r + δ 0 ) be some item of r. ( r , min r + δ 0 ) d -→ for some d > 0. Thus (by induction hypothesis) in N there is a step sequence of (M r , ν r + proj r (δ 0 )) d 0 t 1 ...t n d n -------→ with all transitions labelled by and d k = d. Let d k be the first non zero elapsing of time. By application of lemma 1-(ii), the firing sequence t 1 . . . t k is fireable from (M r , ν r ).

Let us choose (M r , ν r ) the configuration reached by this sequence. By application of lemma 1-(i), this firing sequence is also fireable from any (M r , ν r + proj r (δ)) bisimilar to ( r , min r +δ) ∈ r and it leads to (M r , ν r +proj r (δ)) (still bisimilar to ( r , min r +δ)) where φ r (resp. ν r ) is equal to φ r (resp. ν r ) for transitions always enabled during the firing sequence and φ r (resp. ν r ) is obtained by associating the class of index 1 (resp. by associating the value 0) with the transitions newly enabled. Since (M r , ν r ) let the time elapse and since N is a g-TPN, we note that ∀t ∈ En(M r ), ν r (t) + 1/g ∈ I(t) ↓ . Now let ( r , min

, this last configuration being necessarily bisimilar to ( r , min r + δ + d).

2. A time step from a time-open region (see figure 8(2)). Let r be an time-open region and let us denote r = succ(r). Note that r ⊂ r. Let us define X max r the class [x] r with maximal index. We remark that min r = min r + δ 0 where if x ∈ X max r then δ 0 (x) = 1/g else δ 0 (x) = 0. We choose (M r , ν r ) = (M r , ν r + proj r (δ 0 )). Let t ∈ En(M r ) and x ∈ φ r (t) then φ r (t) = [x] r (letting time elapse does not split the classes). So proj r and proj r are identical. Now let (l r , min

For this step, we have not used the characteristics of time Petri nets.

3. A discrete step into a time-closed region (see figure 8(3)).

Case a. We first consider the case where r is a time-closed region. Let ( r , min r +δ 0 ) be some element of r. Suppose that ( r , min r +δ 0 )

Then in N there is an instantaneous firing sequence (M r , ν r + proj r (δ 0 )) w -→ labelled by e. Due to lemma 1, this firing sequence is also fireable from any (M r , ν r + proj r (δ)) bisimilar to ( r , min r + δ) ∈ r. By bisimilarity, ( r , min r +δ) e -→ for any ( r , min r + δ) ∈ r. Let r be the region including ( , v +δ 0 ), then any configuration of r is reachable by this discrete step. Note that r = l and min r = v . From (M r , ν r + proj r (δ)), the sequence w leads to some (M , ν ) bisimilar to ( r , min r + δ )). We now show how to define M r , ν r and φ r . First M r = M . Second, ν r (t) = ν r (t) for transitions t always enabled during the firing sequence and ν r = 0 otherwise. At last, φ r is obtained from φ r We achieve the proof with an auxiliary lemma and the fact that R is a weak timed bisimulation.

The following lemma which relates regions and classes, shows how the class automaton will be used to control the firing of a transition when the minimal point c is in not in the same region than v. Lemma 6. Let A be an automaton satisfying the conditions of theorem 1, let C = ( , Z) be a class of the class automaton and ( , v) ∈ C. Let ( , v) ∈ r where r is a region w.r.t. to the choice K = ∞ (which means that there is a infinite number of regions). Then ∀( , v ) ∈ r, ( , v ) ∈ C.

In particular, ( , v ) ∈ C (note that v = min r ).

Proof. The proof is by induction on the reachability relation between regions.

The case of a discrete step follows from conditions (b) and (c) of theorem 1. The case of a time step follows from the choice of K = ∞ which implies that given a region r, every item of succ(r) is reached by a time step from an item of r.

Recall that classes are closed by time elapsing.

Lemma 7. The relation R defined above is a weak timed bisimulation.

Proof. Assume that (M, ν)R( , v) and consider a move in A.

Case 1:

In this case, we must consider different subcases, according to the regions that can be reached by elapsing time. We consider only moves in which at most one different region is reached, the general case would be a combination of those elementary moves. First note that since v can be reached, no transition related to an invariant condition in N is enabled before d. Moreover, if (M, ν) is an intermediate configuration, we first apply the sequence described above and reach the equivalent configuration (M 1 , ν 1 ). Also in this case, since classes are unchanged by elapsing time, if we prove that a delay move is possible from (M 1 , ν 1 ), we immediately obtain that the class is the same in the resulting configuration. Thus, the resulting configuration will be equivalent to ( , v + d).

• If v belongs to a time-open region, the case where v belongs to the same time-open region is easy, it simply corresponds to a delay transition from (M 1 , ν 1 ) in N , each clock being in some h x c and staying inside (no token move), with (M 1 , ν 1 + d) equivalent to ( , v + d).

If v has reached an integer value, we consider a clock x with greatest integral part, so that v (x) = v(x) +1 = v(x)+d with v(y)+d ≤ v(y) +1 for every other clock. In this case also, we obtain a delay move in N from (M 1 , ν 1 ).

• If there are some clocks x for which v(x) has an integer value, then elapsing time leads to the successor region, which is time-open. From (M 1 , ν 1 ), it is possible to reach with instantaneous transitions a configuration (M 2 , ν 2 ) where for all clocks with integer values, M 2 (h x c ) = 1 with its associated c maximal, and (M 2 , ν 2 ) still equivalent to ( , v). Now from (M 2 , ν 2 ), a delay move can be applied so that (M, ν)