S Akshay

Blaise Genest

Loïc Hélouët

Timed Petri Nets with (restricted) Urgency

Keywords:

 are two incomparable classes of concurrent models with timing constraints: urgency cannot be expressed using Timed Petri Nets, while TPNs can only keep track of a bounded number of continuous values ("clocks"). We introduce Timed Petri Nets with Urgency, extending Timed Petri Nets with the main features of TPNs.

We present upto-our-knowledge the first decidability results for Petri Net variants combining time, urgency and unbounded places. First, we obtain decidability of control-state reachability for the subclass of Timed Petri Nets with Urgency where urgency constraints can only be used on bounded places. By restricting this class to use a finite number of "clocks", we further show decidability of (marking) reachability. Formally, this class corresponds to TPNs under a new, yet natural, timed semantics where urgency constraints are restricted to bounded places. Further, under their original semantics, we obtain the decidability of reachability for a more restricted class of TPNs.

Introduction

Petri nets are a simple yet powerful mathematical formalism for modeling distributed systems. In order to specify real-time behaviors, they can be enriched with quantitative information in the form of timing constraints. There are several such extensions of Petri Nets. We first discuss the features and short-comings of two main variants, namely: Time Petri Nets (TPNs) [START_REF] Merlin | A Study of the Recoverability of Computing Systems[END_REF] and Timed Petri Nets [START_REF] Walter | Timed Petri-Nets for Modelling and Analysing Protocols with Real-Time Characteristics[END_REF][START_REF] Abdulla | Timed Petri nets and BQOs[END_REF].

TPNs can constrain each transition with a timing interval. To be fireable, a transition needs to have been enabled for an amount of time inside the given interval. Also, when a transition has been enabled for the maximal amount of time according to its associated interval, it must fire. This is called urgency. Formally, a (continuous, positive valued) clock is associated to each transition. Hence the number of such clocks is bounded by the number of transitions. Although the number of clocks is bounded, most problems (reachability, termination, control-state reachability, boundedness) are undecidable for TPNs [START_REF] Jones | Complexity of some problems in Petri nets[END_REF], as two counter machines can easily be encoded. To obtain decidability, one either restricts to bounded TPN [START_REF] Berthomieu | Modeling and verification of time dependent systems using time Petri nets[END_REF], or gives up urgency [START_REF] Reynier | Weak time Petri nets strike back![END_REF]. In this latter case, the untimed language of a TPN without urgency (also known as its weaktime semantics) is the language of the associated Petri Net without timing constraints, weakening the interest of TPNs.

On the other hand, Timed Petri Nets associate (continuous, positive valued) ages to each token. The number of continuous values is thus a priori unbounded. Each arc from a place to a transition can be constrained by a timing interval, meaning that only tokens with age in the interval can be consumed by this transition. Timed Petri Nets cannot encode urgency [START_REF] Haddad | Time and timed Petri nets[END_REF][START_REF] Abdulla | Timed Petri nets and BQOs[END_REF]. Although the number of token ages is unbounded, control-state reachability and boundedness are decidable for Timed Petri Nets [START_REF] Abdulla | Timed Petri nets and BQOs[END_REF]. The reason is that without urgency, we obtain monotonicity properties for tokens (as they can be "lost" by just staying forever at a place), which permits the application of the theory of well structured transition systems [START_REF] Finkel | Well-structured transition systems everywhere![END_REF]. However, reachability is still undecidable for Timed Petri Nets [START_REF] Ruiz | On non-decidability of reachability for timed-arc Petri nets[END_REF].

In terms of expressivity, Timed Petri Nets cannot express that a token is produced exactly every unit of time: due to lack of urgency, it is not possible to force a transition to fire. On the other hand, TPNs cannot express that an unbounded number of tokens (with slightly different ages) are consumed at least two units of time after they have been created. We now propose a formalism which can easily specify these two characteristics (see Fig. 1), and more. Namely, we introduce Timed Petri nets with Urgency, extending Timed Petri Nets [START_REF] Walter | Timed Petri-Nets for Modelling and Analysing Protocols with Real-Time Characteristics[END_REF][START_REF] Abdulla | Timed Petri nets and BQOs[END_REF] with explicit urgency requirements, à la Merlin [START_REF] Merlin | A Study of the Recoverability of Computing Systems[END_REF]. This is done by introducing, in Timed Petri Nets, urgency constraints on transitions, forcing the transition to fire if it remains enabled for long enough.

Unsurprisingly, most problems are undecidable because of urgency (Proposition 2), as is the case for TPNs. To get around this, we consider a class of systems where urgency can be used, but is restricted in a meaningful way. In this class of nets, transitions consuming tokens exclusively from bounded places can use urgency; other transitions that consume tokens from at least one unbounded place do not have urgency constaint. We say that such systems (be it Timed Petri Nets or TPN) are with restricted Urgency. Notice that it is in general not the case that the untimed language of a TPN with restricted Urgency is the language of the associated Petri Net (without the timing constraints).

From a practical point of view, this allows to specify e.g. a timed system of finite state machines communicating through bag channels [START_REF] Clemente | Decidable topologies for communicating automata with fifo and bag channels[END_REF]: each process is a finite-state machine -hence can use urgency. However, (unbounded) channels can use (latency) constraints on tokens but not urgency: a message from a channel cannot be forced to be received in a given time bound (but it can be lost after a time out period). This extends the channel models of [START_REF] Clemente | Reachability of communicating timed processes[END_REF], where urgency is not allowed.

We present upto-our-knowledge the first decidability results for such Petri Net variants combining time, urgency and unbounded places. For Timed Petri Nets with restricted Urgency, we obtain decidability of control-state reachability (Theorem 1), and more generally of timed marking coverability, boundedness, termination, etc. The proof is based on the fact that we can transform such a system into an equivalent Timed Petri Net. The construction separates the bounded and unbounded part, processing the bounded part to remove urgency thanks to the finite number of states, and then reinserts the unbounded part (which does not use urgency, hence is already a Timed Petri Net).

Undecidability of the reachability problem for Timed Petri Nets with restricted Urgency, inherited from Timed Petri Nets, is due to the presence of unboundedly many timed tokens. We thus want to define a subclass of Timed Petri Nets with Urgency where the number of (useful) timed tokens is bounded. This leads us to consider TPNs, which inherently use a bounded number of "clocks". We define an alternative timed semantics for TPNs, presenting them as a subclass of Timed Petri Nets with Urgency. We then obtain our main result: a class of Timed Petri Nets with restricted Urgency such that reachability is decidable (Theorem 4). This class corresponds to TPNs with restricted urgency under the timed semantics.

The timed semantics is close to the original semantics, in the sense that both semantics coincide for a large class of TPNs (Proposition 1). Under their standard semantics, we obtain decidability of reachability only for a strict subclass of TPNs with restricted urgency (Theorem 3), showing the algorithmic advantage of the timed semantics.

The paper is organized as follows: Section 2 introduces Timed Petri Nets with Urgency and their semantics. Section 3 compares this model with TPNs and define their timed semantics. Section 4 introduces the reachability and boundedness problems that we consider and shows that these are all undecidable in general for Timed Petri Nets with Urgency. Section 5 defines restricted urgency subclasses for Timed Petri nets with Urgency and for TPNs and states the associated decidability results. Section 6 gives a sketch of the proofs, whose details can be found in the appendix.

Timed Petri nets with Urgency

We will denote by Q ≥0 the set of positive rational numbers, and by

I(Q ≥0 ) the set of intervals over Q ≥0 ∪ ∞. These intervals can be of the form (a, b), (a, b], [a, b), or [a, b].
We will denote by M R the set of multisets of positive real numbers. For two multisets A and B, we denote by A B the disjoint union of A and B, i.e., the multiset that gathers elements of multisets A and B without deleting identical elements. Similarly, we define A \ B as the operation that removes from A exactly one occurrence of each element of B (if it exists). We introduce our main model, Timed Petri Net with urgency constraints. The model is based on a timed semantics using timed markings m : P → M R which associate to each place a multiset describing the ages of all the tokens in this place.

Definition 1. A Timed Petri net with Urgency, denoted Timed PNU, is a tuple N = (P, T, • (), ()

• , m 0 , γ, U ) where -P is a set of places, -T is a set of transitions, -• () : T → P is a backward flow relation indicating tokens consumed by each transition, -()

• : T → P is a forward flow relation indicating tokens produced by each transition, m 0 is the initial timed marking, γ : P × T → I(Q ≥0 ) is a set of token-age constraints on arcs, -U : T → Q ≥0 is a set of urgency constraints on transitions.

For a given arc constraint γ(p, t) = [α(p, t), β(p, t)] we will call α(p, t) the lower bound and β(p, t) the upper bound of γ(p, t). Such constraints mean that the transition t is enabled when for each place p of its preset • t, there is a token in p of age in γ(p, t), i.e., between α(p, t) and β(p, t). The urgency constraint U (t) means that a transition must fire if it has been enabled (by its preset of tokens) for U (t) units of time. A Timed Petri Net [START_REF] Abdulla | Timed Petri nets and BQOs[END_REF] can be seen as a Timed PNU with U (t) = +∞ for all t ∈ T . Notice that we do not label transitions, as we are interested in properties on markings rather than on languages. Each transition can be seen as labeled by its unique name. When building equivalent models for a given net N , we will have to duplicate transitions. In this case, every transition of the new net will be associated to a transition (name) of N in an obvious way.

As an example, consider the Timed PNU N 1 of Figure 1. Places are represented by circles, transitions by narrow rectangles, and flow relation by arcs between places and transitions. Urgency of a transtion t is represented below the transition (in the example, transition t 1 has urgency 0). Arc constraints γ are represented as intervals below arcs. When unspecified, an arc constraint is set to [0, +∞) and an urgency constraint to +∞ (e.g. U (t 2 ) = +∞). Intuitively, this net represents process r sending messages to process s via channel c. Process r sends messages with bandwidth of one message per unit of time. The messages reach s with latency of at least 2. Messages not received after the time out period of 100 units of time are considered "lost".

Formal Semantics of Timed PNU We now define the semantics of a Timed PNU N = (P, T, • (), () In other words, when t fires, a token with age age p that satisfies the arc-constraint γ(p, t) is consumed in each input place of t, and a new token with age 0 is produced in each output place. In particular, tokens that are consumed by firing a transition t are the tokens which enabled the transitions. They need not be unique: several ages from the same place can enable the transition, any of them can be consumed. Hence discrete moves are not a priori deterministic. Further, note that as in TPNs, timed moves are not allowed when a transition is urgent. This ensures that a discrete move must happen when a transition t is urgent. Note however that another transition t may be fired (t needs not be urgent). After t fires, it is possible that no transitions (including t) are urgent anymore (because the corresponding tokens have been consumed), and then time can elapse. Else, urgency remains and a discrete move still needs to happen.

With the above semantics, a Timed PNU N defines a timed transition system N whose states are timed markings and transitions are discrete and timed moves. We will denote by Reach(N ) the set of reachable timed markings of N (starting from m 0 ). An (untimed) marking is a function from P → N. For a timed marking m, we will denote by m : P → N the marking that associates to every place p ∈ P the number of tokens in m(p). We will say that a place p ∈ P of a Timed PNU is bounded if there exists an integer K such that for every timed marking m ∈ Reach(N ), m (p) ≤ K. We will say that N is bounded iff there exists a K such that all the places are bounded by K. Continuing with our channel example of Fig. 1, the initial timed marking m 0 has m 0 (r) = {0}, m 0 (c) = m 0 (s) = ∅, i.e., one counter with age 0 in place r. The only moves allowed from m 0 are a sequence of timed moves with maximal duration of 1 time unit, leading to a timed marking m 1 with m 1 (r) = {1}, m 1 (c) = m 1 (s) = ∅. In m 1 , transition t 1 is enabled and urgent, hence time cannot elapse further. As t 1 is the only enabled transition, it fires, and marking m 2 is reached with m 2 (r) = {0}, m 2 (c) = {0}, m 2 (s) = ∅. From m 2 , no transition is enabled, but as there is no urgent transition, time can elapse. After letting one unit of time elapse, a timed marking m 3 is reached with m 3 (r) = {1}, m 3 (c) = {1}, m 3 (s) = ∅. From m 3 , t 1 is enabled and urgent, and it fires as the only enabled transition. After t 1 fires, one unit of time must elapse, leading to timed marking m 4 with m 4 (r) = {1}, m 4 (c) = {1, 2}, m 4 (s) = ∅. Both transition t 1 and t 2 are enabled in m 4 . Transition t 1 is urgent (but not transition t 2 ), hence time cannot elapse. Transition t 2 can fire, and then timed marking m 5 is reached with m 5 (q) = {1}, m 5 (r) = {1}, m 5 (s) = {0}. Then t 1 is still urgent and it is the only transition enabled in m 5 , thus it fires and the run proceeds in this manner.

Example: Imul in Intel Silvermont Architecture (2014 Atom line). Timed PNU can be used to specify models describing systems with time constraints such as latency or throughput. The Intel Optimization Guide specifies that integer multiplication on port 1 of Silvermont Architecture has 3 to 5 units of time of latency (because of pipeline stages) and throughput of one instruction per 1 to 2 unit of time (see also http:// www.realworldtech.com/silvermont/5/).

The net N 2 of Fig. 2 models this situation. A token in imul-inst models the issue of an integer multiplication instruction. A latency token is created 3 to 5 units of time after a token in imul-inst. The throughput token is ready 1 to 2 unit of time after the previous instruction fired (else it is not-ready). The instruction is processed as soon as both latency and throughput places are filled. This consumes one instruction and restarts the throughput process. If too many instructions are scheduled exceeding the throughput, they are stuck in the pipeline till the throughput token is ready, which is what actually happens in a processor. Note that without urgency, an instruction might stay forever in imul-inst or in latency.

Comparison with TPNs

Introduced in [START_REF] Merlin | A Study of the Recoverability of Computing Systems[END_REF], Time Petri nets (TPNs for short) associate a time interval to each transition of a Petri net. A time Petri net N is a tuple (P, T, • (.), (.)

• , m 0 , I)

where P is a finite set of places, T is a finite set of transitions, • (.) : P → T is the backward flow relation, (.)

• : P → T is the forward flow relation, m 0 ∈ N P is the initial (untimed) marking, and I : T → I(Q ≥0 ) associates with each transition a firing interval. We denote by A(t) (resp. B(t)) the lower bound (resp. the upper bound) of interval I(t). A configuration of a TPN is a pair (m, ν), where m is an (untimed) marking (recall that m(p) is the number of tokens in p), and ν :

T → R ≥0 associates a real-time value to each transition. 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 valuation ν associates to each enabled transition t ∈ En(m) the amount of time that has elapsed since this transition was last newly enabled. An enabled transition t is urgent if ν(t) ≥ B(t), with B(t) the upper bound of I(t). We use the classical intermediate marking semantics (see for instance [START_REF] Berthomieu | Modeling and verification of time dependent systems using time Petri nets[END_REF]) defined as follows, using timed and discrete moves between configurations.

A timed move consists of letting time elapse in a configuration.

For (m, ν), ν + δ is defined by ν + δ(t) = ν(t) + δ, for all t ∈ En(m). A timed move from (m, ν) to (m, ν + δ), denoted (m, ν) δ -→ (m, ν + δ)
, is allowed if for every 0 ≤ δ < δ, the configuration (m, ν + δ ) has no urgent transition. A discrete move consists of firing an enabled transition t that has been enabled for a duration that fulfills the time constraints attached to t. We have (m, ν)

t - → (m , ν ) if t ∈ En(m), ν(t) ∈ I(t) and m = m -• t + t • ,
for ν defined below. We call intermediate marking the marking m -• t which is obtained after t consumes tokens but did not create new ones yet. We will say that a transition t ∈ En(m ) is newly enabled by firing of t if either t = t, or t / ∈ En(m -• t), i.e. is not enabled in the intermediate marking m -• t. Now, we define ν (tt) = 0 if tt is newly enabled, and ν (tt) = ν(tt) for all tt ∈ En(m) but not newly enabled. That is, for a transition both consuming and producing a token in p having a single token, a transition t with p ∈ • t is disabled then newly enabled when t is fired.

We define newly enabledness via intermediate markings since other options (e.g, using the so-called atomic or persistent semantics [START_REF] Reynier | Weak time Petri nets strike back![END_REF]) lead to undecidability even in the absence of urgency [START_REF] Reynier | Weak time Petri nets strike back![END_REF].

• p [2, ∞) t1 [2, ∞) t2 t0 {0} p {0} {0} {0} t1 t2 t0 [2, ∞) [2, ∞) Fig. 3. A (non simple) TPN N3 (left) which is not bisimilar to Timed(N3) (right).
The semantics of TPN is somewhat similar to that of Timed PNU, but is based on configurations instead of timed markings. The only continuous values kept in the configuration of a TPN are in ν. Hence, only |T | "clock" values are kept, and configuration cannot keep track of the exact time elapsed since their creation for arbitrary number of tokens. Hence no TPN can encode that an unbounded number of tokens are processed at least 2 unit of times after they are created (latency at least 2), which can be easily done using Timed Petri Nets (see our two examples in Fig. 1,2).

For a TPN N = (P, T, • (), ()

• , m 0 , I), we can define Timed(N ) its associated Timed PNU. Intuitively, Timed(N ) preserves all places and transitions of N , adds one place p t per transition t, adds p t to the pre and post flow of t, and adapts the timing constraints. We let Timed(N ) = (P , T, (), () , m 0 , γ, U ) where:

-P = P ∪ P T with P T = {p t | t ∈ T }. -(), () extend respectively • (), () • in the following way: p ∈ t iff p = p t or p ∈ • t and p ∈ t iff p = p t or p ∈ t • . -For all t, for I(t) = [A(t), B(t)], we let U (t) = B(t) -A(t) and for all p ∈ t, we set γ(p, t) = [A(t), +∞) (for I(t) = (A(t), B(t)] we let γ(p, t) = (A(t), +∞)), -We let m 0 (p) = 0 m0(p)
for all p ∈ P and m 0 (p t ) = {0} for all transitions t.

We display in Fig. 3 a TPN N 3 on the left and Timed(N 3 ) on the right. We show that for a subclass of (possibly unbounded) TPNs, Timed(N ) and N are timed bisimilar. Definition 2. A TPN N is said to be simple if for all reachable configurations, for all places p, either p has at most 1 token, or only one transition t is enabled with p ∈ • t.

The TPN N 3 on Figure 3 is not simple. However, it becomes simple if we remove e.g. transition t 2 . Intuitively, simple TPNs have the property that immediately after firing a transition with input p, the clock of every enabled transition with input p is 0.

Proposition 1. Let N be a simple TPN. Then Timed(N ) and N are timed bisimilar.

Proof (sketch). The bisimulation relation R between reachable configurations of N and reachable timed markings of Timed(N ) is the following. We associate a timed marking m of Timed(N ) to each configuration (m, ν) of N , with m (p) = m(p) for all p ∈ P , and such that for all t ∈ En(m), ν(t) = min p∈ t (max p ), with max p the oldest token in m (p) for all p. Recall that p t ∈ t. Notice that we can safely consider max p as by definition β(p, t) = +∞ for all p, t.

That is, we consider the oldest tokens oldest p in every place p of the net. Then we consider the youngest oldest p for p in the preset of t. When N is simple, this token age measures the time elapsed since the transition t became enabled in Timed(N ). This is exactly what is measured by ν(t) in N . This is true for all transitions, which implies that (m, ν) of N and m of Timed(N ) are bisimilar. A formal proof of this is included in the appendix.

Notice however that if N is not simple, then N and Timed(N ) may differ. Consider for instance the TPN N 3 in Figure 3. Consider the execution where the TPN fires t 0 twice: first at date 0 and then at date 1. At date 2, both t 1 and t 2 have been enabled for 2 unit of time (ν(t 1 ) = ν(t 2 ) = 2), hence any one of them can fire. Let say t 1 fires. Now, t 1 cannot fire again immediately as it is newly enabled (hence ν (t 1 ) = 0), but t 2 can fire immediately after t 1 , because ν (t 2 ) = 2 (in particular, it is not newly enabled by firing t 1 as there are two tokens in the input place p, i.e., m(p) -• t(p) = 2 -1 = 1). By contrast, in Timed(N ), if t 0 is fired at date 0 and again at date 1, then at date 2, m(p) = {1, 2}, and any one of t 1 or t 2 can fire, let say t 1 . But after this firing of t 1 , the other transition t 2 cannot fire because m (p) = {1} and 1 < 2. It is only at date 3 that t 2 can fire. At date 3, transition t 1 cannot fire because m (p t1 ) = {1}, and 1 < 2.

We now consider Timed(N ) as a new semantics of a TPN N , called the timed semantics of N . One advantage of this timed semantics with respect to the standard (time) semantics is that firing of transitions consume tokens that have enabled this transition. Further, we will show in the following that the timed semantics enjoy better algorithmic properties: the class of TPN for which reachability is decidable is more restricted for the standard semantics (Theorem 3) than for the timed semantics (Theorem 4).

We do not believe that TPN are included into Timed PNU in general: ν(t) cannot be computed in general by looking only at age of actual tokens as it may depends on consumed tokens which prevented disabling t. Also, knowing whether a transition is newly enabled corresponds to performing a kind of zero test, hence it seems hard to code it with new transitions and places. As it subsumes the class of Timed Petri Nets, the class of Timed PNUs is not included into the class of TPNs [START_REF] Haddad | Time and timed Petri nets[END_REF].

Problems Statement and Undecidability

In this paper we will tackle the decidability of the following problems:

-Reachability: given a Timed PNU (or a TPN) N , given an (untimed) marking m, does there exists m ∈ Reach(N ) with m = m? -Control State reachability (also called place-reachability) : given a Timed PNU N and a place p, does there exist m ∈ Reach(N ) with m (p) ≥ 1? -Boundedness : given a Timed PNU N , does there exist K such that for all m ∈ Reach(N ), we have m (p) ≤ K for all places p? -Place boundedness: given a Timed PNU N and a place p, does there exist K such that for all m ∈ Reach(N ), we have m (p) ≤ K?

Another problem that is frequently addressed is the coverability question: given a timed marking m, is there a marking m in Reach(N ) such that m ≤ m ? For Timed Petri Nets (and extensions), it is easy to show that this problem and control state reachability are inter-reducible, hence we do not consider it explicitly.

Because of urgency, every non-trivial problem is undecidable for Timed PNU, following the proof of undecidability for TPNs from [JLL77]: Proposition 2. Control State reachability, Reachability and (place) boundedness are undecidable for Timed PNU.

An unsurprising solution to obtain decidability in TPNs is to drop the urgency requirements [START_REF] Reynier | Weak time Petri nets strike back![END_REF], but then reachable (untimed) markings are just the (untimed) markings reachable by the untimed Petri Net obtained by dropping every timing constraint.

Restricted Urgency and Decidability

As general Timed PNU are Turing equivalent, we now introduce subclasses ensuring decidability. We will provide the decidability results in this section, as well as the sequence of lemmas that lead to them. Some proof ideas will be given in the next section, while the details can be found in the appendix.

We start by defining the restriction of a Timed PNU to a subset of places. Let N = (P, T, • (), ()

• , m 0 , γ, U ) be a timed PNU, and let Q ⊆ P be a subset of places. The

restriction of N to Q is the Timed PNU N Q = (Q, T, () Q , () Q , m 0Q , γ Q , U ), where
() Q , () Q , m 0Q , γ Q are respectively restriction of • (), () • , m 0 , γ to Q × T, T × Q and Q.
Note that every run of N is a run of N Q (by projecting markings on Q), but the converse is not true in general. Our main notion is restricted urgency, which intuitively means that urgency is allowed only on the bounded part of the system. Definition 3. A Timed Petri Net with restricted Urgency (denoted Timed PNrU) is a Timed PNU N = (P, T, • (), ()

• , m 0 , γ, U ) together with a partition P u P b = P of its places such that:

-For each transition t ∈ T with • t ∩ P u = ∅, we have

U (t) = ∞.
-The restriction of N to places of P b is bounded.

Intuitively, this means that urgency cannot be used for transitions consuming tokens from unbounded places. For instance, Fig. 1 displays a Timed PNrU (only place c is unbounded). This is not the case of the Timed PNU in Fig. 2 (latency and imul-inst are unbounded places red by two transitions with urgency). However, the number of instructions in flight in a processor is actually bounded (around 50), hence it is possible to express the system using a Timed PNrU.

Urgency allows to perform zero test-like operations as shown in the undecidability proof of proposition 2. Forbidding zero testing unbounded places seems reasonable to obtain decidability. Proofs showing decidability for TPNs without urgency (as defined and proved in [START_REF] Reynier | Weak time Petri nets strike back![END_REF]) use the fact that timing constraints can be forgotten everywhere without impacting the untimed language. This is not the case with our restriction as urgency is allowed in some parts of the net.

As each Timed Petri Net is a Timed PNrU (it suffices to choose P u = P ), the undecidability of reachability for Timed PNrU is inherited from Timed Petri Nets. We show that we can however decide control state reachability and boundedness.

Theorem 1. Control-State reachability and (Place) boundedness are decidable for Timed PNrU. However, reachability is not decidable for Timed PNrU.

The decidability proofs are obtained by encoding any Timed PNrU into an equivalent Timed Petri Net. Hence they have the same set of reachable markings. Now, we immediately obtain decidability from the following result of [AN01]: Theorem 2. [AN01] Control-State reachability and (Place) boundedness are decidable for Timed Petri Nets.

Decidability of Reachability for a subclass of TPNs

A natural question is whether decidability can be obtained for TPNs as well, by restricting urgency. In fact, a condition stronger than restricted urgency is needed. Definition 4. Let N = (P, T, • (), ()

• , m 0 , I) be a TPN and P = P u P b be a partition of its places such that the restriction of N to places of P b is bounded. Then,

-N is called a TPN with restricted urgency (TPNrU for short) if for each transition t ∈ P u with • t ∩ P u = ∅, we have

I(t) = [c, ∞) with c ∈ Q ≥0 .
-N is called a TPN with restricted constraints if for each transition t ∈ P u with

• t ∩ P u = ∅, we have

I(t) = [0, ∞).
The class of TPNs with restricted constraints is strictly contained in the class of TP-NrU. As an example, the TPN N 3 on Fig. 3 has restricted urgency but not restricted constraints, since place p is unbounded and there is a transition with non-trivial lower constraints reading from p, but no transition with urgency constraints. We show that reachability is decidable for TPNs with restricted constraints. This is done by encoding N into an (untimed) bisimilar Petri Net: Proposition 3. For each TPN with restricted constraints N , one can construct a Petri Net N such that N and N are bisimilar.

Decidability of reachability for Petri Nets can thus be extended:

Theorem 3. Reachability is decidable for TPNs with restricted constraints.

We do not know if reachability is decidable for the class of TPNrU. However, when we consider TPNrU under the timed semantics, we obtain decidability of reachability, as shown now.

Decidability of Reachability for a subclass of Timed PNrU

Let N be a TPNrU. Clearly, Timed(N ) is a Timed PNrU. Then: Theorem 4. Let N be a TPN with restricted Urgency. Then the reachability problem for Timed(N ) is decidable.

In order to prove Theorem 4, we encode Timed(N ) as a machine Timed(N ) such that N is a TPN with restricted constraints. By adapting Proposition 3 to produce a Petri Net bisimilar to Timed(N ), we obtain decidability of reachability.

Thus, the set {Timed(N ) | N is a TPNrU} is a subclass of Timed PNrU for which we obtain decidability of reachability.

Proofs

Proof of Theorem 1

We start by defining a notion of timed equivalence that we need for this proof. Let S be a system, either a Timed PNU, a Timed Petri Net or a timed automaton [START_REF] Alur | A theory of timed automata[END_REF], where each transition is associated to one transition of T . A timed sequence of S is a finite sequence (t 1 , d 1 ) . . . (t n , d n ) with t i ∈ T a transition name and 0 < d 1 < • • • < d n timing instants, such that from the initial state s 0 of the (timed transition) semantics of S, one can perform the sequence of transitions: s 0

d 1 -→ r 1 t 1 -→ s 1 d 2 -d 1 ----→ r 2 • • • d n -d n-1 ------→ r n t n
-→ s n . Two systems are said be timed equivalent if they have the same set of (finite) timed sequences. A crucial observation is that if two systems are timed bisimilar, they are timed equivalent (the converse does not hold in general). Now, the proof of Theorem 1 is performed in two steps. First, given a Timed PNrU N , we construct a 1-bounded (labeled) Timed Petri Net N 1 which is timed equivalent to the bounded part N B of N (it is not possible to get bisimilarity because Timed Petri Nets do not use urgency). This can be done by first converting the bounded part of the Timed PNrU into a bisimilar timed automaton with all states accepting (as done for TPNs e.g., in [START_REF] D'aprile | From time Petri nets to timed automata: An untimed approach[END_REF]), and then using the construction from [BHR08] (Theorem 7 and Corollary 1) to convert the timed automaton to 1-bounded Timed Petri Net which is timed equivalent to it. We denote N 1 = (P 1 , T 1 , • ., . • , m 1 , γ 1 ) this 1-bounded Timed Petri Net.

In the second step, we show that the original Timed PNrU N is timed equivalent to the net N 2 formed by adding unbounded places of N to the N 1 . Formally, we construct the Timed Petri Net N 2 = (P 2 , T 1 , ., . , m 2 , γ 2 ) as follows:

-The set P 2 of places of N 2 is P 2 = P 1 ∪ P u , for P u the unbounded places of N .

-Initial timed marking m 2 is the union of m 1 and of the restriction of the initial timed marking of N restricted to its unbounded places P u . -Finally, the set of transitions of N 2 is the set T 1 of transitions of N 1 , and the flow relations and γ 2 are defined in the following way. Let t 1 ∈ T 1 , corresponding to a transition t ∈ T in the original net N . We have p ∈ t 1 if:

• p ∈ P 1 and p ∈ • t 1 (arc from p to t 1 in N 1 ), and then γ 2 (p, t 1 ) = γ 1 (p, t), or • p ∈ P u and there was an arc from p to t in N , and then γ 2 (p, t 1 ) = γ(p, t), the constraints from N . Similarly, we have p ∈ t 1 if p ∈ P 1 and p ∈ t 1

• (arc from t 1 to p in N 1 ), or if p ∈ P u and there is an arc from t to p in N .

Lemma 1. N and N 2 are timed equivalent.

The first step along with Lemma 1 thus completes the proof of Theorem 1.

Proof of Proposition 3

The proof is similar to the above proof. First, given a TPNrU N , we construct a 1bounded (untimed) Petri Net N 1 which is bisimilar to the bounded part N B of N . This can be done by using [START_REF] D'aprile | From time Petri nets to timed automata: An untimed approach[END_REF] to build a timed automata bisimilar to N B and interpreting its regions as a 1 safe Petri Net. Notice that the exact same process can be done starting with Timed(N B ) instead of N B . We provide the proof in appendix.

Lemma 2. [DDSS07]

If N is a K-bounded TPN, we can construct a 1-bounded Petri Net N 1 such that N 1 and N are (untimed) bisimilar. Now, the second step shows that the original TPNrU N is bisimilar to the Petri net obtained by adding unbounded place of N to the Petri net N 1 = (P 1 , T 1 , • ., . • , m 1 ). Formally, we construct the Petri net N 2 = (P 2 , T 1 , ., . , m 2 ) as previously:

-The set P 2 of places of N 2 is P 2 = P 1 ∪ P u , for P u the unbounded places of N .

-Initial marking m 2 is the union of m 1 and of the restriction of the initial marking of N restricted to its unbounded place P u . -Finally, the set of transitions of N 2 is the set T 1 of transitions of N 1 , and the flow relations are defined in the following way. Let t 1 ∈ T 1 corresponding to a transition t ∈ T in the original net N . We have p ∈ t 1 if:

• p ∈ P 1 and p ∈ • t 1 (arc from p to e in N 1 ), or • p ∈ P u and there was an arc from p to t in N . Similarly, we have p ∈ t 1 if p ∈ P 1 and p ∈ t 1

• (arc from e to p in N 1 ), or if p ∈ P u and there is an arc from t to p in N .

Proof of Theorem 4

Let (N , P, Q), with N = (P ∪ Q, T, • (), ()

• , m 0 , I) be a TPNrU, where P is the set of bounded places and Q the set of unbounded places. The idea of the proof is the following: intuitively, the timed semantics of N is that for a transition to fire, each of its token need to be old enough. If the transition has an unbounded place from Q in its preset, then there is no urgency, and this condition is sufficient. Else it is bounded and we can deal with it easily. Assume wlog. that N P is 1-bounded. For unbounded places, we need their ages only for a bounded number of them, as there is a finite number of transitions, and each transition time is reset after it is fired. Construction of the TPN with restricted constraints N : In order to obtain a TPN with restricted constraints N , we will keep (an overapproximation of) ages for a bounded number of tokens from an unbounded place. Basically, for each unbounded place p ∈ Q, we will create |T | channels (C t p ) t∈T for this place. Each channel C t p from place p ∈ Q is a TPN with restricted constraints. Each channel is similar: It has 2 places: 0 t p (that is C t p empty) and 1 t p (one token in C t p ). The initial marking is 0 t p . There is an associated transition start t p : we have start t p = {p, 0 t p } and start t p = {1 t p }. The timing constraint is I (start t p ) = [0, +∞). That is, N will non deterministically guess the transition to start counting for. Now, we transform every transition to be able to read from any of these channels c i p instead of the places p. If a transition t reads from unbounded places {p

1 , • • • , p k } = • t∩Q, then we have t = • t\{p 1 , • • • , p k }∪{1 t pj | j ≤ k} and t = t • ∪{0 t pj | j ≤ k}. The timing constraint is left unchanged: I (t) = I(t).
Now, let N = (P , T , (), () , m 0 , I ):

-P = P ∪ Q ∪ {O i p , 1 i p | p ∈ P, i ≤ |T |}, -T = T ∪ {start i p | i ≤ |T |, p ∈ Q}, - (
), () , I as defined above, and m 0 (p) = m 0 (p) for p ∈ P , and m 0 (0 i p ) = 1, m 0 (1 i p ) = 0 for all i, p It is clear that N is a TPN with restricted constraints, with Q = Q the set of unbounded states, as for all t with t ∩ Q = ∅, we have t = start i p , and thus

I(t ) = [0, +∞).
Let m be a marking of Timed(N ). Define c = f (m ) :

P ∪ Q ∪ P T such that for all p ∈ P ∪ Q ∪ P T , c(p) = m (p) + i≤|T | m (1 i p )
(the second part is ignored for p ∈ P ∪ P T ). Notice that because i≤|T | m (1 i p ) ≤ |T | for all p, fixing c, there exists only a finite number of m such that f (m ) = c. For two timed marking m, m , we write m ≡ m whenever f (m ) = m . Now, remark that because there is only one token possible in 1 t p and it can be started only after t fired (because of 0 t p filled when t fired), m (1 i p ) can never be older than m (p t ), the age since the last firing of t. Let t be a transition, Let c be an untimed marking of Timed(N ). Let c be any untimed marking of Timed(N ) with f (c ) = c. To obtain the proof of Theorem 4, it suffices to apply the following proposition, whose second statement is decidable because N is a TPN with restricted constraints. Proposition 4. c is reachable in Timed(N ) iff c is reachable in Timed(N ).

I(t) = [a, ∞) and let p ∈ Q ∩ • t. Now,
The proof uses the two following lemmas relating N and N . m ≡ m and for all p ∈ P ∪ P T , we have m (p) = m(p) and for all t ∈ T , p ∈ P , we have either m (0 t p ) = ∅ or m (0 t p ) = m (p t ), and for all q ∈ Q, letting T q = {t ∈ T | m (1 t q ) = ∅}, there exists m(q) = m (q) {age t | t ∈ T q } with m (1 t q ) = min(m (p t ) = m(p t ), age t ) for all t ∈ T q . Lemmas 4 and 5 imply Proposition 4.

Conclusion

In this paper, we extend Timed Petri Nets to express urgency constraints, thus capturing the essential feature of TPNs. While general Timed Petri Nets with Urgency are undecidable (as are TPNs), we obtain decidability when urgency is used only in the bounded part of the system. We then consider an alternative timed semantics for general TPNs in terms of Timed Petri Nets with Urgency. Compared to the original semantics, our timed semantics ensures that transitions only consume tokens that enabled them long enough. Also, decidability of reachability can be proved for a larger class of systems.

We plan to study robustness properties, i.e, whether the system can withstand infinitesimal timing errors. Robustness has been extensively studied for timed automata [Pur00,DDMR08,BMS13], etc. We would like to extend the study started for TPNs (e.g. [START_REF] Akshay | Robustness of time Petri nets under guard enlargement[END_REF]) to Timed Petri Nets with restricted Urgency.

-Else, tt is newly enabled, with some p ∈ • tt ∩ t • and m 2 (p) = {0}. Thus ν 2 (tt) = 0 = min p∈m 2 (max p ) as max p = m 2 (p): P 1 holds Thus we have proved that ((m 2 , ν 2 ), m 2 ) ∈ R.

Last, let transition t be fireable from timed marking m and leading to timed marking m 2 . As m (p) = m(p) for any place p ∈ P , t ∈ En(m). As t is fireable from m , there exists age p ∈ m (p) with α(p, t) ≤ age p ≤ max p . Hence α(p, t) ≤ min p∈ t max p = ν(t).

As no urgency constraint is ever violated (the timed marking and configurations are reachable), we also have

ν(t) = min p∈ t (max p ) ≤ α(t) + U (t) = A(t) + B(t) - A(t) = B(t).
Hence t is fireable from (m, ν), obtaining marking m 2 with m 2 (p) = m 2 (p) for all p ∈ P . The proof that (P1) holds for (m 2 , ν 2 ), m 2 is exactly the same as above. s As a conclusion, we have that R is a bisimilation.

Proof for Section 4

Proposition 2. Control State reachability, Reachability and (place) boundedness are undecidable for Timed PNU.

Proof. As mentioned earlier, the proof follows on the same lines as the undecidability proof in [START_REF] Jones | Complexity of some problems in Petri nets[END_REF]. The proof is a standard encoding of reachability for a 2 counters machine with zero test (Minsky Machine). A Minsky machine is given as a set of counters {C 1 , . . . C k }, and a sequence of instructions inst 1 .inst 2 . . . inst n . Each Instruction inst i is of the form inst i : inc(j, k), meaning that the machine increments counter C j and moves to instruction inst k , or inst i : Jzdec(j, k, k ) meaning that the machines tests whether counter C j is zero or whether it is strictly greater. If it is 0, the machine moves to counter k . Else it decrements C j and moves to instruction k. A well known result is that it is undecidable whether a Minsky machine with two counters can reach an instruction x.

We can now show how to encode any two-counter Minksy machine M with a Timed PNU N M = (P M , T M , • () M , ()

• M , m 0 , γ M , U M ).
The set of places P M contains two places p 1 , p 2 (one per counter), and one place q i per instruction inst i of the machine. The set of transitions T M contains one transition t i for each increment instruction inst i : inc(j, k), with • t iM = {q i } and t i

• M = {p j , q k }. Further, U M (t i ) = 0 and γ(q i , t i ) = [0, ∞).
T M also contains a pair of transitions t i , t z i for each decrement instruction inst i : Jzdec(j, k, k ). Intuitively, t i will simulate the move of the machine when counter C j is not empty, and t z i the move of the machine when counter C j is empty. We have

• t iM = {q i , p j } and t i • M = {q k }. Further, U M (t i ) = 0 and γ M (q i , t i ) = γ M (p j , t i ) = [0, ∞),
that is transition t i fires as soon as both places p i and q j contain at least one token. For transition t z i , we have

• t z i M = {q i } and t z i • M = {q k }. Further, U (t z i ) = 0 and γ M (q i , t z i ) = [1, ∞)
, that is transition t z i fires exactly 1 time unit after place q i is filled. Let us show that urgency prevents firing of transition t z i from a marking m with m (q i ) = 1 and m (p j ) > 0. Let us suppose that the machine moves from a marking m -to m, with place q i marked. This means that place q i contains a token with age 0. Notice that at a given instant, only one place q j , j ∈ {1, . . . , n} can be marked in a reachable marking of N M . Suppose that transition t z i can fire from a marking m with m (q i ) = 1 and m (p j ) > 0, obtained from m by letting at least one time unit elapse. This means that m (p j ) ≥ 1, and hence, at least one time unit has elapsed from marking m. However, transition t i is urgent from any marking with at least one token in q i and one token in p j , and in particular from m. Thus time cannot elapse from m, a contradiction. So, our encoding of M is faithful and a run

t i1 • • • t in can happen in N M iff run inst i1 • • • inst in can happen in M .
Hence a two-counter machine M reaches instruction x iff place q x is reachable in N M . This reachability question can be equivalently encoded as a coverability problem where the marking to cover is m(p x ) = {0} and m(p) = ∅ for all other places. It is also known that checking boundedness of a counter in a Minsky machine is undecidable. Hence, boundedness and place boundedness are also undecidable in general for Timed PNU.

Proofs and details for Section 5 and 6

Proof of Theorem 1 A first step in our proofs is to show that the semantics of bounded Timed PN with Urgency can be encoded in a bisimilar way by timed automata. Let X be a finite set of real-valued variables called clocks. We write C(X) for the set of constraints over X, C ub (X) of upper bound constraints over X as usual [START_REF] Alur | A theory of timed automata[END_REF].

Definition 5 (Timed Automata (TA) [START_REF] Alur | A theory of timed automata[END_REF]). A timed automaton A over Σ ε is a tuple (Q, q 0 , X, δ, I) where Q is a finite set of locations, q 0 ∈ Q is the initial location, X is a finite set of clocks, I ∈ C ub (X) Q assigns an invariant to each location and

δ ⊆ Q × C(X) × Σ ε × 2 X × Q is a finite set of edges. A valuation v is a mapping in R X ≥0 . 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 constraint γ is satisfied by v. The semantics of a TA A = (Q, q 0 , X, δ, I) is the transition system A = (S, s 0 , →) where

S = {(q, v) ∈ Q × (R ≥0 ) X | v |= Inv(q)}, s 0 = ( 0 , 0) and → is defined by delay moves: ( , v) d -→ ( , v + d) if d ∈ R ≥0 and v + d |= Inv( ); and 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).

The encoding of bounded Timed PN with Urgency into timed automata is not a real surprise, as similar bisimilar encodings have already been proposed for bounded TPNs. [START_REF] D'aprile | From time Petri nets to timed automata: An untimed approach[END_REF] propose to compute a marking timed automaton from TPN: the construction starts from the finite set of markings, and creates transitions of the form (m, g t , t, m ) for any pair of markings such that m = m -• t + t • with guard g t = ν(t) ∈ [A(t), B(t)]. We can then obtain the construction of finite timed automata from bounded TPNUs.

Proposition 2. Let N be a K-bounded TPNU. Then one can compute a finite timed automaton A B N that is timed bisimilar to N .

Proof. We set A B N = (Q, q 0 , X, δ, I), where Q is a set of states, δ a transition relation, I : Q → CST is an invariant relation attaching a constraint on clock values to each state, and X is a set of clocks.

The set of clocks X is computed as follows: X = {x p,i | p ∈ P ∧ i ∈ 1..K}. Intuitively, x p,i will measure the age of the i th token in place p. We denote by CST the set of all linear constraints that can be defined over X. Note that as we associate one clock per token in each place, as a place can be marked with less than K tokens, all clocks are not meaningful. We will compute inductively a set Q ⊆ 2 X × CST . Each state q = (A, cst) of the automaton will remember a set A of active clocks, and a constraint cst on the values of clocks. This construction is almost the state class construction of [Lime &Roux, DEDS, 06], with the slight difference that an active clock measures the age of a tokens instead of measuring the time since a transition was last newly enabled. To each state q = (A, cst) and valuation ν q : qR, we can associate a timed marking m q,ν such that m q,ν (p) = {ν(x p,i ) | x p,i ∈ X}. Similarly, to each clock selection A, we can associate a marking m (A)(p) = |{x p,k ∈ A}|. We will say that A enables t if for every place p in • t, m (A)(p) ≥ 1.

Let us now define the transition relation. We do not need to define timed moves, that will simply consist in letting time elapse from a state of the automaton. However, transitions of the automaton have to encode discrete moves of the net. As already pointed out, from a timed marking m, a discrete firing of a transition t can result in a finite number of new markings m 1 , . . . , m k , as the tokens to be consumed from each place can be chosen non-deterministically. Note however that as places are bounded by K, the number of markings that can be reached is bounded by K |P | .

Let q = (A, cst), and let t be a transition such that ∀p ∈ • t there exists at least one clock x p,i in A. We define EXS(A, t) as the set of sets of clocks that contain exactly one clock of A per place in • t. To fire, a transition needs to select a set of tokens that will be consumed, that is choose a element Y of EXS(A, t). However, to be fireable, every clock x p,i in Y has to satisfy x p,i ∈ γ(p, t). For every Y ∈ EXS(A, t), we define g t,Y = xp,i∈Y x p,i ∈ γ(p, t) as the guard attached to transition t when choosing set Y of token clocks. For a fixed origin state q = (A, cst), a transition t and a chosen set of clocks Y , we will denote by q = N ext(q, t, Y ) the state reached after firing t from q, provided clocks in Y satisfy g t,Y . State q is of the form q = (A , cst ), where A = A\Y ∪R(A, t, Y ), where R(A, t, Y ) = {x p1,k1 , . . . x pq,kq } is a set of clocks that contains exactly one clock per place in t • , and such that each k j is the minimal index of clock attached to place p j that does not appear in A \ Y (this avoids introducing nondeterminism when reusing clocks). This index exists, as N is bounded. The constraint attached to the new state is computed as follows:

We add to cst conjunction of constraints x p,j ≤ x p ,i for each pair of clocks in R, A \ Y . Intuitively, this additional constraint means that the age of newly created tokens must be smaller or equal to the age of remaining tokens. We then eliminate variables x p,i ∈ Y , using a variable elimination technique such as Fourrier-Motzkin . We then rename variables x p,j to x p,j to obtains cst . One can note that appying arbitrary number of conjunction of inequations of the form x ≤ c, c ≤ x where c is a constant and x a clock and elimination of variables, we can only reach a bounded number of constraints from cst 0 . Hence, Q is finite.

We can now define δ as follows δ = {(q = (A, cst), g t,Y , t, R(A, t, Y ), q = (A , cst )) | g t,Y ∧ cst is satisfiable ∧ t enabled by A}. One can remark that a transition t can be enabled from several states, as two distinct clock selections may represent the same markings. The initial state of the automaton is q 0 = (A 0 , cst 0 ) where A 0 is the set A 0 = {x p,1 , x p,k | m 0 (p) = k}, and cst 0 is the set of constraints

cst 0 = {x = y | x, y ∈ A 0 }
The last ingredient of our timed automaton A N is the invariant attached to each state. Invariants must guarantee that clock values must not increase beyond urgency of a transition, i.e one can not reach a clock valuation ν such that for each place of the preset of some enabled transition t there exists a clock x p,i such that α(t) + U (t) < ν(x p,i ) ≤ β(t). Now, we turn to the proof of Theorem 1. The proof is performed in two steps. First, given a Timed PNrU N , we construct a 1-bounded (labeled) Timed Petri Net N 1 which is timed equivalent to the bounded part N B of N (it is not possible to get bisimilarity because Timed Petri Nets do not use urgency). This is done by first converting the bounded part of the Timed PNrU into a timed automaton using Prop. 2, and then using the following result from [BHR08] (Theorem 7 and Corollary 1) to convert timed automata to Timed Petri Nets with equivalent (finite) language. Lemma 6. [START_REF] Bouyer | Timed Petri nets and timed automata: On the discriminating power of Zeno sequences[END_REF] Let A be a timed automaton. Then we can construct a K -bounded Timed Petri Net N 1 such that N 1 and A are timed equivalent. Now, the second step shows that the original Timed PNrU N is timed equivalent to the net N 2 formed by adding unbounded places of N to the Timed Petri Net N 1 .

Lemma 1. N and N 2 are timed equivalent.

Proof. First, let (t 1 , d 1 ) • • • (t n , d n ) be a finite word in the language of N , where t i are transitions of N and d 1 < • • • < d n are dates at which t n occurs (that is, d i -d i-1 units of time occured between t i-1 and t i ). Let m be some timed marking reached in N after

(t 1 , d 1 ) • • • (t n , d n ). First, as (t 1 , d 1 ) • • • (t n , d n ) is a timed word of N , it
is also a timed word of N B , the bounded restriction of N , and thus of N 1 Let m 1 be a timed marking reached in N 1 after (t 1 , d 1 ) • • • (t n , d n ). We now show by induction that the timed word

(t 1 , d 1 ) • • • (t n , d n ) is a timed word of N 2 ,
reaching a timed marking m 2 = m 1 ∪ m u with m u the restriction of m to P u . First, it is trivial for the empty timed word.

Induction step: Let δ = d n -d n-1 and t = t n . Let m 1 , m be two markings such that

m 1 δ -→ m 1 +δ t - → m 1 in N 1 and m δ -→ m +δ t - → m in N . By the induction hypothesis, the timed marking m 2 = m 1 ∪ m u is reached in N 2 after (t 1 , d 1 ) • • • (t n-1 , d n-1
). We want to show that from m 2 , δ timed units can elapse and then t is allowed, leading to m 2 . First, δ time units can elapse from m 2 in N 2 as there is no urgency in N 2 (it is a Timed Petri Net). Further, tokens consumed in m 1 + δ t -→ m 1 can be consumed in m 2 + δ as well, and so do tokens consumed from P u in the transition m + δ Conversely, take (t 1 , d 1 ) • • • (t n , d n ) be a finite word in the language of N 2 . Denote by m 2 = m 1 ∪ m u a timed marking reached by this timed word, with m 1 a timed marking of N 1 and m u the timed marking over P u the infinite places of N . We have that

(t 1 , d 1 ) • • • (t n , d n ) is
= m b ∪ m u is reached in N 2 after (t 1 , d 1 ) • • • (t n-1 , d n-1
). We want to show that from m , δ timed units can elapse and then t is allowed, leading to m. Thus, from Lemma 1 we obtain that for each Timed PNrU N , one can construct a Timed Petri Net N 2 such that N and N 2 are timed equivalent. By Theorem 2, we can then conclude the proof of Theorem 1.

Proof of Proposition 3 for the timed semantics

The exact proposition we prove for the timed semantics is the following.

Proposition 5. For each TPN with restricted constraints N , one can construct a Petri Net bisimilar to Timed(N ).

The proof is again in two steps. First, given a TPNrU N , we denote by N B its bounded part. We construct a 1-bounded (labeled) Petri Net N 1 which is bisimilar to Timed(N B ). As Timed(N B ) is a bounded Timed PNU, we use proposition 2 to build a timed automaton A 1 bisimilar to Timed(N B ). We interpret the regions automaton of this timed automata as a 1-safe Petri Net. Note that this net has no timed constraints. We call the resulting Petri Net N 1 = (P 1 , T 1 , • ., . • , m 0,1 ). As A 1 is time bisimilar to Timed(N B ), and N 1 is (untimed) bisimilar to A 1 , we have that N 1 is (untimed) bisimilar to Timed(N B ). Now, the second step shows that the original TPNrU Timed(N ) is bisimilar to the Petri net obtained by adding unbounded place of N to N 1 . Formally, we construct the Petri Net N 2 = (P 2 , T 1 , ., . , m 0,2 ) as previously:

-The set P 2 of places of N 2 is P 2 = P 1 ∪ P u , where P u denotes the unbounded places of N . -Initial marking m 0,2 is the union of m 0,1 and of the restriction of the initial marking m 0 of N to its unbounded place P u . -Finally, the set of transitions of N 2 is the set T 1 of transitions of N 1 , and the flow relations are defined in the following way. Let t 1 ∈ T 1 corresponding to a transition t ∈ T in the original net N . We have p ∈ t 1 if:

• p ∈ P 1 and p ∈ • t 1 (arc from p to t 1 in N 1 ), or • p ∈ P u and there was an arc from p to t in N .

Similarly, we have p ∈ t 1 if p ∈ P 1 and p ∈ t 1 • (arc from t 1 to p in N 1 ), or if p ∈ P u and there is an arc from t to p in N . Case: the transition is start t p . Then it is easy to see that m (q) = m(q) for all q but for m(p) = m (p) {age}, m(1 t q ) = ∅ and m (1 t q ) = 0. It is easy to check that m satisfies the hypothesis wrt m . As m is known to be reachable in Timed(N ), we conclude.

Case t makes time elapse by δ unit of time. m and m agrees on the bounded places, hence as the urgency is not violated in m by elapsing δ unit of time, it is not violated in m by elapsing δ unit of time. Thus m + δ is reachable in Timed(N ). Last, it is easy to see that m + δ satisfies the hypothesis wrt m = m + δ.

Case t ∈ T . If • t has only bounded places, then m and m agree on these places, and one can apply t from m to obtain m + which satisfies the hypothesis wrt m . Else, consider an unbounded place q ∈ • t ∩ Q. Thus I(t) = [a, +∞). We have m (1 q ) = {nage q } with nage q ≥ a. Thus there exists age q ∈ m(q) with age q ≥ age q . In particular, t is enabled wrt q. This is true for all q, so t is enabled from m. Denote m + the reached configuration of Timed(N ) after deleting the chosen tokens age q with age q ≥ nage q . Now, firing t in m creates the same tokens in the same place with the same age 0 as firing t from m . It deletes token m (1 q ) and one token in q of age bigger or equal. Hence we still have for all q ∈ Q, m + (q) = m (q) {age 1 , • • • age k } and there exists a bijection f : T q → [1, k] with m (1 t q ) ≤ age f (t) for all t ∈ T q . That is, m + satisfies the hypothesis wrt m .

Fig. 1 .

 1 Fig. 1. Timed Petri Net with Urgency N1.

Fig. 2 .

 2 Fig. 2. Timed Petri Net with Urgency N2.

Lemma 3 .

 3 N and N 2 are (untimed) bisimilar. The bisimulation relation we use is: (m, ν) is in relation with m 2 iff there exists m u a marking of P u and m = m b ∪ m u , m 2 = m 1 ∪ m u with (m b , ν b ) bisimilar to m 1 according to Lemma 2. Lemma 3 thus completes the proof of proposition 3.

Lemma 4 .

 4 Let m be a reachable marking of Reach(Timed(N )). Then there exists a marking m ∈ Reach(Timed(N )) with m ≡ m . Lemma 5. Let m be a reachable marking of Reach(Timed(N )). Then one can reach in Timed(N ) any m with:

  Thus we indeed have m2 δ -→ m 2 + δ t -→ m 2and the proof is completed by induction.

  a timed word of N 1 and thus of N B the bounded part of N .Let m b be a timed marking of N B reached by this timed word. Then we prove by induction that (t 1 , d 1 ) • • • (t n , d n ) is a timed word of N reaching m = m b ∪ m u . The initial step is trivial for the empty timedword. Induction step: Let δ = d n -d n-1 and t = t n . Let m 2 such that m 2 δ -→ m 2 + δ t -→ m 2 in N 2 , with m 2 = m 1 ∪ m u decomposed between P 1 and P u , and let m b such that m b δ -→ m b + δ t -→ m b in N B the bounded part of N . By the induction hypothesis, the timed marking m

  First, δ time units can elapse from m b in N B , and thus it can elapse from m in N because N is a Timed PNrU. Further, tokens consumed from m b + δ t -→ m b can be consumed in m as well, and so do tokens consumed from P u in the transition m 2 + δ t -→ m 2 . Thus we indeed have m δ -→ m + δ t -→ m and the proof is completed by induction.

Lemma 6 .

 6 Timed(N ) and N 2 are (untime) bisimilar.Proof. A timed marking m of Timed(N ) can be decomposed as m = m b ∪ m u , where m b is the restriction of m to bounded places, and m u the restriction to unbounded places. Similarly, a marking of N 2 can be decomposed into m 2 = m 1 ∪ m u again by restriction to bounded/unbounded places. Form proposition 5 and from the construction of N 1 , we know that Timed(N B ) is bisimilar to N 1 , and we denote by R B,1 the unique largest bisimulation from timed markings of Timed(N B ) to markings of N 1 .We denote by R a relation from timed markings of Timed(N ) to markings of N 2 as follows. Let m = m b ∪ m u be a marking of Timed(N ) andm 2 = m 1 ∪ m u be a marking of N 2 . Then, (m, m2) ∈ R iff (m b , m 1 ) ∈ R B,1 , and m u = m u . Obviously, we have (m 0 , m 0,2 ) ∈ R. We can now prove that R is a bisimulation. Let (m, m 2 ) ∈ R. Assume that m δ -→ m+δ t -→ m in N . Thus m b δ -→ m b +δ t -→ m b in N b with m b the bounded part of m . Furthemore, m u ≥ • t ∩ P u . Thus we have m 1 t -→ m 1 in N 1 , and furthermore, (m 1 , m b ) ∈ R B,1. By definition of N 2 , firing t results in a flow of tokens among places of P u that is identical (regardless of ages) in N and in N 2 , so we indeed havem 1 ∪ m u t -→ m 1 ∪ m u . Furthermore m u = |m u , so (m , m 1 ∪ m u ) ∈ R.Conversely, assume that m 2 t -→ m 2 . We denote m 2 = m 1 ∪ m 3 and m 2 = m 1 ∪ m 3 where m 3 , m 3 denote respectively the projections of m 2 and m 2 on P u . In particular, t as t can fire, we have m 1 t -→ m 1 . So, there exists a marking m b of Timed(N B ) such that (m b , m 1 ) ∈ R B,1 and there exists δ such that m b δ -→ m b + δ t -→ m b . Now, N is a TPN with restricted constraints. First, it means that m δ -→ m + δ does not violate any urgency constraints, as they are all in the bounded part of N . Now, we want to show that m + δ t -→ m is possible in N , for some m u with m = m b ∪ m u and(m u ) = m 3 . First, because (m, m 2 ) ∈ R, with m 2 = m 1 ∪ m 3 , we have m (p) = m 3 (p) ≥ 1 for all p ∈ P u ∩ • t. Also, we have trivially that m (p) = m b (p) ≥ 1 for all p ∈ P B ∩ • t as t is enabled from m 1 ,and (m b , m 1 ) ∈ R b , 1. Thus t is enabled. Now, m+δ respects all the timings constraints of t: as N is a TPN with restricted constraints, all constraints apply to the bounded part. Transition t is enabled from m 1 , thus t can fire from m + δ. For the unbounded part, firing of t can consume any token in places of P u ∩ • t and we easily get (m u ) = m 3 . For the bounded part, we chose to consume the tokens consumed during the transition m b + δ m -→ b . We thus obtain m = m b + m u , and (m , m 2 ) ∈ R. Hence R is a bisimulation relation.Lemma 6 thus complete the proof of proposition 5 for the timed semantics. Thus we can decide reachability in Timed(N ) for N a TPN with restricted constraints.

  Note that as m(p) is a multiset, two tokens in place p may have identical ages.We will say that a transition t is enabled from a timed marking m if and only if for each p ∈ • t, there exists age p ∈ m(p) such that age p ∈ γ(p, t). A transition t is urgent from a timed marking m if ∀p ∈ • t, ∃age p ∈ m(p) such that α(p, t) + U (t) ≤ age p ≤ β(p, t). Notice that any urgent transition t is enabled. An urgent transition t will force occurrence of a discrete move, but not necessarily of this transition t as several transitions can be enabled (or even urgent) at the same time. As formally defined below, presence of urgent transitions disallows time from elapsing. Because of this, for every reachable urgent transition t, there will exist a place p ∈ • t such that the oldest token age p ∈ m(p) with age p ≤ β(p, t) will satisfy age p = α(p, t) + U (t). Formally, the semantics of Timed PNU is decomposed into timed moves and discrete moves.Timed moves symbolize elapsing of δ time units from a timed marking in the following way: for a given timed marking m, we denote by m + δ the timed marking obtained by adding δ to the age of every token: if m(p) = {age 1 , . . . , age k }, then (m + δ)(p) = {age 1 + δ, . . . , age k + δ}. A timed move of δ > 0 time units is allowed from m if for every 0 ≤ δ < δ, the timed marking m + δ has no urgent transition, and we denote m Discrete moves represent firings of transitions from a marking m. One can fire transition t from marking m and reach marking m , denoted m \ S p ) S p , where -S p = {age p } where age p ∈ m(p) ∩ γ(p, t) if p ∈ • t, and S p = ∅ otherwise.-S p = {0} if p ∈ t • , and S p = ∅ otherwise.

	t -→ m iff t is enabled
	and for each place p, we have m (p) = (m(p)

• , m 0 , γ, U ) in terms of timed markings and discrete and timed moves. For a given place p and timed marking m, we will denote by age ∈ m(p) real values from m(p), depicting the age of one token in place p. δ -→ m + δ such time moves.

  assume that we have an age age p ∈ m(p) greater than m(p t ). A necessary condition for firing the transition t is both τ (p t ) ≥ a and age p ≥ a. This necessary condition can be summed up as min(τ (p t ), age p ) ≥ a. It is actually what our construction does: keeping min(τ (p t ), age p ) for some age of a token in p, because it is uncessary to know the real age of age p if older than τ (p t ). Notice that this condition holds with both the original and the timed semantics of TPNs.

Appendix

We present the detailed proofs below.

Proposition 1. Let N be a simple TPN. Then Timed(N ) and N are timed bisimilar.

Proof. The bisimulation relation R between reachable configurations of N and reachable timed markings of Timed(N ) is the following. We associate a timed marking m of Timed(N ) to each configuration (m, ν) of N , with m (p) = m(p) for all p ∈ P , and such that (P1) holds:

(P1) for all t ∈ En(m), ν(t) = min p∈ t (max p ), with max p the oldest token in m (p) for all p. Recall that p t ∈ t. Notice that we can safely consider max p as by definition β(p, t) = +∞ for all p, t.

We prove that for each pair (m, ν), m in R a timed or discrete move a is allowed from (m, ν) if and only if a is also allowed from m , and the resulting configurations and timed marking is in R. Clearly, ((m 0 , ν 0 ), m 0 ) ∈ R.

Take (m, ν), m ∈ R. Thus m (p) = m(p) for all p ∈ P and (P1) holds. First, assume that the elapse of δ units of time is possible from (m, ν). It means that no urgent transition is met after δ < δ units of time. In particular, for all t ∈ En(m), ν(t) + δ ≤ B(t). As ν(t) = min p∈ t (max p ), there exists p ∈ t with max p +δ ≤ B(t) = A(t) + (B(t) -A(t)) = α(p, t) + U (t), thus t is not urgent in m either for any δ . Both moves are allowed, and we have ((m, ν + δ), m + δ) ∈ R as ν(t) = min p∈ t (max p ), with max p the oldest token in m (p), we have ν + δ(t) = ν(t) + δ = min p∈ t (max p ) + δ = min p∈ t (max p ), with max p the oldest token in m + δ(p). Symetrically, if a δ time units move is possible from m , then it is possible from (m, ν) as well and lead to this same bisimilar configuration. Now we address discrete moves: let t be a transition fireable from configuration (m, ν), and leading to configuration (m 2 , ν 2 ). Thus t ∈ En(m) and ν(t) ∈ I(t). For all p ∈ t, max p ≥ ν(t) ≥ A(t) = α(t), hence t is enabled in m . When firing t from a timed marking of a Timed PNU, there is no unicity of the set of tokens consumed for each place. Hence, we can obtain several timed markings m 2 . No matter the chosen m 2 , we get easily m 2 (p) = m 2 (p) for all p ∈ P .

To finish proving that ((m 2 , ν 2 ), m 2 ) ∈ R, we need to show that P 1 holds. Let max p denote the maximal value of a token in the timed marking m 2 . For all tt ∈ En(m 2 ), we have several cases:

On the other hand, we also have that p ∈ t • (else tt would not be in En(m 2 )) and m 2 (p) = {0}. Hence max p = 0 and hence min q∈m 2 (max q ) = 0, that is P 1 holds. -Else, if tt ∈ En(m), we have max p = max p for any place p in tt, as no token from tt has been consumed. We hence have ν 2 (tt) = ν(tt) = min p∈ tt (max p ) = min p∈ tt (max p ), and P 1 holds.

Proof of Theorem 4

Let (N , P, Q), with N = (P ∪ Q, T, • (), ()

• , m 0 , λ, I) be a TPNrU, where P is the set of bounded states and Q the set of unbounded states. We prove the two remaining lemmas.

Lemma 5. Let m be a reachable marking of Reach(Timed(N )). Then one can reach in Timed(N ) any m with:

m ≡ m and for all p ∈ P ∪ P T , we have m (p) = m(p) and for all t ∈ T , p ∈ P , we have either m (0 t p ) = ∅ or m (0 t p ) = m (p t ), and for all q ∈ Q, letting

Proof. of Lemma 5. We proceed by induction on the lenght of run reaching m in N .

For run of lenght 0, this is trivial. Assume that m is reached after applying t from m -. Let m be any marking satisfying the condition above wrt m. Let us show that we can reach m in Timed(N ). Assume that t let time elapse by δ > 0 units of time. For all p ∈ P ∪ Q, for all age p ∈ m(p), age p ≥ δ. We first show that for all p ∈ P , for all age p ∈ m (p ), age p ≥ δ. For q = 1 t p for some t, p, we have m (q) = {min(m(p t ), age p )} with age p ∈ m(p). Now, we have m(p t ) ≥ δ and age p ≥ δ. For other p ∈ P , age ∈ m (p), there exists p ∈ P ∪ Q with age ∈ m(p). We thus obtain for all p ∈ P , for all age ∈ m (p ), age ≥ δ. Hence we can define m = m -δ as a marking.

The number of tokens in m, m -is the same, and the number of tokens in m , m is the same (only timing changed). Thus, as m ≡ m , we have m -≡ m . Now, m -≡ m satisfies the conditions above, we can thus apply the induction hypothesis telling us that m is reachable in Timed(N ). Now, waiting δ units of time from m is allowed in Timed(N ) as it does not violate any urgency. Indeed, by contradiction, if the urgency of t is violated, it implies that I(t) = [a, b] and thus • t ⊆ P is made of only bounded places. As m -and m coincide on bounded places, it would also violate urgency on m -, which is by definition not the case, a contradiction. Hence δ units of time can ellapse from m , and the marking reached is m . That is, m is reachable in Timed(N ). Now, consider t a discrete transition. Let say (age p ) p∈ • t are the tokens which are consumed by t from m -to m. Let S - q = {0} if q ∈ t • and ∅ otherwise. We have m(p t ) = 0. Thus for all q ∈ • t, m (1 t q ) = ∅ or m (1 t q ) = 0. We define m in the following way with m -≡ m :

for all p ∈ P ∪ P T , we have m (p) = m -(p).

-For all q ∈ Q, let t q be the (possibly ) transition and nage q be the (possible ) token age with • If t ∈ T q (in particular q ∈ • t and m (1 t q ) = {0}), then t q = t, and nage q is the token associated with m (1 t q ) = {min(nage q , 0}, • Else, (m (1 t q ) = ∅) if q ∈ t • and 0 / ∈ m (q), then we let t q be any transition with m (1 tq q ) = {0}, and nage q = 0,

• Else t q = nage q = , In both case, a token of nage q ∈ m (q) has just been consumed with a start tq q to create a token with age 0 in m (1 tq q ). for all q ∈ Q, we have m (q) = m (q) {nage q } \ S - q , for all t ∈ T, q ∈ • t ,

, Let show that m -≡ m satisfies the hypothesis. First, for every p ∈ P ∪ P t , this is trivial. Now let q ∈ Q. We have m -(q) S - q = m(q) S q . We have m(q) = {age tt | tt ∈ T q } m (q).

Hence m -(q) = m (q) {age tt | tt ∈ T q \ {t q }} {age tq } S q \ S - q . Now, for all tt ∈ T q \ {t q } (in particular, tt = t), we have m (1 t q ) = m (1 t q ), thus this part is covered. Also, if q ∈ • t, then S q = {age q } is the token associated with m (1 t q ) = min(m -(p t ), age q ). It remains m (q) {age tq } \ S - q to associate with m (q) = m (q) {nage q } \ S - q , which is trivial (either nage q = 0 and any token can be associated with it, or else nage q is by definition the token associated with age tq .).

Hence by the induction hypothesis, m is reachable in Timed(N ). Now performing t from m then start tq q for all q such that t q = , we obtain m . That is, m is reachable in Timed(N ).

We turn now to the proof of the other lemma.

Lemma 4. Let m be a reachable marking of Reach(Timed(N )). Then there exists a marking m ∈ Reach(Timed(N )) with m ≡ m . Proof. of Lemma 4.

We will prove by induction on the size of a path that if one can reach m in Timed(N ), then one can reach m in Timed(N ) with m ≡ m , for all p ∈ P ∪ {p t | t ∈ T }, m(p) ≥ m (p), let T q be the set of t ∈ T such that m(1 t q ) = ∅ for all q ∈ Q, for all q ∈ Q, m(q) = m (q) {age 1 , • • • age k } and there exists a bijection f :

T q → [1, k] with m (1 t q ) ≤ age f (t) for all t ∈ T q .

For m = m 0 , this is trivial. Induction step: Let m be a reachable marking of Timed(N ). A path reaching m ends with m → (t)m . Hence m is reached in less steps than m , and we can apply the induction hypothesis. One can reach m in Timed(N ) with:

m ≡ m , for all p ∈ P ∪ {p t | t ∈ T }, m(p) ≥ m (p), let T q be the set of t ∈ T such that m(1 t q ) = ∅ for all q ∈ Q, for all q ∈ Q, m(q) = m (q) {age 1 , • • • age k } and there exists a bijection f : T q → [1, k] with m (1 t q ) ≤ age f (t) for all t ∈ T q .


Sihem Loukil
email: sihem.loukil@redcad.org

Slim Kallel

Ismael Bouassida Rodriguez

Mohamed Jmaiel

Monitoring of Quality of Service in Dynamically Adaptive Systems

Dynamic reconfiguration has been widely recognized as an effective approach to deal with the increasing complexity of dynamically adaptive systems. One of the main challenges in such systems is to provide guarantees about the required runtime quality of service (QoS) attributes, such as performance, reliability, etc. Therefore, it is of paramount importance to make these systems able to monitor the QoS parameters that allow to evaluate such QoS attributes, analyze these parameters in order to detect QoS changes and therefore trigger reconfiguration actions. In this paper, we propose an approach that allows monitoring the QoS parameters of a dynamically adaptive system in order to detect QoS degradation. The proposed approach is based on the Aspect-Oriented Software Development (AOSD) paradigm which allows to keep the monitoring code separated from the business logic code.

Introduction

Dynamically Adaptive Systems that can automatically adapt to changes in their environments are increasingly requested [START_REF] Salehie | Self-adaptive software: Landscape and research challenges[END_REF]. To further increase its usability and reliability, such system needs to keep a certain Quality of Service (QoS) level during its execution. Therefore, it should be able to monitor some quantifiable parameters that allow to evaluate its QoS attributes. Such monitoring allows detecting degradation in the QoS of the system and therefore adapt its structure and/or behavior autonomously in response to this degradation.

As dynamically adaptive systems change behavior and structure at runtime, the monitoring of the QoS of such system poses some challenges. First, these systems need to continuously monitor QoS parameters in order to detect QoS degradation. These parameters are collected from different interacting entities that may be distributed which may require several QoS monitors displayed at different levels. Second, the level of the QoS specification is relatively low which requires access to source code to specify or modify QoS parameters such as data rate, error rate, etc. Thus, it is desirable to specify QoS parameters at a higher level of abstraction and then automatically map these specifications to source code while providing sufficient flexibility. Third, the QoS concern need to be considered in several parts of the system. Mixing such concerns with business logic concerns increases the complexity of the system and makes both its development and maintenance more difficult [START_REF] Dowling | The k-component architecture meta-model for self-adaptive software[END_REF].

In our previous work [START_REF] Loukil | Managing architectural reconfiguration at runtime[END_REF][START_REF] Loukil | Verifying runtime architectural reconfiguration of dynamically adaptive systems[END_REF], we presented an approach which mainly consists in conceiving a whole development process of dynamically adaptive systems ranging from modeling to code generation. This approach allows to specify componentbased systems and ensure their reconfiguration at runtime. It allows to handle both the anticipated and unanticipated reconfigurations at design time. This approach is based on the combination of the Architecture Analysis and Design Language (AADL) [START_REF]SAE: Architecture Analysis & Design Language[END_REF] and its aspect oriented extension AO4AADL [START_REF] Loukil | Toward an Aspect Oriented ADL for Embedded Systems[END_REF][START_REF] Loukil | Ao4aadl: Aspect oriented extension for aadl[END_REF].

In this paper, we present how our approach can be applied to monitor the QoS of a dynamically adaptive system. For this purpose, we first define and classify QoS parameters that can be monitored at runtime. The proposed classification is based on the architectural vision of distributed component-based systems. More specifically, this classification is tied to distributed component-based systems specified using AADL concepts. Second, we detail how our approach allows specifying QoS parameters at a high level of abstraction using the AOSD paradigm. In fact, several aspects are defined in our work in order to monitor QoS parameters at runtime. These aspects are specified at architectural level using the AO4AADL language. These AO4AADL aspects will be the input of an AspectJ generator, developed in our previous work [START_REF] Loukil | Toward an Aspect Oriented ADL for Embedded Systems[END_REF][START_REF] Loukil | Ao4aadl: Aspect oriented extension for aadl[END_REF], in order to generate aspects in AspectJ [START_REF] Kiczales | An overview of aspectj[END_REF]. These aspects will be automatically weaved with the functional code of the system to obtain the final code to be executed. Third, we present how these high level QoS specifications are automatically transformed to executable code that allows the system to continuously monitor QoS parameters at runtime in order to detect QoS degradation.

The remainder of this paper is structured as follows: In Section 2, we present our proposed QoS classification for distributed component-based systems. Section 3 presents the proposed approach to ensure the monitoring of QoS parameters. An illustrative example is introduced in Section 4. Section 5 presents some research studies related to our work. Finally, Section 6 concludes the paper and gives some directions for future work.

Quality of Service : parameters and classification

We propose a classification of the QoS parameters in order to make easier the evaluation of the QoS attributes of a software system. This classification is inspired from the one proposed by the standard ISO/IEC 9126 [START_REF] Organization | ISO/IEC 9126: Information Technology -Software Product Evaluation -Quality Characteristics and Guidelines for Their Use[END_REF]. This standard proposes to classify the QoS attributes into two categories : (1) internal quality attributes which are properties of subsystems and components, and (2) external ones that are visible on the system level. Inspired from this classification, we propose to classify the QoS parameters based on the architectural vision of a distributed component-based system specified using AADL concepts.

From an architectural perspective, the software architecture of a distributed component-based system (system in AADL) is composed of a set of communicating composite components (processes in AADL). Similarly, each composite component is composed of a set of interconnected indivisible components (threads in AADL). The communication between components is ensured via a set of connections (connection in AADL). Our idea consists in classifying QoS parameters according to the level at which such parameter can be monitored. An indivisible component and a composite component in AADL have the same architectural structure. For this reason, we consider that QoS parameters that can be monitored at indivisible component level and at composite component level are the same. We distinguish three levels of QoS monitoring according to the structure of distributed component-based systems : indivisible component/composite component level, architecture level and communication level.

The adopted generic QoS attributes that can be measured and evaluated at runtime for a distributed component based system are :

-Performance is an indication of the responsiveness of a system. It can be measured in terms of throughput, latency and processing time. -Reliability is the ability of a system to remain operational over time. It can be measured through the loss rate of transmitted messages. -Load Balancing is the distribution of workloads across system components.

It can be measured as the distribution of the components on the system.

Overview of the proposed approach

In this section, we present a general overview of our proposed approach towards specifying and monitoring QoS parameters in order to detect QoS degradations.

Our approach involves a main component namely a QoS manager. This later is defined at two levels : at the composite component level (process level) to be able to manage QoS parameters of its interacting AADL subcomponents (threads), and at the architecture level to manage the QoS parameters of the interacting AADL composite components (processes) that form the whole system architecture. At both levels, the QoS manager is in change of monitoring QoS parameters, analyzing collected data and perform reconfiguration actions when QoS degradations are detected. Therefore, the activity of the QoS manager is divided into three main modules.

-A QoS monitor module : This module is composed of a set of monitoring aspects responsible for monitoring and collecting QoS parameters. Gathered QoS parameters are stored into a QoS database for further retrieval. -A QoS analyzer module : Towards inspecting the collected information and track down QoS degradation. This module sends notifications to the reconfiguration module when QoS degradation is detected in order to trigger appropriate reconfiguration actions. -A reconfiguration module : Defines a list of reconfiguration actions that can be applied to the system when QoS degradations are detected. These reconfigurations are encapsulated into a set of reconfiguration aspects.

The proposed QoS manager is then able to handle a closed feedback loop (MAPE) with four phases : Monitoring, Analysis, Planning and Execution. In this paper, we focus on the first phase of the MAPE loop. For this purpose, we detail in the following how the QoS parameters are specified at architectural level using AO4AADL aspects. We present also some examples of the generated AspectJ code from such AO4AADL specifications. These AspectJ aspects will ensure the monitoring of the QoS parameters at runtime.

QoS monitoring

Monitoring the QoS of a dynamically adaptive system aims to observe its constituting components to collect data about QoS parameters. This monitoring is performed through a set of AspectJ aspects that are automatically generated from a high level QoS specification using the AO4AADL language. In fact, our proposed QoS monitor module is composed of a set of architectural monitoring aspects specified in AO4AADL. These aspects are intended to intercept the architectural elements through which QoS parameters can be captured.

As mentioned previously, the QoS parameters can be monitored at three levels. For each level, we define the considered QoS parameters and we give some examples of the structure of the AO4AADL aspects used to specify such QoS parameters. Such aspect is composed of two parts : pointcut and advice. The pointcut defines the architectural element to intercept in order to get the value of the corresponding QoS parameter. The advice defines the information value to save in the QoS database. We present also some examples of the generated AspectJ code from AO4AADL specifications to ensure the monitoring of QoS parameters at runtime.

QoS parameters monitored at indivisible/composite component level

Throughput is the number of sent messages through a set of output ports of a given indivisible or composite component within a time interval. Formula 1 is used to calculate this information.

T hroughput c = T hroughput outporti (1)
-i={1..p}, p ≤ n and n = the number of output ports of the component.

-T hroughput outporti is the number of sent messages through an output port of the component within a given time interval.

The monitoring of the throughput is achieved through one AO4AADL aspect whose structure is given in Listing 1.1. The pointcut (lines 2-3) of such an aspect intercepts the set of output ports of the given component to be monitored. The advice (lines 7-13) captures the number of sent messages through this set of output ports. Once the time interval of monitoring is elapsed, this advice sends the captured number of sent messages to the QoS database. Loss rate of messages defines, within a time interval, the percentage of unprocessed messages compared with the number of received messages by a given component. This information can be measured only for components characterized as follows: To each input port that receives a message corresponds an output port that sends a result. To compute this information, we use formula 2.

Loss c = 1 - T hroughput outporti Input inporti (2)
-i={1..p}, p ≤ n and n = the number of output ports of the component.

-Input inporti is the number of received messages through an input port of the component within a given time interval.

To monitor the loss rate of messages within an indivisible/composite component, two architectural aspects are needed. The first aspect is intended to capture the throughput of the considered component. The second aspect captures the number of received messages through the set of input ports of the component.

Processing time measures the elapsed time to execute an operation within a given component. It is measured using the following formula:

T ime P rocop = T ime EndExecop -T ime StartExecop (3)
-T ime EndExecop is the end time of execution of the operation.

-T ime StartExecop is the start time of execution of the operation.

One architectural aspect is needed to monitor the processing time. This aspect intercepts the execution of the subprogram that corresponds to the operation to be monitored. Two types of advices are defined in this aspect : a before advice which will capture the start time of the execution and an after advice that will capture the end time of execution.

QoS parameters monitored at architecture level Distribution measures the dispersion rate of a specified component type C i on the set of composite components of the system. This information is related to the architectural style of the system. It is monitored at architecture level since its computation requires knowledge of the total number of components deployed throughout the system. It is measured for each composite component using formula 4:

Distribution node = N ode components(Ci) System components(Ci) (4)
-N ode components(Ci) is the number of components of type C i deployed in a given composite component. -System components(Ci) is the number of components of the same type C i deployed in the whole system.

The monitoring of the distribution parameter is performed through a set of aspects. One aspect is attached to every composite component that may contain components of type C i . The structure of the corresponding AO4AADL aspect is given in Listing 1.3. The number of components of type C i deployed on one composite component can change due to reconfiguration actions that can affect the system during its execution. To be able to capture the new number of components of type C i within one composite component, the aspect should intercept the reconfiguration actions related to the addition, removal and migration of components (lines 2-4). Therefore, after each invocation of one of these reconfiguration actions, the aspect transmits the new number of components of type C i to the QoS database module (lines 8-12). Distribution can refer also to the dispersion rate of a specified composite component type N i on the system. This information is monitored on a cluster of composite components. The formula used to monitor such parameter is similar to formula 4 except that here we are interested in composite components instead of indivisible components. To monitor such paramter, an aspect is attached to each composite component of the cluster. Such aspect intercepts the reconfiguration action related to the connection and disconnection of composite components of type N i and transmits the new number of these components to the QoS database.

QoS parameters monitored at communication level

Loss rate of messages measures, within a time interval, the percentage of lost messages through a connection. This parameter is computed using formula 5.

Loss conn = Received msg Sent msg (5)
-Received msg is the number of received messages through the destination port of the connection. -Sent msg is the number of sent messages through the source port of the connection.

Two architectural aspects should be specified to monitor such QoS parameter. One aspect is used to monitor the throughput of the source output port of the connection. The other aspect is intended to monitor the number of received messages through the destination input port of the connection.

Latency represents the elapsed time to transfer a message through a given connection. Formula 6 is used to compute this parameter.

Latency conn = T ime Receiptmsg -T ime Sendingmsg (6)
-T Receiptmsg is the receipt time of the message on the destination port.

-T Sendingmsg is the sending time of the message through the source port.

The monitoring of this QoS parameter needs the specification of two architectural aspects as mentioned in the previous QoS parameter. The only difference here lies in the advice part. In fact, the first aspect in this case is intended to capture the sending time of the message through the source output port of the connection and the second one is responsible of capturing the receipt time of this message on the destination input port of the connection.

All gathered QoS parameters from the monitoring module are stored in a QoS database for later use by the analysis module in order to be able to detect QoS degradations. This QoS database allows keeping a trace of all the captured QoS parameters for further retrieval when needed.

Illustrative example

To demonstrate the benefits of our approach, we introduce the Flood Prediction System (FPS) [START_REF] Hughes | Gridstix: Supporting flood prediction using embedded hardware and next generation grid middleware[END_REF] as an illustrative example. This system presents a set of nodes that communicate and cooperate to carry out flood predictions. Three types of components are considered : sensor nodes, computation nodes and office nodes.

Sensor nodes sense and collect the data relevant for calculations such as pressure, rainfall, and temperature. Sensed data are periodically transmitted to the corresponding computational node. Computation nodes connect the sensor nodes, examine the data correctness and maintains a record of all draw values. Some calibrations are performed on the draw data. Later, a prediction operation is invoked to execute some static measurements in order to provide prediction on river flow. This prediction is transmitted to the office node. The Office Node verifies the results with the available online information, predicts for the entire region, issues alerts and initiates evacuation procedures.

In the following, we will detail the usefulness of monitoring the considered QoS parameters using aspects.

Processing time To ensure more system reliability, the processing time of data within computation nodes should not be out of a certain time interval. Results provided so quickly or so late are not reliable for prediction measurements performed at the office node level. Therefore, the processing time of subprograms responsible for data checking, calibration and prediction should be monitored. Listing 1.4 presents the AO4AADL aspect to monitor such QoS parameter. Distribution Due to several reconfiguration actions or to nodes failure, the distribution of sensor nodes may be unfair. For example, let's suppose that we dispose of three computation nodes. The first one is connected to six sensor nodes (2 sensor nodes of each type), the second one is connected to three sensor nodes (one sensor node of each type), however, no sensor node is connected to the third one. To ensure a fair distribution of sensor nodes along the river, three sensor nodes (one of each type) which are connected to the first computation node should be disconnected from this later and connected to the third computation node. Listing 1.5 presents the structure of the AO4AADL aspect responsible for monitoring the distribution. This aspect is attached to every computation node of the system and intercepts the addition and removal of connections between a sensor node and a computation node. Authors in [START_REF] Rosenberg | Bootstrapping performance and dependability attributes of web services[END_REF] propose an approach for monitoring the QoS of web services. This approach relies on monitoring tools such as Jpcap for latency measurement. It is based on aspect-oriented programming and requires implementation details. Therefore, this approach stills implementation dependent, as the language of coding aspect is dependent on the selected programming language. Our approach is different since it allows the monitoring of QoS parameters through specifying architectural aspects at a high level of abstraction (architectural level) independently from the programming language.

Authors in [START_REF] Mdhaffar | Aop4csm: An aspect-oriented programming approach for cloud service monitoring[END_REF] present an approach to Cloud service monitoring based on Aspect-Oriented Programming. This approach monitors QoS parameters using AspectJ aspects. Similarly to [START_REF] Rosenberg | Bootstrapping performance and dependability attributes of web services[END_REF], aspects are hard coded and the approach is dependent on the selected programming language.

The work presented in [START_REF] Zhang | Aspect-oriented qos modeling for cyber-physical systems[END_REF] proposes an aspect-oriented QoS specification method based on the combination of UML and RTL. The main objective of this approach is to specify the QoS parameters separately from the system concerns and facilitate their monitoring. Similarly to our approach, this work allows to specify the QoS parameters at a high level of abstraction. However, no details are mentioned about the code generation of these aspects.

Conclusion and Future work

In this paper, we have proposed an approach for monitoring QoS attributes in dynamically adaptive systems. For this purpose, we proposed a QoS parameters classification taking into account the level at which a QoS parameter can be monitored in the case of a distributed component-based system specified using AADL concepts. We presented later how our approach ensures the monitoring of the QoS parameters using the AOSD paradigm. First, these QoS parameters are specified into AO4AADL. Then, they are automatically translated into AspectJ code to ensure the monitoring of these parameters at runtime.

As future work, we aim to focus on the analysis and reconfiguration phases. We plan to apply our approach to specific domains such as event-based systems.

1 aspect Monitoring_Throughput_<Identifier> { 2 pointcut

 2 Throughput_<Identifier>(): execution(outport(<Out_port_identifier_1>(..))) 3 || ... ||execution (outport(<Out_port_identifier_n>(..)));

4 variables{counter: 6 7 10 counterListing 1 . 1 : 5 6 13 COUNTER

 461011513 Integer_Type; t : Time_Type;} 5 initially{counter = 0; t=System.currentTimeMillis()+period;} advice after(): Throughput_<Identifier> (){ 8 if(System.currentTimeMillis()<t){counter:=counter+1;} 9 else if(System.currentTimeMillis()=t){ Monitoring the throughput of a component Listing 1.2 presents the generated AspectJ code from Listing 1.1. The interception of the execution of the output port is transformed to the interception of the method sendOutput() of the PortsRouter class (lines 3-4). This class carries out the correct routing of messages through ports. Moreover, the subprogram send Value is transformed to a simple execution of the method send ValueImpl() of a generated SubPrograms class (line 14). PortsRouter.sendOutput(<Out_port_identifier_1>(..))) 4 || ... ||execution (* PortsRouter.sendOutput(<Out_port_identifier_n>(..))); public static final GeneratedTypes.IntegerType COUNTER = new GeneratedTypes.IntegerType(0); 7 public static final GeneratedTypes.TimeType T = 8 new GeneratedTypes.TimeType(System.currentTimeMillis()+period);9 10 void after(): Throughput_<Identifier> (){ 11 if(System.currentTimeMillis()<T){COUNTER = COUNTER+1;} 12 else if(System.currentTimeMillis()==T){ ()+period;}}} Listing 1.2: Generated AspectJ code from Listing 1.1

1 aspect Monitoring_Distribution { 2 pointcut

 2 Distribution(): execution(subprogram(addThread(ComponentType,..))) 3 || execution(subprogram(removeThread(ComponentType,..))) 4 || execution(subprogram(migrateThread(ComponentType,..)));

12 } 13 } 1 . 3 :

 121313 "addThread") {counter:=counter+1;} 10 else if((this="removeThread") or (this="migrateThread")) {counter:=counter-1;} 11 send_Value!(counter); Listing Monitoring the distribution on a composite component

1 aspect Monitoring_ProcTime_CompNode { 2 pointcut

 2 ProcTime_CompNode(): execution(subprogram(Data_Checking(..))) 3 || execution(subprogram(Calibration(..))) 4 ||execution(subprogram(Prediction(..)));

5 6

 5 advice before(): ProcTime_CompNode(){send_Time!(System.currentTimeMillis());} 7 advice after(): ProcTime_CompNode(){send_Time!(System.currentTimeMillis());}} Listing 1.4: Monitoring the processing time

1 aspect Monitoring_Distribution_Cluster { 2 pointcut

 2 Distribution_Cluster(): 3 execution(subprogram(ConnectNodes(SensorNode, ComputationNode))) 4 || execution(subprogram(ConnectNodes(SensorNode, ComputationNode))) 5 || execution(subprogram(DisconnectNodes(SensorNode, ComputationNode))) 6 || execution(subprogram(DisconnectNodes(SensorNode, ComputationNode)));

  ): Distribution_Cluster (){ 12 if (this="ConnectNodes") {counter:=counter+1;} 13 else if(this="DisconnectNodes"){counter:=counter-1;} 14 send_Value!(counter);}} Listing 1.5: Monitoring the distribution on a cluster of nodes 5 Related work