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

Ramchandra

S Akshay
email: akshayss@cse.iitb.ac.in

Ramchandra Phawade

Combining Free

Keywords: Petri nets, Time, Free-choice, Robustness

HAL is

Introduction

Modern systems are composed of several distributed components that work in real-time to satisfy a given specification. This makes them difficult to reason about manually and encourages the use of formal methods to analyze them automatically. This in turn requires the development of models that capture all the features of a system and still allow efficient algorithms for analysis. Further, to bring formal models closer to real world implementations, it is important to design robust models, i.e., models that preserve their behavior or at least some important properties under imprecise time measurement.

In this paper, we consider Petri nets extended with time constraints for modeling real-time distributed systems. For timed variants of Petri nets, many basic problems are usually undecidable or algorithmically intractable. Our goal is to consider structural restrictions which allow us to model features such as unbounded resources as well as time-deadlines while remaining within the realm of decidability and satisfying some robustness properties.

Time Petri nets (TPNs) [START_REF] Merlin | A study of the recoverability of computing systems[END_REF] are a classical extension of Petri nets in which time intervals are attached to transitions and constrain the time that can elapse between the enabling of a transition and its firing date. In such models, the basic verification problems considered include: reachability, i.e., whether a particular marking (or a configuration) can be reached in the net; termination, i.e., whether there exists an infinite run in the net; boundedness, whether there is a bound on the number of tokens in the reachable markings; and firability, i.e., whether a given transition is fireable in some execution of the net.

It turns out that all these basic problems are in general undecidable [START_REF] Jones | Complexity of some problems in Petri nets[END_REF] for TPNs, though they are decidable for the untimed version of Petri nets. The main reason is that TPNs are usually equipped with an urgent semantics: when the time elapsed since enabling of a transition reaches the maximal value of its interval, a transition of the net has to fire. This semantics breaks monotony (the behaviors allowed from a marking, and from a larger marking can be completely different). Indeed, with a TPN, one can easily encode a two-counter machine, yielding undecidability of most of the verification problems (see [START_REF] Jones | Complexity of some problems in Petri nets[END_REF][START_REF] Reynier | Weak time Petri nets strike back![END_REF] and Section 7 for such an encoding). Decidability can be obtained by restricting to the subclass of bounded TPNs, for which the number of tokens in all places of reachable markings is bounded by some constant. Other ways to obtain decidability are by weakening the semantics [START_REF] Reynier | Weak time Petri nets strike back![END_REF], or restricting the use of urgency [START_REF] Akshay | Decidable classes of unbounded Petri nets with time and urgency[END_REF].

Another important problem in this setting is the question of robustness. Robustness can be defined as the preservation of properties of systems that are subject to imprecision of time measurement. The main motivation for considering this is that formal models usually have an idealized representation of time, and assume an unrealizable precision in measurement of time which cannot be guaranteed by real implementations. Robustness has been studied extensively for timed automata since [START_REF] Puri | Dynamical properties of timed automata[END_REF], and more recently for TPNs [START_REF] Akshay | Robustness of time Petri nets under guard enlargement[END_REF], but decidability results are only known in a bounded-resource setting.

The definition of the semantics plays an important role both to define the expressive power of a model, and to obtaining decidability results. When considering unbounded nets, where multiple (and a possibly unbounded number of) tokens may be present at every place, one has to decide whether transitions should be considered as multiply-enabled, and if so, fix a policy to handle multiple instances of enabling. This becomes even more complicated when real-time constraints are considered. Indeed, several possible variants for the multiple enabling semantics have been considered, as discussed in [START_REF] Boucheneb | On multi-enabledness in time Petri nets[END_REF]. In this paper, we fix one of the variants and consider TPNs equipped with a multi-enabling urgent semantics, which allows to start measuring elapsed time from every occurrence of a transition enabling. This feature is particularly interesting: combined with urgency, it allows for instance, to model maximal latency in communication channels. We adopt a semantics where time is measured at each transition's enabling, and with urgency, i.e. a discrete transition firing has to occur if a transition has been enabled for a duration that equals the upper bound in the time interval attached to it. Obviously, with this semantics, counter machines can still be encoded, and undecidability follows in general.

We focus on a structural restriction on TPNs, which restricts the underlying net of the given TPN to be free-choice, and call such nets Free-choice TPNs. Free-choice Petri nets have been extensively studied in the untimed setting [START_REF] Esparza | Free Choice Petri nets[END_REF] and have several nice properties from a decidability and a complexity-theoretic point of view. In this class of nets, all occurrences of transitions that have a common place in their presets are enabled at the same instant. Such transitions are said to belong to a cluster of transitions. Thus, with this restriction, a transition can only prevent transitions from the same cluster to fire, and hence only constrain firing times of transitions in its cluster. Further, we disallow forcing of instantaneous occurrence of infinite behaviors, that we call (forced) 0-delay firing sequences. This can easily be ensured by another structural restriction forbidding transitions or even loops in TPNs labeled with [0, 0] constraints.

Our main results are the following: we show that for a free-choice TPN N under the multi-enabling urgent semantics, and in the absence of 0-delay firing sequences, the problem of checking firability of a transition and of termination are both decidable. The main idea is to show that, after some pre-processing, we can reduce these problems to corresponding problems on the underlying untimed free-choice PN. More precisely, we are able to show that every partially-ordered execution of the underlying untimed PN can be simulated by N , i.e., it is the untimed prefix of a timed execution of N . To formalize this argument we introduce definitions of (untimed and timed) causal processes for unbounded TPNs, which is another contribution of the paper.

Finally, we address several robustness questions. The problem of robustness for TPNs has previously been considered in [START_REF] Akshay | Robustness of time Petri nets under guard enlargement[END_REF], but shown decidable only for bounded classes of nets. We show that the problem of robustness of firability with respect to guard enlargement, i.e., whether there exists a ∆ > 0 such that enlarging all guards of a TPN by ∆ preserves the set of fireable transitions, is decidable for free-choice TPNs without 0-delay firing sequences. We also consider the same question for guard shrinking, i.e. existence of a > 0 such that shortening the guards of a TPN by preserves the set of fireable transitions. We show that this problem is also decidable in our model. Finally, we consider robustness of termination (whether there exists an infinite run) w.r.t. guard enlargement or shrinking, and show that this question is decidable as well. To the best of our knowledge, these are the first decidability results on robustness for a class of unbounded TPNs.

Related work. Verification, unfolding, and extensions of Petri nets with time have been considered in many works. Other than TPNs, a different yet common approach to integrate time to Petri nets is to attach time to tokens, constraints to arcs, and allow firing of a transition iff all constraints attached to transitions are satisfied by at least one token in each place of its preset. This variant, called Timed-arc Petri nets, enjoys decidability of coverability [START_REF] Abdulla | Timed Petri nets and BQOs[END_REF], but cannot impose urgent firing, which is a key issue in real-time systems. A variant of Timed-arc Petri nets with place invariants is proposed in the TAPAAL tool [START_REF] Byg | TAPAAL: editor, simulator and verifier of timed-arc petri nets[END_REF]. This allows for the modeling of urgency, but at the cost of decidability of coverability in unbounded nets [START_REF] Jacobsen | Verification of timed-arc Petri nets[END_REF]. In TPNs, [START_REF] Reynier | Weak time Petri nets strike back![END_REF] propose a weak semantics for TPNs, where clocks may continue to evolve even if a transition does not fire urgently. With this semantics, TPNs have the same expressive power as untimed Petri nets, again due to lack of urgency, which is not the case in our model. Recently, [START_REF] Akshay | Decidable classes of unbounded Petri nets with time and urgency[END_REF] considered variants of time and timed-arc Petri nets with urgency (TPNUs), where decidability of reachability and coverability is obtained by restricting urgency to transitions consuming tokens only from bounded places. This way, encoding of counter machines is not straightforward, and some problems that are undecidable in general for time or timed-arc Petri nets become decidable. The free-choice assumption in this paper is orthogonal to this approach and it would be interesting to see how it affects decidability for TPNUs.

Finally, partial-order semantics have been considered in the timed setting: [START_REF] Ruiz | Timed processes of timed Petri nets[END_REF] defines a notion of timed process for timed-arc Petri nets and [START_REF] Winkowski | Algebras of processes of timed Petri nets[END_REF] gives a semantics to timed-arc nets with an algebra of concatenable weighted pomsets. However, processes and unfoldings for TPNs have received less attention. An initial proposal in [START_REF] Aura | A causal semantics for time Petri nets[END_REF] was used in [START_REF] Bushin | Time process equivalences for time Petri nets[END_REF] to define equivalences among time Petri nets. Unfoldings and processes were refined by [START_REF] Chatain | Complete finite prefixes of symbolic unfoldings of safe time Petri nets[END_REF] to obtain symbolic unfoldings for safe Petri nets. The closest work to ours is [START_REF] Chatain | Back in time Petri nets[END_REF], where processes are defined to reason about the class of free choice safe TPNs. However, this work does not consider unbounded nets, and focuses more on semantic variants w.r.t. time-progress than on decidability or robustness issues.

This paper is an extended version of results presented at [START_REF] Akshay | Combining free choice and time in petri nets[END_REF]. With respect to this first contribution, it contains all the proofs in full details, and an extended comparison between the single and multi-enabling of TPNs. It also establishes new results on robustness of firability and termination, that are now considered with respect to guard enlargement as well as shrinking. The paper is organized as follows: Section 2 introduces notations and defines a class of TPNs with multi-enabling semantics. Section 3 defines processes for these nets. Section 4 introduces the subclass of Free-choice TPNs and relates properties of untimed and timed processes. In Section 5, this relation is used to prove decidability of firability and termination for FC-TPNs and, in Section 6 to address robustness of firability and termination to guard enlargement and shrinking. Section 7 discusses the assumptions needed to obtain decidability, and issues related to decidability of other problems in FC-nets, before conclusion.

Multi-enabledness in TPNs

Let Σ be a finite alphabet, Σ * be the set of finite words over Σ. For a pair of words w, w ∈ Σ * , we will write w ≤ w iff w = w.v for some v ∈ Σ * . Let N, Q, R ≥0 , respectively, denote the sets of naturals, rationals, and non-negative real numbers. An interval I of R ≥0 is a Q ≥0 -interval iff its left endpoint belongs to Q ≥0 and right endpoint belongs to Q ≥0 ∪ {∞}. An interval is closed if it is of the form [α, β], and open otherwise. Let I denote the set of Q ≥0 -intervals of R ≥0 . For a set X of (clock) variables, a valuation v for X is a mapping v : X → R ≥0 . Let v 0 (X) be the valuation which assigns value 0 to each clock in X. For any

δ ∈ R ≥0 , the valuation v + δ is : ∀x ∈ X, (v + δ)(x) = v(x) + δ.
A Petri net (PN) U is a tuple U = (P, T, F ), where P is a set of places, T = {t 1 , t 2 , . . . , t K } is a set of transitions, and F ⊆ (P × T ) ∪ (T × P ) is a flow relation. A marking M is a function P → N that assigns a number of tokens to each place. We let M 0 denote an initial marking for a net. For any

x ∈ P ∪ T (called a node) let • x = {y ∈ P ∪ T | (y, x) in F } and x • = {y ∈ P ∪ T | (x, y) in F }.
For a transition t, we will call • t the preset of t, and t • the postset of t. The semantics of a Petri net is defined as usual: starting from a marking M , a transition t can be fired if for every p ∈ • t, M (p) > 0. This firing results in new marking M such that

M (p) = M (p) -| • t ∩ {p}| + |t • ∩ {p}|.
We denote a discrete move of a Petri net from M to M using transition t by M t → M , and we write M → M when there exists a discrete move from M to M . The language Lang(U, M 0 ) of a Petri net U is the set of words of the form

t 1 • • • t n such that M 0 t1 -→ M 1 • • • tn -→ M n .
The set of reachable markings that can be obtained via an arbitrary number of moves starting from M 0 are denoted as Reach(U, M 0 ). We say that a Petri net is safe if, for every marking M ∈ Reach(U, M 0 ), for every place p ∈ P , M (p) ≤ 1. Let x be any node of a net. The cluster of x (denoted by [x]) is a minimal set of nodes of P ∪ T satisfying following conditions:

i) x ∈ [x], ii) if a place p is in [x], then p • ⊆ [x], and iii) if a transition t is in [x], then • t ⊆ [x].
Intuitively, two transitions belong to the same cluster if they share a place in their preset, and two places belong to the same cluster if they share a transition in their postset. The notion of cluster of a node and the flow relation of a Petri net U allows for the definition of a partition of nodes from P ∪ T . The subsets in this partition are called the clusters of U.

Time Petri nets

Definition 1. A time Petri net (TPN) N is a tuple (U, M 0 , I) where U = (P, T, F ) is the underlying net, M 0 is an initial marking, and I : T → I(Q ≥0 ) associates with each transition a firing interval.

We denote by ef t(t) and lf t(t) the lower and upper bound of interval I(t). For a TPN N = (U, M 0 , I) let Untime(N ) = (U, M 0 ) denote the underlying net i.e., with no timing constraints for any transitions. The clusters of a TPN N = (U, M 0 , I) are the clusters of the underlying untimed net U. The example of Figure 1 is a TPN. The time intervals attached to transition t 1 , t 2 , t 3 , t 4 are respectively [START_REF] Jones | Complexity of some problems in Petri nets[END_REF][START_REF] Akshay | Decidable classes of unbounded Petri nets with time and urgency[END_REF], [0, 1], [START_REF] Merlin | A study of the recoverability of computing systems[END_REF][START_REF] Puri | Dynamical properties of timed automata[END_REF], [2, ∞). Note that intervals attached to transitions t 3 and t 4 are open. This net contains three clusters:

p 1 t 1 p 2 p 3 t 2 t 3 t 4 p 4 [2, 4] [0, 1] [1, 5) [2, ∞)
C 1 = {p 1 , p 2 , t 1 } and C 2 = {p 3 , t 2 , t 3 , t 4 } and C 3 = {p 4 }.
So far, we have defined the syntax of TPNs, but their semantics is not obvious from the notation. In fact, several semantics for TPNs exist in the literature (see for instance [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][START_REF] Boucheneb | On multi-enabledness in time Petri nets[END_REF][START_REF] Reynier | Weak time Petri nets strike back![END_REF]). A frequently used semantics for TPNs is a single server semantics [START_REF] Merlin | A study of the recoverability of computing systems[END_REF]: it attaches a clock x t to each enabled transition t. This clock is initialized and starts measuring time as soon as transition t becomes enabled. Other semantics consider every occurrence of enabling of transitions and memorize the time elapsed since every enabling. This is called a multi-enabling semantics. In the next sections, we define formally these two frequently used semantics, namely the single server semantics of [START_REF] Merlin | A study of the recoverability of computing systems[END_REF], and a multi-enabling semantics with a FIFO policy, which is a standard setting (see e.g., [START_REF] Boucheneb | On multi-enabledness in time Petri nets[END_REF]).

Single server semantics for TPNs

A frequently used semantics for TPNs is a clock-on-transition and single server semantics, that can be found for instance in [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][START_REF] Reynier | Weak time Petri nets strike back![END_REF]. This semantics associates a clock x t to every transition t of the considered TPN. Formally, given a TPN N = (U, M 0 , I) with U = (P, T, F ), we define a set of clocks

X N = {x t | t ∈ T }. A configuration of N is a pair (M, ν)
where M is a marking, and ν is a valuation. Intuitively, valuation ν associates a real value to every clock in X N that encodes the time elapsed since enabling of transitions. A transition is enabled in (M, ν) iff M (p) > 1 for every place p ∈

• t. It is fireable if ν(t) ∈ I(t). It is urgent if ν(t) = lf t(t).
From a given configuration (M, ν) , one can let δ ∈ R time units elapse iff ν(t) + δ < lf t(t) for every transition t enabled in (M, ν), that is if no transition is urgent. Every fireable transition t in configuration (M, ν) can fire, leading to a configuration (M , ν ). A transition t i is newly enabled by firing of t if t i is enabled in M and either t i = t and t i is not enabled in M \ • t, or t i = t. The single server semantics of a TPN can be formally defined as moves from a configuration (M, ν) to a configuration (M , ν ). These moves can be timed or discrete moves:

• timed moves are of the form (M, ν) δ -→ (M, ν + δ), with δ ∈ R. Such a move is allowed if for all t enabled at marking M , ν(x t ) + δ ≤ lf t(t) (or ν(x t ) + δ < lf t(t) if I(t) is an open interval of the form [a, b) or (a, b)), i.e.
, no transition becomes urgent while letting δ time units elapse,

• discrete moves are moves of the form (M, ν) t -→ (M , ν ), where M (p) = M (p) \ • t + t • for every p in P , and for every t i ∈ T , ν (x ti ) = 0 if t i is newly enabled by firing of t, and ν (x ti ) = ν(x ti ) otherwise.

Consider the example of Figure 2. This net defines a set of timed words of the form

(t 1 , d 1 )• (t 1 , d 2 ) • • • (t 1 , d k )||(t 2 , d 1 )((t 2 , d 2 ) • • • (t 2 , d k )
where || is the usual shuffle of words, and that satisfies ∀i ∈ {1, . . . , k},

d i ≤ d i , ∀i ∈ {2, . . . , k}, d i -d i-1 ≤ 1, d 1 -d 1 = 1 and d i -d i-1 = 1.
Informally, transition t 1 produces tokens that are consumed by t 2 . Tokens are produced at a rate of more than one token per time unit, but every instance of t 2 must occur exactly 1 time unit after the preceding instance of t 2 , except for the first one, that occurs exactly one time unit after the first occurrence of t 1 .

p 0 t 1 p 1 t 2 p 2 [0, 1] [1, 1]
Figure 2: A TPN that discriminates between single and multi-enabling semantics

Multi-enabling semantics for TPNs

Let us now describe the semantics of Time Petri nets with multi-enabledness. In a multi-enabling semantics, when a marking associates to each place in the preset of a transition a number of tokens that is several times the number of tokens needed for the transition to fire, then this transition is considered as enabled several times, i.e. several occurrences of this transition are waiting to fire. Defining a multi-enabling semantics needs to address carefully which instances of enabled transitions can fire, what happens when an instance of a transition fires, in terms of disabling and creation of other instances. Several policies are possible as discussed in [START_REF] Boucheneb | On multi-enabledness in time Petri nets[END_REF][START_REF] Cerone | Time-based expressivity of time Petri nets for system specification[END_REF][START_REF] Boyer | Multiple enabledness of transitions in Petri nets with time[END_REF]. In the rest of the paper, we adopt a semantics where the oldest instances of transitions fire first, are subject to urgency requirements, and the oldest instances are also the disabled ones when a conflict occurs. We formalize this below. Definition 2. Let M be a marking of a TPN N = (U, M 0 , I). A transition t ∈ T is k-enabled at marking M , for k > 0, if for all p ∈ • t, M (p) ≥ k and there exists a place p ∈ • t such that M (p) = k. In this case, k is called the enabling degree of t at marking M , denoted deg(M, t).

Therefore, from a marking M , and for each transition t, there are exactly deg(M, t) instances of transition t which are enabled. A configuration of a time Petri net under multi-enabling semantics associates a clock with each instance of a transition that has been enabled. This is called threshold semantics in [START_REF] Boucheneb | On multi-enabledness in time Petri nets[END_REF]. Time can elapse if no urgency is violated, and an occurrence of a transition t is allowed to fire if it has been enabled for a duration that lays within the interval attached to t. The notion of configuration in a multi-enabling semantics differs from that used in single server semantics, as clocks used in a single server semantics can only remember one elapsed duration per transition.

Formally, a configuration in a multi-enabling semantics is a pair C = (M, enab), where M is a marking, and enab is a partial function enab : T → (R ≥0 ) * . We denote by enab(t) i the i th entry of enab(t), and by dom(enab) the set of transitions that have at least one enabled instance, i.e. such that enab(t) = . For a marking M , t ∈ T , enab(t) is defined iff there exists k > 0 such that t is k-enabled at M . We further require that the length of vector enab(t) is exactly deg(M, t), and if 1 ≤ i < j ≤ deg(M, t), then enab(t) i ≥ enab(t) j . Intuitively, in a configuration C = (M, enab) each enabled transition t is associated with a vector enab(t) of decreasing real values, that record the time elapsed since each instance of t was newly enabled. With this convention, the first enabled instance of a transition t (that must have the maximal clock value) is the first entry enab(t) 1 of the vector. For a value δ ∈ R, we will denote by enab(t) + δ the function that associates enab(t) i + δ to the i th occurrence of t. The initial configuration is a configuration C 0 = (M 0 , enab 0 ) such that for every t ∈ T we have enab 0 (t) = 0 deg(M0,t) , i.e. enab 0 (t) associates deg(M 0 , t) entries to each enabled occurrence of t and initializes their clocks.

The semantics of TPNs under multi-enabling semantics differs from the single server semantics. In particular, one has to remember for each enabling instance of a transition the age of this enabling, and define which instances of other transitions are competing for the same resources. As for single server, the multi-enabling semantics will be decomposed into timed and discrete moves. Discrete moves fire the oldest instance of some transition t, disable conflicting instances of other transitions, and enable new ones. The set of conflicting transitions and the set of newly enabled transitions are computed as follows: Let t and t be two transitions enabled in M and let k = deg(M, t) and k = deg(M , t ) be their enabling degrees at marking M . Transition t is in conflict with transition t in M iff in the intermediate marking M = M \ • t computed when firing t, the enabling degree of t is decreased w.r.t M , i.e if firing t consumes one token from at least a place p with marking M (p) = deg(M, t ) in the preset of t . So if the enabling degree of t at M is k and its enabling degree at M = M -• t is k -1 then one enabled instance of t is disabled when firing t to move from M to M . We disable transitions according to the First Enabled First Disabled (FEFD) policy: disabling the oldest instance of a transition t simply consists in removing enab(t ) 1 from enab(t ). We will denote by cnf l(M, t) the set of enabled transitions that are in conflict with t at marking M . Let newenab(M, t) denote the set of newly enabled instances in the marking reached from M after firing oldest instance of transition t. If a transition t has k enabled instances at M and k + 1-enabled instances M as defined in the above paragraph, then firing t creates one new enabled instance of t . Note that as we consider intermediate markings, firing t can disable the oldest instance of some transition t , and at the same time create a new enabled instance of t .

With these policies in place, we are ready to define formally the multi-enabling semantics of TPNs. Let C = (M, enab) and C = (M , enab ) be configurations. A move from C to C can be either a timed move (that simply lets time elapse), or a discrete move, that represents a transition firing. A transition t is urgent in a configuration C = (M, enab) iff enab(t) 1 = lf t(t).

A timed move from a configuration C = (M, enab) consists in letting δ time units elapse, i.e. move to a new configuration C = (M, enab + δ). Such a move is allowed only if it does not violate urgency. Formally, a timed move of δ > 0 time units from a configuration (M, enab) to a transition (M , enab ) is denoted by (M, enab) δ -→ (M , enab ), and is allowed iff Note that urgency disallows time elapsing: as soon as a transition t is urgent, i.e. enab(t) 1 = lf t(t), one can not increase its clock value, and has to fire t or a conflicting transition t that discards the first enabled instance of t before elapsing time.

• M = M , • enab = enab + δ • for every t ∈ dom(enab), enab(t) 1 + δ ≤ lf t(t) if I(t)
A discrete move consists of firing an enabled instance of a transition t whose clock lies in interval I(t). When firing transitions, we will use the First Enabled First Fired (FEFF) policy, that is the instance of transition t fired is the one with the highest value of time elapsed, i.e., enab(t) 1 . A standard way to address time in the TPN semantics is to start measuring time for a transition as soon as this transition is newly enabled. However, as highlighted in [START_REF] Reynier | Weak time Petri nets strike back![END_REF], there are several possible interpretations of new enabledness. A frequently used semantics is the intermediate semantics, which considers intermediate markings, i.e. when firing a transition t, we consider the marking M = M -• t obtained after removing the tokens in • t from M , and comparing the set of enabled transitions in M with those enabled after production of tokens in the places of t • . Let transition t be k-enabled at marking M for k > 0, and enab(t) 1 ∈ I(t). Then, an instance of t can fire, and we obtain a new marking M via an intermediate marking M as follows:

M (p) = M (p) -1 if p in • t else M (p) = M (p).
Then we define marking M as

M (p) = M (p) + 1 if p in t • and M (p) = M (p) otherwise.
Firing an instance of a transition t changes the enabling degree of several transitions (and not only of t). We will say that a transition is newly enabled by firing of t from M iff its enabling degree is larger in M than in M . Then newly enabled transitions are attached an additional clock initially set to 0 in enab. For transitions whose enabling degree decreases in M (i.e. that are in conflict with t), the first clock in enab is discarded.

Thus, formally, a discrete move that fires an instance of transition t from a configuration (M, enab) to reach a configuration (M , enab ) is denoted by (M, enab) t -→ (M , enab ), and is allowed iff:

• t ∈ dom(enab), and enab(t) 1 ∈ I(t)

• for every p ∈ P , M (p) = M (p) -• t(p) + t • (p),
• enab is computed as follows. Let enab(t) = (v 1 , . . . , v k ), and let enab(t ) = (v 1 , . . . , v k ) for every t ∈ dom(enab).

We first define enab as enab (t) = (v 2 , . . . , v k ) or if deg(M, t) = 1. Then for every t ∈ T \ {t}, Finally, for every t i ∈ T , we set: Intuitively, when an instance of transition t is fired at configuration (M, enab), for every transition t i which is in conflict with t, the first enabling instance of t i is removed from the enab(t i ) list, i.e. we remove from enab(t i ) the value representing the age of the oldest enabling instance of t i to obtain enab . Similarly, moving tokens when firing t creates new enabling instances of some transitions. The clock attached to each new instance of some newly enabled transition t j is set to 0 and this instance is inserted at the end of vector enab (t j ) to obtain enab . Note that the timing information attached to a transition instance is not reset in the time period starting from the moment it is inserted into the enab list to the moment it is removed from the list (either after being fired or disabled).

enab (t ) =    (v 2 , . . . v k ) if t ∈ dom(enab) ∩ cnf l(M,
enab (t i ) =                    enab (t i ).0 if deg(M , t i ) = deg(M , t i ) +
Consider again the example net of Figure 2. Under the multi-enabling semantics, this net defines a set of timed words of the form :

(t 1 , d 1 )• (t 1 , d 2 ) • • • (t 1 , d k )||(t 2 , d 1 )•(t 2 , d 2 ) • • • (t 2 , d k ) where ∀i ∈ 1..k, d i -d i = 1 and ∀i ∈ 2..k, d i -d i-1 ≤ 1.
Informally, t 1 produces an arbitrary number of tokens every time unit. Each token produced is consumed by t 2 exactly 1 time unit after its production. Clearly, such a language cannot be encoded with a TPN under single server semantics, as this needs memorizing time elapsed since the creation of each token, and single server semantics associates only one clock to every transition. Conversely, the set of timed words for this net under the single server semantics is not contained in the language of a TPN under multi-enabling semantics, as this semantics cannot remember the time elapsed between two consecutive firings of the same transition as soon as multiple instances of this transition are enabled. Thus, the single and multi-enabling semantics define incomparable timed languages.

Sequences, timed languages, and diverging behaviors

TPNs can be seen as defining timed languages over the alphabet of transitions. Regardless of the semantics used, we will write C -→ N C when there exists a move from C to C allowed by net N . A timed firing sequence of N starting from configuration q 1 is a sequence of timed and discrete moves

ρ = q 1 α1 -→ q 2 α2 -→ • • • αn-1
---→ q n where α i is either a transition of T (and q i αi -→ q i+1 is a discrete move) or a value from R ≥0 (q i αi -→ q i+1 is a timed move). A configuration C is reachable iff there exists a firing sequence from the initial configuration to C. Let Reach(N , C 0 ) denote the set of reachable configurations of a TPN N , starting from configuration C 0 . For a configuration C = (M, enab) in the multi-enabling semantics, or C = (M, v) in a single server semantics, we denote by Untime(C) = M the untiming of configuration C. In a similar way, we let R(N , C 0 ) = Untime(Reach(N , C 0 )) be the set of (untimed) reachable markings, i.e., R(N , C 0 ) = {M | ∃(M, v) ∈ Reach(N , C 0 )} in the single server semantics, and R(N , C 0 ) = {M | ∃(M, enab) ∈ Reach(N , C 0 )} in the multi-enabling semantics. Note that Reach and Untime operations are not commutative and Reach(Untime(N )) can be different from Untime(Reach(N , C 0 )) for a TPN N . This remark holds for both semantics. A TPN N is bounded if Untime(Reach(N )) is finite, and safe if for every configuration in Reach(N , C 0 ), the marking part M of reached configurations is such that M (p) ≤ 1 for every p ∈ P .

A timed word over T is a word of (

T × R ≥0 ). Let ρ = q 1 α1 -→ q 2 α2 -→ • • • αn-1
---→ q n be a firing sequence starting from q 1 , and let i 1 , . . . , i k denote the indexes of discrete moves in ρ. The timed word associated with ρ is the word w = (t 1 , d 1 ) • • • (t k , d k ), where each t j is transition α ij , d 1 = j<i1 α j , and for every m > 1, d m = d m-1 + im-1<j<im α j . A timed word w is enabled at configuration C if there exists a timed firing sequence ρ starting from C, and w is the timed word associated with this sequence. The untiming of a timed word w = (t 1 , d 1 )

• • • (t n , d n ) is the word Untime(w) = t 1 • • • t n .
For a TPN N = (U, M 0 , I), let Lang(N ) denote the set of all timed words enabled at initial configuration C 0 , and ULang(N ) be defined as Untime(Lang(N )), i.e., the set of words obtained by removing the timing component from words of Lang(N ). Observe that ULang(N ) can be different from Lang(Untime(N )).

Proposition 1. The sets of timed languages defined by TPNs under the single server and multi-enabling semantics coincide for the subclass of safe TPNs, and are different otherwise, i.e., for general TPNs.

Proof: For the first part of the proposition, it suffices to remark that in the single server semantics, x t remembers the same information as enab(t) 1 in the multi-enabling semantics, to show that single and multienabling semantics of every safe net are in fact timed bisimilar. For the second part, the example of Figure 2 shows a Petri net which timed language under the single server semantics is not the language of a net under the multi-enabling semantics, and conversely. 2 Definition 3. A forced 0-delay firing sequence (0-delay firing sequence for short) of N is a sequence from (Q × T ) ∞ such that q i-1 αi -→ q i where α i is a transition of T with ef t(α i ) = lf t(α i ) = 0 for all i ∈ N.

In 0-delay firing sequences, transitions are enabled at each configuration and fired immediately without letting any other transition of the net fire. One can consider that TPNs with 0-delay firing sequence are ill-formed, as they allow diverging behaviors that take no time. A correct specification should not allow such behaviors. Note that forbidding 0-delay firing sequences does not prevent infinite sequences of 0-duration. For example, a TPN in which each transition has ef t(t) = 0 and lf t(t) > 0 can have infinite sequences of 0-duration.

Processes of untimed and timed nets

It is usual to define semantics of nets with discrete firing and time elapsing rules such as the ones proposed in sections 2.2 and 2.3. However, such semantics is defined in terms of sequences of discrete and timed moves, i.e. it is an interleaved semantics. Though one can reason on this timed language, it is often useful and interesting to consider concurrency in the semantics of true concurrency models. For Petri nets, non-interleaved semantics are frequently given in terms of processes, that are roughly speaking, collections of transition occurrences ordered by causal dependencies. Processes have been introduced in Petri nets a long time ago [START_REF] Goltz | The non-sequential behavior of petri nets[END_REF][START_REF] Best | Nonsequential Processes -A Petri Net View[END_REF] and branching processes [START_REF] Engelfriet | Branching processes of petri nets[END_REF][START_REF] Couvreur | Branching processes of general Petri nets[END_REF] have been considered that merge common parts of processes and allow to consider choices in partially ordered semantics. These can be computed inductively using unfolding-based techniques [START_REF] Mcmillan | A technique of state space search based on unfolding[END_REF][START_REF] Esparza | An improvement of McMillan's unfolding algorithm[END_REF].

The notion of time causal process for timed nets with multi-enabledness defined hereafter is a way to equip TPNs with a partial-order semantics. This notion will also be central to reason about TPNs and their properties. The notion of time causal processes for TPNs has been introduced by [START_REF] Aura | A causal semantics for time Petri nets[END_REF], and later used by [START_REF] Chatain | Complete finite prefixes of symbolic unfoldings of safe time Petri nets[END_REF] to study a truly concurrent semantics for (safe) TPNs. First, we recall the definitions in the untimed setting.

Definition 4 (causal net).

A causal net ON = (B, E, G) is a finitary (each node has finite number of predecessors) acyclic net with B as a set of conditions, E as set of events, flow relation When causal nets are used to give a partial order semantics to Petri nets, events represent occurrences of transitions firings, and conditions occurrences of places getting filled with tokens. The last condition in the definition states that a token in a place is produced by a single transition firing, and is consumed by a single transition. As conditions have a single successor, causal nets are conflict free. They are hence well suited to represent executions of nets. Let ≺= G + and = G * . We define e↓ as the downward closure

G ⊆ B × E ∪ E × B, such that E = {e | (e, b) ∈ G} ∪ {e | (b, e) ∈ G}
e↓ = {f ∈ E | f e}. A set E ⊆ E is downward closed iff E ↓ = E . We define ON • = {b ∈ B | b • = ∅} and • ON = {b ∈ B | • b = ∅};
Note that if we are looking at finite causal nets then ON • is always defined. For any downward-closed subset E of E we define Cut(E ) = {E • ∪ • ON } \ • E . As conditions are occurrences of places, Cut(E ) can be interpreted as the marking of N reached after executing E . Definition 5 (causal process). Given a PN U, a causal process of U is a pair U = (ON, π) where, π is mapping from B ∪ E → P ∪ T , satisfying following conditions:

1. π(B) ⊆ P and π(E) ⊆ T , 2. π e • is a bijection between sets e • and π(e) • (where π X denotes the restriction of map π to elements of X), 3. π• e is a bijection between sets • e and • π(e), 4.

For each p, M 0 (p) = |{b ∈ • ON | π(b) = p}|.
To relate transitions of a PN and events of a causal net, we will consider that events are of the form e = (X, t), where π(e) = t and X = • e i.e., event e corresponds to firing of transition t and X is a set of conditions consumed when firing t. We will also let conditions be of the form b = (e, p), where e is the event that creates condition b, and p = π(b) is the place that is represented by condition b. We let posb(ON ) denote the set of possible events which could be added to ON and is defined as

posb(ON ) = {e = (X, t) | X ⊆ B ∧ π(X) = • t ∧ ∀x ∈ X, x • = ∅}.
Following these definitions, one can inductively build processes to capture the semantics of (even unbounded) Petri nets. The construction is as follows : we start from initial causal process U 0 = (ON 0 , π 0 ), where ON 0 = (B 0 , E 0 ) is an occurrence net. B 0 is a multiset of conditions computed from M 0 that associates a condition of the form b = (⊥, p) to every marked place in M 0 , E 0 is an empty set of events, and π 0 maps every condition (⊥, p) to place p. A causal process U i+1 is built inductively from U i by choosing an event from posb(ON i ) and adding it to U i with the obvious extension of map π i . Obviously, causal processes capture the semantics of Petri nets, even in an unbounded setting. Causal processes can be seen as Petri nets, and hence the notions of enabled transition, markings, and languages apply. Given a causal process U for an Petri net U, we define as Lang(U ) the set of words of the form w = t 1 • • • t k such that there exists a sequence of transitions w = e 1 • • • e k in U starting from marking B 0 and w = π(w ). Using the above definitions and by a straightforward induction, we have the following proposition: Proposition 2. Let U be any untimed net. For any word w ∈ Lang(U, M 0 ), there exists a causal process U of U, such that w ∈ Lang(U ). Now we define the notions of timed causal net, and time causal process for Time Petri nets with multienabling semantics. Similar notions appear in [START_REF] Aura | A causal semantics for time Petri nets[END_REF] for Time Petri nets.

Definition 6 (timed causal net). A timed causal net is a tuple ON = (B, E, G, τ ) where (B, E, G) is a causal net, and τ : E → R ≥0 is a timing function such that eG + e ⇒ τ (e) ≤ τ (e ).
For a timed causal net ON = (B, E, G, τ ), we define Untime(ON ) as the net (B, E, G) i.e., ON without its timing function.

Definition 7 (Prefixes). Given two untimed causal nets

ON = (B, E, G) and ON = (B , E , G ), ON is said to be a prefix of ON , denoted by ON ≤ ON if B ⊆ B, E ⊆ E , G = G ∩ (B × E ∪ E × B )
, where E is a finite and downward closed subset of E.

Given two timed causal nets

ON = (B, E, G, τ ) and ON = (B , E , G , τ ), ON is a prefix of ON iff (B , E , G ) ≤ (B, E, G
) and E is timely sound, i.e., for all e in E we have τ (e ) ≤ τ (e ).

Definition 8 (time causal process).

A time causal process of a TPN N is a pair N = (ON, π) where ON = (B, E, G, τ ) is a timed causal net, and π is a mapping from B ∪ E → P ∪ T , satisfying conditions 1.-4. of a causal process, and: 5. for every event e = (X, t), min x∈X {τ (e) -τ ( • x)} ∈ I(π(e)), i.e. the time elapsed between enabling of the occurrence of t represented by e and its firing belongs to I(t). 6. if there exists X ⊆ B such that ∀x, x ∈ X, x x , and a transition t such that π(X) = • t then either

• (X, t) ∈ E, or • there exists e = (X , t ) ∈ E such that X ∩ X = ∅ and τ (e ) -max(τ ( • X )) ≤ lf t(t), or • max(τ (E)) -max(τ ( • X)) < lf t(t).
This last condition means that if a transition was urgent before the date of the last event in ON , then it belongs to the timed causal net, or was not appended due to firing of a conflicting transition.

For a time causal process (ON, π) we define Untime(ON, π) as (Untime(ON ), π). As for Petri Nets, for a timed causal net ON = (B, E, G, τ ), we denote by posb(ON ) (and we define similarly) the set of events that can be appended to ON (regardless of timing considerations). Abusing our notation, for a condition b = (e, p) we will define τ (b) as τ (b) = τ (e).

As for Petri nets, we can show that time causal processes faithfully describe the semantics of Time Petri nets. Given a time causal process N = (ON, π), where

ON = (B, E, G, τ ), a timed word of N is a timed word w = (e 1 , d 1 ) • • • (e |E| , d |E| ) such that e 1 , . . . , e |E| is a linearization of Untime(ON ), d i = τ (e i ).
Note that as w is a timed word, this means in addition that for every i < j, we have d i < d j . We denote by Lang(N ) the set of timed words of time causal process N . Note that there exist some words w ∈ Lang(Untime(N )) such that w is not the untiming of a word in Lang(N ). We have: Proposition 3. Let P be the set of time causal processes of a time Petri net N . Then,

Lang(N ) = N ∈P

Lang(N ).

Proof: We will proceed by induction on the length of words and processes. For a time causal process N , we denote by |N | the number of its events. Let us define the property P (i): for every word of length i,

we have {w ∈ Lang(N ) | |w| = i} = N ∈P,|N |=i
Lang(N ). Obviously, this property holds for i = 0, as the empty word of length 0 is a word of any process starting from initial conditions. Let us assume that P (i) holds up to n. For a given timed word, there exists a unique firing sequence C 0 , . . . , C n , where C n is the configuration reached immediately after execution of event e n . Let ON = (B, E, G, τ ) be a timed causal net of size n such that w ∈ Lang(ON ). At least one such net exists, as P (i) holds up to n. Now suppose that w can be extended to a word of size n + 1, i.e. that C n allows execution of an additional event e n+1 at date d n+1 , that is an occurrence of some transition t. There is a connection between clocks in configurations and dates in timed causal nets: every occurrence of a clock x i t attached to the i th occurrence of a transition t is created when a new complete occurrence of • t is created. For event e n+1 , the date of creation of such clock is a date d k ≤ d n+1 of occurrence of some event e k , that appended enough new tokens in • t to increase the degree of t. When e n+1 fires, it consumes tokens from a marking, that are maximal conditions in ON . So, there is a correspondence between clocks instances and conditions in timed causal nets: ON • is an union of conditions that contains occurrences of places p 1 , .., p j ∈ • t, and such that max{τ (p 1 ), . . . , τ (p j )} = d k . Note that d k is not necessarily the maximal date attached to a condition in ON , but is maximal in • e n+1 ∩ ON • . Now if e n+1 , representing an occurrence of t can occur at date d n+1 starting from C n = (ON • , enab) then there exists a clock x i t ∈ enab and a delay δ such that x i t is the oldest remaining clock created for an instance of t in C n and x i t + δ = d n+1 , and δ ∈ I(t). Recall that x i t was initialized at date d k . Hence, there exists a set of conditions X in ON • such that the places appearing in X are exactly • t, d n+1 -max(τ (X)) = δ ∈ I(t), and hence the process ON obtained by adding

{e n+1 = (X, t)} to E and {(e n+1 , p) | p ∈ t • } to B and setting τ (e n+1 ) = d n+1 is a process of N , as d n+1 -d k ∈ I(t), we have τ (e n+1 ) -τ (e k ) = min x∈X (τ (e n+1 ) -τ ( • x)) ∈ I(t).
One can prove similarly that if a new event e n+1 can be appended to ON , then this event is allowed from C n after elapsing τ (e n+1 ) -max(τ (E)) time units, and hence w.(e n+1 , τ (e n+1 )) is a word of N of size n + 1.

2

p 1 p 2 p 3 a [1,1] b [2,2] c [2,2] q 1 q 2 q 3 d [2,2] e [2,2] f [1,1]
. One can notice that ON 1 ≤ ON 2 . p 1 p 2 p 3 p 1 q 3 q 1 q 2 q 3 a b c d e f p 1 p 2 p 3 p 1 q 3 q 1 q 2 q 3 q 1 a b c d e f d
1 p 2 p 3 p 1 q 3 q 1 q 2 q 3 a b c d e f 1 3 5 2 4 5 p 1 p 2 p 3 p 1 p 2 q 3 q 1 q 2 q 3 q 1 a b c a d e f d

Free Choice Time Petri Nets

Problems addressed for Petri nets and their variants are often boundedness, termination, reachability or coverability questions. A marking M covers a marking M (denoted M ≥ M ) iff for every place in p ∈ P , M (p) ≥ M (p). Most problems are decidable for Petri nets, and are undecidable for Time Petri nets with urgent semantics [START_REF] Merlin | A study of the recoverability of computing systems[END_REF]. Indeed, this model is rather expressive. It can be used to specify distributed timed systems with unbounded resources, and urgency easily allows for the modeling of 2-counter machines (see for instance [START_REF] Reynier | Weak time Petri nets strike back![END_REF]). For completeness, we recall this encoding in Section 7.1, and show that it can be used to encode a counter machine even with multi-enabling semantics. As a consequence, undecidability results for Time Petri nets with urgent semantics extend to Time Petri nets with multi-enabling semantics. We formalize below the firability, termination, coverability, reachability, and boundedness problems for TPNs with multi-enabling semantics:

• Firability: Given a TPN N = (U, M 0 , I) and a transition t, is there a configuration (M, enab) ∈ Reach(N , C 0 ) such that t is fireable at (M, enab).

• Termination: Given a TPN N = (U, M 0 , I), does it have a non-terminating or infinite run?

• Coverability: Given a TPN N = (U, M 0 , I) and a marking M , is there a configuration (M , enab ) ∈ Reach(N , C 0 ) such that M ≥ M ?

• Reachability: Given a TPN N = (U, M 0 , I) and a marking M , decide if M ∈ R(N , C 0 ).

• Boundedness: Given a PN N = (U, M 0 , I) decide if R(N , C 0 ) is finite.

To obtain decidability, one often considers bounded TPNs, where the number of tokens in places cannot grow arbitrarily. In this case, TPNs can be translated into finite timed automata (see for instance [START_REF] Lime | Model checking of time Petri nets using the state class timed automaton[END_REF]). As a consequence, all properties decidable on timed automata are decidable for bounded TPNs. However, bounded TPNs cannot represent systems with unbounded resources. Furthermore, it is undecidable in general whether a TPN is bounded. One usually has to rely on a priori known bounds on place contents, or restrict to the class of nets such that Untime(N ) is bounded.

Considering multi-enabling semantics in unbounded nets does not change decidability issues in general: undecidability originates from the fact that one can encode a counter machine: counters are encoded with places, and zero test with urgent transitions (one can find such an encoding in [START_REF] Reynier | Weak time Petri nets strike back![END_REF]). However, we will show that multi-enabling semantics, beyond the practical fact that it allows encoding of queues with latency, also contain non-trivial decidable subclasses. Hence, in the rest of the paper, we will mainly focus on TPNs under multi-enabling semantics. We consider a structural restriction of TPNs, which is based on the untimed underlying PN, namely free-choice. This is a standard restriction in the untimed setting, that does not impose boundedness of nets, and allows for efficient algorithms (see [START_REF] Esparza | Free Choice Petri nets[END_REF]) in the untimed setting. In this section and next, we show the interesting properties it engenders in TPNs and subsequently we will show how it affects their robustness under guard enlargement and shrinking. Definition 9 (Free choice PN and Free choice TPN). A Petri net U = (P, T, F ) is called (extended) free choice, denoted FC-PN, if for any pair of transitions t and t in T :

• t ∩ • t = ∅ =⇒ • t = • t .
A TPN N = (U, M 0 , I) is called a free choice TPN (FC-TPN for short), if its underlying untimed net Untime(N ) = U is free choice.

Pruning a TPN while preserving reachability

As mentioned above, the firability and termination problems are undecidable for TPNs in general. In next section we show that they are decidable for FC-TPNs under multi-enabling semantics. As a first step, given a FC-TPN N , whose underlying net is free choice, we construct another FC-TPN P rune(N ) in which we remove transitions from a cluster if they can never be fired (due to the lower bound of their time constraint) and tighten timing constraints. Note that we do not delete all dead transitions from the net, but remove only transitions for which we can decide locally, by considering their clusters, that they will never fire. Let us illustrate this with an example. Similarly, in the cluster [e], we cannot say for sure that some transition will be never fired, but only that the maximum amount of time that an enabling instance of a transition in [e] can let elapse after its creation is 2 time units. Hence, we can safely set 2 as upper bound for intervals I(e) and I(f ) without changing the semantics of the net. Note that, in fact, neither transition f nor e is fireable in this net, but we cannot decide it just by looking at the clusters. Indeed in order to decide if e and f are fireable, we have to study the behaviour of the net. Hence our pruning operation does not modify this. Thus, after removing transition c from its cluster, modifying flow relation accordingly, and changing the upper bounds of remaining transitions, we obtain the free choice net in Figure 7. One can see that Reach(N , M 0 ) = Reach(Prune(N ), M 0 ). Therefore, we also get that Lang(N ) = Lang(Prune(N )). g h Definition 10 (pruned cluster and pruned net). Given an FC-TPN N = (U = (P, T, F ), M 0 , I)), and a transition t ∈ T , let β [t] = min t ∈[t] {lf t(t )}. We define the pruned cluster of a transition t as follows:

[0,3] [0,1] [2,3] [0.5,3] [0,2] [1,3] [2,8] [0,9]
Prune([t]) = {t ∈ [t] | ef t(t ) < β [t] } if [t] contains a transition with an interval of the form [α, β [t] ) or (α, β [t] ), {t ∈ [t] | ef t(t ) ≤ β [t]
} otherwise The pruning of a FC-TPN N is the net Prune(N ) = (U = (P, T , F ), M 0 , I ), where:

• T = t∈T P rune([t]) ∩ T , p 1 p 2 p 3 p 4 p 5 p 6 p 7 p 8 p 9 p 10 a b d e f g h [0,3] [0,1] [0.5,1] [0,2] [1,2] [2,8] [0,9]
• F = F ∩ (P × T ) ∪ (T × P )
• For each transition t in T :

I (t) =                                                [ef t(t), β [t] ] if β [t] = ∞ and ∀t i ∈ [t], β [t] ∈ I(t i ) and I(t) is of the form [ef t(t), lf t(t)) or [ef t(t), lf t(t)] (ef t(t), β [t] ] if β [t] = ∞ and ∀t i ∈ [t], β [t] ∈ I(t i ) and I(t) is of the form (ef t(t), lf t(t)) or (ef t(t), lf t(t)] [ef t(t), β [t] ) if β [t] = ∞, and ∃t i ∈ [t], I(t i ) is of the form (ef t(t i ), β [t] ) or [ef t(t i ), β [t] )
and

I(t) is of the form [ef t(t), lf t(t)) or [ef t(t), lf t(t)] or β [t] = ∞ and I(t) is of the form [ef t(t), ∞) (ef t(t), β [t] ) if β [t] = ∞, and ∃t i ∈ [t], I(t i ) is of the form (ef t(t i ), β [t] ) or [ef t(t i ), β [t]
) and I(t) is of the form (ef t(t), lf t(t)) or (ef t(t), lf t(t)] or

β [t] = ∞ and I(t) is of the form (ef t(t), ∞)
One can immediately remark from the way transitions are pruned that a pruned cluster P rune([t]) contains a transition with I (t) of the form [a, ∞) or (a, ∞) only if every transition t i in cluster [t] is attached a firing interval I(t i ) with an infinite upper bound. Notice also that in this case, I associates a firing interval that has an infinite upper bound to all transitions in P rune([t]).

Lemma 1 below shows that pruning away unfireable transitions from clusters of a FC-TPN, does not modify its semantics. More precisely, the LTS obtained for a pruned FC-TPN is isomorphic to the LTS for the original net. This is not surprising and has already been considered in [START_REF] Chatain | Back in time Petri nets[END_REF], where pruning is called "normalization" and is used to reason about free-choice but safe untimed nets.

Lemma 1 (Pruning Lemma). Let N be a FC-TPN, and

N = P rune(N ). Then, Reach(N , C 0 ), -→ N is isomorphic to Reach(N , C 0 ), -→ N .
Proof: We can build a map R from configurations of N to configurations of N , and show that it is an isomorphism. A configuration is a pair C = (M, enab) where M is a marking, and enab assigns a finite sequence of real values enab(t) (clock values) to every transition of the net. For every configuration C of N , enab(t) is a map that attaches to every transition t a set of real values r t 1 , r t 2 , . . . , r t deg(t) . One can notice that in configurations of free choice nets, all transitions from a cluster are newly enabled at the same date, and hence are attached the same valuations.

Let us now consider a transition t that was pruned out. This transition comes from a cluster [t ], that contains a set of transitions T (t ) = t 1,T (t ) , . . . , t k,T (t ) , t of size greater than 1. Without loss of generality, we will assume that t 1,T (t ) is not a pruned transition. Let R be the map that associates to every configuration C = (M , enab ) from N the configuration R(C ) = (M , enab), i.e. with identical marking M , and such that enab(t) = enab (t) if t is not a pruned transition, and enab(t) = enab (t 1,T (t ) ) otherwise. This map R is reversible, and R -1 (C) is simply obtained using a restriction of enab to unpruned transitions. Roughly speaking, R copies values of clocks attached to any unpruned transition and attaches them to pruned transitions in the cluster to obtain a configuration of N .

We can now prove that R is an isomorphism between Reach(N , C 0 ), -→ N and Reach(N , C 0 ), -→ N . First of all, let C 0 be the initial configuration of N and C 0 be the initial configuration of N . We obviously have R(C 0 ) = C 0 . Now, we have to prove that for every timed or discrete transition C 1 -→ N C 2 and every configuration

C 1 such that R(C 1 ) = C 1 , we have C 1 -→ N C 2 and C 2 = R(C 2 ). • C 1 δ -→ N C 2 . We have C 1 = (M 1 , enab 1 ) and C 2 = (M 1 , enab 2 )
, with enab 2 (t) = enab 1 (t) + δ for every transition t, and δ violates no urgency, i.e. for every transition t, the maximal value r in enab

1 (t) is such that r + δ ≤ lf t(t). Obviously, in C 1 = R(C 1 ), of the form C 1 = (M 1 , enab 1 )
, values of clocks are unchanged for unpruned transitions. As for pruned transitions the earliest firing time is greater than the minimal latest firing time of unpruned transition in the same cluster, then a timed move of δ from C 1 violates no urgency, and is also allowed in

C 1 . Elapsing time from C 1 results in a new configuration C 2 = (M 1 , enab 1 + δ). One can easily show that C 2 = R(C 2 ). • C 1 t -→ N C 2 . This transition t can fire from C 1 if enab 1 (t) 1 ∈ [ef t(t), lf t(t)],
and the marking M 1 associated with C 1 is greater than pre(t). This transition can also fire from C 1 as R does not change markings nor clocks of unpruned transitions (and t is necessarily an unpruned transition), and as the time interval I(t) attached to a transition in N contain the interval

I (t) attached to t in N . Hence if t is fireable from C 1 , it is also fireable from C 1 = R(C 1 ). We hence have a discrete move C 1 t -→ N C 2 , for some C 2 = (M 2 , enab 2 ).
The effect of firing t on markings is the same from C 1 and C 1 , i.e. markings M 2 and M 2 are identical in C 2 and C 2 . Let us now consider the clock part of configurations C 2 , C 2 . Firing t removes the first clock value from enab 1 (t i ) (resp. from enab 1 (t i )) for every transition t i such that pre(t i ) = pre(t), i.e., transition from the same cluster as t, and adds a clock with value 0 to every transition which degree is modified w.r.t. the intermediate marking. In We now prove the other direction: for every timed or discrete transition C 1 -→ N C 2 and letting C 1 be the configuration such that

C 1 = R(C 1 ), we have C 1 -→ N C 2 and C 2 = R(C 2 ). • Suppose C 1 δ -→ N C 2 and not C 1 δ -→ N C 2 or C 2 = R(C 2 )
. Note that for a chosen δ allowed in a configuration, the next configuration reached after elapsing δ time units is deterministically chosen. If δ time units can elapse from C 1 = R(C 1 ), then obviously C 2 = R(C 2 ). So the remaining possibility is that elapsing δ time units is not allowed from C 1 . However, this is impossible, as C 1 has more transitions than C 1 for each cluster, identical clocks attached to unpruned transitions but imposes the same constraint on possible values of δ: requiring enab 1 (t) i + δ ≤ min{lf t(t ) | t ∈ [t]} for every enabled transition t and every entry i in enab 1 (t) is the same constraint as enab

1 (t) i +δ ≤ min{lf t (t ) | t ∈ P rune([t])}. • Suppose C 1 t -→ N C 2 and not C 1 t -→ N C 2 or C 2 = R(C 2 ). Transition t is allowed in configuration C 1 = (M 1 , enab 1 ) iff M 1 ≥ pre(t), and enab 1 (t) 1 ∈ [ef t(t), lf t(t)]. As we have C 1 = (M 1 , enab 1 )
, the first condition is met, and as t can only be an unpruned transition, enab 1 (t) 1 = enab 1 (t) 1 , so firing t is also enabled in C 1 , there is a discrete move C 1 t -→ N C 2 for some configuration C 2 , and it remains to show that C 2 = R(C 2 ) to obtain a contradiction. As the marking part of configurations is the same in C 1 and C 1 , it is also the same in C 2 and C 2 , and it remains to compare the clock part. The clocks attached to transition t by enab 2 (t) (resp. enab 2 (t)) are updated iff the enabling degree of t is modified either from M 1 (resp. M 1 ) to the intermediate marking

M 1,temp = M 1 \ • t (resp. M 1,temp = M 1 \ • t)
or from the intermediate marking to the target marking M 2 (resp. M 2 ). For transitions with decreased degree in the intermediate marking, we have enab 1,temp (t) = enab 1 (t) \ enab 1 (t) 1 , and for other transitions enab 1,temp (t) = enab 1 (t) (and similarly for enab 1 and enab 1,temp ). For transitions which degree increases w.r.t. intermediate marking, we have enab 2 (t) = enab 1,temp (t) {0}, and for remaining ones, enab 2 (t) = enab 1,temp (t). This applies similarly for enab 2 (t) w.r.t. enab 1,tmp (t). In enab 2 (t), the value of clocks is identical for all transitions from the same cluster, and hence in particular for pruned transitions. Hence, after firing a transition t, enab 2 (t) is still a restriction of enab 2 (t) to unpruned transitions, and

C 2 = R(C 2 ) (contradiction).
Hence, R is a bijective relation from Reach(N ) to Reach(N ) that preserves moves, i.e. it is an isomorphism from Reach(N , C 0 ), -→ N to Reach(N , C 0 ), -→ N .

2 An immediate consequence of Lemma 1 is that Lang(N ) = Lang(Prune(N )). Note that this lemma holds only under the free-choice assumption. Indeed, in a standard TPN, one can disable the most urgent transition from a cluster without disabling other instances of transitions in this cluster. In the example of Figure 8, for instance, transition t 2 and t 3 belong to the same cluster, and pruning would remove t 3 . However, in the unpruned net, transition t 2 can be disabled by firing of t 1 , which allows t 3 to fire later. Hence, for this non-FC-TPN, Lang(N ) = Lang(Prune(N )). In this section, we prove our main theorem, which relates time causal processes of pruned FC-TPNs with untimed causal processes of their untimed nets. In the next section, we will use this theorem to show decidability of the firability and termination problems.

p 1 p 2 t 1 t 2 [0, 1] t 3 p 3 p 4 p 5 [0, 2] [3, 5]
Theorem 1 (Inclusion of untimed prefixes). Let N = (U, M 0 , I) be a pruned FC-TPN (without forced 0-delay time firing sequences) and let U = Untime(N ). Let U be an (untimed) causal process of U . Then there exists a time causal process N of N such that U ≤ Untime(N ).

Proof: We are given U a causal process of net U . We will iteratively construct a pair ρ i , σ i , where ρ i is a causal process of U , σ i a time causal process of net N , and such that ρ i is a prefix of Untime(σ i ).

The construction ends at some n ∈ N such that ρ n = U . At that stage of the algorithm, σ n is a time causal process such that U ≤ Untime(σ n ) which is the desired result. For this, we maintain the following invariants at every intermediate step, i.e., for all 0 ≤ i ≤ n:

(I1) ρ i is a prefix of U and (I2) ρ i is a prefix of Untime(σ i ) (I3) either |ρ i | + 1 = |ρ i+1 | or |σ i | + 1 = |σ i+1 | (I4) e ∈ posb(ρ i ) and e / ∈ σ i implies that e ∈ posb(σ i ) (I5) eG + i e ⇒ τ (e)≤ τ (e ), ( with
G + i the flow relation of σ i ).
The first two conditions have been explained above. Condition (I3) ensures that the algorithm progresses at every iteration, either in ρ i or σ i . Condition (I4) says that if an event e is enabled in the untimed causal process ρ i and has not yet been fired in σ i , then it must be enabled at σ i . Note that due to urgency, it might be the case that e is not yet fireable in σ i . Finally, Condition (I5) ensures that the time stamps that we add in σ i are consistent with its causal order.

We start by defining, for a time causal process ON , the maximal firing date mfd (ON, e) for an event e = (X, t) ∈ posb(ON ) as

mfd (ON, e) = max x∈X (τ (x) ) + lf t(t) if lf t(t) < ∞ max x∈X (τ (x) ) + ef t(t) + 1 otherwise.
This value mfd (ON, e) represents the date that can be attached to event e = (X, t) when it is appended to ON . When this event corresponds to a transition with urgency, mfd (ON, e) is the maximal date allowed by urgency, and if the event corresponds to a non-urgent transition with lf t(t) = ∞, mfd (ON, e) is an arbitrary consistent execution date (here we choose ef t(t) + 1, which is consistent and guarantees time progress). Further, we use td (ON, e) to denote the difference between mfd (ON, e) and the maximal date attached to an event in ON , i.e., td(ON, e) = mf d(ON, e) -max e∈ON (τ (e) ). Note that this value can be negative if the maximal date in ON is greater than mfd (ON, e), i.e., e has already been fired in ON . This represents the time that has to elapse before event e becomes urgent, or that has elapsed after e. Finally, for a (time) process ON and an event e, we denote by ON ∪ {e} the (time) process obtained by appending event e to ON , when it is possible to do so. Algorithm 1 gives a procedure that starts from an untimed causal process U and computes time-stamps and additional events needed to obtain a timed causal process N .

Let us give a short explanation of the algorithm. At initialization, B 0 is the set of conditions corresponding to marked places in M 0 , and CLK, a real valued variable which stores the time-elapsed till now, is set to 0. ρ i and σ i are respectively, untimed and time causal processes at i-th iteration. S i is the set of events that are the most urgent instances of transitions in σ i .

The idea is that, at each iteration, we pick (in line 4) an event e enabled in the current ρ i , which would grow ρ i to eventually reach the untimed causal process U . If this event has already been fired in σ i , then we just add it to ρ i and go to the next iteration. Else, we try to fire it in σ i . However, to do so, we first compute S i the set of all events that are the events that will fire. These are the transitions that must fire either because they are urgent, or because their mf d was set to a date that is the minimal among possible next events. If there is a transition instance e t ∈ S i whose corresponding event is also in U , then we pick it (in line 11) and fire it, i.e., add it to σ i and update time information correctly (line [START_REF] Cerone | Time-based expressivity of time Petri nets for system specification[END_REF][START_REF] Boyer | Multiple enabledness of transitions in Petri nets with time[END_REF][START_REF] Goltz | The non-sequential behavior of petri nets[END_REF][START_REF] Best | Nonsequential Processes -A Petri Net View[END_REF]. This guarantees that σ i has grown at this iteration so we go to the next iteration. On the other hand, if there is no urgent transition in S i which is also in U , we check if there is an urgent transition that must fire before e. If this is not the case, then e ∈ S i . In this case, we elapse time till e can fire and fire it as soon as possible (line 14), updating clocks appropriately. Finally, if there is some urgent transition in S i but this transition is not in U , then we fire it as late as possible (line [START_REF] Cerone | Time-based expressivity of time Petri nets for system specification[END_REF][START_REF] Boyer | Multiple enabledness of transitions in Petri nets with time[END_REF][START_REF] Goltz | The non-sequential behavior of petri nets[END_REF][START_REF] Best | Nonsequential Processes -A Petri Net View[END_REF]. The fact that this does not change the enabling of e (due to conflicts) is proved by our invariant I4. Thus, if the invariants I1, I2, I3, I4 and I5 are satisfied for all iterations, then it follows that the Algorithm 1 is correct when it terminates. It is left to show that the invariants are preserved and the algorithm always terminates.

Lemma 2. In Algorithm 1, all invariants are preserved at the end of each iteration of while loop.

Proof: The proof is by induction on the number of iterations. We note that each iteration must end either in 6, 17 or 22 (before incrementing i and going to the next iteration). For each invariant, we prove that it holds in the beginning, i.e., right after the initializations of σ 0 and ρ 0 . We then rely on the fact that they hold at step i to prove preservation of each invariant at step i + 1 of the algorithm. (I1) (ρ i is a prefix of U ) It is true at the beginning of loop i.e., base step of i = 0. Assume that it is true at the end of i th iteration of the while loop. Now we have to prove that this holds at the end of the (i + 1) th iteration. If we exit the iteration in step 17 or step 22, then it means that ρ i+1 = ρ i and by induction hypothesis, we have ρ i ≤ U hence ρ i+1 ≤ U . Otherwise we have exited the iteration in step 6 and it means that σ i+1 = σ i and ρ i+1 = ρ i ∪ {e}. So we have e ∈ posb(ρ i ) and e ∈ U \ ρ i . Hence ρ i+1 ≤ U .

Algorithm 1: Causal-net-to-time-causal-net Input:

-N = (U, M 0 , I) a pruned FC-TPN without 0-delay firing sequences,

-U = (B , E , G ) a (untimed) causal process of U = Untime(N )
Output: N a timed causal process of N such that U ≤ Untime(N ) // For all i, ρ i is a untimed causal process // σ i is a timed causal process 1 Initializations: 2 CLK := 0, ρ 0 := (B 0 , ∅, ∅), σ 0 := (B 0 , ∅, ∅, ∅);

3 while ρ i = U do 4
Choose an event e = (X e , t e ) from posb(ρ i ) ∩ U ;

5 if e ∈ σ i then 6 ρ i+1 ← ρ i ∪ {e}; σ i+1 ← σ i ;
σ i+1 ← σ i ∪ {e t }; ρ i+1 ← ρ i ; 23 i ← i + 1 ; (I2) (ρ i is a prefix of Untime(σ i ))
It is true at the beginning of loop i.e., base step of i = 0, since ρ 0 = σ 0 . Assume that is true at the end of i th iteration of the while loop. Now we have to prove that this holds at the end of the (i + 1) th iteration. If we exit the iteration in step 17 or step 22 then it means that ρ i+1 = ρ i and σ i+1 = σ i ∪ {e i } for e i = e or e i = e t . By induction hypothesis we have that ρ i ≤ U ntime(σ i ). Hence we have ρ i = ρ i+1 ≤ σ i ≤ σ i+1 . Otherwise we have exited the iteration in step 6 and it means that σ i+1 = σ i and ρ i+1 = ρ i ∪ {e}. So we had e ∈ σ i in the previous (i.e., i th ) iteration and therefore

ρ i ∪ {e} ≤ U ntime(σ i ) ≤ U ntime(σ i+1 ). (I3) (|ρ i | + 1 = |ρ i+1 | or |σ i | + 1 = |σ i+1 |)
At the beginning of loop i.e., at i = 0, we have ρ 0 = σ 0 , and |ρ 0 | = |σ 0 | = 0. At the first iteration, we necessarily begin the loop discovering any event in posb(ρ 0 ) ∈ σ 0 . Hence, an event is appended to σ 0 to obtain σ 1 and ρ 1 = ρ 0 . So invariant I3 holds for i = 0. Assume that I3 holds up to i th iteration of while loop. Now we have to prove that it holds at the end of (i + 1) th iteration. If we exit the iteration in step 17 or step 22 then it means that ρ i+1 = ρ i and σ i+1 = σ i ∪ {e i } for e i = e or e i = e t . To perform this step of growing σ i+1 we need to add the event e corresponding to an instance of some transition in N . This transition must be enabled at σ i , which is guaranteed by Claim A, given in I4 (proof given below). Hence we have that

|σ i | + 1 = |σ i+1 |.
Otherwise we have exited the iteration in step 6 and this means that σ i+1 = σ i and ρ i+1 = ρ i ∪ {e}. Therefore we have that

|ρ i | + 1 = |ρ i+1 |.
(I4) (e ∈ posb(ρ i ) and e / ∈ σ i , implies e ∈ posb(σ i )) Again, recall that for ease of writing, we slightly abuse notation here; when we say that an event of an untimed causal process belongs (or does not) to a time causal process, we implicitly mean that it belongs to the untiming of the time causal process and so on.

The invariant holds at the beginning of the loop i.e., at base step i = 0. Indeed, all enabled transitions in marking M 0 correspond to transitions enabled in the initial configuration of N , and as N is pruned, all of them can fire if a sufficiently large delay elapses. Assume that it is true at the end of i th iteration of while loop. Now we have to prove that this holds at the end of the (i + 1) th iteration. So we enter the i + 1 th iteration with i, ρ i , σ i and exit with values i + 1, ρ i+1 , σ i+1 . Let I4 i+1 denote the invariant I4 at the i + 1 th iteration and I4 i denote the invariant I4 at the i th iteration:

I4 i+1 : f ∈ posb(ρ i+1 ) and f / ∈ σ i+1 =⇒ f ∈ posb(σ i+1 ) I4 i : f ∈ posb(ρ i ) and f / ∈ σ i =⇒ f ∈ posb(σ i ).
Let f be some event of posb(ρ i+1 ) (we use f as a generic event to not confuse with e, the event picked in step 4). We have two cases:

-Case(exit by step 6). This means that σ i+1 = σ i and ρ i+1 = ρ i ∪ {e i } for some event e i . To execute this step, e i ∈ posb(ρ i ) is a pre-requisite, and e i ∈ posb(ρ i+1 ). Hence f = e i . Then either f was newly enabled after adding e i or f was already enabled before adding e i .

• Let us first consider the case where f was newly enabled after adding e i . Since f was enabled at ρ i+1 and not at ρ i , event f / ∈ posb(ρ i ). By I2 i+1 proved above, ρ i+1 is a prefix of U ntime(σ i+1 ). As time is not considered in the definition of posb(σ i ), one of the following must be true: Either f is enabled at σ i+1 or f ∈ σ i+1 . But, following the premise of I4 i+1 , we have that f / ∈ σ i+1 and hence f / ∈ σ i either. Hence it must be that f is enabled at σ i+1 i.e, f ∈ posb(σ i+1 ) as required.

• Now consider the case in which f was already enabled before adding e i to ρ i . Assume that it satisfies premise of I4 i+1 , i.e. f ∈ σ i+1 . Now we have to prove that f ∈ posb(σ i+1 ). Since it satisfies premises of I4 i+1 we have f / ∈ σ i+1 , implying f / ∈ σ i . Now, as I4 holds up to step i, i.e. I4 i holds, and as we know that f ∈ posb(ρ i ) we get that f ∈ posb(σ i ). Now when we exit at step 6, we have that σ i+1 = σ i and hence posb(σ i+1 ) = posb(σ i ). Therefore we get that f ∈ posb(σ i+1 ).

-Case(exit by step 22 or step 17): If we exit the iteration in either step, then it means that ρ i+1 = ρ i and σ i+1 = σ i ∪ {e i } for some event e i (in case of exit by step 17, e i = e of that iteration). In both cases, there are two cases to consider: f = e i or f = e i , i.e., whether f is the event which is used to grow σ i to get σ i+1 or not.

• First, we prove this invariant for f = e i satisfying premise of I4 i+1 . After adding e i to σ i , we cannot have event f newly enabled i.e., f ∈ posb(ρ i+1 ) and f / ∈ posb(ρ i ) because ρ i = ρ i+1 . So we consider the case when f was already enabled i.e., f ∈ posb(ρ i+1 ) and f ∈ posb(ρ i ) also. Since f satisfies premise of I4 i+1 we have that f / ∈ σ i+1 , implying f / ∈ σ i as σ i ≤ σ i+1 . So we have both clauses of I4 i satisfied for event f . Therefore we have that f ∈ posb(σ i ). Let t be the transition corresponding to event e i and let s be the transition corresponding to event f . Let M (σ i ) denote the marking reached after execution of σ i . Let t u and s u be the most urgent transition instances of t and s respectively at M (σ i ). Both these transition instances were fireable at marking M (σ i ). So when σ i+1 was obtained by adding event e i to σ i , correspondingly we have

M (σ i ) t - → M (σ i+1
). Now if s and t were independent-i.e., have no common place in their presetsin the net (and it does not matter if s u and t u were equally urgent) transition s u is still enabled at marking M (σ i+1 ) and fireable, implying that its event f ∈ posb(σ i+1 ) which was what we wanted to prove. Otherwise s and t are in conflict-i.e., have a common place in their preset-in the net, and both s u and t u were enabled at marking M (σ i ), which means that both the corresponding events e i and f were in conflict too. But ρ i ≤ U , and we had e i and f from U and in posb(ρ i ), so we have ρ i ∪ {f, e } ≤ U also, but U being a causal net, we could have only one of these events in it. So this case never arises.

• Now, on the other hand, if f = e i , event e i is added to σ i , then we have f = e i ∈ σ i+1 which falsifies a clause in the premise of I4 i+1 hence trivially satisfying it. But for this, we crucially need to show that we can indeed add e i to σ i , i.e., we can fire t the transition corresponding to event e i in the net N (it has not got disabled by firing of any other urgent transitions). We show this below to complete the proof.

In the untimed net, at a marking, multiple enabled instances of a transition are indistinguishable from each other. One such instance of transition t gave rise to event e i in the untimed causal net.

To get the matching event in the timed causal net, it is sufficient to fire some instance of t in the timed net. Since transition instances of same transition are not in conflict with each other, and by FEFF policy, all we need to prove is that the first enabled transition instance of t is fireable at M (σ i ). Let t u be this transition instance.

Claim A. Transition t u is fireable at marking M (σ i ) Proof: Assume the contrary, i.e., transition instance t u is not fireable at M (σ i ). Inductively, let us assume that this is the first time that such transition which was not fireable, while building timed causal net N , from the beginning where initial conditions were same and set of enabled events same for both causal nets N and N . Let e i denote the set of predecessors for e i in causal net N ; it contains all events and conditions needed for event e i to occur. As we are in (i + 1) th iteration, e i ∈ posb(ρ i ) and since we are exiting this iteration by step 22 or 17, it means e i / ∈ σ i . By induction we have invariant I2 true at i th iteration so ρ i ≤ σ i , implying e i / ∈ ρ i , so e i \{e i } ≤ ρ i , which gives us e i \{e i } ≤ σ i . Therefore all the places in the preset • t are marked at the configuration with marking component M (σ i ). Now the only possible reason for which transition instance t u is not fireable in the timed net at this configuration, is that there exists some instance t u of another transition t which shares a pre-place with t (and hence by FEFD policy, transition instance t u is in conflict with t u ), and more urgent than it, i.e., at M (σ i ), we have lf t(t )-v(t u ) < lf t(t)-v(t u ). Note that if • t∩ • t = ∅ and lf t(t )-v(t u ) < lf t(t)-v(t u ), then we could have fired t u first and then t u ; so we can assume that all such transitions are fired before. As the net is free choice we have • t = • t and therefore, transition t u is enabled at marking M (σ i ). Since N is a pruned net, the cluster [t] is pruned, and so lf t(t) = lf t(t ), which is a contradiction even in the case when lf t(t) = ∞. So it must be the case that e i ∈ posb(σ i ) in the timed causal net N . Note that this step of the proof essentially relies on the assumptions that N is free-choice and pruned, and also uses the particularities of the multi-enabling semantics. 2 (I5) (eG + i e =⇒ τ (e) ≤ τ (e )) In the base case of i = 0, the timed causal net σ 0 has no events and so the invariant is trivially satisfied. Assume that induction holds up to the i th iteration. That is when we enter with σ i and ρ i in the loop and come out with σ i+1 and ρ i+1 . So we have (I5) i+1 : eG + i+1 e =⇒ τ (e) ≤ τ (e )

Now for the inductive step, assume that we are in (i + 1) th iteration and eG + i+1 e . If events e and e both are in σ i then by (I5) i we have that τ (e) ≤ τ (e ). Let us now consider cases where e and e are not both in σ i . Adding an event e = (X, t) to an existing causal net means creating causal dependencies from predecessors of conditions in X to e. Since we add at most one event to σ at each iteration of the loop, and since we have eG + i+1 e it cannot be the case that e ∈ σ i+1 \ σ i and e ∈ σ i ∩ σ i+1 . Therefore, e ∈ σ i+1 \ σ i and e ∈ σ i ∩ σ i+1 . But eG + i+1 e also implies that e ∈ e which means event e was added at some iteration k where k ≤ i. When an event e = (X, t) is appended to a timed causal net σ k , it gets a time stamp τ (e) = CLK + lf t(t e ) -td (σ k , e) or t(e) = CLK + max{0, td (σ i , e)}. Now, it is easy to see that during the execution of the algorithm, the value of CLK only increases. Hence, we have τ (e ) ≥ τ (e). This completes the proof of this lemma.

2 The last thing left to prove is that Algorithm 1 terminates for any input. We show that σ cannot grow unboundedly. Each step of the algorithm adds either an event to ρ i , or to σ i . While the number of steps that add events to ρ i is finite, the algorithm may still not terminate if σ can grow unboundedly, i.e. the while loop is exited at step 22 or 17 an unbounded number of times without progress in ρ. Now, the crux of the proof is that at every step, a set of events from U are listed as possible events. At every step, since we do not have forced 0-delay firing sequences, all events have a bounded maximal firing date, and since we choose event dates that enforce time progress for transitions with lf t(t) > 0, these events can not remain ignored forever. A complete proof follows.

Lemma 3. Algorithm 1 terminates in finitely many steps.

Proof: We prove that eventually ρ i = U for some i. For that it is sufficient to prove that we do not exit by first choosing an event in S i at step 19 followed by step 22 or by step 17 infinitely often in the while loop, growing σ i but not ρ i . Indeed, if this loop is exited in steps 22 and 17 a finite number of times, then the algorithm ends with ρ i = U in a finite number of steps.

Let CLK = θ, σ i , ρ i be the processes built at iteration i, and let e be the event chosen in step 4 at the beginning of while loop at the i + 1 th iteration and let t be the transition corresponding to this event. Suppose that we exit by step 22 infinitely often, and in particular after iteration i, without adding event e to ρ. One can also notice that mf d(e) < ∞. To prevent e from being selected during an unbounded number of steps, one cannot exit at step 17 at the i + 1 th , i + 2 th , .... iteration as otherwise, event e will eventually be chosen from posb(ρ i+k ) for some k ≤ |U |, and as at that stage e ∈ σ i+k , e will be appended to ρ i+k .

If we exit infinitely often using steps 19 and (or) 22, then at each iteration, we have S i , S i+1 , S i+2 = ∅, and for every event e t,i+k chosen from S i+k at step i + k, we have mf d(e t,i+k ) ≤ mf d(e). So it implies that we have an infinite execution of the algorithm q i t1 -→ q i+1 t2 -→ . . . starting from configuration q i where CLK = θ, σ i , ρ i , and appending an occurrence e tj ,i+k of some transition t j to σ i+k-1 at each step i+k of the algorithm. Since net N is finite, the set of transitions occurring in this execution is finite. So there exists at least one transition which occurs infinitely often in this run. Let s be this transition. Now if lf t(s) > 0 then there exists a minimal constant K such that for the K th occurrence s K of s, mf d(s K ) > θ + K • lf t(s) > mf d(t). Therefore, before the K th occurrence of transition s in this infinite execution, the maximal firing date of event e would have become minimal. Consequently, the algorithm would have exited by step 17, appending e to σ, and subsequently allowing appending e to ρ a finite number of steps later. This contradicts the fact that there is no transition in the infinite execution which adds event e to ρ i . So it must be the case that lf t(s) = 0 for every transition occurring infinitely often during the execution of the algorithm. Now there exists m ≥ 1 such that each transition occurring after q m occurs infinitely often. It means that we have a 0-delay timed firing sequence starting q m , which is a contradiction.

2

Thus, we can assemble the correctness proof in Lemma 2 and the termination proof of Lemma 3 to conclude the proof of Theorem 1.

2

Let us comment on the prefix relation in Theorem 1. In general, a process of untime(N ) need not be the untiming of a time causal process of N . This is due to urgency, which forces firing some transitions that become urgent before a particular event can be appended. Consider for instance the example of Figure 3. The process U containing a sequence of transitions with labels d, e, f, e is a possible process of this FC-TPN. However, in a timed setting, a process containing a timed version of U needs to contain also the sequence of transitions a, b, c, a, due to urgency. This Process ON 4 is shown in Figure 5. One can verify that U ≤ U ntime(ON 4), but there exist no time causal process ON of N such that U = U ntime(ON ).

We can now extend Theorem 1 from causal nets to words. Let U = (P, T, F ) be an untimed Petri net. Given a causal process U = (ON = (B, E, G), π) of U, consider the partial order = G * . We denote by lin(U ), the set of words over alphabet of transitions obtained by considering linearizations of the partial order of G * and projecting onto the labeling alphabet (of transitions T ), i.e., lin(N ) = {ρ ∈ T * | there exists ρ a linearization of G * such that π| E (ρ ) = ρ}. Recall that given an untimed net U, its language Lang(U, M 0 ) is a set of firing sequences, i.e., words over the alphabet of transitions. We obtain our characterization for words rather than causal processes.

Corollary 1 (Words version).

Let N be a pruned FC-TPN (without 0-delay time firing sequences) and let U = Untime(N ). Then, for each w ∈ Lang(U , M 0 ) there exists a time causal process N of N and w ∈ Lang(Untime(N )) such that w w . Proof: Given a word w ∈ Lang(U , M 0 ), using Proposition 2, we get an untimed causal process U of net U , such that w ∈ lin(U ). By Theorem 1, we get a timed causal process N of net N such that U ≤ Untime(N ). Now since w ∈ lin(U ), and U ≤ Untime(N ), we can extend w to w ∈ lin(Untime(N )).

Decidability results for FC-TPNs

A first natural question in Petri nets is whether some transition is fireable or not. When a Petri net models the control flow of a program, this amounts to asking whether some instruction can be executed. In this section, we will show two significant consequences of the connections between time causal processes of N and processes of U ntime(N ) shown in Theorem 1. Namely, we show that both firability and termination can be decided for FC-TPNs with no 0-delay time firing sequences. We say that a transition t is fireable in a (FC-)TPN N iff there exists a run C 0 -→ • • • t -→ C k of N that contains t. We denote by F ireable(N ) the set of transitions that are fireable.

Theorem 2 (Firability). Given an FC-TPN N = (U, M 0 , I) without 0-delay time firing sequences, and a transition t ∈ T , checking firability of transition t in N is decidable.

Proof: Given a FC-TPN N , one can compute an equivalent pruned version N P runed , i.e. a Petri net with the same timed language and the same set of processes, but which clusters have only fireable transitions. One can compute a Petri net U = Untime(N P runed ). For every PN, it is well known that coverability of a marking is decidable [START_REF] Rackoff | The covering and boundedness problem for vector addition systems[END_REF]. A particular transition t is fireable in a Petri net U iff its preset • t is coverable. Coverability can be obtained by construction of a coverability tree, or using backward algorithms (see for instance [START_REF] Finkel | Recent and simple algorithms for Petri nets[END_REF] for recent algorithms). In both cases, one can exhibit a sequence of transitions witnessing coverability of a particular marking. If w = t 0 • • • t k is such a sequence witnessing coverability of • t from M 0 in Untime(N P runed ), then one can immediately infer that w • t ∈ Lang(U ), and hence t is fireable in U . Using Corollary 1, there exists a timed word v = (t 0 , d 0 ) • • • (t k , d k ) • (t, d k + 1) ∈ Lang(N P runed ), and hence v ∈ Lang(N ) and t is fireable in N . Conversely, assume that t is not fireable in Untime(N ) and that t it is fireable in N . Then there exists a run ρ of N firing t. Then, Untime(ρ) is a run of Untime(N ) which fires t, which is a contradiction.

2 Next we turn to the problem of termination (i.e., does there exist a non-terminating run) and show that for FC-TPNs without 0-delay time firing sequences, this too is decidable.

Theorem 3 (Termination). Given an FC-TPN N (without 0-delay time firing sequences), it is decidable to check if N terminates.

Proof: Let N be a FC-TPN and let N p be its pruned version. Since the reachability graphs of N and N p are isomorphic by (Pruning) Lemma 1, it is sufficient to decide if N p has only terminating runs. Let N = Untime(N p ). As classically done, one can decide whether the untimed net N has a non-terminating run by building the coverability tree. In particular, N has a non-terminating run iff in its coverability tree CT (N ) we can find markings M, M such that M (p) ≥ M (p) for every place p ∈ P and M is reachable from M . Indeed, in this case, there is a sequence of transitions

t 1 • t 2 • • • t i • • • t i+k where t 1 • • • t i-1 isa sequence from M 0 to M and t i • • • t i+k a sequence from M to M . Then, t 1 • t 2 • • • (t i • • • t i+k ) k is a sequence of N for every k ∈ N, and N has an infinite sequence t 1 • t 2 • • • (t i • • • t i+k ) ω .
As we know from Corollary 1 that for every word w of Lang(N ), there exists a timed word w of Lang(N p ) of length |w| ≥ |w |, then N p (and hence N ) allows sequences of transitions of unbounded lengths, i.e., it does not terminate either. In the other direction, if N p has an infinite run, as time constraints in free choice TPNs can only prevent occurrence of a transition, then the untimed net clearly has an infinite run too. Thus, we have reduced the problem to termination of an untimed Petri net, which is decidable (by Dickson's Lemma as usual, see [START_REF] Desel | Lectures on Petri Nets I: Basic Models[END_REF] for details).

2 Thus, using the proof technique we developed in the last section, we were able to easily tackle termination and firability for FC-TPNs as shown above. However, this technique of using the relation between untimed processes and processes of untimed nets does not allow us to tackle all properties immediately. Further discussion about properties that cannot be tackled directly by pruning a FC-TPN and then studying its untiming is deferred to Section 7.

Robustness for FC-TPNs

As mentioned in the introduction, robustness problems address the question of preservation of properties of systems that are subject to imprecision of time measurement. In this section, for any property or decision problem of TPNs, e.g., firability, termination, we define formally what we mean by robustness for this property under imprecision. Then, we focus on two particular properties, namely, firability and termination and show decidability results in this setting. To the best of our knowledge, this is the first decidability result of robustness for an unbounded class of TPNs allowing urgency.

Let us now formally define the notion of robustness considered in this paper. Inspired by the definitions for robustness in timed automata [START_REF] Puri | Dynamical properties of timed automata[END_REF], we define two notions of robustness with respect to guard enlargement and shrinking:

• Given an interval I(t) = [a, b] for a transition t, and ∆ ∈ Q >0 , the enlargement of I(t) by ∆ is the interval

I ∆ (t) = [max(0, a -∆), b + ∆]. For a TPN N = (U, M 0 , I), the enlargement of N by ∆ ∈ Q >0 , is the net N ∆ = (U, M 0 , I ∆ )
, obtained from (U, M 0 , I) by replacing every interval I(t) by its enlarged version I(t) ∆ .

• Given an interval I(t) for transition t, and ∈ Q >0 , the shrinking of I(t) by , denoted I (t), is the interval obtained by replacing its lower bound ef t(t) by the bound ef t(t) + , and its upper bound lf t(t) by the bound max{0, lf t(t) -}. Given a TPN N = (U, M 0 , I), the shrinking of N by ∈ Q >0 is the net N , obtained by replacing interval I(t) of each transition t, by the interval I (t).

With a slight abuse of notation, in this article ∆ will always mean enlargement (by value ∆) and will be used for shrinking (again by the value ). The first robustness question, is for a chosen enlargement ∆ ∈ Q >0 (resp. shrinking ∈ Q >0 ), to decide whether, properties of a net (reachability, boundedness, coverability) or its (untimed) language are preserved in N ∆ (resp. N ). A more general robustness question consists of deciding whether there exists a value of ∆ ∈ Q >0 (resp.

∈ Q >0 ) such that N ∆ (resp. N ) preserves reachability, coverability, or the (untimed) language of N . A positive answer to this question means that slightly changing guards preserves the considered property, i.e. this property of the system is robust with respect to a small time imprecision. In general, robustness problems (including checking firability of a transition and termination of the net) are undecidable for TPNs, as shown in [START_REF] Akshay | Robustness of time Petri nets under guard enlargement[END_REF], and become decidable when the considered nets are bounded. An interesting question is, whether robustness of some of the above mentioned problems is decidable for TPNs with multiple enabling outside bounded classes of nets. Answering this question would provide useful tools to check properties of systems made of bounded timed processes communicating through bag channels [START_REF] Clemente | Reachability of communicating timed processes[END_REF].

In this section we focus on both variants of robustness (w.r.t. guard enlargement and shrinking), for two particular properties/problems, namely, robustness of firability and robustness of termination and show decidability results.

Robustness of firability for FC-TPNs

When timing in a system is imprecise, a natural question is whether this imprecision impacts the behavior of the system. In particular, one may wonder whether the set of reachable instructions is changed. This can be captured as a firability robustness problem. This robustness problem can be defined both for guard enlargement and guard shrinking.

Definition 11 (Firability robustness problems). Given an FC-TPN N :

• (robustness w.r.t. guard enlargement) does there exist an enlargement parameter ∆ ∈ Q >0 such that Fireable(N ) = Fireable(N ∆ )?

• (robustness w.r.t. guard shrinking) does there exist a shrinking parameter

∈ Q >0 such that Fireable(N ) = Fireable(N )?
A net is said to be robustly fireable w.r.t guard enlargement (resp. guard shrinking), if there exists such a ∆ (resp. ).

Robustness of firability with respect to guard enlargement

We start by observing that even in FC-TPNs, firability is not a robust property w.r.t. enlargement i.e., it is not the case that there is always a (non-zero) guard enlargement that preserves firability. Consider, for instance, the FC-TPN N = (U, M 0 = {p 1 }, I) given in Figure 9. Under any perturbation ∆ > 0, transition b becomes fireable, and hence Fireable(N ) = Fireable(N ∆ ). The reachable markings of N are

U ntime(Reach(N , M 0 )) = {{p 1 }, {p 2 }}. Under guard enlargement ∆ > 0, FC-TPN N ∆ has set of reachable markings U ntime(Reach(N ∆ , M 0 )) = {{p 1 }, {p 2 }, {p 3 }}. p 1 p 2 p 3 a b [0,1) [1,2]
Figure 9: A FC-TPN for which firability is not robust w.r.t. guard enlargement However, as checking firability of every transition in a FC-TPN is decidable, given a fixed enlargement ∆, one can decide whether the firability set of N differs from that of N ∆ . So the next question is to decide for a given FC-TPN N , whether there exists a ∆ > 0 such that enlarging the guards of N by ∆ preserves firability.

Theorem 4. Let N be a FC-TPN without 0-delay sequences. Then checking whether N is robustly fireable w.r.t. guard enlargement is decidable. If N is robustly fireable, one can also effectively compute a value ∆ such that Fireable(N ) = Fireable(N ∆ ).

Proof: We first observe that in a pruned FC-TPN N , a transition t is fireable iff all transitions in t's cluster are fireable. Next, all timed words of N are also timed words of N ∆ . So, enlarging a net can only result in new behaviors. As a consequence, if a transition t is fireable in N , it is necessarily fireable in N ∆ . Further, note that as they have the same underlying untimed net, N and N ∆ are both free-choice and they have the same clusters. Now the pruning operation applied to each of these nets results in removing transitions (it can never add transitions) and pruning Lemma 1 holds for both of them. If after the pruning, we still have the same clusters, then the set of fireable transitions remains the same. The only way to have an extra transition that can fire in P rune(N ∆ ) is if this transition t in cluster C has been removed in P rune(N ) but remains in P rune(N ∆ ) due to enlargement. By our pruning construction this means that there must exist another fireable transition in this cluster in P rune(N ) (else we would not remove t). That is, Claim: For any ∆ > 0, Fireable(N ) = Fireable(N ∆ ) iff there exists a cluster C ∆ of P rune(N ∆ ) such that C ⊂ C ∆ for some cluster C of P rune(N ), and at least one transition t of C is fireable. Proof: [of claim] Let us suppose that there exists a cluster C of P rune(N ) that contains transitions t 1 , . . . , t k , such that t 1 is fireable, and let C be the cluster of P rune(N ∆ ) that contains t 1 , . . . , t k , and additional transitions t k+1 , . . . , t k+q . As t 1 is fireable, then there exists a timed word w • (t 1 , d 1 ) ∈ Lang(N ). The word w • (t 1 , d 1 ) is also a timed word of Lang(N ∆ ), so t 1 is fireable in N ∆ . As we know that all transitions from a pruned cluster are fireable if one of them is fireable, then all transitions t k+1 , . . . , t k+q are fireable in P rune(N ∆ ) (and hence in N ∆ ). Let us suppose that for every cluster

C ∆ of N ∆ , either i) the cluster C of N containing a subset of transitions of C ∆ is equal to C ∆ , or ii) no transition of C is fireable.
If C ∆ = C for a cluster, then new fireable transitions of N ∆ do not come from this cluster. If no transition from C is fireable in N but transitions of C and C ∆ are fireable in N ∆ , then, there exists a process in Untime(N ∆ ) that contains transitions from C. This process contains a (possibly empty) prefix N that is a process of Untime(N ). The configuration reached after N allows at least one fireable transition of N ∆ that is not fireable in N . Hence, this both contradicts the fact that all clusters that have fireable transitions remain unchanged or are never fired.

2 Thus, it suffices to look at each cluster of P rune(N ) and compute the smallest possible enlargement that does not give new behaviors. More formally, two intervals I 1 , I 2 are neighbors if the smallest closed intervals containing them have a non-empty intersection. Given two intervals I 1 with end-points a ≤ b and I 2 with end-points c ≤ d that are not neighbors and such that b < c, then one can easily compute a value ∆ I1,I2 < (c-b)/2. One can for instance choose ∆ I1,I2 = (c-b) 4 . For a cluster C of N with transitions t 1 , . . . , t k such that t 1 , . . . , t i are not pruned, and t i+1 , . . . , t k are pruned, we have ef t(t j ) > min{lf t(t q ), q ∈ 1..i} for every j ∈ i + 1..k. Similarly we can compute ∆ C = min{ef t(t j ) -min{lf t(t q ), q ∈ 1..i}}. Then, enlarging N by ∆ C 4 does not change the set of transitions preserved by pruning. Now, if any transition of t i+1 , . . . , t k is a neighbor of a transition having interval [0, min{lf t(t q ), q ∈ 1..i}], then such a ∆ C does not exist.

Consequently to check robustness of firability, it suffices to check existence of a value ∆ C for each cluster C of N that has a fireable transition. If one such cluster does not allow computing a strictly positive enlargement, then the net is not robustly fireable. Otherwise, it suffices to choose as ∆ the smallest value allowing enlargement encountered for a cluster of N , i.e. ∆ = min{∆ C |C ∩ Fireable(N ) = ∅}. Clearly, enlarging N by ∆ does not change the firability set of N .

We can now characterize two classes of unbounded FC-TPNs for which robustness of firability set is guaranteed by definition, i.e., nets from these classes are always robustly fireable under guard enlargement.

Corollary 2. Let N be a FC-TPN such that Untime(Prune(N )) = Untime(N ). Then N is robustly fireable w.r.t guard enlargement. Corollary 3. Let N = (U, M 0 , I) be a FC-TPN which uses only closed guards (in range of I). Then, N is robustly fireable under guard enlargement.

Proof: First of all, recall that enlargement can only add new transitions and hence new behaviors to a net. Now, consider how enlargement affects pruning. Let t 1 , . . . , t k be transitions from the same cluster C, and let

I 1 = [α 1 , β 1 ], . . . , I k = [α k , β k ]
be the closed intervals attached to these transitions. Let maxup C = min{β i , i ∈ 1..k}. Pruning of this cluster enlarged by some value ∆ keeps transition t j such that α j -∆ ≤ maxup C + ∆. Now we can prove that for nets with closed intervals, there exists a value ∆ such that U ntime(P rune(N )) = U ntime(P rune(N ∆ )). For a pruned cluster C, let us denote by minlow C the minimal lower bound of intervals associated with a transition that is in C but not in P rune(C). We have minlow C > maxup C , and we can hence choose a value

d C < 1/4(maxup C -minlow C ) such that α j -d C ≤ maxup C + d C , i.e such that P rune(C) is the same in N and N d C .
If one chooses an enlargement by a value ∆ strictly smaller than md = min{d C | C is a pruned cluster of N }, then the pruned clusters of N and N ∆ are the same, and hence for any such value 0 < ∆ < md, we have U ntime(prune(N )) = U ntime(prune(N ∆ )). Such a value exists iff md > 0, which is guaranteed when intervals are closed, ensuring maxup C -minlow C > 0 for every cluster C. 2

Robustness of firability w.r.t guard shrinking

Consider the net N in Figure 10 which has two fireable transitions a, b. In the net N obtained by shrinking guards, for any value of , only transition a remains fireable. One can also remark that the net in Figure 10 has closed intervals. This means that unlike for guard enlargement (Corollary 3), firability is not robust w.r.t. guard shrinking in the class of FC-TPNS with closed guards. As in Theorem 4, given a value , we can check whether Fireable(N ) = Fireable(N ) by considering reachable clusters and their transitions. Observe that in a cluster of a free choice net, guard shrinking can disable a transition. So given a cluster, such that at least one transition is useful (can be fired eventually) in it (which can be decided using Theorem 2), the set of clusters in N is the set of clusters of N but pruned with intervals I (t). Just as we did for guard enlargement in Theorem 4, for a given cluster C, one can compute the maximal value by wich transitions of C can be shrinked without changing the contents of P rune(C). For a pair of intervals

I 1 = [α 1 , β 1 ], I 2 = [α 2 , β 2 ] such that β 1 > α 2 ,
one can shrink intervals by a value s 1,2 < β 1 -α 2 in such a way that the intersection of both shrinked intervals is not empty. For a cluster C which transitions preserved by pruning are t 1 , . . . , t k , one can shrink intervals I(t 1 ), . . . , I(t k ) by value C = min{s i,j | i, j ∈ 1..k} without changing the set of pruned transitions in C. Then, following the lines of proof of Theorem 4, by considering the minimal shrinking value among all clusters, one can decide whether there exists a shrinking value that does not change the fireable sets of transitions in all clusters for which some transition is fireable in N . Hence we have the following result: Theorem 5. Let N be a FC-TPN without 0-delay sequences. Then checking whether N is robustly fireable under shrinking of guards is decidable. If N is robustly fireable, then one can effectively compute a value such that Fireable(N ) = Fireable(N ).

Robustness of Termination for FC-TPNs

Next, we move to the problem of termination in FC-TPNs. We are interested in formulating when a system modeled as an FC-TPN is robustly terminating, i.e., it terminates even under (infinitesimally) small perturbations. We start with two definitions to capture guard enlargement and shrinking as before.

Definition 12 (Robustness of termination). Let N be a TPN. The termination robustness problem can be formalized as follows.

• (robustness w.r.t. guard enlargement) Does there exist an infinitesimal ∆ > 0 such that all runs of N are terminating iff all runs of N ∆ are terminating ?

• (robustness w.r.t. guard shrinking) Does there exist an infinitesimal > 0 such that all runs of N are terminating iff all runs of N are terminating ?

A net N is said to be robust w.r.t. to termination under guard enlargement (resp. shrinking) if there is a ∆ (resp. > 0), such that N ∆ (resp. N ) satisfies the above property (i.e., it has a non-terminating run iff N has). Termination is robust for class of TPNs under enlargement/shrinking if it is robust for all nets in the class.

Robustness of Termination w.r.t. guard enlargement

As for firability, using open guards gives us a simple example of an FC-TPN that is terminating (i.e., has no non-terminating run), but which enlargement is not terminating. For completeness, we show an explicit example of such a net N in Figure 11. This net is a free choice net, and defines the timed language L N = {(a, d) | 0 ≤ d < 1}. All runs of N are terminating. However, for any value of ∆, the language of

N ∆ becomes L N∆ = L N ∪ {(b, d) • (c, d 1 ) • • • (c, d k ) | 1 ≤ d ≤ 2 ∧ ∀i ∈ 1..k, d i+1 -d i ∈ [0, 1]}.
Clearly, the enlarged net N ∆ has at least one non-terminating run. As intervals of N are closed, every transition t j for j ∈ k +1, . . . , k removed from cluster C to obtain C is attached an interval I j with a lower bound α j > β C . Hence, one can define the positive value m C = min j∈k +1..k {α j -β C }. The transitions appearing is a cluster obtained by pruning C with intervals enlarged by a value smaller than m C /2 are still t 1 , . . . , t k . Then there exists a value m N = min{m C /2 | C cluster of N } such that enlargement of N by a value smaller than m N does not change clusters in the pruned net. We can now consider termination. First, notice that if net N has a non-terminating run ρ, then-as enlargement can only add behaviors-for any value ∆ ∈ R, ρ is also a non-terminating run of enlarged net N ∆ . Then, for any value 0 < ∆ < m N , clusters in N and N ∆ contain the same transitions, so U ntime(P rune(N )) = U ntime(P rune(N ∆ )). If all runs of N ∆ are terminating, then all runs of U ntime(P rune(N ∆ )) terminate. As a consequence, all runs of U ntime(prune(N )) also terminate. Last, terminating runs in an untimed net are blocked in a marking from which no transition can fire. Adding timing constraints does not allow more firings, so all runs of N are terminating runs.

2 Now for general FC-TPNs, which may also have some open/semi-open guards, as non-terminating runs could arise due to enlargement, we would like to check whether a given FC-TPN is robust w.r.t. termination or not. The following theorem shows shows that this problem is indeed decidable. Theorem 6. Robustness of termination w.r.t. guard enlargement is decidable for FC-TPNs without 0-delay sequences.

Proof: For this proof, we need to extend the notion of pruning seen in Section 4.1. Let t 1 , . . . , t k be the set of transitions appearing in a cluster C, and let I 1 , . . . , I k be the intervals associated with these transitions, with respective lower bound α t and upper bound β t . Let maxup C = min{β i , i ∈ {1, .., k}} be the minimal upper bound of intervals attached to transitions in C. Recall that any transition which lower bound α j is greater than maxup C will never fire in N . The extended pruned cluster obtained from C is the set of transitions t i such that α i ≤ maxup C .

The intervals associated with transitions in the extended pruned cluster are the closed intervals I (t i ) = [α i , min(β i , maxup C )]. The major difference between pruning and extended pruning is that extended pruning does not remove transitions that are neighbors of transitions that can fire in N . Intuitively, these additional transitions are the transitions that would become fireable under any enlargement.

Let N = (U, M 0 , I) be a TPN, and let N = (U , M 0 , I ) be the net obtained by restricting U to its extended pruned clusters as shown above. Then we have the following claim: N is robust w.r.t. to termination under guard enlargement iff either

• N has non-terminating runs, or

• N and N only have runs that terminate.

One can immediately notice that these two conditions can be effectively checked (due to Theorem 3). Now we proceed to prove the first implication (⇒) given above, i.e., assuming that N is robust w.r.t. termination we prove that one of the two conditions must hold.

Let us consider the first condition, i.e., if N has a non-terminating run, then so has N . If N has a non-terminating run ρ then, as enlargement can only add new behaviors to the original language of a net, ρ is also a non-terminating run of N . Now, assuming the first condition is false, i.e., all runs of N are terminating, we have to prove that second condition holds, i.e., all runs of N are terminating. We show this by contradiction. If N has only terminating runs and N has a non-terminating run ρ then take any ∆ > 0 and consider N ∆ . We can observe easily that ρ is a run in N ∆ as well (since all transitions in clusters of N are neighbors of transitions of N ). Hence, for any value of ∆ > 0 the termination property differs for N and N ∆ , which violates the assumption that N was robust w.r.t. termination under guard enlargement. This completes the proof of the forward direction.

Let us now prove the reverse direction (⇐): Assuming the first condition, that N has a nonterminating run, it is easy to see that for any ∆ > 0, this non-terminating run is also a run of N ∆ . Now, assume that N and N only have runs that terminate. Then we have to show that one can find a value ∆ for enlargement such that N δ has only terminating runs for any value δ ≤ ∆. We can exhibit a value ∆ such that U ntime(N ) = U ntime(N ∆ ), i.e. such that the enlargement by ∆ does not create new untimed behaviors, and consequently no new non-terminating runs. Let us consider again the original clusters C 1 , . . . , C k of N , and their extended pruning C 1 , . . . , C k . One can notice that the clusters of N contain transitions that become fireable for the smallest enlargement by some infinitesimal > 0. For a given pair of transitions t i , t j such that t i ∈ C m and t j ∈ C m , we have that I(t i ) has a lower bound α i smaller that or equal to the minimal upper bound maxup Cm in the cluster C m , and I(t j ) has a lower bound α j greater than maxup Cm , and it is not either a neighbor of any interval I (t q ) associated with a transition in t q ∈ C m . Hence for every such pair of transitions, there exists a value d j = α j -maxup Cm > 0. In any enlargement by a value δ j smaller than d j , t j will not appear in a cluster of P rune(N δj ). Now, let δ denote the minimal value separating all transitions that are kept or removed from clusters by extended pruning. One can also notice that the example of Figure 12 has closed guards. Thus, unlike for guard enlargement (Proposition 4), the class of FC-TPNs with closed guards is not robust w.r.t. termination under shrinking of guards. However, with a slight modification, we still obtain a decidable procedure to check for robustness.

Theorem 7. Let N be a FC-TPN without 0-delay sequences. Then, checking robustness of termination of N under guard shrinking is decidable.

Proof: We reuse the same principle as in Theorem 6, but consider clusters that will be obtained under the smallest shrinking. Let C be a cluster with transitions t 1 , . . . , t k , which intervals have lower bounds α 1 , . . . , α k and upper bounds β 1 , . . . , β k . As in Theorem 6, we can compute maxup C = min{β i | i ∈ 1..k}, the minimal upper bound of intervals attached to transitions in C. The reduction of cluster of C is a cluster C red , obtained as a restriction of C to transitions {t i | α i < maxup C }. Clearly, a transition t i with interval [α i , β i ] such that α i > maxup C will never fire, and is not part of the pruned cluster P rune(C) nor of its reduced cluster.

Second, considering two transitions t i , t j in C, we will say that I(t i ) is a neighbor of I(t j ) if we have α i = β j . Neighbor intervals have at most one common point, that will disappear under any shrinking of guards. Moreover, if α i = β j = maxup C and I(t i ) ∩ I(t j ) = maxup C then t i appears in P rune(C), but not in the cluster P rune(C ∆ ), where C ∆ is obtained by shrinking intervals I(t 1 ), . . . , I(t k ) by any value ∆ > 0. One can easily show that is this case, t i ∈ C red .

Let N = P rune(N ) be the pruning of N and let U be the untiming of N . Let N red be the restriction of N to its reduced clusters, and U red be the untiming of N red . Now, by definition of termination in FC-TPNs, we have the following property: termination is a robust property of N under guard shrinking iff U has a non-terminating run ⇔ U red has a non-terminating run As before, checking this property is feasible on untimed Petri nets, and hence we obtain a decision procedure for robustness of termination. 2

7. Discussion

Undecidability in TPNs

In general, all problems listed in Section 4 are undecidable for TPNs, regardless of the choosen semantics. It is well known since [START_REF] Jones | Complexity of some problems in Petri nets[END_REF] that TPNs can encode a two-counter machine. Let us recall this encoding. A counter machine is given as a set of counters C 1 , . . . , C k and a finite list of instructions that increment or decrement counters. An instruction of the from i : inc(C j ), means that the machine increments a counter C j and moves to instruction i + 1. An instruction of the form i : if C j > 0 dec(C J ) else goto q means that the machine has to decrement counter C j if it holds a value greater than 0, or move to instruction q otherwise. An instruction of the from i : ST OP halts the machine. One usually assumes that there exists a single instruction of this form. We say that a machine terminates iff it can reach a halting instruction, that it is bounded iff there is an upper bound on the value of its counters. It is well known that termination and boundedness are undecidable for such machines with at least two counters. Getting back to TPNs, one can encode counters with places denoted C 1 , . . . , C k , and associate to each line of instruction i as place p i . A machine is at instruction i if place p i contains a token, and the value of a counter C j is the number of tokens in place C j . Then using the gadget of Figure 13-a), one can encode a decrement instruction: if place (counter) C 1 is not empty and place p i holds a token, then transition t i,nz will fire at latest 1 time unit after its enabling, consuming a token in C 1 and moving a token from p i to p i+1 . If C 1 is empty, then transition t i,z will fire between 2 and 3 time units after enabling, and move a token from p i to p j . Similarly, using the gadget of Figure 13-b), one can encode an increment. This is a standard encoding by TPNs with single server semantics, and we do not prove here that termination, boundedness of a TPN can be brought back to the undecidable questions of termination and boundedness of a counter machine. Interestingly, this encoding still works under a multi-enabling semantics: counter machines are simulated by Time Petri nets in which transitions have at least one 1-bounded place in their preset (the "instruction" place). Within this setting, in a multi-enabling semantics, all configurations of a TPN have at most one instance of a transition enabled. Hence, in this setting the single server and multienabling semantics coincide, and the encoding originally defined for TPNs still works. More interestingly, one can encode a termination question as a question of firability of a transition t in a TPN, by connecting a new transition t to place p n , where instruction n is the halting instruction of the machine. This is depicted by the gadget of Figure 13-c), where the ellipse symbolizes all places and transitions of a TPN encoding a counter machine. Clearly, in this gadget, transition t can fire iff a token can be put in place p n . This shows that firability of transition t is undecidable for TPNs, as well as coverability (as one cannot decide if • t is coverable). In the rest of this section, we use the gadget of Figure 13-c) to represent a piece of TPN that encodes a particular counter machine, allowing us to fire transition t, if it reaches halting instruction n. The counter machine gadget can be reused to prove undecidability of robustness questions. Consider the example of Figure 14. In this Figure, a token circulates each integer date among places p 1 , p 2 , p 3 and another one among places p 4 , p 5 , p 6 . It is never the case that M (p 1 ) and M (p 6 ) are marked together, so regardless of the behavior of the gadget CM , transition t never fires. Now, under any enlargement ∆, transitions can be delayed, and configurations where M (p 1 ) = M (p 6 ) = 1 can occur an arbitrary number of times at increasing dates during an execution. Hence, if CM terminates, then t will fire. Note that with the encoding used in the gadgets of Figure 13, choosing ∆ < 1 does not change the untimed behavior of the counter machine gadget. Note also that t 1 , t 2 , t 3 , t 4 , t 5 , t 6 clearly belong to the set of fireable transitions of this net, and of its enlarged version. Hence, firability is not robust for this net iff t can fire, i.e. iff the counter machine part terminates. One can similarly encode a net which set of fireable transitions is robust under guard shrinking iff a particular counter machine terminates, as shown in the example of Figure 15. One can notice that the counter machine and the examples of Figures 14 and15 cannot be encoded with Free-Choice TPNs.

p i C 1 p i+1 p j t i,nz [0, 1] t i,z [2, 3] a) p i C 1 p i+1 t i,inc [0, 1] b) CM p p n p n+1 t c)
p 1 p 2 p 3 t 1 [1, 1] t 2 [2, 2] t 3 [2, 2] p 4 p 5 p 6 t 4 [1, 1] t 5 [2, 2] t 6 [2, 2] CM p p n t [0, ∞)
Figure 14: Connections between counter machines and the robustness of firability question.

p 1 p 4 t 1 [0, 1] CM p p n t [1, ∞)

Necessity of assumptions

The proof techniques used to obtain decidability of firability and termination holds for free-choice Time Petri nets with a multi-enabling semantics, when we disallow forced 0-delay sequences. We now show that all these conditions are necessary for our proofs to hold. Let us first address the free choice assumption. The two-counter machine encoding of [START_REF] Jones | Complexity of some problems in Petri nets[END_REF] relies on urgency and uses non-free choice nets. As the counter machine encoding is rather simple, we believe that without the free-choice assumption, all problems listed in Section 4 are undecidable. Moreover, the inclusion relation between untimed causal processes and timed causal processes of a TPN established by Theorem 1 does not hold without the free choice assumption. Consider the non-free choice net N nf c in Figure 16 (left). A causal process ON 5 for Untime(N nf c ) is shown in Figure 16 (right, above). One can verify in this untimed net that transition c is fireable. However, there is no way to build a timed causal net of N nf c that contains ON 5 . Indeed, transition c is not fireable in N nf c and one cannot add event e 3 in the only timed causal net ON 6 defined by N nf c depicted in Figure 16 (right, below). Note also that marking {p 1 , p 3 } is reachable in Untime(N nf c ) (and allows firing of c), but not in N nf c .

Next, we discuss the choice of a multi-enabling semantics. With this semantics, one can consider that a new clock is initialized at any enabling of a cluster (as all transitions from a cluster carry the same set of clocks). Furthermore, when a transition is fired, all remaining instances of transitions in a cluster keep their clocks unchanged. Such a semantics is meaningful and arguably powerful enough, for instance, to address business processes with time that do not contain fork-join constructs, i.e. where inputs are processed through sequences of choices up to completion. Unsurprisingly, with a single server semantics, where we keep only one clock per transition instead of one for every instance of a multiple enabled transition, even our Pruning Lemma 1 fails. This is due to the fact that one cannot remove useless transitions as easily as in multi-enabling semantics. When multiple instances of a transition are enabled, under single server semantics, firing a transition in a cluster does not always reset clocks of competing transitions. These competing transitions-including the ones which would have been pruned otherwise-may become fireable and even urgent at a later date. Consider for instance, the example of Figure 17. With the multi-enabling semantics, the only allowed behavior is to fire a at date 1, and then, as the second enabling of transition a remains urgent, fire it, leading to a single possible execution (a, 1) • (a, 1). With this semantics, pruning removes transition b and does not change the behavior of the net. On the other hand, under single server semantics, one can fire a at date 1, but needs to wait one more time unit before firing another occurrence of a, as the clock attached to the transition is reset. However, 0.5 time units later, transition b can fire. Hence, pruning does not preserve the semantics of nets under a single server semantics. One can also notice from this example that firability of transitions from the same cluster is not a local property of the cluster anymore. Indeed, in the example above, transition b can fire if dob 1 + 2 * lf t(a) ≥ dob 2 + ef t(b), where dob 1 Is the arrival date of the first token in place p 1 and dob 2 the arrival date of the second token. Informally, this means one cannot fire two occurrences of a without allowing b to fire. One can note that this condition refers to arrival dates of tokens, and that hence firability of a transition in a cluster depends on the formerly executed transitions and cannot be checked syntactically as with a multi-enabling semantics. We believe that such a gadget can be used to encode a zero-test, hence yielding undecidability of many questions for free-choice TPNs under a single server semantics. Finally, the 0-delay assumption forbids an arbitrary number of transitions to occur at the same time instant. If this condition is not met, then our algorithm used to build a timed process of N from an untimed process of Untime(P rune(N P )) does not necessarily terminate (Lemma 3). Furthermore, eagerness of urgent transitions firing in zero time can prevent other transitions from firing, which may result in discrepancies between untiming of timed processes of a net and untimed processes of the untiming of this net. Consider the pruned and free choice net N 2 depicted in the Figure 18 below. The only allowed executions of N 2 are Lang(N 2 ) = {(a, 0) k | k ∈ N}. Hence, N 2 has a 0-delay firing sequence a ω , and transition b is not fireable. However, Untime(N 2 ) allows sequences of the form a k • b, and hence transition b is fireable. The example net N 2 of Figure 18 shows that the correspondence between untimed processes of U ntime(N ) and untiming of timed processes of N of Theorem 1 does not hold in presence of forced zero-sequences. The main reason is that as soon as an execution enters a forced zero-sequence, time progress stops, forbidding firing of other timed transitions that cannot occur immediately. The example net N 3 of Figure 18 shows that forced zero-sequences can even constrain components of a net that do not share places. This net contains a forced zero-sequence, that can repeat an arbitrary number of occurrences of transition t 1 without letting time elapse. As a consequence, the behavior of this net is the set of timed words of the form {(t 1 , 0) k | k ∈ N}.

The timed process corresponding to a timed word (t 1 , 0) k is a sequence of k occurrences of transition t 1 . However, there exist processes of Untime(N ) that contain an arbitrary number of occurrences of t 1 and one occurrence of t 2 . Hence, Theorem 1 does not hold if zero-sequences are allowed. Note that this does not mean that there is no effective procedure to build a timed causal net from an untimed causal net when forced zero-sequences can appear. We think that our algorithm could be adapted to handle such Zeno behaviors. One can notice that transitions that initiate forced zero-sequences can be easily detected in a net. They are necessarily transitions which associated interval is [0, 0]. Let T 0 ⊆ T be the set of transitions with [0, 0] interval. Checking existence of forced zero-sequences amounts to checking existence of infinite behaviors containing only transitions in T 0 . This can be decided by building a finite reachability tree (as defined for instance in [START_REF] Desel | Lectures on Petri Nets I: Basic Models[END_REF][START_REF] Finkel | A well-structured framework for analysing petri net extensions[END_REF]) for U ntime(P rune(N )). Indeed, if the reachability tree of U ntime(P rune(N )) shows existence of an infinite sequence (t 1 • • • t k ) ω with t 1 , . . . , t k from T 0 , then this sequence can prevent firing of any transition other than t 1 , . . . , t k and forbids time progress. One can only avoid such a sequence if some transition with ef t equal to 0 is enabled along this run, or if a transition is urgent at the date at which the zero-sequence is entered. We believe that the firability question can be answered in presence of forced zero-sequence, and brought back to another close question. As an execution cannot exit a forced zero-sequence, one can transform the firability question "is there a timed process of a free-choice TPN N that contains an occurrence of transition t" into the equivalent question "is there a timed process of a free-choice TPN N that contains an occurrence of transition t and does not contain an unavoidable forced zero-sequence". t 2 [1, 2] N 3

Difficulty with tackling other decision problems

As mentioned earlier, our proof technique, using relation between untimed processes and processes of untimed nets does not work for any property. In particular for reachability, coverability and for boundedness, we hit some roadblocks that we now explain.

We start with reachability. Consider, for instance, the net shown in Figure 19. It is clear that marking {p 1 , q 1 } is not reachable from the initial marking {p 1 , q 3 } with a multi-enabling semantics. However, it is reachable in the corresponding untimed net. Note also that marking {p 1 , q 3 } is also reachable for this net under a weak semantics (as proposed in [START_REF] Reynier | Weak time Petri nets strike back![END_REF]), which proves that strong multi-enabling and weak semantics of TPNs differ. f [1,1] Let us now address coverability. Consider the FC-TPN N cov shown in Figure 20. Clearly, when removing time constraints from N cov , the obtained (untimed) Petri net allows sequence of transitions a•b, which leaves the net in a marking M such that M (p 1 ) = M (p 3 ) = 1 and M (p 2 ) = 0. However, the timed language of N contains only w = (a, 1)(a, 1)(b, 9)(b, 9) and its prefixes. So, marking M is not reachable or even coverable by N . Thus, unlike for firability and termination, one cannot immediately decide coverability (or reachability) of a marking in an FC-TPN just by looking at its untimed version. This does not contradict Corollary 1: once untimed, the causal process for w does indeed contain the causal process associated with word ab.

Finally, the question of boundedness also does not immediately follow on the same lines as the proofs of Theorems 2 and 3. Consider, for instance, the net N bd of figure 21. The untimed version of this net allows sequences of transitions of the form (t 1 • t 2 ) k , for any arbitrary value k ∈ N. At each iteration of this sequence, place p 3 receives a new token. This net is free choice, and following the result of Theorem 1, for every untimed process U k associated with a sequence (t 1 • t 2 ) k , there exists a timed process N k of N bd . However, this process necessarily contains as many occurrences of t 3 , t 1 and t 2 . As transition t 3 fires immediately as soon as p 3 is filled, the only sequences of moves allowed by N k are of the form (t 1 • t 2 • t 3 ) k , and hence N bd is bounded, even if Untime(N bd ) is unbounded.

Conclusion

In this paper, we defined a class of unbounded time Petri nets with free-choice, which are well-behaved with respect to several properties. In particular, we showed decidability of firability and termination. We crucially use the free choice property and the multi-enabling semantics to obtain these results. Next, we looked at robustness questions under both guard enlargement and shrinking for the problem of firability and termination for these FC-TPNs. In both cases, we show subclasses that are robust and decision procedures to check for robustness in general. The table below summarizes known results for classes of TPNs under multienabling semantics, without forced zero-sequences. In each cell of the table, U stands for an undecidable property for the considered class, D for a decidable property, and C for a property that is granted for all members of the class.

Most of the undecidability results in the first column of the table have already been explained in Section 7.1. One can remark that computing a value for enlargement/shrinking that preserves firability of termination is obviously undecidable as soon as one cannot decide the corresponding robustness question. Let us now address the subclass of bounded TPNs. If a TPN is K-bounded, then one can easily simulate it with a finite timed automaton with |P | • K clocks. As a consequence, firability, coverability and termination are decidable using standards results for timed automata [START_REF] Alur | A theory of timed automata[END_REF]. Similarly, results of [START_REF] Bouyer | Robust model-checking of timed automata via pumping in channel machines[END_REF] can be reused to prove robustness questions on this class. The rest of the table stems from the results of this paper. Theorem 2 shows decidability of firability of some transition t in a FC-TPN, and this result obviously holds for the subclass of FC-TPNs with closed intervals. Similarly, Theorem 3 shows decidability of termination for FC-TPNs, and for their closed intervals subclass. Theorem 4 shows decidability of robustness of firability under enlargement, and how to compute upper bounds for the enlargement values that preserve sets of fireable transitions in an FC-TPN. Interestingly, robustness of firability is guaranteed for nets with closed intervals, as shown in corollary 3. Robustness of firability w.r.t. guard shrinking is shown decidable for FC-TPN in Theorem 5. Note that unlike for guard enlargement, robustness w.r.t guard shrinking is not guaranteed for nets with closed intervals. Finally, robustness of termination w.r.t. guard enlargement is proved in Theorem 6. This property always hold for FC-TPNs with closed guards, as shown in Proposition 4. A similar theorem w.r.t. guard shrinking is proved in Theorem 7.

The results obtained in this paper hold mainly for FC-TPNs, under a multi-enabling semantics, and without forced zero-sequences. The free choice assumption is essential, as otherwise TPNs can encode counter machines, as explained earlier in this section. One can also notice that isomorphism of the LTS of a net and of its pruned version (Lemma 1) holds only for free choice TPNs, but that absence of forced zero-sequences is not required to prove this equivalence. However, it is essential to prove Theorem 1. This does not immediately means, that firability and robustness questions are undecidable for FC-TPNs with forced zero-sequences. As explained earlier, we conjecture that firability of a particular transition can be addressed for TPNs with such Zeno behaviors, but with additional tests that check that such sequences do not "freeze time" before reaching a configuration allowing to fire t.

Closely-related problems such as coverability and boundedness for FC-TPN and robustness of these properties are still open questions. Indeed, the proofs relying of the relation between timed causal nets and their untimed versions established by the pruning Lemma 1 cannot be immediately extended to handle these problems as shown through the examples earlier. Despite this, we believe that we can indeed modify the techniques in this paper to get decidability for coverability and boundedness problems for FC-TPNs, and leave this as another an interesting line for future research. On the other hand, it is unclear whether reachability for FC-TPNs would even be decidable.

Figure 1 :

 1 Figure 1: An example TPN

  , and for any condition b of B we have |{e | (e, b) ∈ G}| ≤ 1 and |{e | (b, e) ∈ G}| ≤ 1.

Figure 3 :

 3 Figure 3: An example of FC-TPN

Figure 4 : 2 Figure 5

 425 Figure 4: Untimed causal nets ON 1 and ON 2

  p

Figure 5 :

 5 Figure 5: Timed causal net ON 3 and ON 4

Example 2 .

 2 Consider the FC-TPN N in Figure6. Consider transition b, and its cluster[b]. One can notice from the definition of FC-TPNs that all transitions from the same cluster have a new enabling instance created as soon as any transition from the same cluster has a new enabling instance. Note also that in this example it is clear that transition c will never be fired: in a configuration (M, enab), every enabling instance of c is created at the same time as another instance of b and d, and hence we have enab(c) = enab(b) = enab(d).Let enab(c) = enab(b) = r 1 . . . r k . Transition b has to fire or be disabled at lf t(b) -r 1 , lf t(b) -r 2 , . . . . If b fires or is disabled, then the oldest instance of c is also disabled. As we have ef t(c) > lf t(b) every i th instance of b will fire or be disabled before the i th instance of c is allowed to fire. Hence one can safely remove transition c without changing the semantics of the net.

Figure 6 :

 6 Figure 6: a FC-TPN N

Figure 7 :

 7 Figure 7: The pruned net Prune(N )

  C 2 and C 2 modified clock values are identically updated for unpruned transitions in enab 2 and enab 2 , and clock values in enab 2 for pruned transitions remains copies of clock values for transitions in their cluster. Hence, C 2 = R(C 2 ).

Figure 8 :

 8 Figure 8: Pruning only works for FC-TPNs

7 else 8 min 9 S 13 if e ∈ S i then 14 CLK 19 Pick 21 τ

 78913141921 = min e ∈posb(σi) mfd (σ i , e ); i = {e ∈ posb(σ i ) | mfd (σ i , e ) = min}; 10 if S = S i ∩ E = ∅ then 11 Pick an event e t = (X, t) from S ; 12 else = CLK + max{0, td (σ i , e)}; 15 τ (e) = CLK ; 16 σ i+1 ← σ i ∪ {e} ; ρ i+1 ← ρ i ; 17 GOT O Step-23; 18 else an event e t = (X, t) from S i ; 20 CLK = CLK + lf t(t) -td (σ i , e t ) ; (e t ) = CLK // adding time stamp 22

Figure 10 :

 10 Figure 10: A FC-TPN and guard shrinking

Figure 11 :Proposition 4 .

 114 Figure 11: A FC-TPN that is not robust w.r.t. terminating under guard enlargement

2 6. 2 . 2 .

 222 Formally δ = min{d j | ∃t j ∈ i∈1..k C i }. Then, any enlargement by a positive value ∆ < δ gives a net whose clusters contain the same transitions as C 1 , . . . , C k , and hence U ntime(N ) = U ntime(N ∆ ). Robustness of Termination w.r.t. guard shrinkingThe class of FC-TPNs is not robust w.r.t. termination under guard shrinking. As in the case of guard enlargement, we can easily exhibit a net N which has an infinite run, but which shrunk version N has only terminating runs, for any value of δ. Consider for instance the net of Figure12.

Figure 12 :

 12 Figure 12: A non-robust FC-TPN w.r.t. termination under guard shrinking

Figure 13 :

 13 Figure 13: Encoding instructions i : if C!1 > 0 dec(C 1 ) else goto j; and i : inc(C 1 ) and a complete counter Machine with TPNs.

Figure 15 :

 15 Figure 15: Connections between Counter machines and the robustness of firability with shrinking.

3 a : e 1 b : e 2 c : e 3 p 1 p 1 p 2 p 2 p 3 a : e 1 a : e 4 b : e 2 1 1 1 9 Figure 16 :

 312112231421916 Figure 16: A non-free choice TPN N nf c (left), a causal process ON 5 (right, up) and a timed causal process ON 6 (right, below) of N nf c .

Figure 17 :

 17 Figure 17: A net showing that multi-enabling semantics is essential.

Figure 18 :

 18 Figure 18: A Free choice TPN N 2 with Zeno behavior, and a free choice TPN N 3 showing that Lemma 1 does not hold with forced zero-sequences.

Figure 19 :

 19 Figure 19: Pruning and untiming does not preserve reachability

Figure 20 :

 20 Figure 20: A free-choice TPN Ncov

Figure 21 :

 21 Figure 21: An FC-TPN N bd that is bounded, but whose untimed version is not

  1 and t i ∈ dom(enab ),

	enab (t i )	if deg(M , t i ) = deg(M , t i ) and t i ∈ dom(enab ),
	(0)	if t i ∈ dom(enab ), and deg(M , t i ) = 1
		otherwise.

Table 1 :

 1 Summary of the results for (FC)-TPNs. U : undecidable, D decidable, C property guaranteed by the class.