Hanifa Boucheneb
email: hanifa.boucheneb@polymtl.ca

Didier Lime
email: didier.lime@ec-nantes.fr

Olivier H Roux
email: olivier-h.roux@ec-nantes.fr

Charlotte Seidner
email: charlotte.seidner@univ-nantes.fr

Optimal-cost reachability analysis based on time Petri nets

This paper investigates the optimal-cost reachability problem in the context of time Petri nets, where a rate cost is associated with each place. This problem consists in deciding whether or not there exists a sequence of transitions reaching, with minimal cost, a given goal marking. This paper shows that for some subclasses of cost time Petri nets, the optimalcost reachability problem can be solved more efficiently using a method based on the state classes, without resorting to linear programming or splitting state classes.

I. INTRODUCTION

Time Petri nets (TPNs for short) are a simple yet powerful formalism useful to model and verify real-time, concurrent systems that are therefore subject to time constraints. In TPNs, a firing interval, associated with each transition, specifies the minimum and maximum duration it must be maintained enabled before its firing. Thus, TPNs can model time constraints, even when the exact delays or durations of events are not known. The verification of a TPN is based on the state space abstraction that takes into account the time constraints of the model, while preserving its markings and firing sequences.

This paper deals with the cost time Petri nets (cTPNs for short) and investigates the optimal cost reachability problem. A cTPN is a TPN extended with rate costs associated with its places. The rate cost of a place p is the sojourn cost (per time unit) of each token in place p. These rate costs do not affect the behaviour of the TPN but they allow to determine the sojourn cost in each marking and also the cost of firing a sequence of transitions.

The optimal cost reachability problem can be stated as the problem of deciding if there exists a sequence of transitions ω that allows to reach with minimal cost a given goal marking. Starting from the initial marking, the marking of the model evolves by firing transitions. Each time a transition is fired, some tokens are consumed and some others are produced. We define, for each transition t, a rate cost called incidence rate cost of t as the sum of rate costs of tokens produced by t minus the sum of rate costs of tokens consumed by t. We show that for sequences such that the incidence rate costs of their transitions are all non-negative or all non-positive, their optimal-costs can be computed more efficiently based on the state class method without using techniques of linear programming or decomposing state classes, as done previ-ously. Moreover, we show how to compute the optimal-cost of sequences such that the firing interval of their transitions are all singular. Therefore, the optimal cost reachability problem can be solved more efficiently for some subclasses of cTPNs.

Such subclasses might seem restrictive but can in fact model a wide range of applications. Consider for instance a leak in a pressure pipe: until its fixing, the rate at which the water leaks will surely increase, as the leak keeps getting larger. The subclass of model can also describe any economic system based on rarefying resources such as oil or Bitcoins, where the cost of things keep increasing.

The optimal-cost reachability problem has been addressed for Priced Timed Automata (PTAs for short) in [START_REF] Alur | Optimal paths in weighted timed automata[END_REF]- [START_REF] Bouyer | Symbolic optimal reachability in weighted timed automata[END_REF] using the region graphs and the zone based graphs. In [START_REF] Alur | Optimal paths in weighted timed automata[END_REF], the authors have proved the decidability of the optimal-cost problem for PTAs with non-negative costs. In [START_REF] Behrmann | Minimum-Cost Reachability for Priced Timed Automata[END_REF]- [START_REF] Larsen | As cheap as possible: Efficient cost-optimal reachability for priced timed automata[END_REF], the computation of the optimal-cost to reach a goal location is based on a forward exploration of zones extended with linear cost functions. The linear cost function of a zone gives the optimal-costs to reach each state within the zone. In [START_REF] Bouyer | Symbolic optimal reachability in weighted timed automata[END_REF], the authors have improved the approach, developed in [START_REF] Behrmann | Minimum-Cost Reachability for Priced Timed Automata[END_REF]- [START_REF] Larsen | As cheap as possible: Efficient cost-optimal reachability for priced timed automata[END_REF], so as to ensure termination of the forward exploration algorithm, even when clocks are not bounded and costs are negative, provided that the PTA is free of negative cost cycles.

For priced timed/time Petri nets, the optimal-cost reachability problem has been addressed in [START_REF] Abdulla | Priced timed Petri nets[END_REF], [START_REF] Boucheneb | Optimal reachability in cost time Petri nets[END_REF]. In [START_REF] Abdulla | Priced timed Petri nets[END_REF], the considered model is a timed arc Petri net, under weak firing semantics, extended with rate costs and firing costs associated with places and transitions, respectively. The computation of the optimal-cost for reaching a goal marking is based on similar techniques to those of PTAs [START_REF] Alur | Optimal paths in weighted timed automata[END_REF]. In [START_REF] Boucheneb | Optimal reachability in cost time Petri nets[END_REF], the authors have investigated the optimal-cost reachability problem for time Petri nets where each transition has a firing cost and each marking has a rate cost (represented as a linear rate cost function over markings). To compute the optimal-cost to reach a goal marking, the authors have first revisited, to include costs, the state class graph method and then reduced the computation, as all other techniques, to a linear programming problem.

The rest of the paper is organised as follows. Section II is devoted to the TPN model, its semantics and its state class graph method. Section III presents the TPN extended with costs considered here and then defines the cost of a run and the optimal-cost of a sequence. It also shows how to rewrite the cost of a run based on the incidence rate costs of its transitions. Section IV investigates efficient computation procedures of the optimal-cost of firing a sequence of transitions from a state class that need neither minimisation techniques nor splitting state classes. Section V shows by means of a case study how the optimal-costs are computed. Section VI concludes the paper by some future work.

II. TIME PETRI NETS A. Definition and semantics

Syntactically, a time Petri net is a Petri net where a firing time intervals is associated with each transition.

Let N, Z, Q + and R + be the set of non-negative integers, the set of integers, the set of non-negative rational numbers and the set of non-negative real numbers, respectively. Let Q + [ ] be the set of non-empty intervals of R + whose bounds are in Q + and Q + ∪ {∞}, respectively. For an interval I ∈ Q + [ ] , ↓ I and ↑ I denote its lower and upper bounds, respectively.

Formally, a TPN is a tuple N = (P, T, pre, post, M 0 , Is) where P and T = {t 1 , ..., t m } (with m > 0) are finite sets of places and transitions such that P ∩ T = ∅, pre and post are the backward and the forward incidence functions (pre, post :

P × T -→ N), M 0 is the initial marking (M 0 : P -→ N),
and Is is the static firing interval function (Is :

T → Q + [ ]
). Let N = (P, T, pre, post, M 0 , Is) be a TPN, M : P -→ N a marking and t i a transition of T . Transition t i is enabled for M iff all required tokens for firing t i are present in M , i.e., ∀p ∈ P, M (p) ≥ pre(p, t i ).

In this paper, we use the original semantics of the TPN [8]: If a transition is multi-enabled in some state, only one instance of this transition is considered (single-server semantics), and when a transition is fired, all transitions disabled and enabled again, during this firing, are newly enabled.

We denote En(M ) the set of all transitions enabled for M , i.e., En(M

) = {t i ∈ T | ∀p ∈ P, pre(p, t i ) ≤ M (p)}.
If M results from firing some transition t f from some marking, N w(M, t f ) denotes the set of all transitions newly enabled in M , i.e., N w(M, t

f ) = {t i ∈ En(M ) | t i = t f ∨ ∃p ∈ P, M (p) -P ost(p, t f ) < pre(p, t i )}.
The TPN state is defined as a pair s = (M, I), where M is a marking and I is a firing interval function (I :

En(M ) → Q + [ ] )
. The initial state of the TPN model is s 0 = (M 0 , I 0 ) where I 0 (t i ) = Is(t i ), for all t i ∈ En(M 0 ). The TPN state evolves either by elapsing time or by firing transitions. When a transition t i becomes enabled, its firing interval is set to its static firing interval Is(t i ). The bounds of this interval decrease synchronously with time, until t i is fired or disabled by another firing. t i can fire if the lower bound of its firing interval reaches 0 but must fire, without any additional delay, as far as any conflict avoids it, if the upper bound of its firing interval reaches 0. The firing of a transition takes no time and leads to a new marking.

Let (M, I) and (M ′ , I ′ ) be two interval states of the TPN model, θ ∈ R + and t f ∈ T . We write (M, I) θ -→ (M ′ , I ′ ), also denoted (M, I) + θ, iff from state (M, I), we reach the state (M ′ , I ′ ) by a time progression of θ units, i.e.,

∀t i ∈ En(M ), θ ≤ ↑ I(t i ), M ′ = M and ∀t j ∈ En(M ′ ), I ′ (t j ) = [M ax(↓ I(t j ) -θ, 0), ↑ I(t j ) -θ]
We write (M, I) t f -→ (M ′ , I ′ ) iff from state (M, I), we reach the state (M ′ , I ′ ) by firing immediately the transition t f , i.e.,

t f ∈ En(M ), ↓ I(t f ) = 0 ∀p ∈ P, M ′ (p) = M (p) -pre(p, t f ) + post(p, t f ) and ∀t i ∈ En(M ′ ), I ′ (t i ) = Is(t i ) if t i ∈ N w(M ′ , t f ) I(t i ) otherwise.
We also use the abbreviation (M, I)

θt f -→ (M ′ , I ′ ) for (M, I) θ -→ (M, I) + θ t f -→ (M ′ , I ′ ).
The TPN state space is the transition system (S, -→, s 0 ), where s 0 is the initial state of the TPN and S = {s|s 0 * -→ s} ( * -→ being the reflexive and transitive closure of the relation -→ defined above) is the set of reachable states of the model.

A run in the TPN state space (S, -→, s 0 ), starting from a state s 1 , is a sequence σ = s 1 θ1t1 -→ s 2 θ2t2 -→ s 3 . . .. Sequences θ 1 t 1 θ 2 t 2 . . . and t 1 t 2 . . . are the timed trace and the trace (firing sequence) of σ, respectively. A marking M is reachable iff ∃s ∈ S s.t. its marking is M . The runs of a TPN are all the maximal runs starting from its initial state s 0 .

B. State class graphs

Among the TPN state space abstractions proposed in the literature, we consider here the state class graph (SCG) [START_REF] Berthomieu | State class constructions for branching analysis of time Petri nets[END_REF], [START_REF] Boucheneb | A more efficient time Petri net state space abstraction useful to model checking timed linear properties[END_REF]. A SCG state class α consists of a marking M and a conjunction F of atomic constraints1 over the firing dates of the enabled transitions in marking M and the firing date, denoted by t 0 of the transition leading to α. It represents an over-approximation of the set of states reached by the same firing sequence from the initial TPN state. Note that for convenience purposes, firing delays in the classical SCG state classes in [START_REF] Berthomieu | State class constructions for branching analysis of time Petri nets[END_REF] are replaced by firing dates. The formula F characterises the union of the firing date domains of all states within α, reached by the same firing sequence from the initial state of the TPN.

The initial SCG state class of the TPN is the pair α 0 = (M 0 , F 0 ), where M 0 is the initial marking and

F 0 = ti∈En(M0) ↓ Is(t i ) ≤ t i -t 0 ≤ ↑ Is(t i ),
where t i is a non-negative real valued variable representing the firing date of the transition t i and t 0 is a variable representing the date of α 0 , which is supposed to be 0 for the initial state class.

From the practical point of view, F is represented by a Difference Bound Matrix (DBM in short) [START_REF] Bengtsson | Clocks, DBMs and States in Timed Systems[END_REF]. The DBM of F is a square matrix D, indexed by variables of F . Each entry d ij represents the atomic constraint t it j ≤ d ij . If there is no upper bound on t it j with i = j, d ij is set to ∞. Entry d ii is set to 0. Although the same non-empty domain may be encoded by different DBMs, they have a canonical form. The canonical form of a DBM is the representation with tightest bounds on all differences between variables, computed by propagating the effect of each entry through the DBM. A DBM can be seen as the matrix representation of a graph, called a constraint graph [START_REF] Cormen | Introduction to Algorithms[END_REF]. Its canonical form can be computed in O(n 3 ), n being the number of variables in the DBM, using a shortest path algorithm, like Floyd-Warshall's all-pairs shortest path algorithm [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF].

Let C S be the set of all syntactically correct SCG state classes and succ a state class successor function:

C S × T -→ C S ∪ {∅}, defined by: ∀α = (M, F ) ∈ C S , ∀t f ∈ T , • succ(α, t f ) = ∅ iff t f ∈ En(M ) and the following for- mula is consistent (i.e., satisfiable): F ∧( t∈En(M) t f ≤ t).
Intuitively, it means that t f is enabled in M and t f is firable from α before all other transitions enabled at M . In other words, t f is enabled in M and there is, at least, a valuation of firing dates in F s.t. t f has the smallest firing date.

• If succ(α, t f ) = ∅ then succ(α, t f ) = (M ′ , F ′ ), where: ∀p ∈ P, M ′ (p) = M (p) -pre(p, t f ) + post(p, t f ) and F ′ is computed in 3 steps: 1) Set F ′ to F ∧ t∈En(M) t f ≤ t ∧ t∈N w(M,t f ) ↓ Is(t) ≤ t -t f ≤↑ Is(t).
Notice that without loss of generality, for economy of notations, we suppose that the transitions of En(M ) are different from those newly enabled by transition t f from M . 2) Put F ′ in canonical form 2 .

3) Eliminate t 0 and all variables associated with transitions of CF (M, t f ) -{t f } and rename t f in t 0 . Canonical forms make operations over DBMs much simpler [START_REF] Bengtsson | Clocks, DBMs and States in Timed Systems[END_REF]. Two state classes are said to be equal iff they have the same canonical form (i.e., they have the same marking and the DBMs of their formulas have the same canonical form). Note that, in the following, we will use indifferently (M, F ) or (M, D) to refer to the state class α, and we suppose that all DBMs are in canonical form. DBM canonical forms allow also to reduce the complexity of the firing rule as follows [START_REF] Boucheneb | A more efficient time Petri net state space abstraction useful to model checking timed linear properties[END_REF].

Let α = (M, D) be a state class and t f ∈ T a transition.

• t f is firable from α iff t f ∈ En(M ) ∧ ∀t i ∈ En(M ), d if ≥ 0.
• If t f is firable from α then its successor state class by t f is the state class α ′ = (M ′ , D ′ ), where M ′ and the canonical form of the DBM of D ′ are computed as follows:

∀p ∈ P, M ′ (p) = M (p) -pre(p, t f ) + post(p, t f ) and ∀t i , t j ∈ En(M ′ ), d ′ i0 =    ↑ Is(t i ) if t i ∈ N w(M, t f ), d if if t i / ∈ N w(M, t f ), d ′ 0j =    -↓ Is(t j ) if t j ∈ N w(M, t f ), M in tu∈En(M) d uj if t j / ∈ N w(M, t f ), d ′ ij =        0 if i = j, M in(d ij , d ′ i0 + d ′ 0j ) if i = j ∧ t i , t j / ∈ N w(M, t f ), d ′ i0 + d ′ 0j otherwise III. COST TIME PETRI NETS

A. Definition and semantics

A cost time Petri net (cTPN for short) is a time Petri net where a rate cost is associated with each place, giving the sojourn cost per time unit of each token in that place. Formally, a Cost Time Petri Net is a tuple N c = (P, T, pre, post, M 0 , I s , r) where:

• N = (P, T, pre, post, M 0 , I s ) is a TPN, • r : P -→ Z is a rate cost function that associates a rate cost with each place of the TPN. Note that no cost is associated with the discrete firings of transitions; however, these costs can be added without affecting the results provided in this paper.

Let N c be a cTPN, t ∈ T a transition and M a marking of the cTPN. We denote by rm(M ) the rate cost of M :

rm(M ) = p∈P M (p) × r(p).
The rate costs of places can be defined as in [START_REF] Boucheneb | Optimal reachability in cost time Petri nets[END_REF] by a linear function over markings. We define the incidence rate cost of t by:

rt(t) = p∈P (post(p, t) -pre(p, t)) × r(p).
Intuitively, it represents the impact of firing t on the rate cost of a marking.

The semantics of a cTPN N c = (P, T, pre, post, M 0 , I s , r) is the semantics of the TPN N = (P, T, pre, post, M 0 , I s ). However, the rate costs associated with places allow to compute different costs such as the costs of runs and the optimal costs of firing a sequence from a state or a state class of N .

B. Cost of a run

Let

s 1 = (M 1 , I 1 ) be a state of N c and σ = (M 1 , I 1 ) θ1t1 --→ (M 2 , I 2 ) • • • (M n , I n ) θntn ---→ (M n+1 , I n+1 ) a run of s 1 .
The cost of σ is defined by:

Cost(σ) = n i=1 (θ i × rm(M i )).
Let τ 0 the date at which the state s 1 is reached and

τ j = τ 0 + j i=1
θ i be the firing date of the transition t j in σ, for j = 1, n. Proposition 1 rewrites Cost(σ) by means of the firing dates and incidence rate costs of transitions of σ (see Fig. 1). As we will show, this form is more useful to deal with the optimal-cost problem in some cases. The optimal-cost of Cost(σ) can be also rewritten by means of the firing dates and the rate costs of markings as shown in Proposition 2.

Proposition 1:

Cost(σ) = rm(M 1 ) × (τ n -τ 0 ) + n-1 j=1 rt(t j ) × (τ n -τ j ). Proof: By definition, Cost(σ) = n i=1 (θ i × rm(M i )). For i = 2, n, the rate cost of the successor marking M i of M i-1 by t i is rm(M i ) = rm(M i-1 )+rt(t i-1 ). Therefore, for i = 2, n, rm(M i ) = rm(M 1 ) + i-1 j=1 rt(t j ).
Then:

Cost(σ) = θ 1 × rm(M 1 ) + n i=2 (θ i × (rm(M 1 ) + i-1 j=1 rt(t j ))).
It can be developed and rewritten as follows:

θ 1 × rm(M 1 )+ θ 2 × (rm(M 1 ) + rt(t 1 )) + ....+ θ n × (rm(M 1 ) + rt(t 1 ) + rt(t 2 ) + .... + rt(t n-1 )).
Finally, Cost(σ) can be rewritten so as the rate cost of M 1 (i.e., rm(M 1 )) is the coefficient of n i=1 θ i , the incidence rate cost of t 1 (i.e., rt(t 1 )) is the coefficient of n i=2 θ i , ..., and so on, the incidence rate cost of t n-1 (i.e., rt(t n-1 )) is the coefficient of θ n . It follows that:

Cost(σ) = rm(M 1 ) × ( n i=1 θ i ) + n-1 j=1 rt(t j ) × ( n i=j+1 θ i ).
To achieve the proof, it suffices to replace

n i=1 θ i with τ n -τ 0 and n i=j+1 θ i with τ n -τ j . Proposition 2: Cost(σ) = ( n-1 i=1 -rt(t i ) × τ i ) + rm(M n ) × τ n . Proof: By definition, Cost(σ) = n i=1 (θ i × rm(M i )). For i = 1, n, θ i = τ i -τ i-1
. Then:

Cost(σ) = n i=1 ((τ i -τ i-1 ) × rm(M i ))
.

For i = 1, n -1, the rate cost of the successor marking M i+1 of M i by t i is rm(M i+1 ) = rm(M i ) + rt(t i ). Therefore, for i = 1, n -1, rt(t i ) = rm(M i+1 ) -rm(M i ).
The previous expression of Cost(σ) can be developed and rewritten as follows:

(

n-1 i=1 (rm(M i ) -rm(M i+1 ) × τ i ) + rm(M n ) × τ n .
To achieve the proof, it suffices to replace rm(M i )rm(M i+1 ) with -rt(t i ).

C. Optimal cost of a firing sequence

Let α 1 be a state class of

N c and ρ = α 1 t1 -→ α 2 • • • α n tn -→ α n+1 a path of α 1 , ω = t 1 • • • t n and Π(α 1 , ω)
the set of runs of α 1 that support the same sequence of transitions ω and lead to states of α = α n+1 . The optimal-cost of firing ω from α 1 (or the optimal-cost of ρ) is:

OptCost(α 1 , ω) = M in σ∈Π(α1,ω) Cost(σ).
The optimal-cost of firing ω from α 1 can be computed by extending state classes with costs and using linear programming techniques as in [START_REF] Boucheneb | Optimal reachability in cost time Petri nets[END_REF].

D. Optimal-cost reachability problem

The classical forward exploration algorithm in [START_REF] Behrmann | Minimum-Cost Reachability for Priced Timed Automata[END_REF]- [START_REF] Larsen | As cheap as possible: Efficient cost-optimal reachability for priced timed automata[END_REF], [START_REF] Boucheneb | Optimal reachability in cost time Petri nets[END_REF] is adapted in Algorithm 1 to compute the optimal-cost to reach, from the initial marking, a marking belonging to a given set of markings Goal. For each state class α such that its marking is in Goal, its optimal-cost is computed and compared with M inCost, where the smallest cost computed so far is saved. As usual, the lists P assed and W aiting are used to store the already processed and not yet processed state classes, respectively. The notation ω ≺ ω ′ means that ω is a prefix of ω ′ .

For bounded TPNs with no negative cost cycles, the algorithm terminates as for infinite sequences only finite prefixes, yielding the longest elementary paths, are explored.

In the following sections, we investigate cases where the optimal-costs of firing sequences can be computed without splitting state classes nor using linear programming techniques.

IV. COMPUTING OPTIMAL COST OF FIRING SEQUENCES

Let

α 1 = (M 1 , F 1 ) be a state class of N c and ρ = α 1 t1 -→ α 2 • • • α n tn -→ α n+1 a path of α 1 and ω = t 1 • • • t n .
For ease of notation, we suppose that all transitions within En(M 1 ) and those enabled by every transition of ω are all different. The firing date domain of transitions of ω from α 1 can be retrieved by modifying the firing rule given in Section II-B. Indeed, it suffices, in step 3 of succ(α i , t i ), for i ∈ [1, n], to keep t i . More precisely replace step 3 with: Eliminate all variables associated with transitions of CF (M i , t i ) -{t i }. With this modification, each variable t i , for i ∈ [1, n], represents the firing date of the i th transition of ω. The variable t 0 is the τ1 τ2

... τn-1 τn if M ∈ Goal and OptCost((M 0 , D 0 ), ω) < M inCost then 7:

τ 0 rt(t 2 ) × (τn -τ 2 ) rm(M 1 ) × (τn -τ 0 ) rt(t n-1 ) × (τn -τ n-1 ) rt(t 1 ) × (τn -τ 1 )
M inCost ← OptCost((M 0 , D 0 ), ω) 8: end if 9:
if (for all end if 13: end while 14: return M inCost date when α 1 is reached. Let F G be the resulting formula. The firing date domain of transitions of ω from α 1 is the projection of the domain of F G to t i for i ∈ [0, n].

((M ′ , D ′ ), ω ′ ) ∈ P assed, ((M ′ , D ′ ) = (M, D)) or ¬(ω ′ ≺ ω))

A. Case of non-negative incidence rate costs

For this section, we suppose that the incidence rate costs of all transitions of ω, except the last one are non-negative and rm(M 1 ) ≥ 0. We will show that, under these assumptions, to compute the optimal-cost of firing ω from α 1 , we need to keep track of the minimal delay between the previously fired transitions and the coming ones, including the current one. But we do not need to retrieve delays between the previously fired transitions. Consequently, the relevant part of F G needed to compute the optimal-costs can be represented by a DBM of order (|ω| + 1) × |En(M ) ∪ {t n }|.

We denote by G the DBM in canonical form of order

(|ω| + 1) × |En(M ) ∪ {t n }| defined by ∀i ∈ [0, |ω|], ∀t j ∈ En(M ) ∪ {t n }, g ij = M ax(t i -t j |F G).
Since t it j ≤ 0, the value -g ij is the minimal delay between the firing dates t j and t i . Note that G is a sub-matrix of the DBM in canonical form of F G. The size of the DBM of F G is

(|ω| + 1 + |En(M )|) 2 . Theorem 1: OptCost(α 1 , ω) = -g 0n × rm(M 1 ) + n-1 i=1 rt(t i ) × -g in .
Proof: Let GG be the DBM in canonical form of F G. Recall that G is a sub-matrix of GG. To achieve the proof, we first show that the valuation v i = g ing 0n for i ∈ [1, n] is a feasible firing schedule for ω, i.e., for i, k

∈ [1, n], -gg 0i ≤ v i ≤ gg i0 and v i -v k ≤ gg ik . By definition, for i ∈ [1, n], v i = g in -g 0n = gg in -gg 0n , then for i, k ∈ [1, n], v i -v k = g in -g kn = gg in -gg kn . Since
GG is in canonical form, it holds that gg in ≤ gg i0 + gg 0n , gg 0n ≤ gg 0i + gg in , and gg in ≤ gg ik + gg kn . It follows that -gg 0i ≤ v i ≤ gg i0 and v iv k ≤ gg ik . The run corresponding to this firing schedule of ω is shown in Fig. 2. Its cost is:

-g 0n × rm(M 1 ) + n-1 i=1 rt(t i ) × -g in .
By assumption, rm(M 1 ) ≥ 0 and for i ∈ [1, n-1], rt(t i ) ≥ 0. Furthermore, for i ∈ [0, n], -g in is the minimal value of t n -t i in F G, where t n is the firing date of last transition of ω. Therefore, OptCost(α

1 , ω) = -g 0n × rm(M 1 ) + n-1 i=1 rt(t i ) × -g in .
According to the definition of G, for ω = ǫ, G is a DBM of order 1 × (|En(M )| + 1) defined by ∀t j ∈ En(M ) ∪ {t 0 }, g 0j = d 0j . Let us show now how to compute progressively the DBM G of a nonempty sequence.

Proposition 3: Let α be the state class reached by a path ρ, G the corresponding DBM and t f a transition firable from α and α ′ = (M ′ , D ′ ) = succ(α, t f ).

Then, the DBM G ′ of the path ρ

t f -→ (M ′ , D ′ ) is the DBM in canonical form of order (|ωt f |+ 1)× |En(M ′ )∪{t f }| defined by: ∀i ∈ [0, |ωt f |] and t j ∈ En(M ′ ) ∪ {t f }, g ′ ij =        M in(g ij , g if + d ′ 0j ) if i ≤ |ω| ∧ t j ∈ N w(M, t f ) g if + d ′ 0j if i ≤ |ω| ∧ t j ∈ N w(M, t f ) d ′ 0j if i = |ωt f | where d ′ 0j = M in tu∈En(M) d uj , if t j / ∈ N w(M, t f ) and d ′ 0j = -↓ Is(t j ), otherwise.
Proof: The proof is based on the constraints added to compute succ(α, t f ). Indeed, the firing condition is obtained by adding to D, the constraints: t f ≤ t u , for t u ∈ En(M ) and ↓ Is(t j ) ≤ t jt f ≤↑ Is(t j ), for t j ∈ N w(M, t f ).

Notice that all the added constraints involve t f and in the corresponding constraint graph, they are represented by arcs (t f , t u , 0), for t u ∈ En(M ), (t j , t f , ↑ Is(t j )) and (t f , t j , -↓ Is(t j )), for t j ∈ N w(M, t f ). Therefore, the shortest path connecting a node t i , for i ∈

[0, |ωt f |], to a node t j ∈ En(M ′ ) is: M in(g ij , g if + M in tu∈En(M) d uj ), if t j ∈ N w(M, t f ) and g if -↓ Is(t j ), otherwise.
By the firing rule given in II-B, it holds that:

d ′ 0j =    -↓ Is(t j ) if t j ∈ N w(M, t f ), M in tu∈En(M) d uj if t j / ∈ N w(M, t f ),
Note that, M in tu∈En(M)

d uf = 0 as t f is firable. Consequently, g ′ if = g if , for i ∈ [0, |ωt f |]. For i = |ωt f |, g ′ ij = d ′ 0j as g ′ ij is the smallest path connecting t f to t j .
The computation of the optimal-cost of firing ω from α 1 needs to carry in the DBM G the minimal firing delay between each fired transition of ω and the coming ones, including the current one. Thus, the size of G grows with the size of ω: indeed, the optimal-cost of ωt f is reached when t f is fired as soon as possible (i.e., -g nf = -d 0f ) from α and the previous ones are fired as late as possible (i.e., -g if ) without causing any delay to t f . It means that, to retrieve the firing schedule yielding the optimal-cost of ω, the firing dates of its previous transitions need to be updated to take into account the fact that t f is fired as soon as possible and the previous ones are fired as late as possible but before t f . However, for bounded TPNs with no negative cost cycles, each infinite sequence ω ′′ of N c , has some prefix ω followed by a repetitive sequence ω ′ that loops on a state class α reachable from the initial state class α 0 by ω. It follows that OptCost(α 0 , ω) ≤ OptCost(α 0 , ω ′′ ) and OptCost(α, ω ′ ) ≤ OptCost(α, ω ′k ), for k ≥ 1. The cost of a cycle is nonnegative, if the sum of the incidence rate costs of all its transitions is non-negative and the rate cost of one of its marking is non-negative. This sufficient condition guarantees for a cycle a non-negative cost.

In the following, we investigate the possibility to reduce the size of the DBM G.

B. Memoryless state classes w.r.t. optimal-costs

Let α = (M, D) be the state class reached by a sequence ω from a state class α 1 of N . The state class α is said to be memoryless w.r.t. optimal-costs iff for each sequence

ω ′ of α, OptCost(α 1 , ωω ′ ) = OptCost(α 1 , ω) + OptCost(α, ω ′ )
Therefore, for any state classes α 1 and α ′ 1 leading by sequences ω and ω ′ , respectively, to the same memoryless state class α = (M, D) w.r.t. optimal-costs, it holds that for each firable sequence ω ′′ from α,

OptCost(α 1 , ω) ≤ OptCost(α ′ 1 , ω ′ ) ⇒ OptCost(α 1 , ωω ′′ ) ≤ OptCost(α ′ 1 , ω ′ ω ′′ )
Lemmas 1 and 2 provide two different sufficient conditions for the state class α to be memoryless w.r.t. optimal-costs. The first one depends on the DBM G of ω. The second one depends on α.

Lemma 1: Let α = (M, D) be the state class reached by some sequence ω = t 1 • • • t n from a state class α 1 = (M 1 , D 1 ) and G the DBM of its firing domain. If ∀i ∈ [0, |ω|], ∀t j ∈ En(M ), g ij = g in + d 0j then, α is memoryless w.r.t. optimal-costs.

Proof: Suppose that ∀i ∈ [0, |ω|], ∀t j ∈ En(M ), g ij = g in + d 0j . Let us show that for every sequence ω ′ of α, OptCost(α 1 , ωω ′ ) = OptCost(α 1 , ω) + OptCost(α, ω ′ ). We consider 2 cases: 1) ω = t 1 ...t n and ω ′ = t j , and

2) ω = t 1 ...t n and |ω ′ | > 1. 1) Case ω = t 1 ...t n and ω ′ = t j : Since ∀i ∈ [0, |ω|], g ′ ij = g in + d 0j .
Consequently, if t j is firable from α = (M, D) then the optimal-cost of the successor of α by t j is:

OptCost(α 1 , ω) + (rm(M 1 ) + i∈[1,|ω|] rt(ω(t i ))) × -d 0j . Note that rm(M ) = rm(M 1 ) + i∈[1,|ω|] rt(ω(t i )) and rm(M ) × -d 0j is the optimal-cost of firing t j from (M, D). 2) Case ω = t 1 ...t n and |ω ′ | > 1: Suppose that in the DBM G ′ of ω ′ from α, ∀t j ∈ En(M ′ ), g ′ ij = g in + c j
, where c j does not depend on i and is the opposite of the minimal delay between firing dates of t j and t n . Let us show that in any extended sequence of ω ′ by any firable transition t k leading to the state class (M ′′ , D ′′ ), it holds that ∀t j ∈ En(M ′′ ), g ′′ ij = g in + c ′ j , where c ′ j does not depend on i and is the opposite of the minimal delay between firing dates of t j and t n , and G ′′ is the DBM of the extended path. By Proposition 3,

∀t j ∈ En(M ′′ ) ∪ {t n }, if t j ∈ N w(M ′ , t k ) then, g ′′ ij = M in(g ′ ij , g ′ ik + M in tu∈En(M ′ ) d ′ uj ) = g in + M in(c j , c k + M in tu∈En(M ′ ) d ′ uj ).
Otherwise,

g ′′ ij = g ′ ik -↓ Is(t j ) = g in + c k -↓ Is(t j ).
Then, g ′′ ij = g in + c ′ j , where c ′ j does not depend on i and c ′ j is the opposite of the minimal delay between the firing dates of t j and t n (the proof of this claim is similar to the one provided for Proposition 3). Therefore, the optimal reachability cost of any extended sequence ωω ′ of ω is the sum of OptCost(α 1 , ω) and the optimal cost of firing ω ′ from α (i.e., OptCost(α, ω ′ )).

Lemma 2: Let α = (M, D) be a state class such that all transitions of En(M ) are newly enabled in M . Then, α is memoryless w.r.t. optimal-costs.

t 1 t 2 ... t n-1 t n t 0 -g 2n -g 0n -g (n-1)n -g 1n
Fig. 2. The run corresponding to the firing schedule v i = g ing 0n , for i ∈ [1, n], of ρ Proof: Suppose that α is reached from some state class α 1 by a sequence ω = t 1 • • • t n and G the DBM of its firing domain. As all transitions of α are newly enabled, it follows that ∀i ∈ [0, |ω|], ∀t j ∈ En(M ), g ij = g in + d 0j . According to Lemma 1, α is memoryless w.r.t. optimal-costs.

Thanks to lemmas 1 and 2, when a memoryless state class α w.r.t. optimal-costs is reached, there is no need to explore its successors, in case there is in the list P assed an identical memoryless state class with smaller optimal-cost. Among the identical memoryless state classes reached by different paths, the one with the smallest optimal-cost will yield the optimal reachable cost, for all state classes reachable from α. Therefore, Algorithm 1 can be improved for this subclass of cTPNs.

C. Case of non-positive incidence rate costs

For this section, we suppose that the incidence rate costs of all transitions of ω, except the last one, are non-positive and rm(M n ) ≥ 0.

Theorem 2: Let ρ = α 1 = (M 1 , D 1 ) t1 -→ α 2 = (M 2 , D 2 ) • • • α n = (M n , D n ) tn -→ α n+1 = (M n+1 , D n+1 ) be a path in the SCG of N c , supporting the sequence ω = t 1 • • • t n .
Let GG be the DBM in canonical form of F G (the firing domain transitions of ω and those enabled in M n ). Then,

OptCost(α 1 , ω) = ( n-1 i=1 rt(t i ) × gg 0i ) -gg 0n × rm(M n ).
Proof: We first show that the valuation v i = -gg 0i for i ∈ [1, n] is a feasible firing schedule for ω, i.e., for i, k ∈

[1, n], -gg 0i ≤ v i ≤ gg i0 and v i -v k ≤ gg ik . By definition, for i ∈ [1, n], v i = -gg 0i , then for i, k ∈ [1, n], v i -v k = gg 0k -gg 0i . Since GG is in canonical form, it holds that gg 0k ≤ gg 0i + gg ik . It follows that -gg 0i ≤ v i ≤ gg i0 and v i -v k ≤ gg ik . By assumption, rm(M n ) ≥ 0 and for i ∈ [1, n-1], rt(t i ) ≤ 0. Furthermore, for i ∈ [0, n],
-gg 0i is the minimal value of t i in F G (i.e., the firing date of the i th transition of ω). By Proposition 2, the cost of each run supporting the sequence ω is:

( n-1 i=1 -rt(t i ) × τ i ) + rm(M n ) × τ n . Therefore, OptCost(α 1 , ω) = ( n-1 i=1 rt(t i ) × gg 0i ) -rm(M n ) × gg 0n .

D. Case of singular intervals

For this section, we suppose that the firing intervals of all transitions of ω are singular but the incidence cost rate of each transition of ω is negative, null or positive.

Theorem 3: Let ρ = α 1 = (M 1 , D 1 ) t1 -→ α 2 = (M 2 , D 2 ) • • • α n = (M n , D n ) tn -→ α n = (M n+1 , D n+1 ) be a path in the SCG of N c , supporting the sequence ω = t 1 • • • t n . Then, OptCost(α 1 , ω) = n i=1 -d i0i × rm(M i ).
Proof: The cost of each run σ = (M 1 , I 1 )

θ1t1 --→ (M 2 , I 2 ) • • • (M n , I n ) θntn ---→ (M n+1 , I n+1 ) supporting ω is: n i=1 (θ i × rm(M i )). The domain of each θ i , for i ∈ [1, n], [-d i0i , d ii0 ].
As the firing interval of all transitions of ω are singular, each transition is fired at an exact date. Therefore, for i ∈

[1, n], -d i0i = d ii0 .

V. CASE STUDY

In the French academic system, faculty positions with both teaching and research activities can be held either by an associate professor (maître de conférences, or MCF) or by a full professor (professeur des universités, or PU). In this system, a typical career path is:

• start as an associate professor at the 1st grade (échelon 1); • get promoted to higher grades; such promotions are automatic and usually3 happen every 34 months (that is, 2 years and 10 months after the last promotion); • after some years, defend a habilitation thesis and obtain a higher degree (known as the habilitation à diriger des recherches), a qualification needed to supervise PhD students; • depending on the opportunities, get a promotion from associate to full professor; keep getting automatic promotions to higher grades according to seniority 4 . To each grade corresponds an indice (a salary scale grade), on which the salary is based; additionally, when promoted from associate to full professor, the indice cannot decrease.

Let us consider the case of an associate professor who reaches the 4th échelon when 32 years old. Let us further suppose that the university wishes that all faculty members become full professors and reach the last grade by the time they are 55. Obviously, the cheapest way for the university to reach this goal is to promote anyone at the latest possible time: given the durations between grades, this means letting the person reach the 9th grade after 14 years and 10 months; keep them in that grade for 2 years and 8 months; promote them to full professor and let them reach the last grade after 5 years and 6 months.

However, this strategy does not take into account the frustration of the person, which increases each time a promotion is denied, starting from the moment they reach the 6th grade and begin questioning their life choices.

We propose a model for this optimisation problem, shown in Fig. 3 5 . Each place with a M CF xyz label corresponds to a grade in the associate professor scale; its rate cost is equal to xyz (and is actually equal to the indice for this grade). Similarly, each place with a P U xyz label corresponds to a grade in the full professor scale. In the following, we give various values to R = r(unhappy) so as to show the interest of our method; the rate cost of all the other places is set to 0.

The state class graph of the model is depicted in Fig. 4 and Table I; note that a total of 10 paths in the SCG lead to a marking where goal contains 1 token; in the following, we denote Goal the set of such markings.

To keep the model simple enough, it should be noted that it does not guarantee that the place goal is attained when the person is exactly 55 years old (a token could stay in place wait for more than 0 time unit, for instance). However, we can show that, in the following, all optimal-cost strategies are such that the place goal is attained as early as possible, that is, after 23 years.

Let us first set R = 0. The optimal cost of each path leading to a marking in Goal is given in Table II and the minimum is equal to 208 668. The computation steps of this cost are reported in Fig. 5: as expected, the optimal strategy is to give the promotion at the latest possible time, thus leading to the following timed trace6 : echelon5@34, echelon6@34, echelon7@42, echelon8@34, echelon9@34, up6@32, PUech6@42, chevron2@12, chevron3@12, age55years@0, end@0.

Let us now change the value of R; whenever R ≤ 32, the optimum strategy remains the same. For R = 33, the strategy consists in giving the promotion not too early, just before switching from 6th to 7th grade. The timed trace, with a total cost of 228 480, is: echelon5@34, echelon6@34, up3@42, PUech4@12, PUech5@12, PUech6@42, chevron2@12, chevron3@12, age55years@76, end@0.

Whenever R ≥ 34, the strategy consists in giving the promotion just before risking unhappiness, that is right before switching from 5th to 6th grade. For R = 35, the computation steps are reported in Fig. 6 and the timed trace, with a total cost of 228 660, is: echelon5@34, up2@34, PUech3@12, PUech4@12, PUech5@12, PUech6@42, chevron2@12, chevron3@12, age55years@106, end@0.

VI. CONCLUSION

This paper deals with the optimal-cost reachability problem in the context of time Petri Nets extended with costs (cTPNs). It establishes, for some interesting subclasses of cTPNs, efficient algorithms that compute the optimal-cost of firing a sequence of transitions from a given state class. Unlike the approaches developed in [START_REF] Alur | Optimal paths in weighted timed automata[END_REF]- [START_REF] Boucheneb | Optimal reachability in cost time Petri nets[END_REF], the algorithms, presented here, are not based on techniques of linear programming. Finally, a case study is provided to show the interest of the proposed method.

As a future work, we will investigate the optimal-cost reachability problem in the context of parametric cTPNs.

Fig. 1 .Algorithm 1

 11 Fig. 1. The cost of the run σ based on the firing dates and incidence rate costs of its transitions

  then

10 :

 10 add ((M, D), ω) to P assed 11: for all t ∈ F r(M, D), add (succ((M, D), t), ωt) to W aiting 12:

Fig. 4 .Fig. 5 .

 45 Fig.4. The SCG of the TPN at Fig.3

( 276 -Fig. 6 .

 2766 Fig. 6. Optimal-Cost of the sequence (echelon5 up2 PUech3 • • • PUech6 chevron2 chevron3 age55years end) is 228 660

TABLE I STATE

 I CLASSES OF THE SCG IN FIG.4

					276 * 623 = 171948
	t 0	echelon5	up2	PUech3	PUech4	PUech5	PUech6	chevron2	chevron3	age55years	end

TABLE II OPTIMAL

 II -COST OF EACH PATH OF THE SCG IN FIG.4 THAT LEADS TO A MARKING IN Goal

An atomic constraint is of the form xy ≤ c, where x, y are real valued variables, c ∈ Q ∪ {∞} and Q is the set of rational numbers (for economy of notation, we use operator ≤ even if c = ∞).

The canonical form of F ′ is the formula corresponding to the canonical form of its DBM.

For some reason, the switch from 1st to 2nd grade only takes 12 months, whereas the switch from 6th to 7th takes

months (3 years and 6 months).[START_REF] Larsen | As cheap as possible: Efficient cost-optimal reachability for priced timed automata[END_REF] After a while, échelons are called chevrons or stripes.

Note that, keeping in tune with the French spirit, unhappiness keeps building up and that even after getting a promotion from associate to full professor, the resentment is such that the unhappiness level is maintained.

For the sake of legibility, we denote t 1 @θ 1 , t 2 @θ 2 . . . the sequence θ 1 t 1 θ 2 t 2 . . .