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

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

Claude Jard
email: claude.jard@univ-nantes.fr

Pierre-Alain Reynier
email: pierre-alain.reynier@lif.univ-mrs.fr

P.-A Reynier

/ Robustness

Robustness of Time Petri Nets under Guard Enlargement

Keywords: Time Petri nets, Robustness, timed automata

Robustness of timed systems aims at studying whether infinitesimal perturbations in clock values can result in new discrete behaviors. A model is robust if the set of discrete behaviors is preserved under arbitrarily small (but positive) perturbations. We tackle this problem for time Petri nets (TPNs, for short) by considering the model of parametric guard enlargement which allows time-intervals constraining the firing of transitions in TPNs to be enlarged by a (positive) parameter.

We show that TPNs are not robust in general and checking if they are robust with respect to standard properties (such as boundedness, safety) is undecidable. We then extend the marking class timed automaton construction for TPNs to a parametric setting, and prove that it is compatible with guard enlargements. We apply this result to the (undecidable) class of TPNs which are robustly bounded (i.e., whose finite set of reachable markings remains finite under infinitesimal perturbations): we provide two decidable robustly bounded subclasses, and show that one can effectively build a timed automaton which is timed bisimilar even in presence of perturbations. This allows us to apply existing results for timed automata to these TPNs and show further robustness properties.

Introduction

Formal methods can be used to specify and verify properties of complex real-life systems. For instance, safety-critical systems with several interacting components have been studied by modeling them as networks of timed automata [START_REF] Alur | A Theory of Timed Automata[END_REF] (TA), time Petri nets [START_REF] Merlin | A Study of the Recoverability of Computing Systems[END_REF] (TPNs) and so on. However, the usual semantics of many of these classical models rely on hypotheses which may not be met at the implementation level, such as the infinite precision of clocks or instantaneous mode transitions. Obviously, the semantics of these systems is idealized : first, in implementations of timed systems, clock values are discretized, which may lead to approximations of real clock values. Second, in distributed systems, the clocks of two different processes may evolve at slightly different rates. As a result, the extreme precision of the models leads to unexpected outcomes when there is even a slight imprecision at the level of implementation. A solution to handle this problem is to introduce perturbations in the models, and then study implementability issues for these systems. This means providing tools to verify properties of models under perturbation, and also developing robust models of systems, which preserve some good properties even in the presence of small perturbations. For timed automata, a model of guard enlargement has been extensively studied in the last decade [START_REF] Puri | Dynamical Properties of Timed Automata[END_REF][START_REF] Bouyer | Robust Model-Checking of Linear-Time Properties in Timed Automata[END_REF][START_REF] Bouyer | Robust Analysis of Timed Automata via Channel Machines[END_REF][START_REF] De Wulf | Robust Safety of Timed Automata[END_REF][START_REF] Bouyer | Robust Model-Checking of Timed Automata via Pumping in Channel Machines[END_REF][START_REF] Sankur | Untimed Language Preservation in Timed Systems[END_REF]. In [START_REF] De Wulf | Systematic Implementation of Real-Time Models[END_REF], it is proved that this model of perturbation covers both the issue of discretization and drift of clocks, by reducing the implementability problem to the analysis of the enlarged semantics.

In this paper, we tackle the problem of robustness under small perturbations in the distributed and timed setting of time Petri nets [START_REF] Merlin | A Study of the Recoverability of Computing Systems[END_REF]. TPNs associate time intervals to transitions representing "guards" within which the transition must fire once it is enabled and our aim is to study the effect of small enlargement of intervals. In this work, we address mainly three problems. The first is the robust boundedness problem, which consists of deciding, for a given bounded TPN, whether there exists a positive enlargement for which the set of reachable markings is finite. The second problem considered in this paper is robust untimed language preservation, which consists in deciding whether there exists a positive enlargement for which the untimed language remains unchanged. The third problem considered is preservation of markings for a subset of places under enlargement. As mentioned, robustness issues have been well studied for TA. Hence, a possible way to address the robustness problem for TPNs is to translate TPNs to TA, and reuse existing techniques. However, we show in this paper that results on TA do not always extend to TPNs. For instance, robust safety, i.e., avoidance of some bad configurations under perturbation, is decidable in TA, but not for TPNs. The objectives of this paper are to consider robustness issues for TPNs, and to study to what extent results proven for TA can be applied on TPN.

We first show that the phenomenon of accumulation of perturbations, which Puri exhibited in TA in [START_REF] Puri | Dynamical Properties of Timed Automata[END_REF], also occurs in TPN, but in a slightly different way. In a TPN, firing of transitions which are not causally related may occur systematically at distinct dates in a non-perturbed model, and after accumulation of some delays, become concurrent in the perturbed model. This has two consequences: first, reachable markings of a net may change under perturbation. Second, a bounded net may become unbounded under perturbation. This is a significant difference from the TA model which is defined over a finite set of locations which does not change under perturbation. We show an example of a TPN whose unbounded perturbed semantics cannot be captured by a finite timed automaton. We then use this example to prove that the three problems we consider are undecidable. There are several translations from TPN to TA [START_REF] Gardey | A Zone-Based Method for Computing the State Space of a Time Petri Net[END_REF][START_REF] Cassez | Structural translation from Time Petri Nets to Timed Automata[END_REF][START_REF] Lime | Model Checking of Time Petri Nets Using the State Class Timed Automaton[END_REF][START_REF] D'aprile | From Time Petri Nets to Timed Automata:An Untimed Approach[END_REF]. We study which of these translations can be used to lift robustness results on TA to the model of TPNs. In particular, we prove that the marking class timed automaton construction of [START_REF] D'aprile | From Time Petri Nets to Timed Automata:An Untimed Approach[END_REF] is compatible with guard enlargement, in the sense that the property of timed bisimulation is preserved when guards are enlarged by the same parameter in the TA and in the TPN. We use this result to exhibit subclasses of bounded TPNs for which robust boundedness, language preservation and the preservation of markings for a subset of places are decidable.

This paper is an extended version of [START_REF] Akshay | Robustness of Time Petri Nets under Guard Enlargement[END_REF], and is organized as follows: Section 2 defines the models used. Section 3 introduces our perturbation model for TPNs, and the robust boundedness and language, markings preservation problems. Section 4 shows that many robustness issues are undecidable for TPNs. Section 5 presents a robust translation from TPNs to TA, i.e. compatible with guard enlargement. Sections 6 and 7 build on this result to exhibit decidable subclasses of TPNs. Section 8 considers robustness of markings of a subset of places under enlargement. Section 9 presents a case study, namely the robustness of schedules in a train carrousel, before conclusion.

Preliminaries

Let Σ be a finite alphabet, Σ * is the set of finite words over Σ. We also use Σ ε = Σ ∪ {ε} with ε (the empty word) not in Σ. The sets N, Q ≥0 and R ≥0 are respectively the sets of natural, non-negative rational and non-negative real numbers. An interval I of R ≥0 is a Q ≥0 -interval iff its left endpoint belongs to Q ≥0 and its right endpoint belongs to Q ≥0 ∪ {∞}. We set I ↓ = {x ∈ R ≥0 | x ≤ y for some y ∈ I}, the downward closure of I. We denote by I(Q ≥0 ) the set of Q ≥0 -intervals of R ≥0 . A valuation v over a finite set X is a mapping from X to R ≥0 . We denote by 0 the valuation which assigns to every x ∈ X the value 0. For any value d ∈ R ≥0 , the valuation v + d is defined by (v + d)(x) = v(x) + d, ∀x ∈ X. Definition 2.1. (Timed Transition System (TTS)) A timed transition system over Σ ε is a transition system S = (Q, q 0 , →), where Q is the set of states, q 0 ∈ Q is the initial state, and the transition relation → consists of delay moves q d -→ q (with d ∈ R ≥0 ), and discrete moves q a -→ q (with a ∈ Σ ε ). Moreover, we require standard properties of time-determinism, additivity and continuity for the transition relation →.

TTSs describe systems combining discrete and continuous evolutions. They are used to define and compare semantics of TPNs and TA. With these properties, a run of S can be defined as a finite sequence of moves ρ = q 0

d 0 -→ q 0 a 0 -→ q 1 d 1 -→ q 1 a 1 -→ q 2 . . . an -→ q n+1
where discrete actions and delays alternate, and which starts in the initial state. To such a run corresponds a word a 0 . . . a n over Σ ε ; we say that this word is accepted by S. The language of S is the set of words accepted by S.

Definition 2.2. (Time Petri Nets (TPNs))

A time Petri net N over Σ ε is a tuple (P, T, • (.), (.) • , m 0 , Λ, I) where P is a finite set of places, T is a finite set of transitions with P ∩ T = ∅, • (.) ∈ (N P ) T is the backward incidence mapping, (.) • ∈ (N P ) T is the forward incidence mapping, m 0 ∈ N P is the initial marking, Λ : T → Σ ε is the labeling function and I : T → I(Q ≥0 ) associates with each transition a firing interval. We denote by α(t) (resp. β(t)) the lower bound (resp. the upper bound) of interval I(t).

Semantics. Introduced in [START_REF] Merlin | A Study of the Recoverability of Computing Systems[END_REF], TPNs associate a time interval with each transition of a Petri net. A configuration of a TPN is a pair (m, ν), where m is a marking in the usual sense, i.e. a mapping in N P , with m(p) the number of tokens in place p. A transition t is enabled in a marking m if m ≥ • t. We denote by En(m) the set of enabled transitions in m. The second component of the pair (m, ν) is a valuation over En(m) which associates with each enabled transition its age, i.e. the amount of time that has elapsed since this transition was last enabled. We choose the classical semantics1 (see for instance [START_REF] Berthomieu | Modeling and Verification of Time Dependent Systems Using Time Petri Nets[END_REF]) defined as follows. An enabled transition t can be fired if ν(t) belongs to the interval I(t). The set of configurations from which a transition t can be fired is called the firing domain of t. The result of this firing is as usual the new marking m = m -• t + t • . Moreover, some valuations are reset. We say that transition t is newly enabled by firing of t from marking m, and write ↑enabled(t , m, t) iff:

t ∈ En(m -• t + t • ) ∧ ((t ∈ En(m -• t)) ∨ t = t )
Reset valuations correspond to newly enabled clocks. Thus, firing a transition is not an atomic step and the transition currently fired is always reset. The set ADM(N ) of (admissible) configurations consists of the pairs (m, ν) such that ν(t) ∈ I(t) ↓ for every transition t ∈ En(m). Thus time can progress in a marking only when it does not leave the firing interval of any enabled transition. The semantics of a TPN N = (P, T, • (.), (.) • , m 0 , Λ, I) is a TTS N = (Q, q 0 , →) where Q = ADM(N ), q 0 = (m 0 , 0) and → is defined by: -delay moves: (m, ν)

d -→ (m, ν + d) iff ∀t ∈ En(m), ν(t) + d ∈ I(t) ↓ , -discrete moves: (m, ν) Λ(t) --→ (m -• t + t • , ν ) iff t ∈ En(m) is s.t. ν(t) ∈ I(t), and ∀t ∈ En(m -• t + t • ), ν (t ) = 0 if ↑enabled(t , m, t) and ν (t ) = ν(t) otherwise. • p 0 p 1 p 2 (2, 3] a [1, 2] a ′ Figure 1. The TPN N 0 .
One may immediately notice that the semantics of TPN integrates a notion of urgency: as time can elapse only up to a point that does not violate any upper bound of time constraints attached to enabled transitions, some transitions have to fire before other ones. Consider for instance the TPN of Figure 1. Transition a has to fire at a date d that lays between 1 and 2 time units after its enabling, and transition a at a date d that is strictly greater than 2 time units after its enabling. According to the semantics, one cannot let 2 time units elapse without firing a . Hence, within this setting, only transition a can fire. The (untimed) language of N is defined as the untimed language of N and is denoted by L(N ). The reachability set of N , denoted Reach(N ), is the set of markings m ∈ N P such that there exists a reachable configuration (m, ν). A bounded TPN is a TPN N such that Reach(N ) is finite.

Timed automata: First defined in [START_REF] Alur | A Theory of Timed Automata[END_REF], the model of timed automata associates a set of non-negative real-valued variables called clocks with a finite automaton. Let X be a finite set of clocks. We write C(X) for the set of constraints over X, which consist of conjunctions of atomic formulae of the form x c for x ∈ X, c ∈ Q ≥0 and ∈ {<, ≤, ≥, >}. We also define the proper subset C ub (X) of upper bounds constraints over X where ∈ {<, ≤}.

Definition 2.3. (Timed Automata (TA))

A timed automaton A over Σ ε is a tuple (L, 0 , X, E, Inv) where L is a finite set of locations, 0 ∈ L is the initial location, X is a finite set of clocks, Inv ∈ C ub (X) L assigns an invariant to each location and

E ⊆ L × C(X) × Σ ε × 2 X × L is a finite set of edges.
An edge e = ( , γ, a, R, ) ∈ E represents a transition from location to location labeled by a with constraint γ and reset R ⊆ X.

Semantics. For R ⊆ X, the valuation v[R] is the valuation v such that v (x) = v(x) when x ∈ R and v (x) = 0 otherwise. Finally, constraints of C(X) are interpreted over valuations: we write v |= γ when the constraint γ is satisfied by v. The semantics of a TA A = (L, 0 , X, E, Inv) is the TTS

A = (Q, q 0 , →) where Q = {( , v) ∈ L × (R ≥0 ) X | v |= Inv( )}, q 0 = ( 0 , 0) and → is defined by: -delay moves: ( , v) d -→ ( , v + d) if d ∈ R ≥0 and v + d |= Inv( ); -discrete moves: ( , v) a -→ ( , v ) if there exists some e = ( , γ, a, R, ) ∈ E s.t. v |= γ and v = v[R].
The (untimed) language of A is defined as that of A and is denoted by L(A).

Timed (bi)-simulation:

Let S = (Q, q 0 , →) and S = (Q , q 0 , → ) be two TTSs. A relation R ⊆ Q×Q is a timed simulation if and only if, (q 0 , q 0 ) ∈ R and for every σ

∈ Σ ∪ R ≥0 , q 1 ∈ Q, q 1 ∈ Q such that (q 1 , q 1 ) ∈ R, if q 1 σ -→ q 2 ,
then there exists q 2 such that q 1 σ -→ q 2 and (q 2 , q 2 ) ∈ R. We will say that S simulates S and write S S when such a relation R among states of S and S exists. If in addition R -1 is a timed simulation relation from S to S, then we say that R is a timed bisimulation. We say that S and S are timed bisimilar when such a relation R among states of S and S exists, and write S ≈ S .

Perturbations in TPN

Perturbations in timed automata [START_REF] Bouyer | Robust Model-Checking of Linear-Time Properties in Timed Automata[END_REF][START_REF] Bouyer | Robust Analysis of Timed Automata via Channel Machines[END_REF][START_REF] De Wulf | Robust Safety of Timed Automata[END_REF]: We start by fixing a parameter ∆ ∈ R ≥0 . Given a constraint g ∈ C(X), we define its ∆-enlargement as the constraint obtained by replacing any atomic formulae of the formulae x c for x ∈ X, c ∈ N and ∈ {<, ≤, ≥, >}, by the formulae x c + ∆ if ∈ {<, ≤}, and by the formulae x c -∆ if ∈ {≥, >}. Now, given a timed automaton A, we denote by A ∆ the TA obtained by replacing every constraint by its ∆-enlarged version (both in guards and invariants). In the rest of the paper, we will denote by Reach(A ∆ ) the set of locations of A that are reachable in A ∆ ). This model of perturbation verifies the following monotony property: for TA A and any ∆ ≤ ∆ ∈ R ≥0 , we have A ∆ A ∆ . In the sequel, we will use the following result:

Proposition 3.1.

([9])

Let A be a timed automaton and S be a subset of locations of A. One can decide whether there exists

∆ ∈ Q >0 such that Reach(A ∆ ) ∩ S = ∅.
This property means that one can decide robustness of some simple safety properties for timed automata. If one takes a set Bad of locations that are not in Reach(A), and that the modeled system should never reach to remain safe, then finding ∆ ∈ Q >0 such that Reach(A ∆ ) ∩ S = ∅ amounts to ensuring that some clock precision allows to preserve safety of the system.

Introducing perturbations in TPNs: Our goal is to consider a similar model of perturbation for time Petri nets. Given an interval I ∈ I(Q ≥0 ), we denote by I ∆ the interval obtained by replacing its lower bound α by the bound max(0, α -∆), and its upper bound β by the bound β + ∆. Given a TPN N , we denote by N ∆ the TPN obtained by replacing every interval I by the interval I ∆ . We can then easily prove that Petri nets enjoy a monotony property similar to that of timed automata. This entails that if the system verifies a safety property for some perturbation ∆ 0 , it will also verify this property for any ∆ ≤ ∆ 0 : Lemma 3.2. Let N be a TPN and ∆ ≤ ∆ ∈ R ≥0 . We have N ∆ N ∆ .

Proof:

First of all, one can notice that moves of a TPN are deterministic, that is if we have (m, ν)

d -→ (m , ν ) or (m, ν) Λ(t)
--→ (m , ν ), (m , ν ) is uniquely defined. It is then sufficient to prove that every run of N ∆ is a run of N ∆ to show existence of a simulation relation. We can now reason by induction on the length of runs of N ∆ to prove the following claim. Let ρ = (m 0 , ν 0 ) -→ . . . -→ (m n , ν n ) be a run of N ∆ and N ∆ . Then, any move (m n , ν n ) -→ (m n+1 , ν n+1 ) of N ∆ , is also a move of N ∆ . Suppose ρ is of size 0. If there is a delay move from (m 0 , ν 0 ) for some value d, then we have ∀t ∈ En(m 0 ), ν(t)

+ d ∈ I ∆ (t) ↓ , that is ν(t) + d ≤ β(t) + ∆ ≤ β(t) + ∆ and this delay move is also allowed in N ∆ . If there is a discrete move (m 0 , ν 0 ) t - → (m 1 , ν 1 ) in N ∆ ,
then t is enabled in m 0 , and we have α(t) -∆ ≤ x t ≤ β(t) + ∆. Hence, we have α(t) -∆ ≤ x t ≤ β(t) + ∆ , and discrete transition t is allowed from (m 0 , ν 0 ) in N ∆ . Similar reasoning holds for any configuration reached after a run of arbitrary length in N ∆ .

Problems considered

We now define robustness problems on TPNs in a way which is consistent with the monotony property stated above. Recall that given a TPN N over a set of places P and a marking m ∈ N P , N is said to cover m iff there exists m ∈ Reach(N ) such that m ≤ m (i.e., m(p) ≤ m (p) for all p ∈ P ).

Robust boundedness: Given a bounded TPN N , does there exist ∆ ∈ Q >0 such that N ∆ is bounded?

Robust untimed language preservation: Given a bounded TPN N , does there exist

∆ ∈ Q >0 such that L(N ∆ ) = L(N )?
Subset-markings robustness (SMR): Given a bounded TPN N defined over a set of places P , and given a subset of places X ⊆ P , does there exists ∆ ∈ Q >0 such that the projection onto X of Reach(N ) is equal to the projection onto X of Reach(N ∆ )?

We call a TPN N robustly bounded if there exists ∆ ∈ Q >0 such that N ∆ is bounded. This problem is strongly related to the problem of robust safety asking, given a bounded TPN N with set of places P , and a marking m ∈ N P , whether there exists ∆ ∈ Q >0 s.t., N ∆ does not cover m. In fact, our undecidability and decidability results for robust boundedness will easily extend to this problem. However, the situation differs for robust untimed language preservation and so we treat this problem separately.

The above properties are considered in the setting of bounded TPNs. However, from the undecidability results presented in section 4, we can infer undecidability in the unbounded setting as well.

Robustness under a bounded horizon

Consider again the example net N 0 in Figure 1. Due to the open interval and urgency condition, transition a has to fire before transition a, and furthermore, it has to fire at most 2 time units after enabling. Hence, in the non-enlarged semantics of this net, transition a never fires, and no marking in which place p 1 is marked can be reached. However, any enlargement of guards results in reachability of markings with place p 1 marked. From this example, we can easily construct TPNs that are not robustly bounded nor robustly safe. Now, we observe that, in this example, the firing domain of transition a is not reachable, but is a "neighbor" of the reachable configuration (p 0 , ν(a ) = 2).

Formally, given a set of configurations S and a configuration (m, ν) ∈ S, we say that S is a neighbor of (m, ν) if ν is in the topological closure of the set V = {ν | (m, ν ) ∈ S}. As in the above example, it is immediate to see that the presence of such neighbors leads to additional behaviors under the enlarged semantics. However, this simple form of non-robustness can be easily checked in bounded TPNs. Proposition 3.3. Let N be a bounded net. Then one can check whether there exists a reachable configuration (m, ν) and a transition t such that, the firing domain of t is a neighbor of (m, ν).

Proof:

We can compute a (finite) symbolic representation of the reachability set (using the state-class graph construction [START_REF] Berthomieu | Modeling and Verification of Time Dependent Systems Using Time Petri Nets[END_REF][START_REF] Lime | Model Checking of Time Petri Nets Using the State Class Timed Automaton[END_REF] for instance). The state class graph is a transition system where states are pairs of the form (m, C) in which m is a reachable marking of the net, and C is a constraint on the values of the clocks attached to transitions that are enabled in m. Transitions of the state class graph are of the form (m, C) t -→ (m , C ), where m is the marking reached from m after firing t. Furthermore, t is fireable iff C ∧ I(t) is satisfiable. The resulting constraint C is obtained from C by performing the following operations: i) add to C the constraints that the value of clock x t , attached to transition t, belongs to I(t), and that no other urgent transition could have been fired, ii) eliminate constraints attached to transitions that are disabled by the firing of t, and iii) add new constraints for transitions that are newly enabled. We refer readers to [START_REF] Berthomieu | Modeling and Verification of Time Dependent Systems Using Time Petri Nets[END_REF][START_REF] Lime | Model Checking of Time Petri Nets Using the State Class Timed Automaton[END_REF] for technical details on this construction. Now, for a bounded net, the state class graph is finite, and for every state class (m, C) and any transition t such that • t ≤ m with open interval

I(t) = (a, b], I(t) = [a, b) or I(t) = (a, b) that cannot be fired from (m, C), one can check whether t is fireable with I (t) = [a, b].
Requiring that all intervals must be closed solves robustness problems due to neighbor configurations. In the next subsection, we will show that robustness issues may not be only due to neighbor configurations. In fact, when we consider unbounded executions, some delay accumulation mechanisms -similar to those exhibited in [START_REF] Puri | Dynamical Properties of Timed Automata[END_REF] for timed automata, can occur in TPNs and may result in new reachable markings.

But first let us examine the case of bounded executions. Instead of considering infinite or unboundedly long executions, the authors of [START_REF] Swaminathan | The Surprising Robustness of (Closed) Timed Automata against Clock-Drift[END_REF] study robustness issues for timed automata under a bounded horizon, i.e. considering executions with a fixed number of discrete transitions. In the setting of TPN, assuming that we only use closed intervals one can prove that any net is robust under such a bounded horizon. Formally, this means that given an integer K, one can always pick a sufficiently small ∆ > 0 to ensure that no new behavior occurs during the K first discrete steps of the system. Lemma 3.4. Let N be a net with closed intervals, and let K ∈ N. Then, we can compute ∆ K > 0 s.t.:

• the set of markings reachable by runs with at most K discrete moves is the same in N and in N ∆ K ,

• the restrictions of the untimed languages of N and N ∆ K to words of length at most K are the same.

Proof:

We will consider, without loss of generality, that the considered net has integral bounds. We first build a (finite) unfolding of N , that is an acyclic automaton that memorizes paths of length at most K in the state class graph of N . Its states are of the form (m, C, n), meaning that a marking (m, C) is reached at step n, and a transition (m, C, n)

t -→ (m , C , n + 1) occurs iff (m, C) t -→ (m , C
) is a transition of the state class graph of N , and n < K. Note that constraints are conjunctions of inequations of the form a ≤ x t ≤ b and a ≤ x t -x t ≤ b. Indeed, it is known that given a TPN with closed intervals, every state class built is defined as a conjunction of non-strict inequalities. Let us denote by U K (N ) this finite unfolding.

We then build a parametric unfolding of N ∆ up to depth K, that memorizes (parameterized) constraints attached to transitions, a constraint on the value of ∆, and the number of transitions already fired. States of this parametric unfolding are of the form (m, C, D, n) where m is a marking of N , C is a conjunction of constraints on clocks and clock differences involving the parameter ∆, D is an interval describing admissible values for ∆ and 0 ≤ n ≤ K indicates the depth in the unfolding. More precisely, C is a conjunction of constraints of the form a-q.∆ ≤ x t ≤ b+q .∆ and a-q.∆ ≤ x t -x t ≤ b+q .∆, with q, q ∈ N. Given such a constraint C, we denote by C ∆=0 the constraint on clocks and clock differences (without parameter ∆) obtained by setting ∆ to 0. For every transition t, the time interval

I(t) = [a, b] is represented by the constraint φ t = a -∆ ≤ x t ≤ b + ∆. We start from initial configu- ration (m 0 , ν 0 , [0, ∞), 0). Then for each configuration (m, C, D, n) we can stop if n = K, or add a new transition (m, C, D, n) t -→ (m , C , D , n + 1)
, where C and D are computed as follows. Observe that considering the constraint C ∆=0 , the triple (m, C ∆=0 , n) is a state of U K (N ), for which we know which transitions are fireable, and which are not. Let us consider some transition t fireable in U K (N ) from the state (m, C ∆=0 , n). Observe that when enlarging intervals, it may happen that enabled transitions which were not fireable from (m, C ∆=0 , n) become fireable. To avoid this situation, we will identify an upper bound constraint on ∆. Let us denote by T ⊆ T the set of transitions enabled in m, but not fireable from (m, C ∆=0 , n). We consider the constraint C ∧ φ t ∧ t ∈T ¬φ t , eliminate all variables but ∆, and end up with a constraint on ∆ expressed as some interval I ∆ . First observe that ∆ = 0 is a solution of this set of constraints. Second, the integral bounds appearing in C match those of the corresponding state of U K (N ). Moreover, as N only has closed intervals, every transition t that is not fireable has a firing interval which is at least 1-unit far away from the domain of its clock variable (in a setting with rational upper and lower bounds for intervals, this firing interval is at a computable and strictly positive rational distance). This implies that the interval I ∆ of admissible values for ∆ is of the form [0, d] or [0, d) with d > 0. We thus let D = D ∩ I ∆ , and compute C from C as usually in the state class graph by elimination of variables attached to disabled transitions from C ∧ φ t , and adding new constraints φ t attached to each newly enabled transition t .

The construction of the unfolding terminates, and the maximal value allowed for ∆ K is given by the tightest interval D appearing in the leaves of the parametric unfolding. As the two unfoldings built are in bijection, both the sets of runs and the untimed languages are preserved.

•

p 1 • p 2 red a, [2, 3] a ′ , [1, 2] t 1 , [0, 2] t 2 , [0, 1] b ′ , [1, 2] b, [2, 3] t 3 , [0, 2] t 4 , [0, 1] t, [1, ∞)

An example of accumulated non-robustness

We have already mentioned that neighbor configurations could lead to new behaviors of a TPN under enlargement. These neighbor configurations can be easily detected in bounded nets, and for a fixed horizon, can be avoided in TPNs with closed intervals. The remaining cases concern TPNs in which new behaviors are not neighbors of the reachability set, considered for an unbounded horizon. In this case a new behavior cannot appear directly from a reachable configuration, and there must be several discrete firings before this new behavior is witnessed. Further the number of steps may depend on enlargement ∆: the smaller ∆ is, the larger will be the number of steps required. Intuitively, the new behavior is due to an accumulation of clock perturbations, rather than a single clock perturbation.

Puri [START_REF] Puri | Dynamical Properties of Timed Automata[END_REF] gave an example of a TA that exhibits accumulations of perturbations. This TA uses two clocks x and y and a location such that, under the exact semantics, the difference between y and x in location always lies in the interval [0, 1]. Under any enlarged semantics (by some value ∆), this difference lies in the interval [0, 2]. There is in addition a transition t leaving location with a guard that can be satisfied only if the difference between y and x is equal to 2. As a consequence, t yields behaviors in the enlarged semantics which are not present in the exact semantics (for any value of ∆).

Though translations from TA to TPN do exist for the exact semantics (see for instance [START_REF] Bérard | Comparison of the Expressiveness of Timed Automata and Time Petri Nets[END_REF]), it is not guaranteed that they also preserve the enlarged semantics. As a consequence, it is not clear that the TPN resulting from the application of such translations to the TA proposed in [START_REF] Puri | Dynamical Properties of Timed Automata[END_REF] will exhibit such accumulations. Instead, we directly build a TPN which exploits the concurrency of Petri nets while using ideas similar to those of Puri.

This TPN, denoted N 1 , is depicted on Figure 2. Informally, it is composed of two components performing periodic behaviors around places p 1 and p 2 respectively. These components can be synchronized using transition t if places p 1 and p 2 are marked simultaneously. Intuitively, these components simulate the behavior of clocks x and y of the TA of Puri in the sense that in the exact semantics, places p 1 and p 2 are marked respectively for the k-th time at timestamps τ k and τ k such that τ k -τ k = 1, and thus t is never fired. On the other hand, in the enlarged semantics, the value of τ k -τ k may 'drift' and thus t may be fired. Observe that this example can be simplified using singleton intervals, but we avoid this to show that problems due to accumulation may arise even without singletons.

We give now some details on the executions of N 1 . With the usual (exact) semantics, the red state in N 1 is not reachable as transition t is never fireable. Indeed, one can verify that any run of N 1 which does not fire transitions t 1 , t 2 , t 3 or t 4 always fires transition a (resp. a , b , b) at time 3k + 2 (resp. 3k + 3, 3k + 1, 3k + 3), for some integer k. By observing the time intervals of transitions t, a and b , one can deduce that to be able to fire transition t, one has to fire simultaneously the transitions a and b, which is impossible.

Consider the net (N 1 ) ∆ , for some positive ∆. We will prove that in this case, it is possible to fire simultaneously transitions a and b. In (N 1 ) ∆ , one can delay the firing of transitions a and a by up to ∆ time units. As a consequence, it is easy to verify that after n iterations of the loop aa , the timestamp of the firing of the last occurrence of a can be delayed by up to (2.n -1).∆ time units (w.r.t. the firing date of this occurrence of a under non-enlarged semantics). Similarly, transitions b and b can occur earlier, and after the n th iteration of the loop b b, the last occurrence of b can be advanced by 2.n.∆ time units (w.r.t. the firing date of this occurrence of b under non-enlarged semantics). Hence, after a number n of occurrences of loops aa and b b with n ≥ 1+∆ 4.∆ , it can be the case that the firing date of the n th occurrences of a and b are identical. Place p 1 and p 2 can remain marked for 1 time unit, and the red place is reachable in (N 1 ) ∆ , for any positive ∆.

Sequential TPNs

The accumulation in the above example was due to concurrent loops in the TPN. When we disallow such concurrency, we obtain a very simple class of sequential TPNs which is a strict subclass of timed automata. We state their properties in detail here as they will be useful in later proofs. Also this exhibits a clear way to distinguish the relative power of TPNs and TA. A TPN N is sequential if it satisfies the following property: for any reachable configuration (m, ν), and for any transitions t, t ∈ T that are fireable from (m, ν) (i.e. such that t, t ∈ En(m), ν(t) ≥ α(t) and ν(t ) ≥ α(t )), t and t are in conflict, i.e. there exists a place p such that m(p) < • t(p) + • t (p). The following lemma states robustness properties of sequential TPNs and their relation to timed automata. Lemma 3.5. We have the following properties:

(i) Checking whether a bounded TPN N is sequential is decidable.

(ii) If N is a sequential bounded TPN, then it can be translated into a timed automaton which resets every clock on each transition.

(iii) If N is sequential, then there exists ∆ ∈ Q >0 such that Reach(N ∆ ) = Reach(N ) and L(N ∆ ) = L(N ).
Proof: Decidability follows from the construction of the state class graph, which is possible as the TPN is bounded. Clearly, this can be done in time linear in the size of the state class graph. The second and third properties follow from the observation that in a sequential TPN, each time a discrete transition is fired, each transition that is enabled in the new/resulting marking is newly enabled. Thus, all the clocks are reset and this implies property (ii). Further, since clocks are reset, there is intuitively no memory in clock values. Considering ∆ < 1 2 to ensure that exactly the same transitions are enabled, we prove by induction on the length of runs that the configurations reached immediately after a discrete transition are the same in N and in N ∆ .

Consider a run ρ = (m 0 , ν 0 )

d 1 ,a 1 ---→ (m 1 , ν 1 ) . . . (m n 1 , ν n-1 )
dn,an ---→ (m n , ν n ) in N ∆ . We prove by induction on the length of ρ that every valuation ν i verifies ν i (t) = 0 for all t ∈ En(m i ), and that there exists a run ρ = (m 0 , ν 0 )

d 1 ,a 1 ---→ (m 1 , ν 1 ) . . . (m n 1 , ν n-1 )
dn,an ---→ (m n , ν n ) in N which only differs in the time elapsing, but which is such that the configurations reached after each discrete action are the same.

The base case (ρ has length 0) of the induction is trivial. Consider a new step (m n , ν n ) dn,an ---→ (m, ν) in N ∆ . By definition, there exists a transition t ∈ T which verifies the following conditions:

• t ∈ En(m n ),
• t is labeled by a n ,

• ∀t ∈ En(m n ), ν n (t ) + d n ≤ β(t ) + ∆, • ν n (t) + d n ≥ α(t) -∆ By induction property, we have ν n (t ) = 0 for all t ∈ En(m n ). As a consequence, we can deduce that α(t) -∆ ≤ d n ≤ min{β(t ) | t ∈ En(m n )} + ∆.
As transitions have rational bounds, one can choose a small rational value for ∆ such that α(t)

-∆ ≤ d n ≤ min{β(t ) | t ∈ En(m n )} + ∆ implies the inequality α(t) ≤ min{β(t ) | t ∈ En(m n )}.
For instance letting γ = min{β(t ) -α(t) | α(t) < β(t )}, any value of ∆ < γ 2 guarantees this implication. If all intervals attached to transitions of the net have integral bounds, taking ∆ < 1 2 suffices. We thus pick d n = α(t), which ensures:

• ∀t ∈ En(m n ), ν n (t ) + d n = α(t) ≤ β(t ), • ν n (t) + d n ≥ α(t)
As a consequence, we have (m n , ν n ) d n ,an ---→ (m, ν ) in N . Thanks to the property of being sequential, we can observe that every transition that is enabled in the new marking m is newly enabled by the firing of the discrete transition t. In particular, this implies ν (t ) = 0 for every transition t ∈ En(m), and in particular ν = ν. The expected properties on Reach(N ∆ ) and L(N ∆ ) then directly follow.

Undecidability results

We use the TPN N 1 of Figure 2 to prove undecidability of all the robustness problems considered for bounded TPNs.

Theorem 4.1. The problems of (i) robust boundedness, (ii) robust untimed language preservation, (iii) robust safety and (iv) subset-markings robustness are undecidable for bounded TPNs.

Proof:

To prove undecidability, we combine the standard construction of a TPN from a Minsky machine with the example TPN N 1 from Figure 2 and Lemma 3.5 on sequential TPNs.

For the sake of completeness, we start by briefly recalling the Minsky machine reduction. A Minsky machine M (which w.l.o.g. we assume deterministic) is defined by a finite set of states q i with 0 ≤ i ≤ n, where q 0 is the initial state and q n the final one. There are no transition rules from q n . The machine contains two counters c 1 and c 2 and transition rules corresponding either to incrementations (q i c k ++ ---→ q j ) or to decrementations with test to zero (q i c k -----→ q j if c k > 0, and q i → q l otherwise). As the machine is deterministic, it has a single execution. It is well known that the reachability of state q n is undecidable, so boundedness of c 1 and c 2 along the unique execution of M is also undecidable. The machine M is encoded into a TPN N M as follows: we consider a set of places P = {q i } ∪ {c 1 , c 2 }. Initial marking is {q 0 }. Transitions are represented on Figure 3. In the TPN of Figure 3(b), firing intervals are used to enforce priorities between transitions: if decrementation is possible (meaning that places q i and c k are non-empty, which enables transition t >0 ) then it must occur between 0 and 1 time units. Note that in this situation, transition t =0 is also enabled, as place q i is filled. However, as the firing interval of t =0 is [START_REF] Alur | A Theory of Timed Automata[END_REF][START_REF] Bérard | Comparison of Different Semantics for Time Petri Nets[END_REF], transition t >0 fires first, that is decrementation is prioritary when places q i and c k are non-empty. We make two observations. First, as N M simulates exactly executions of M, N M is bounded iff M is, and N M covers marking m = {q n } iff M reaches state q n . Second, in every reachable configuration, exactly one of the places {q i , 0 ≤ i ≤ n} contains a token. As a consequence, the net N M is sequential.

q i q j t ++ c k (a) Incrementation q i q j q l t =0 , [2, 3] t >0 , [0, 1] c k (b) Decrementation
We then combine the TPNs N 1 from Figure 2 and N M as depicted on Figure 4 to obtain the TPN N 2 . More precisely, N 2 is a sequential composition of N 1 and N M , defined as the disjoint union of nets N 1 and N M plus a new place f , and two new transitions t s and t f . Place red of N 1 is connected to place q 0 of N M through a transition t s . Place q n of N M is connected to place f through transition t f . First note that N 2 is a bounded TPN: without perturbation, transition t (in N 1 ) is never fired, and thus the set of reachable markings is finite. Second, we label transition t f by a and every other transition by ε2 . As N M is sequential, by Lemma 3.5(iii) it follows that

• (1) N 2 is robustly bounded iff N M is bounded, and • (2) N 2 robustly preserves its untimed language iff N M does not cover marking m.

We note that for (2), N M may not be bounded (if M is not bounded), however the statement still holds since Lemma 3.5(iii) does not require the boundedness assumption. Now, from the undecidability of halting and boundedness of Minsky machines, it follows that the problems we considered are also undecidable. We remark that the above proof also shows that robust safety is undecidable, as N 2 covers marking {f } iff N M covers marking m. Finally, the net N 2 defined in Figure 4 also shows that subset markings robustness problem is undecidable for bounded TPNs. To see this consider the following problem instance: is the set of markings of N 2 of place f (i.e., X = {f }) equivalent under some positive enlargement by some ∆? We know that f is reachable if and only if the Minsky machine modeled by N M terminates its computation. Hence the subset marking robustness problem is undecidable.

q 0 q n f N 1 red t s t f N M
Before we proceed, let us consider a special case of the SMR problem, where we fix X = P , that is, choose the subset to be the set of all places. Then the subset marking problem is reduced to the question of whether the set of reachable markings of the considered net is robust under enlargement, that is if Reach(N ) = Reach(N ∆ ). We call this the robustness of reachable markings problem. In Section 6, we will prove that this problem, unlike the many problems considered so far, is decidable for all bounded TPNs. However, for unbounded nets, even this problem is undecidable as we now demonstrate. Proposition 4.2. The robustness of reachable markings problem is undecidable for unbounded TPNs.

Proof:

Again, we will show that there exists a reduction from Minsky machines halting problem. Consider the net N M encoding a deterministic Minsky machine as in Figure 3, and consider the place q n of N M . It is undecidable whether q n can be marked, and the Minsky machine encoding is an unbounded, sequential and robust net. Now connect to q n a pair of transitions t, t and two places p, p , such that • t = q n , • t = q n , t • = p, t • = p . Let us define I(t) = [1, 2] and I(t ) = [START_REF] Alur | A Theory of Timed Automata[END_REF][START_REF] Bérard | Comparison of Different Semantics for Time Petri Nets[END_REF]. Intuitively, we connect the net N 0 of Figure 1 to the final place q n of N M . Recalling that N M is deterministic and sequential, we have that only markings of places p, p can vary under enlargement. As N 0 does not have a robust set of markings, it is clear that the obtained net preserves its set of markings under enlargement if and only if q n is unreachable. So, the robustness of Reach(N ) is undecidable in general for unbounded TPNs.

A robust translation from TPN to TA

As robustness issues were first studied for timed automata, and several translations of TPN into TA exist in literature, it is natural to study which of these translations are compatible with robustness. A way to reduce robustness problems for TPNs to robustness problems for TA is to show that an existing timed bisimulation between TPN and its TA translation is preserved under perturbation. We now present a translation which verifies this property.

This construction is close to the marking class timed automaton construction of [START_REF] D'aprile | From Time Petri Nets to Timed Automata:An Untimed Approach[END_REF] but different in two aspects. First, in the TA built in [START_REF] D'aprile | From Time Petri Nets to Timed Automata:An Untimed Approach[END_REF], for efficiency reasons the number of clocks is reduced by using clock sharing techniques of [START_REF] Lime | Model Checking of Time Petri Nets Using the State Class Timed Automaton[END_REF], which may increase the number of locations. For ease of presentation, we do not consider this optimization, but our results also apply for this setting. Second, the construction of [START_REF] D'aprile | From Time Petri Nets to Timed Automata:An Untimed Approach[END_REF] was only stated for TPN whose underlying Petri net (i.e., the Petri net obtained by ignoring the timing information in the given TPN) is bounded. We present the construction in a more general framework: we consider a TPN N which is not necessarily bounded and we consider as input a finite set of markings M . The construction is then restricted to the set M , and we can prove that it is correct for the set of behaviors of N which always remain within M . In the sequel, we will instantiate M depending on the context. For TPNs whose underlying PN is bounded, the construction of [START_REF] D'aprile | From Time Petri Nets to Timed Automata:An Untimed Approach[END_REF] is recovered by letting M be the set of reachable markings of this PN. We begin with a definition and a proposition that can be infered immediately: Definition 5.1. Let N = (P, T, Σ ε , • (.), (.) • , m 0 , Λ, I) be a TPN, M ⊆ N P be a set of markings such that m 0 ∈ M , and let N = (Q, q 0 , →) be the semantics of N . The M -bounded semantics of N , denoted N |M , is defined as the restriction of the TTS N to the set of states

{(m, ν) ∈ Q | m ∈ M }.
Proposition 5.2. Let M be a set of markings of a TPN N containing the initial marking. If Reach(N ) ⊆ M , then N |M = N . Now, let N = (P, T, Σ ε , • (.), (.) • , m 0 , Λ, I) be a TPN, and M ⊆ N P be a finite set of markings such that m 0 ∈ M . The marking timed automaton of N over M , denoted A M , is defined as

A M = (M, m 0 , X, Σ ε , E, Inv), where X = {x t | t ∈ T }, for each m ∈ M , Inv(m) = t∈En(m) x t ≤ β(t),
and there is an edge m g,a,R ---→ m ∈ E iff there exists t ∈ T such that t ∈ En(m), m = m -• t + t • , g is defined as the constraint x t ∈ I(t), a = Λ(t) and R = {x t |↑enabled(t , m, t)}. With this we have the following theorem: Theorem 5.3. Let N be a TPN, M be a finite set of markings containing the initial marking of N , and A M be the marking timed automaton of N over M . Then for all ∆ ∈ Q ≥0 , we have N ∆ |M ≈ (A M ) ∆ .

Proof:

We prove by induction that the following relation R is a timed bisimulation. Let (m, ν) denote a state of the TTS N ∆ |M , i.e. (m, ν) ∈ Adm(N ∆ ) with m ∈ M . Similarly, let ( , v) denote a state of (A M ) ∆ . We define (m, ν)R( , v) if and only if m = , and ∀t ∈ En(m), ν(t) = v(x t ). First, initial configurations are in R. We then have to consider how pairs (m, ν), ( , v) ∈ R evolve with respect to different kinds of moves:

delay moves: Let d ∈ R ≥0 . We have (m, ν) d -→ (m, ν + d) iff ∀t ∈ En(m), ν(t) + d ≤ β(t) + ∆. As ∀t ∈ En(m), v(x t ) = ν(t), this is equivalent to ∀t ∈ En(m), v(t) + d ≤ β(t) + ∆, which itself is equivalent to v |= Inv( ) + ∆,
1. t ∈ En(m) 2. m = m -• t + t • 3. ν(t) ∈ I ∆ (t)
where I ∆ (t) denotes the ∆-enlargement of interval I(t) 4. Λ(t) = a 5. for any t ∈ En(m ), we have ν (t ) = 0 if ↑ enabled(t , m, t) = true, and ν (t ) = ν(t) otherwise.

Conditions 1-5 imply the existence of a transition m g,a,R ---→ m in A M , where g is defined as the constraint x t ∈ I(t), and R as the set of clocks of newly enabled transitions. As t ∈ En(m), we have ν(t) = v(t), and thus the transition can be fired in (A M ) ∆ , and we have

( , v) a -→ (m , v ) where v = v[R].
One can then check that for any transition t ∈ En(m ), we have v (t ) = ν (t ). There are two cases, if t is newly enabled, then the clock value is 0 both in the TA and in the TPN. Otherwise, t is not newly enabled, and we have

v (t ) = v(t ) = ν(t ) = ν (t ).
Conversely, considering a discrete move in (A M ) ∆ , one can similarly prove the existence of a corresponding move in N ∆ |M .

Other TA constructions. The construction proposed in [START_REF] Lime | Model Checking of Time Petri Nets Using the State Class Timed Automaton[END_REF] builds a state class timed automaton incrementally using a forward exploration of reachable markings of a bounded TPN. Gardey et al [START_REF] Gardey | A Zone-Based Method for Computing the State Space of a Time Petri Net[END_REF] use a similar forward-reachability technique to build the reachable state space of TPN, where equivalence classes for clock valuations are encoded as zones. However, as in TPN N 1 of Figure 1, new configurations in an enlarged semantics might be reached after accumulation of small delays. Hence, new reachable markings are not necessarily obtained in one enlarged step from a configuration in the non-enlarged semantics. Thus, forward techniques as in [START_REF] Lime | Model Checking of Time Petri Nets Using the State Class Timed Automaton[END_REF][START_REF] Gardey | A Zone-Based Method for Computing the State Space of a Time Petri Net[END_REF] cannot be directly extended to obtain enlarged semantics and we need a more syntactic translation which builds an over-approximation of the reachable markings (of the TPN) as in Theorem 5.3.

Cassez et al [START_REF] Cassez | Structural translation from Time Petri Nets to Timed Automata[END_REF] propose a different syntactic translation from unbounded TPNs by building a timed automaton for each transition, and then synchronizing them using a supervisor. The resulting timed automaton is bisimilar to the original model, but states contain variables, and hence the automaton may have an unbounded number of locations. It may be possible to extend this approach to address robustness problems, but as we focus on bounded TPNs, we leave this for future work.

Robustly bounded TPNs

This section focuses on the class of robustly bounded TPNs. By Theorem 4.1, we know that checking membership in this class is undecidable. We present two decidable subclasses, as well as a semi-decision procedure for the whole class. We first consider the subclass of TPNs whose underlying Petri net is bounded: Proposition 6.1. The set of TPNs whose underlying net is bounded is a decidable subclass of robustly bounded TPNs. Further, for each net N of this class, one can construct a finite timed automaton A such that N ∆ ≈ A ∆ for all ∆ ≥ 0.

The decidability follows from that of boundedness for (untimed) Petri nets [START_REF] Karp | Parallel program chemata[END_REF]. The second part of the above proposition follows from Theorem 5.3.

Proof:

Observe that a TPN N is robustly bounded iff there exists a finite set of markings M and some ∆ > 0 such that Reach(N ∆ ) ⊆ M . Thus by naively enumerating the set of finite sets of markings and applying the algorithm of Lemma 6.2 at each step of the enumeration, we obtain a semi-decision procedure (to check membership) for the class of robustly bounded TPNs. For the second result, observe that if N is known to be robustly bounded, then this semi-decision procedure terminates and computes a finite set of markings M and there is a value ∆ 0 such that Reach(N ∆ 0 ) ⊆ M . Therefore, for any ∆ ≤ ∆ 0 , Reach(N ∆ ) ⊆ M . By Proposition 5.2, this entails N ∆ |M = N ∆ . In addition, by Theorem 5.3, we have N ∆ |M ≈ (A M ) ∆ where A M is the marking timed automaton of the TPN N . Thus we have

∀0 ≤ ∆ ≤ ∆ 0 , N ∆ ≈ (A M ) ∆ .
This result allows us to transfer existing robustness results for timed automata to TPNs. We will illustrate the use of this property in the following section.

Untimed language robustness in TPNs

We now consider the robust untimed language preservation problem, which was shown undecidable in general in Theorem 4.1. We show that for the subclass of distinctly labeled bounded TPNs (i.e., labels on transitions are all distinct, and different from ε) this problem becomes decidable. We first compare the class RR (for which checking membership is decidable by Theorem 6.4) with the class LR (where, as already noted, checking membership is undecidable by Theorem 4.1). We can then observe that:

• p 1 • p 2 a, [2, 3] a ′ , [1, 2] t 1 , [0, 2] t 2 , [0, 1] b ′ , [1, 2] b, [2, 3] t 3 , [0, 2] t 4 , [0, 1] t 5 , d c, [1, ∞)

Proof:

We first prove one direction of (1), i.e., RR is not included in LR. Consider the TPN in Figure 5. The set of reachable markings is the same under perturbations so the net is in RR, but the language under perturbation sees the action c which is not seen in the unperturbed net, so this net is not in LR. For the converse direction, it suffices in the net N 1 of Figure 1, to label all transitions by and then it is in LR (since untimed language is empty) but not in RR since a new place is reachable. Now for the proof of (2) we have: if N ∈ LR = , then any word w ∈ L(N ) corresponds to a unique sequence of transitions, and hence leads to a unique marking of N . So if L(N ∆ ) = L(N ) for some ∆ > 0, then Reach(N ∆ ) = Reach(N ) for the same ∆. The strictness also follows easily. This inclusion is strict: one can easily design a net N in which a single transition t is fireable only under enlargement, but producing no new marking outside Reach(N ). Hence, such N is not in LR = , but is still in RR = .

Finally, we show that the problem of robust untimed language preservation becomes decidable under the assumption of distinct labeling: Theorem 7.3. The class LR = is decidable, i.e., checking if a distinctly labeled bounded TPN is in LR is decidable.

Proof:

We proceed as follows. We first decide by using Theorem 6.4, whether the given distinctly labeled bounded net N is in RR (and therefore in RR = ). Now, by Proposition 7.2 if the net is not in RR = , then it is not in LR = . Otherwise, by Lemma 6.5, we can build a timed automaton A which is timed bisimilar to N for small perturbations. This entails that this TA preserves its untimed language under small perturbations iff N does. Thus we have reduced the problem of checking if N is in LR = to checking if the timed automaton A constructed from N is language-robust. This completes our proof since this problem is decidable for timed automata. More specifically we want to check that A is in LR, i.e., if there exists ∆ > 0 such that L(A) = L(A ∆ ). In [START_REF] Sankur | Untimed Language Preservation in Timed Systems[END_REF] this exact problem is solved for both finite and infinite words but with an additional restriction on the timed automata. Further, it also follows from Proposition 3.1 for general timed automata in the finite words case. That is, Claim 7.4. Checking if a timed automaton A is LR is decidable.

Proof:

In [START_REF] Bouyer | Robust Model-Checking of Timed Automata via Pumping in Channel Machines[END_REF], it is proved that checking robustness of timed automata with respect to any ω-regular property is decidable. In particular safety properties are decidable, as it is stated in Proposition 3.1. Given a finite timed automaton A, the (untimed) language of A, denoted by L(A), is a regular language. We can build a finite state automaton C accepting the complement of this language, equipped with final states. Let B be another timed automaton, and denote by B ⊗ C the product of B with C. It is easy to verify that B ⊗ C never enters a final state of C iff the (untimed) language of B is included in that of A. As for any non-negative ∆ we have L(A) ⊆ L(A ∆ ), we obtain that A ∆ ⊗ C does not enter the final states of C iff L(A) = L(A ∆ ). As C is untimed, the two timed automata A ∆ ⊗ C and (A ⊗ C) ∆ are equal. Our problem thus reduces to a robust safety problem for the automaton A ⊗ C. This completes the proof of the theorem as detailed above.

Robustness of Subsets of Markings

We now consider the problem of robustness of markings on a subset of places. Given a set of markings M over a set of places P , and a subset of places X ⊆ P , we denote by Π X (M ) the projection of M onto X. Recall that the subset-markings robustness (SMR) problem is formulated as: given a net N defined over a set of places P , and a subset of places X ⊆ P , is there a value ∆ > 0 such that Π X (Reach(N )) = Π X (Reach(N ∆ ))?

From Theorem 4.1, we know that the SMR problem is undecidable for bounded TPNs.

Let us now discuss a particularity of SMR problem with respect to other robustness problems described in the paper. It is well known that the marking equivalence and inclusion problems are undecidable for untimed Petri nets [START_REF] Hack | Decidability Questions for Petri Nets[END_REF]. We recall here the definitions of these problems: for a fixed set of places P and a pair of nets N 1 , N 2 defined over P given with their respective initial markings (i.e., N 1 , N 2 are nets with same set of places but with different sets of transitions), is the set of reachable markings of N 1 included in / equal to the set of reachable markings of N 2 ?

Consider the net of Figure 6, and the SMR problem for places X = {x, y, z}. One wants to decide whether there exists a value ∆ for which the set of markings projected on X is equivalent in N and in N ∆ . When place p 1 is filled, the semantics of the net uses transitions T 1 = {a, b} and if p 2 is filled, then only transitions T 2 = {c, d} are fireable. Similarly, if p 1 is marked, the initial marking in the set of places X is {y}, while it is equal to {x} if p 2 is marked. We know that under any enlargement, place p 2 can be marked, but it can not be marked if the net is not enlarged by some positive ∆. Note that transitions in T 1 , T 2 have [0, ∞) time constraint, and can hence be considered as transitions of an untimed net. Hence, the SMR problem on X resumes to checking marking equivalence of the restriction of this net to places in X and transitions T 1 ∪ T 2 and of a restiction of the net to X with transitions in T 1 . That is, markings of N are robust on X if and only if the markings of N 2 = (X, T 2 , {x}) are included in those of N 1 = (X, T 1 , {y}).

This example can be extended, and hence the SMR problem can be used to encode marking inclusion problems for arbitrary sets of places and transitions. One can remark that the net of Figure 6 can be separated into a constrained part, and an unconstrained part (i.e. with [0, ∞) constraints), but that the fact that the subset of places chosen for the SMR problem concerns unconstrained transitions does not change the undecidability result. Hence this undecidability is not only due to timed properties of the net, but also to undecidable results of inclusion of markings for untimed Petri nets [START_REF] Hack | Decidability Questions for Petri Nets[END_REF]. Now, the question is whether the SMR problem is decidable for some subclasses of bounded TPNs.

Proposition 8.1. The subset markings robustness problem:

• always has a positive answer (i.e., is always true) for RR and sequential nets.

• is decidable for Robustly bounded nets.

Proof:

Obviously, for nets in the reach-robust class, the SMR problem is always satisfied, as Reach(N ) = Reach(N ∆ ) for some ∆ > 0. Hence for any set X ⊆ P , and for the same ∆, we have Π X (Reach(N )) = Π X (Reach(N ∆ )). This property also holds for sequential nets, which are a subclass of RR nets. Next, when a net is robustly bounded, then by lemma 6.5, one can compute a timed automaton A such that there exists ∆ 0 > 0 for which, ∀0 ≤ ∆ ≤ ∆ 0 , N ∆ ≈ A ∆ . The construction of this automaton comes with a finite set of markings M such that Reach(N ∆ ) ⊆ M for any 0 ≤ ∆ ≤ ∆ 0 .

• p 0 p 1 p 2 x y z [0, 1) [1, 2] a, [0, ∞) b, [0, ∞) c, [0, ∞) d, [0, ∞)
Let us denote by Bad the set of markings that are not equivalent on X to some reachable marking of

N , that is Bad = {m ∈ M | m ∈ Reach(N ), Π X (m ) = Π X (m)}.
The SMR problem has a positive answer for N and X if and only if there exists a positive enlargement ∆ ≤ ∆ 0 of A for which the set of markings Bad is not reachable.This safety property can be checked using the results of [START_REF] Bouyer | Robust Model-Checking of Timed Automata via Pumping in Channel Machines[END_REF].

Case Study : regulation of a metro railway system

We propose a case study demonstrating the importance of verifying robustness issues in Petri net models. Petri nets and their colored, timed and stochastic variants have attracted a lot of attention within the context of railway systems. One reason is that the topology of Petri nets mimics that of train networks. One can cite [START_REF] Giua | Modeling and Supervisory Control of Railway Networks Using Petri Nets[END_REF][START_REF] Janczura | Modelling and Analysis of Railway Network Control Logic using Coloured Petri Nets[END_REF] for generic models of trains systems, and the following case studies: [START_REF] Burkolter | Capacity of Railways in Station Areas using Petri Nets[END_REF] considers realizability of time tables for the Bern Metro modeled as a Petri net, [START_REF] Bjork | Challenges in simulating railway systems using Petri Nets[END_REF] proposes a Petri net model that is isomorphic to the real Oslo subway, and [START_REF] Zimmermann | A Train Control System Case Study in Model-Based Real Time System Desig[END_REF] defines a Petri net model for the European Train Control System. Though the literature on Petri net models for train systems is not limited to these references, as far as we could find, none of these or other references directly address timed robustness issues. The case study proposed in this section defines a time Petri net model of a pair of metro lines. From this example, natural security and scheduling questions that can be addressed as robustness questions arise. We show that robustness issues can be used to help evaluating robustness of time tables to imprecision, and can help in the regulation of train systems.

Let us consider a simple but illustrative model of regulation of a metro line. In the rest of this section, we will use it to demonstrate several problematic but yet frequently met features of metro lines. Regulation on a metro line consists of ensuring that train departures and arrivals follow (or at least are close to) a strict pre-planned schedule. Any delay in train arrivals forces re-evaluation of the entire schedule. This task is more involved than it seems at first sight and cannot always be ensured by just increasing/decreasing trains speed. For instance, some track portions may be shared among distinct lines and the regulation needs to ensure that shared tracks are occupied by a single train at any instant.

We consider a specific case of a bidirectional metro train network with two lines establishing connections between pairs of distant sites A, B (through intermediate stations S1, S2, S3) and C, D (through 8(b) (we will denote this net by N in the rest of this section). A token in the place P x,AB represents that a train on the way from A to B is at station x (similarly for P x,BA and C, D). Each transition is attached a time interval [120,120] to depict that the time spent on each portion of the line between two consecutive stations is exactly 2 minutes. One can notice that the net of Figure 8(b) associates one subnet to each line, and that these subnets are two simple independent rings following the lines topologies. One can also notice that the Petri net underlying the TPN N is robustly bounded. We denote by M its finite set of reachable markings. Now, to avoid collisions at station S3, places P S3,AB and P S3,CD as well as place P S3,BA and P S3,DC should be mutually exclusive, i.e., we need to check that the set of markings M bad = {m ∈ M | m(P S3,AB ) + m(P S3,CD ) > 1} ∪ {m ∈ M | m(P S3,BA ) + m(P S3,DC ) > 1} is not reachable. This is indeed the case in the absence of imprecisions: one can easily notice that the occupation dates for station S3 by train from the AB and CD are disjoint in both directions. Furthermore, we can check that N = N |M \M bad .

Let us now consider imprecise timings modeled as guard enlargements. Under the enlarged semantics, the safety of the line may depend on the precision of schedules, that is one should check that there exists ∆ > 0 such that Reach(N ∆ ) ⊆ M \ M bad . According to the results of Lemma 6.2, this can be effectively checked on our network model, since M \ M bad is a finite set of markings. Obviously, any imprecision in timing may result in a collision of trains at station S3, as occurrences of the smallest delay ∆ accumulate at each round of trains. Indeed, for any small value ∆, of can find some n such that 18.(n + ∆) + 2 ≤ 18.(n -∆) + 16 ≤ 18.(n + ∆) + 4, i.e. a number of cycles after which trains from lines AB and CD moving in the A to B and C to D directions may both require access to station S3. Similar inequations can be written for the reverse directions. This safety verification is rather straightforward for our example, as the equations defining occupancy times of station S3 are known. For more complex topologies with mutual exclusion mechanisms, it is not clear that the problem can be solved as satisfiability of some inequations. However, the safety question can still be addressed as a robust safety problem, requiring that Reach(N ∆ ) does not cover markings in M bad .

Of course, real train networks do not rely on precise timings to guarantee safety of passengers, and mutual exclusion mechanisms are implemented to prevent trains from leaving their station when another train is about to enter the same track. Figure 9(a) shows how a critical section forcing trains to wait before entering a track can be implemented with additional places and transitions. In the precise time setting, a token is always available in the places implementing the critical section whenever needed. However, as soon as small delays modify the behavior of the system, critical sections come into play, forcing trains to wait and completely changing the planned schedule. Let us now try to measure the effects of imprecise timing on the overall behavior of this network. Suppose we have a requirement stating that the time interval between two consecutive trains leaving station A should be at most 20 minutes. Checking that such a requirement is achievable can be done by adding a transition and a pair of places as depicted in Figure 9(b): if a train fails to get back to station A within 20 minutes, transition trec can be fired. Now, with precise timing, it is obvious that this transition trec cannot be fired: the schedule of trains is deterministic, and ensures a departure from station A once every 18 minutes. On our model, this corresponds to firing a transition that resets the clock attached to transition trec. However, in an imprecise setting, if the intervals attached to each transition are enlarged by some amount ∆, the train schedules can drift, worsened by mutual exclusion that forces trains to wait. Thus, we would like to check if trec is fireable when guards (on all transitions) are enlarged by some 0 < ∆ < 1, meaning that the upper bound of 20 minutes between departures from station A is not always met. Let us denote by N the net obtained from N by adding the places and transitions for mutual exclusion as well as a transition trec and a place ReqViolated , as depicted on Figure 9. To check the above property, we first check if place ReqViolated can be marked in the enlargement of N by 1. This enlarged net is a bounded time Petri net, and this property can be checked by a construction of its state class graph. If the answer is no, then for any smaller enlargement ∆ ≤ 1, the place cannot be marked (by Lemma 3.2 since N ∆ N 1 ) and hence the 20 minutes upper bound between two trains is respected for any 0 ≤ ∆ ≤ 1. If the answer is yes, then timing of trains cannot drift by 1 second without violating the requirement of one train at most every 20 minute at station A. A question that immediately arises is whether there exists a better precision that can guarantee this upper bound on train departures from station A, that is whether there exists ∆ smaller than 1 such that trec is never fireable, or equivalently such that place ReqViolated is never marked in N ∆ . The net N is robustly bounded, as transitions do not create new tokens. There are several ways to check validity of the 20 mn upper bound requirement at station A with imprecise timing. The first solution is to reduce the question to a robust safety question. Letting m f ail be the marking such that m f ail (ReqV iolated) = 1 and m f ail (p) = 0 for all other places p, satisfying the requirement under enlargement is equivalent to robust safety of N w.r.t. m f ail . Now, if we first check that m f ail is not coverable under perfect semantics, the question can also be addressed as a subset-marking robustness problem, in which the considered subset of places is {ReqV iolated}. Similarly, the upper bound contraint is violated iff transition trec can be fired. If trec does not appear in any sequence of transitions firings of N (which can effectively be checked by construction of the state class graph of N ), then one can attach an label to all transitions in T \ {trec} and any label a to trec. The violation of the upper bound requirement can then be checked as a robust untimed language preservation problem. If we use a translation to timed automata, then the algorithms of [START_REF] Bouyer | Robust Model-Checking of Timed Automata via Pumping in Channel Machines[END_REF] can solve the robustness questions, and allow to compute a value δ 0 such that robustness holds for any value ∆ ≤ δ 0 .

Other interesting robustness properties can be checked for railway systems modeled as time Petri nets. Usually, metro lines work with more than one train. And of course, the resulting network should remain (robustly) 1-bounded on places modeling tracks, i.e., avoid collisions. Injection of several trains can follow a predetermined schedule, defined as a new part of the TPN. of two trains in the network at station A with an interval of 5 min. With a precise time semantics, the resulting network is 1-bounded on places X AB = {P x,AB , P x,BA | x ∈ {A, S1, S2, S3, B}} and X CD = {P y,CD , P y,DC | y ∈ {C, S3, T 1, T 2, D}}, and overall 2-bounded. Now, we may ask whether these bounds are preserved for enlarged semantics. Obviously, on our example, if trains can travel for an unbounded time in a network, a train can always catch up the preceding one even when imprecision is small. Obviously, places in X CD are still 1-bounded after introduction of several trains on line AB, and problems can only arise on places of line AB. Absence of collisions on line AB can be verified as a subset-markings robustness problem for the set of places X = X AB . Equivalently, one can check absence of collisions on line AB as a robust safety problem (one should not cover a marking in which some place in X AB contains 2 tokens).

Note also that metro lines are operated for a bounded duration within one day. Hence, the usual sensible questions are whether the system remains robust during a period that can not exceed one day. When Zeno behaviors are forbidden, this means that one can compute an upper bound on the maximal number K of train departures that can occur within one day, and solve robustness problems under finite horizon, using the techniques of section 3.2, and in particular the construction of lemma 3.4. In particular, an important property to check is that the set of markings remains unchanged on places of X AB . Another possibility is to model explicitly termination of lines operation, and specify the extraction of trains at the end of the day, that is after a fixed delay d. This way, the net deadlocks after some time (no discrete transition can be fired), but there is no need to compute explicitly a bound on the number of train departures. Figure 10(b) shows how to remove trains (tokens) from the network as soon as they arrive at station A at the end of the day. The end of the day is modeled as a transition endday, whose firing allows for the removal of a token by transition rmv as soon as it enters place P A . Clearly, there are small values for enlargement for which this network can still work with bounded place contents for places in X AB . As the network is 2-bounded, one can then compute an equivalent automaton over the set of bounded markings, define a set of bad markings as the set of markings in which a place in X AB contains more than 1 token, and then solve this boundedness problem as a robust safety problem. Now, an interesting question is to find the largest value for ∆ guaranteeing 1-boundedness of places in X AB within one day. These questions can be addressed building a finite symbolic unfolding of the net as in [START_REF] Chatain | Complete Finite Prefixes of Symbolic Unfoldings of Safe Time Petri Nets, Petri Nets and Other Models of Concurrency -ICATPN[END_REF], and the deriving a system of inequations in which firing dates of transitions and ∆ are variables, and trying to maximize ∆ within this system.

The questions addressed in this case study show that safety, language and subset marking robustness questions have a practical interest. For simple cases such as the mutual exclusion on station S3 for the net of Figure 8(b), the question can be rapidly answered by writing the equations for departure and arrival dates of trains. However questions becomes more complex as soon as mutual exclusion mechanisms introduce combinatorics in the model. So far, all robustness questions for this case study are only settled, and the first question is answered on paper. We plan to develop tools to solve robustness problems for TPNs, as it is unlikely that robustness issues with similar or greater complexity can be addressed without the help of a program. In this paper, we have launched an investigation into robustness in time Petri nets with respect to guard enlargements. We transferred several positive results from the TA setting to TPNs and showed that some other problems become undecidable in TPNs due to unboundedness. We summarize our results in the diagram in Figure 11 which shows the relative expressiveness of the various classes and their decidability. In the table below, we give a more detailed picture of the decidability results for each problem and each class of TPNs considered. The leftmost column lists the problems addressed while the top row lists the subclasses of nets. A "yes" entry in a cell means that the problem considered at that row is decidable for the class considered in the column, "no" means that it is undecidable, and "g" means that a positive answer to the problem is always guaranteed for the considered class. For instance, robustness of subset-markings is guaranteed for Reach-robust nets.

Conclusion

The undecidability results stem from Theorem 4.1 and Proposition 4.2, that is from the capacity for unbounded TPNs to encode Minsky machines. Robustness of a subset of markings for unbounded nets can also encode reachability problems for Minsky machines, but in addition can encode undecidable marking equivalence problems for untimed Petri nets [START_REF] Hack | Decidability Questions for Petri Nets[END_REF]. Decidability results on robust language preservation with distinct labels follow from Theorem 7.3, which says that one can decide whether a bounded net belongs to LR = , i.e. preserves its language under some enlargement.

Figure 2 .

 2 Figure 2. The TPN N 1 exhibiting new discrete behaviors under infinitesimal perturbations.

Figure 3 .

 3 Figure 3. Encoding instruction of a Minsky machine M into a TPN N M .

Figure 4 .

 4 Figure 4. TPN N 2 obtained by combining N 1 and N M .

  which is the invariant of location in (A M ) ∆ . This is the condition under which there exists a delay move ( , v) d -→ ( , v + d) in (A M ) ∆ . Thus the result holds for delay moves. discrete moves: Consider a discrete move (m, ν) a -→ (m , ν ) in N ∆ |M . Such a discrete move exists iff m, m ∈ M , and there exists a transition t ∈ T such that:

Definition 7 . 1 .

 71 A bounded TPN N is called Language-Robust if L(N ∆ ) = L(N ) for some ∆ > 0. We denote by LR the class of Language-Robust nets and by LR = (resp. RR = ) the subclass of LR (resp. RR) with distinct labeling.

Figure 5 .

 5 Figure 5. A TPN which is in RR but not LR

Figure 6 .

 6 Figure 6. Marking equivalence for a subset of places

Figure 7 .

 7 Figure 7. A two-bidirectional lines train network

Figure 8 (

 8 a) represents occupation times for each track portion of the network. Occupation of track portions around stations by the train on AB line is represented by solid black segments, and occupation by train on CD line by dashed segments. One can notice that under a precise timing, the trains on AB and CD pass S3 at disjoint intervals: every 18 minutes, the occupation of lines repeats. Hence, S3 is occupied by train CD between dates 18.k +2 and 18.k +4 min in the C to D direction, and then between Occupation of stations with perfect time measurement

Figure 9 .

 9 Figure 9. A more precise model with mutual exclusion

Figure 10 .

 10 Figure 10. A model with many trains

Figure 11 .

 11 Figure 11. RR stands for reach-robust, LR for language-robust, UB for bounded underlying PNs, S for sequential bounded TPNs. Dotted lines represent that checking membership in the class is undecidable, while solid lines represent that it is decidable.

  Behavior and model for precise timing dates 18.k + 14 and 18.k + 16 minutes in the reverse direction, for any k ∈ N. Similarly, S3 is occupied by train AB between dates 18.k + 6 and 18.k + 8 minutes in the A to B direction, and between 18.k + 10 and 18.k +12 minutes in the reverse direction for any k ∈ N. We can model this network as a simple time Petri net as illustrated in Figure

	P S1,AB	P S2,AB	P S3,AB
	P A		P B
	•
	P S1,BA	P S2,BA	P S3,BA
	P S3,CD	P T 1,CD	P T 2,CD
	P C		P D
	•
	P S3,DC	P T 1,DC	P T 2,DC
	(b) A Petri net model
	Figure 8.

Alternative semantics exist, called atomic and persistent atomic (see[START_REF] Bérard | Comparison of Different Semantics for Time Petri Nets[END_REF] for a comparison). They only differ in the definition of the predicate ↑enabled(t , m, t). One can prove that the undecidability results as well as the decidability results presented in this work also hold for TPN equipped with these alternative semantics.

The reduction can be adapted to avoid the use of ε by labeling every other transition by b, and adding a gadget which can perform arbitrarily many b's. It can however not be adapted to the setting of injective labeling, see Section 7.

We now exhibit another subclass of robustly bounded TPNs whose underlying Petri nets can be unbounded. In fact, this class is incomparable with the above defined subclass. The following technical result is central in our approach: Lemma 6.2. Let N be a TPN, and M be a finite set of markings. Determining whether there exists ∆ > 0 such that Reach(N ∆ ) ⊆ M is decidable.

Proof:

Call M = M ∪ {m | ∃m ∈ M, t ∈ T, m = m -• t + t • } the (finite) set of markings reachable from M in at most one-step in the underlying Petri net. Let A M be the marking timed automaton of N over M , and let ∆ ≥ 0. We claim:

To prove this equivalence, we consider successively the two implications. For the direct implication, suppose that Reach(N ∆ ) ⊆ M . By Proposition 5.2 and Theorem 5.3, we obtain N ∆ ≈ (A M ) ∆ . This yields the result as there is a bijection between transitions of N ∆ and those of (A M ) ∆ . Conversely, suppose that Reach((A M ) ∆ ) ⊆ M . By contradiction, suppose that Reach(N ∆ ) ⊆ M . Thus, there exists a run ρ = (m 0 , ν 0 )

we assume that m i ∈ M for any i < n. This entails that m i ∈ M for all i. But then, as we have N ∆ | M ≈ (A M ) ∆ by Theorem 5.3, this entails that the "same" run ρ also exists in (A M ) ∆ . This is a contradiction with Reach((A M ) ∆ ) ⊆ M . Now, determining whether there exists ∆ > 0 such that the right hand side of the previous equivalence holds is decidable thanks to Proposition 3.1.

We consider the following subclass of bounded TPNs:

We denote by RR the class of Reach-Robust TPNs.

RR is the class of bounded TPNs whose set of reachable markings is invariant under some guard enlargement. It is easy to see that these nets are robustly bounded. Recalling the result of Lemma 3.5-iii), we can immediately state that bounded sequential nets form a subclass of RR nets. More interestingly, checking membership in this class is decidable, i.e., given a bounded TPN N we can decide if there is a positive guard enlargement under which the set of reachable markings remains unchanged. This follows from Lemma 6.2, by instantiating the finite set of markings M with Reach(N ): Theorem 6.4. RR is a decidable subclass of robustly bounded TPNs.

We can now address properties of the general class of robustly bounded TPN. Lemma 6.5. The set of robustly bounded TPNs is recursively enumerable. Moreover, given a robustly bounded TPN N , we can build effectively a timed automaton A such that there exists ∆ 0 > 0 for which, ∀0 ≤ ∆ ≤ ∆ 0 , N ∆ ≈ A ∆ . For the case of bounded nets without distinct labels, the language preservation problem is undecidable: this is again a consequence of Theorem 4.1, which shows that LR = is an undecidable class of nets. Once we assume the net to be robustly bounded (or RR or UB which are subsets of robustly bounded TPNs), the "yes" results are proved using Lemma 6.5 and following the same lines as in the proof of Theorem 7.3. Indeed, if a net is robustly bounded, then by Lemma 6.5, one can build a finite automaton A such that there exists ∆ 0 > 0 for which, ∀0 ≤ ∆ ≤ ∆ 0 , N ∆ ≈ A ∆ . Obviously, the set of locations of this automaton is finite, that is it gives us a set of markings preserved by any enlargement smaller than ∆ 0 . One can hence compute the regular untimed language recognized by N and design an untimed automaton C that recognizes its complement. As in Theorem 7.3, language robustness then reduces to a decidable robust safety problem for A ⊗ C.

h h h h h h h h h h h h h h h h h

Problems

Robustness of subset-markings problem is decidable for all subclasses of robustly bounded nets, and guaranteed for Reach Robust and sequential nets, as shown by Proposition 8.1. Decidability of robustness of Reach(N ) for bounded and robustly bounded nets, comes from the fact that RR is a decidable subclass of nets (Theorem 6.4). Robustness of Reach(N ) is guaranteed by definition of RR and bounded sequential nets are a subclass of RR nets. For sequential nets, all robustness properties considered in the table are guaranteed, as demonstrated by Lemma 3.5.

As future work, we would like to show positive results in an unbounded setting. However, we believe that this would require a different approach and new techniques. Another challenge is to address new robustness problems that arise due to concurrency in TPNs. For instance, one may like to check that there is no change in concurrency under enlargement, that is the subset of transitions that can be fired simultaneously remain unchanged. Such issues call for the study of robustness directly on noninterleaved representations.


Pham Cong Cuong

Alexandre Durupt
email: alexandre.durupt@utc.fr

Nada Matta
email: nada.matta@utt.fr

Benoit Eynard

Guillaume Ducellier
email: guillaume.ducellier@utt.fr

Knowledge Sharing Using Product Life Cycle Management

Keywords: Knowledge sharing, PLM, Ontology

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Information Systems, used to share information, lead to the growth of heterogeneous data and then the dependencies between them. Thus, the links and dependencies among heterogeneous and distributed data are more and more complex during quotidian activities of users (engineers, etc.). The data exploitation (interrogation and sharing) has to be adapted to the context of large data and complex dependencies. To overcome this current inconvenience, more and more research works have investigated and studied the Semantic Web (SW) concepts and techniques, as well as their applications to improve the capabilities of PLM solutions in order to efficiently manage lifecycle data. Ontology is a key component of SW in which concepts and the relationships between concepts can be expressed in natural language and understandable by both of human and machine. Ontology is therefore used to enhance the knowledge sharing and the data integration in many actual information systems. Our contribution is to propose a methodology to facilitate the exploitation (interrogation and sharing) of data in an organization. Thus, the PLM domain is considered for industrial companies where the users are engineers. A global approach to construct an ontological model facilitating data exploitation is therefore illustrated from PLM context.

Knowledge sharing

Knowledge play an indispensable role in the long-tern sustainability and success of organization. The need for processes that facilitate the creation, sharing and leveraging of individual and collective knowledge has emerged recently for this reason.

Knowledge sharing (KS) has been introduced as one of the major activities of knowledge management and some definitions of knowledge sharing can be found in the literature [START_REF] Hendriks | Why share knowledge? The influence of ICT on the motivation for knowledge sharing[END_REF]. KS can be defined as activities of transferring or disseminating knowledge from one person, group or organization to another. The individuals initially create knowledge but it can be produced and held collectively. At the most basic level; knowledge sharing involves the process through which knowledge is transferred between a source and a recipient by using knowledge sharing techniques.

Information technology (IT) provides techniques to capture knowledge, categorize, search, extract content information and present it in more meaningful formats across multiple contexts of use. Some authors [START_REF] Sato | A knowledge sharing system using XML Linking Language and peer-to-peer technology[END_REF][START_REF] Zhang | Internet Knowledge-Sharing System Based on Object-Oriented[END_REF][START_REF] Yoo | Ontology-based economics knowledge sharing system[END_REF] have invested their efforts to construct platforms that enable knowledge sharing by using ITs. Sato et al. [START_REF] Sato | A knowledge sharing system using XML Linking Language and peer-to-peer technology[END_REF] used XML Linking Language (XLink) as a method of knowledge representation describing and proposed architecture for sharing that knowledge among users. He used the peer-to-peer technology to help users to better understand how to reuse existing knowledge on computer networks. Zhang et al. [START_REF] Zhang | Internet Knowledge-Sharing System Based on Object-Oriented[END_REF] tried to re-define knowledge resources in the network by object-oriented thinking and proposed three-layer knowledge sharing model. By using technologies on Web 2.0, a knowledge-sharing system is built on the Internet, allows the knowledge acquisition, sharing, extension and retrieving. Several knowledge-sharing systems use ontologies, which are defined as an explicit formal specification of a shared conceptualization [START_REF] Fensel | OIL: An ontology infrastructure for the semantic web[END_REF]. For instance, Yoo et al. [START_REF] Yoo | Ontology-based economics knowledge sharing system[END_REF] proposed a system based on ontology expressing economics knowledge and Semantic Web technologies. Fig. 1 presents the architecture of this system that consists of five layers: registration, ontology, data storage, reasoning and economic knowledge sharing. Users can register economics knowledge pertaining to a certain economics paper. They define then the metadata and the relationships between notions discussed in the paper. According ontology model, the system transforms this knowledge into semantic data in a machine-understandable format. Two functions: basic search and knowledge navigation were implemented.

Ontology-based economics knowledge sharing system architecture [START_REF] Yoo | Ontology-based economics knowledge sharing system[END_REF]. In this Fig. 1.

architecture, different levels are defined, related to the difference between data and knowledge. Ontology is enriched from data by generating semantic data related to ontology concepts. Reasoning engine is used when a data is searched. It allows to infer data using logic links between concepts.

OntoShare [START_REF] Davies | Using Ontologies for Knowledge Sharing[END_REF] is another ontology-based knowledge sharing system, in which, as users contribute information to the community, a knowledge resource annotated with metadata is created by using ontologies that have been defined using Resources Description Framework Schema (RDFS) and populated using RDF.

Before proposing our approach that uses ontology to share knowledge in PLM, let us describe main problem of sharing information in PLM.

The Product Lifecycle Management (PLM) systems integrate constantly all the information produced throughout all phases of a product's lifecycle to everyone in an organization at every level (managerial, technical…) [START_REF] Sudarsan | A product information modeling framework for product lifecycle management[END_REF].

Some key advantages of PLM systems can be noted [START_REF] Eynard | UML based specifications of PDM product structure and workflow[END_REF]:

• Establishing an effective PLM system reduces the enormous data resources to a coherent data flow, avoids redundancies and heterogeneities.

• PLM enables the collaboration through distributed and virtual/extended enterprises (workflow and process management, communication and notifications, secure data exchange...)

• PLM permits the product structure and its evolution management during different steps and track-performed modifications tracking.

• PLM is a mature solution to tackle the heterogeneity, growth and complexity of the data and its processing methods as well as some of the traceability and confidentiality issues. So, PLM system brings together: Products, service, activities, processes, people, skills, data, knowledge, procedures and standards…. It aims to provide the right information for the right people at the right time. It provides an efficient solution to handle the complex and heterogeneous data resources and a mature method to track the evolution and modification of these data.

However, along with these advantages, it also exists some issues:

• Lack of strong stakeholders, ICT tools as well as a common standard between PLM systems causes data integrity problems and limits the access to and sharing of product information and knowledge distributed,

• Another issue of PLM community is the increasing of need for product lifecycle knowledge capitalization and reuse in order to reduce time and cost.

• Database exploitation requires a good understanding of database structure as well as data model especially in the context where the data is heterogeneous and the links and dependencies among data are complex.

To answer these problems, we aim to use ontology to enhance knowledge sharing in PLM. The difficulties in data exploitation and technical information in PLM systems come from the low-level of data model representation, the increasing of the complexity of links and dependencies among heterogeneous data. To exploit data from database, it requires a deep understanding of data model and the dependencies between these data. Ontology promises an efficient solution to enable the sharing this understanding. The data model and the complex relationships could be also presented obviously, visually and easily to perceive by using ontology.

Our approach to share knowledge in PLM

The main problem in information management is to manage the evolution of data and links between information. Each user introduces his own view when he/she adds a new data. So, information search based on database becomes complex. Otherwise, knowledge engineering techniques as shown before provide techniques, which help from one side to respect the logic of a user and from another side to share knowledge.

We propose to use knowledge sharing techniques based on ontology and inference engine in order to help in data management in PLM (Fig. 2). In fact, ontologies must be defined to represent user views. Ontologies' low-level concepts have to be linked to data in database, or unless respect the variable name of these data. An inference engine can help to build a data request and generate links using the propagation of relations between concepts. We present in the following an example of this work for researcher working in bio-imaging (GIN) lab.

Architecture of Knowledge Sharing in PLM. Inference engine can be used when a user Fig. 2. ask for data from PLM. It follow ontologies in order to generate several links between data. The system can then transform these links in a data request which is used for database.

Building ontology in GIN Lab

To ensure a concrete view, we started our work by interviewing some scientists in a research institute where the complexity, variety, heterogeneity and growth of data resources have been handled by using PLM solutions. The goal of this interview is to identify the real needs of researchers, the difficulties in manipulating with information system during daily activities. In fact, most of scientists have difficulties in data querying and they almost cannot accomplish this task without helps of database technicians. For this reason, a visual, dynamic query interface that contains contents non-technician and user-proper, is required and acts an important role in system. Furthermore, as showed in the Fig. 3, the knowledge sharing process in bio-imaging GIN Laboratory initiates by data querying from PLM database through this query interface. Providing an efficient interface therefore becomes crucial and essential.

Knowledge sharing in Bio-Imaging GIN Lab. Fig. 3.

We define an ontology corresponding of the use logic of information in database.

Information belongs to three major categories: Tools, Data, and Process (Fig. 4).

Several relations exist between these concepts like Use, Follow and Provide (Fig. 5).

Conceptual tree of ontology. Three main concepts are used "Tools", "Data" and Fig. 4.

"Process". These concepts are manipulated in different ways: in acquisition, treatment, or results.

Conceptual graph of ontology. Data acquisition follows different protocol in order to Fig. 5.

acquire information from several sources. Acquisition results are then manipulated in treatments, respecting protocols in order to provide results.

Ontology Based Querying Interface

By using ontology tree and ontology graph, ontology-based graph query interface helps users to make a query more easily. By using the ontology tree and ontology graph, users can understand the relationships among concepts and directly choose query parameters. Users also can choose a query in query history to re-execute, modify or complete it. When a user completes his query, our system does as following 1.

Identifying nodes links, following relations in ontologies.

2.

Generating an output query in a format understandable and executable by Query Processor, XQuery Engine for example.

3.

Executing the output query on PLM data file (.xml or .json format).

4.

Results are then visualized as a graph and data in the Interface query.

Conclusion and perspective

In this paper, we presented a knowledge sharing solution using PLM, based on ontology and semantic web studies. A general approach for ontological model construction and an ontology-base query interface then is presented as a solution to tackle the difficulties in queyring PLM database. A use case in BioImaging domain has been also used to illustrate the abilites of our proposed interface. As future work we will focus on the test of proposed query interface with various queries sets (in BioImaging domain) and the case study of engineering design (in PLM). The ontology tree and ontology graph must be also developped to cover all concepts in BioImaging domain.

Ontology will be implemented in semantinc web language (RDF, SPARQL) in order to use inference engine for information search. We plan to test different inference engine for this aim 6 Reference