Uli Fahrenberg
email: ulrich.fahrenberg@irisa.fr

Line Juhl
email: linej@cs.aau.dk

Kim Guldstrand Larsen

Jiří Srba
email: srba@cs.aau.dk

Energy Games in Multiweighted Automata

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Energy games are two-player games played on finite weighted graphs with the objective of finding an infinite run where the accumulated weight is constrained by a lower and possibly also an upper bound. Such games have attracted considerable attention [START_REF] Bouyer | Timed automata with observers under energy constraints[END_REF][START_REF] Bouyer | Infinite runs in weighted timed automata with energy constraints[END_REF][START_REF] Brázdil | Reachability games on extended vector addition systems with states[END_REF][START_REF] Chakrabarti | Resource interfaces[END_REF][START_REF] Chaloupka | Z-reachability problem for games on 2-dimensional vector addition systems with states is in P[END_REF][START_REF] Chatterjee | Generalized mean-payoff and energy games[END_REF][START_REF] Chatterjee | Energy parity games[END_REF][START_REF] Degorre | Energy and mean-payoff games with imperfect information[END_REF][START_REF] Ehrenfeucht | Positional strategies for mean payoff games[END_REF][START_REF] Zwick | The complexity of mean payoff games on graphs[END_REF] in recent years, as they find natural applications in design and analysis of resource-constrained reactive systems, e.g. embedded or hybrid systems.

We study multiweighted energy games, where the weight vectors can have an arbitrary dimension. Let us motivate the study by a small example of an automatic lawn mower with a rechargeable battery and a container for collecting grass. Both the battery and the container have a maximum capacity that cannot be exceeded. We assume that the battery can be recharged and the container can be emptied at nearby servicing stations. The charger is an old-fashioned one, and it charges only for a fixed amount of energy corresponding to going from discharged to fully charged. If the lawn mower starts charging while the battery is not fully discharged, the battery will break. The station for emptying the container removes a unit amount of grass at a time and consumes a unit of battery energy. The container will break if too much grass is stored in it. A weighted game describing the lawn mower behaviour is given in Figure 1a. Each transition has a 2-dimensional vector representing the change to the accumulated battery level in the first coordinate and to the accumulated volume of grass in the container in the second coordinate. The numbers b max and c max represent the maximum capacity of the battery and the container, respectively. The initial state drawn as a diamond is controlled by Player 1 (the existential player), while the other state drawn as a square is controlled by Player 2 (the universal player). In the initial state, Player 1 has the choice of either charging the battery, emptying the container or cutting the grass. Moving to the lawn costs one unit of battery energy, and then Player 2 (the environment) controls whether the actual mowing, which costs again one energy unit, will fill the container with one or two units of grass, depending on whether the grass was short or tall. A configuration of the game consists of the state and the accumulated weight in all coordinates. A run is a sequence of transitions between configurations formed by the players of the game and starting from the initial state with zero accumulated weight.

The question we ask now (the problem called energy games with lower and upper bounds) is whether Player 1 has a strategy so that in the infinite run of actions the lawn mower performs, starting with empty battery and empty container, both the accumulated battery level as well as the container content stay invariantly above zero and do not exceed the given upper bounds b max = 4 and c max = 3. Such a strategy exists and is depicted in Figure 1b. Figure 1c illustrates a finite run of the lawn mower game according to this strategy.

If we lower the volume of the container to c max = 2, no such strategy exists. Player 1 must take the charge transition as the first step, after which cutting is the only opportunity. Player 2 can now choose to cut the short grass, leading to battery level 2 and grass volume 1. From here Player 1 can only empty the container, as cutting would allow Player 2 to break the container. After emptying the container, battery level is 1 and no transition (apart from cutting) is possible.

There are several variants of the above energy game problem. If we e.g. assume a modern battery charger which does not break the battery when it is not empty, then we have another variant of the problem called energy games with weak upper bounds. The weak upper bound game allows taking transitions that will exceed the upper bounds, but these will never accumulate more energy than the maximum capacity. We may also consider infinite runs that are constrained only by a given lower bound but with no upper bound. Finally, we ask questions regarding parameterization of the problems. We want to decide whether there exists some battery capacity b max and some initial battery level such that Player 1 wins the energy game with lower and upper bound (or some of its variants). In our example one can by a simple reasoning argue that for a container capacity c max = 2, there is no battery capacity b max so that Player 1 can guarantee an infinite behaviour of the lawn mower.

Contributions. We define the variants of multiweighted energy games (Section 2) and present reductions involving these games, leading to new decidability and complexity results. Some reductions are to/from Petri nets (Section 3) while others are between different multiweighted energy games (Section 4). This is followed by a a summary of decidability and complexity results we achieved. In Section 6 we consider a parameterized version of existential one-player games and show that some variants of the problem lead to undecidability while others are decidable in polynomial time. We conclude by presenting an undecidability result for a natural timed extension of the energy games (Section 7).

Related work.

The idea of checking whether a given resource stays above zero at all times was first presented by Chakrabarti et al. in [START_REF] Chakrabarti | Resource interfaces[END_REF], treating the subject in relation to interfaces. The lower and (weak) upper bound problems were first formulated in [START_REF] Bouyer | Infinite runs in weighted timed automata with energy constraints[END_REF] for the case with a single weight. The paper presents several complexity results for the 1-weighted case, both timed and untimed, and has given rise to a number of recent papers on 1-weighted energy games [START_REF] Chatterjee | Generalized mean-payoff and energy games[END_REF][START_REF] Chatterjee | Energy parity games[END_REF][START_REF] Degorre | Energy and mean-payoff games with imperfect information[END_REF].

The multiweighted extension has been studied in [START_REF] Brázdil | Reachability games on extended vector addition systems with states[END_REF], but only for energy games with unary weights, i.e. updates by 1, 0 or -1. A continuation of this work presents a polynomial time algorithm for the 2-weighted case with unary inputs [START_REF] Chaloupka | Z-reachability problem for games on 2-dimensional vector addition systems with states is in P[END_REF]. Contrary to this line of work, we consider binary input encoding, hence weight updates are now drawn from the full set of integers. Also in contrast to [START_REF] Brázdil | Reachability games on extended vector addition systems with states[END_REF][START_REF] Chaloupka | Z-reachability problem for games on 2-dimensional vector addition systems with states is in P[END_REF], where only complexity upper bounds are given, we give complexity lower bounds that in most cases match the upper bounds.

Multiweighted energy games with general integer updates have been considered in [START_REF] Chatterjee | Generalized mean-payoff and energy games[END_REF], where the authors show that the problem of deciding the existence of an initial weight vector such that Player 1 can win the lower bound energy game is solvable in polynomial time. In contrast to this, we show here that the non-parameterized variant of this problem: can Player 1 win with a given initial weight vector, is EXPSPACE-hard. We also treat the parameterized setting, where we show that the existential lower and (weak) upper bound problems with both bounds and initial weight vector parameterized are also decidable in polynomial time-unless the upper bound parameter is used in the transitions of the automaton, in which case the problem becomes undecidable.

Multiweighted Automata and Games

We denote by ) k the set of integer vectors of dimension k > 0 and by w

[i] the i'th coordinate of a vector w ∈ ) k . A k-weighted game G is a four-tuple (Q 1 , Q 2 , q 0 , -→)
where Q 1 and Q 2 are finite, disjoint sets of existential and universal states, respectively,

q 0 ∈ Q 1 ∪ Q 2 is the initial state and -→ ⊆ (Q 1 ∪ Q 2 ) × ) k × (Q 1 ∪ Q 2 )
is a finite weighted transition relation, written as q w -→ q ′ whenever (q, w, q ′ ) ∈ -→. Refer to Figure 1a in the introduction for an example of a k-weighted game with k = 2.

We are interested only in infinite runs in multiweighted games, hence for the rest of the paper, we assume that the game G is non-blocking, i.e. for every

q ∈ Q 1 ∪ Q 2 we have q w -→ q ′ for some w ∈ ) k and q ′ ∈ Q 1 ∪ Q 2 .
A weighted run in a k-weighted game G = (Q 1 , Q 2 , q 0 , -→) restricted to a weak upper bound b ∈ (◆ 0 ∪ ∞) k is an infinite sequence (q 0 , v0 ), (q 1 , v1 ), (q 2 , v2 ), . . . where q 0 , q 1 , . . . ∈ Q 1 ∪ Q 2 , v0 = 0 = (0, 0, . . . , 0) and v1 , v2 , . . . ∈ ) k such that for all j ≥ 0 we have q j wj -→ q j+1 and vj+1

[i] = min vj [i] + wj [i], b[i]
for all coordinates i. An illustration of a run in a 2-weighted game is given in Figure 1c in the introduction. Intuitively, a weighted run is a sequence of states together with the accumulated weight gathered along the path. Moreover, the accumulated weight is truncated, should it exceed in some coordinate the given maximum weight b. By WRb(G) we shall denote the set of all weighted runs in G restricted to the maximum accumulated weight b.

A strategy for Player i ∈ {1, 2} in a k-weighted game G = (Q 1 , Q 2 , q 0 , -→) (restricted to a weak upper bound b) is a mapping σ from each finite prefix of a weighted run in WRb(G) of the form (q 0 , v0 ), . . . , (q n , vn ) with q n ∈ Q i to a configuration (q n+1 , vn+1 ) such that (q 0 , v0 ), . . . , (q n , vn ), (q n+1 , vn+1 ) is a prefix of some weighted run in WRb(G). A weighted run (q 0 , v0 ), (q 1 , v1 ), . . . respects a strategy σ of Player i if σ((q 0 , v0 ), . . . , (q n , vn )) = (q n+1 , vn+1 ) for all n such that q n ∈ Q i . Figure 1b in the introduction shows a strategy for the 2-weighted game from Figure 1a; note that the run of the game depicted in Figure 1c indeed respects this strategy.

We shall consider three decision problems related to energy games on a given k-weighted game G = (Q 1 , Q 2 , q 0 , -→). Below we let ∞ = (∞, ∞, . . . , ∞), and we write w

≤ v if w[i] ≤ v[i] for all i, 1 ≤ i ≤ k.
Energy Game with Lower bound (GL): Given a game G, is there a strategy σ

for Player 1 such that any weighted run (q 0 , v0 ), (q 1 , v1 ), . . . ∈ WR ∞ (G) respecting σ satisfies 0 ≤ vi for all i ≥ 0?

Hence we ask whether Player 1 has a winning strategy such that during any play the accumulated weight stays above zero in all coordinates. Energy Game with Lower and Weak upper bound (GLW): Given a game G and a vector of upper bounds b ∈ ◆ k 0 , is there a strategy σ for Player 1 such that any weighted run (q 0 , v0 ), (q 1 , v1 ), . . . ∈ WRb(G) respecting σ satisfies 0 ≤ vi for all i ≥ 0? Hence we ask whether Player 1 has a winning strategy such that during any play the accumulated weight, which is truncated whenever it exceeds the given upper bound, stays in all coordinates above zero. Energy Game with Lower and Upper bound (GLU): Given a game G and a vector of upper bounds b ∈ ◆ k 0 , is there a strategy σ for Player 1 such that any weighted run (q 0 , v0 ), (q 1 , v1 ), . . . ∈ WR ∞ (G) respecting σ satisfies 0 ≤ vi ≤ b for all i? Hence we ask whether Player 1 has a winning strategy such that during any play the accumulated weight stays in all coordinates above zero and below the given upper bound.

The problems GL, GLW and GLU can be specialized in two different ways. Either by giving Player 1 the full control over the game by setting Q 2 = ∅ or dually by giving the full control to Player 2 by assuming that Q 1 = ∅. The first problem is called the existential variant as we essentially ask whether there exists some weighted run with the accumulated weight within the given bounds. The second problem is called the universal variant as we now require that all weighted runs satisfy the constraints of the energy game. We will denote the respective existential problems by EL, ELW and ELU, and the universal problems by AL, ALW and ALU. These special cases are known as one-player games or simply as multiweighted automata, and we denote such games as only a triple (Q, q 0 , -→).

In the general formulation of energy games there is no fixed bound on the dimension of the weight vectors, in other words the dimension k is a part of the input. If we want to consider problems of a fixed dimension k, we use the notation GL(k), GLW(k), GLU(k), EL(k) etc.

As the inputs to our decision problems are numbers, it is important to agree on their encoding. We will use the binary encoding, unlike some other recent work [START_REF] Brázdil | Reachability games on extended vector addition systems with states[END_REF][START_REF] Chaloupka | Z-reachability problem for games on 2-dimensional vector addition systems with states is in P[END_REF] where unary notation is considered and thus enables to achieve better complexity bounds as the size of their input instance is exponentially larger.

Relationship to Petri Nets

We show that infinite run problems on multiweighted automata can be reduced to corresponding problems on Petri nets and vice versa. This allows us to transfer some of the decidability and complexity results from the Petri net theory to our setting. Full proofs and the definition of a Petri net can be found in the appendix. Fig. 2: Translation of a Petri net to a 5-weighted automaton

Lemma 1. The infinite run Petri net problem is polynomial time reducible to EL. The infinite run Petri net problem for 1-safe nets is polynomial time reducible to ELU and ELW. The problem EL is polynomial time reducible to the infinite run problem of Petri nets.

q q ′ (-2, 5, 3) pq p q ′ p1 p2 p3 2 5 3 1 1
Fig. 3: Translation of a 3-weighted automaton to a Petri net For the first part of the lemma, a new weight coordinate is introduced for every place in the Petri net and a new state q t is added for every Petri net transition t, with an additional initial state q 0 ; see Figure 2. For the second part, we notice that in case the Petri net is 1-safe, one can freely impose an upper bound of b = (1, 1, . . . , 1). For the third part, the states of the automaton are converted to places in the Petri net with an additional place for every weight coordinate and corresponding arcs for updating the markings are added; see Figure 3.

Theorem 1. The problem EL is EXPSPACE-complete. The problems ELU and ELW are PSPACE-complete.

Proof. The complexity bounds for EL follow from Lemma 1 above and from the fact that the existence of an infinite run in a Petri net is decidable in EX-PSPACE [START_REF] Yen | A unified approach for deciding the existence of certain Petri net paths[END_REF] and EXPSPACE-hard (see e.g. [START_REF] Esparza | Decidability and complexity of Petri net problems -An introduction[END_REF]). The same problem for 1safe Petri nets is PSPACE-complete (see again [START_REF] Esparza | Decidability and complexity of Petri net problems -An introduction[END_REF]) and by Lemma 1 we get PSPACE-hardness also for ELU and ELW. The containment of the ELU and ELW problems in PSPACE can be shown by noticing that these problems have an infinite run (q 0 , v0 ), (q 1 , v1 ), . . . if and only if there are two indices i < j such that (q i , vi ) = (q j , vj ). As the size of any configuration (q, v) appearing on such a run is polynomially bounded by the size of the input (which includes the upper bound vector), we can use a nondeterministic algorithm to guess such a repeated configuration (q i , vi ) and nondeterministically verify whether it forms a loop which is reachable from the initial pair (q 0 , v0 ). This completes the argument for the containment of ELU and ELW in PSPACE.

⊓ ⊔

Reductions among Energy Games

In this section we present reductions among the variants of one and two-player energy games with a particular focus on the size of the weight vectors. Full proofs

q0 q1 q2 ( -3 , 1 ) (4, -4) (1, 5) ( -2 , 1 ) qs q0 q1 q2 (0, 0, 5, 7) (-3, 1, 3, -1) (4, -4, -4, 4) (1, 5, -1, -5) (-2, 1, 2, -1)
Fig. 4: Example of reduction from GLU with b = (5, 7) to GL are given in the appendix. Our first result can be easily proven by duplicating the coordinates in the weight vector while reversing the sign; see Figure 4.

Theorem 2. The problem GLU(k) is polynomial time reducible to GL(2k) and GLW(2k) for all k > 0. The reduction preserves the existential and universal variants of the problems.

Since we already know that ELU(1) is NP-hard [START_REF] Bouyer | Infinite runs in weighted timed automata with energy constraints[END_REF], using Theorem 2 with k = 1 gives that EL(2) is NP-hard too, which is of course then also the case for EL. Similarly as GLU( 1) is known to be EXPTIME-hard [START_REF] Bouyer | Infinite runs in weighted timed automata with energy constraints[END_REF], we get EXPTIMEhardness also for GL [START_REF] Behrmann | Minimum-cost reachability for priced timed automata[END_REF] and hence also for GL.

Our next reductions show (perhaps surprisingly) that allowing multiple weights in not that crucial in terms of complexity. The first theorem shows that for upper bound games, it suffices to work with one weight only; Theorem 4 then shows that for the existential variant, two weights are enough.

Theorem 3. The problem GLU is polynomial time reducible to GLU(1).

Proof. Let G = (Q 1 , Q 2 , q 0 , -→) be a k-weighted game and b a given upper bound vector for the GLU problem. We assume that G is encoded in binary and let n denote the size of such encoding. This means that all constants that appear in the description of G are less than 2 n . We will construct a corresponding 1weighted game

G ′ = (Q ′ 1 , Q ′ 2 , q s , -→) where Q ′ 1 = Q 1 ∪ {q 2 , q 3 , . . . , q k+5 | q ∈ Q 1 } ∪ {q s } and Q ′ 2 = Q 2 ∪ {q 1 | q ∈ Q 2 } that simulates G. Let w denote any weight vector present in G. Clearly, 0 ≤ w[1], . . . , w[k] < 2 n
due to the encoding of the input. Without loss of generality we can assume that all coordinates of b are the same, i.e. that b = (b, . . . , b) for some 0 ≤ b < 2 n .

We need to encode the weights from G using only one weight. We will do so by placing them into the single (large) weight w ′ . Since b < 2 n , at most n bits are needed to represent each weight w[i]. The weight w ′ is constructed by appending the weights from G in higher and higher bit positions, with a suitable separation sequence to ensure that weights cannot get 'entangled' should their bounds overflow or underflow. Formally, we introduce the following notation for any integer ℓ ∈ ) and any i, 1 ≤ i ≤ k:

ℓ i = ℓ • 2 (i-1)(n+2) . q q ′ ( w[1], . . . , w[k]) q q1 q ′ q2 q3 q4 q5 . . . qk+3 qk+4 qk+5 w[1] 1 + • • • + w[k] k 0 b k+1 -0 +B - 1 k + 1 -1 1 0 -1 2 0 -1 3 0 -1 k
w def = w[1] 1 + 2 n+1 1 + w[2] 2 + 2 n+1 2 + . . . + w[k] k + 2 n+1 k
where the weights w[1], . . . , w[k] written in binary from the less significant bits to more significant ones are separated by the binary string '10'. For example if again n = 4 then the weight vector w = (110, 1, 1011) with the weights written in binary is represented by the binary number w = 10 1011 10 0001 10 0110.

The new upper bound B for G ′ is defined by B = b k+1 + b where apart from the standard encoding of all upper bounds for all coordinates we add one more time the constant b at the most significant bits (we will use these bits for counting in our construction).

Each transition q w -→ q ′ in G is transformed into a number of transitions in G ′ as depicted in Figure 5 where Player 1 (existential) states are drawn as diamonds and Player 2 (universal) states are drawn as squares. The states drawn as filled circles can be of either type, and their type is preserved in the translation. We also add the initial transition q s 0 -→ q 0 which inserts the separation strings 10 at the correct positions.

The idea is that the update of the accumulated weight vector v in G via adding a vector w like in Figure 5 is simulated by adding the numbers w

[1] 1 , w[2] 2 , . . . , w[k] k to the accumulated weight in G ′ .
The chosen encoding of k weights into a single weight is crucial to preserve the soundness of the construction as discussed in the following remark.

Remark 1. Given an accumulated weight vector v and a weight update vector w where 0 ≤ v, w ≤ b < (2 n , . . . , 2 n ), then adding the numbers v and w[i] i in v changes at most the bits that are designated for representing the weight coordinate w[i] and the separating two bits 10 just before it. This can be easily seen by analyzing the two extreme cases of adding 11 . . . Let us now argue about the correctness of this polynomial time construction. Assume that Player 1 has a winning strategy in the game G. As the accumulated weight stays within the bounds during any such play in G, it is clear that the same winning strategy can be performed also in G ′ using only a single weight. One complication is that each transition in G is split in G ′ and a new node for Player 2 (q 1 in Figure 5) is inserted. Hence Player 2 could possibly have an extra winning strategy by playing q 1 b k+1 ----→ q 2 , instead of the expected move to q ′ . However, because the accumulated weight vector v satisfies 0 ≤ v[i] ≤ b < 2 n for all i, we can see that Player 1 wins in this case, by taking the loop q 2 , q 3 , . . . q k+3 , q 2 exactly b times while choosing the zero or -1 i transitions (for all i) in such a way that the bits representing the weight v[i] are all set to 0. What remains in G ′ as the accumulated weight is then the value 0 which consists only of the separation symbols. From here Player 1 takes the transition with weight -0 , setting the accumulated weight to zero, and wins by performing the transition labeled with +B (which is possible only if the accumulated weight is exactly zero) and repeatedly performing in q k+5 the self-loop with weight zero.

On the other hand, assume that a play in G causes the accumulated weight in some coordinate i, 1 ≤ i ≤ k, to get out of the bounds; we shall argue that Player 2 has a winning strategy in G ′ in this case. Should this happen during a transition from q to q ′ in G, then in G ′ , Player 2 will simply move from the intermediate state q 1 to q 2 , while the counter value of size b is added to the most significant bits of the accumulated weight via adding the number b k+1 . It is clear that it is possible to move from q 2 to q k+5 only if the accumulated weight is exactly 0 . In order to achieve this value, the accumulated weight needs to be decreased exactly b times via taking the loop q 2 , q 3 , . . . , q k+3 , q 2 . Because of Remark 1 we can see that only the bits relevant to each weight coordinate were changed before entering the loop, so it is impossible to zero all bits corresponding to the coordinate i while preserving the separation bits 10.

⊓ ⊔

When considering the existential problems, we cannot use only one weight in order to encode the weights with upper and weak upper bounds. Since we do not have the adversary to check for violation of the bounds, we cannot 'destroy' the weights in the overflow checking process, and thus need an extra weight to store the current value of all weights before a check.

Theorem 4. The problem ELU is polynomial time reducible to ELU(2).

Proof. The reduction idea is similar to the one in the proof of Theorem 3. The main complication is that Player 2 has no states in control, hence checking the underflow and overflow of weights has to be performed without resorting to an opponent. As the original weight values are destroyed during such a check, we need to employ the second weight for saving them.

q q ′ ( w[1], . . . , w[k]) q . . . q ′ ( w[1] 1 + . . . + w[k] k , 0) (i) (max, 0) (ii) (-max, 0) (iii) (0, max k+1 ) (iv) (0, -max k+1 ) (v) (-1, 1 + 1 k+1 ) (1, -1 k+1 ) (0, b k+1 ) (vi) (0, -0 ) (vii) (0, max k+1 + max) (viii) (0, -max k+1 -max) (ix) (0, -1 k+1 ) (0, -1 1 ) (0, 0) (0, -1 2 ) (0, 0) (0, -1 3 ) (0, 0) (0, -1 k ) (0, 0) (0, 0)
Fig. 6: Simulation of a transition in a k-weighted automaton by a 2-weighted automaton

Let A = (Q, q 0 , -→) be a k-weighted automaton and b the upper bound vector for the ELU problem. We construct a corresponding 2-weighted automaton A ′ = (Q ′ , q s , -→). Let w denote the weight vectors in A and v [START_REF] Alur | Optimal paths in weighted timed automata[END_REF], v [START_REF] Behrmann | Minimum-cost reachability for priced timed automata[END_REF] the two weights in A ′ . As before for an input automaton of size n we may assume that all weights in A have the same upper bound b = (b, b, . . . , b) where b < 2 n .

The upper bound b′ for the ELU(2) problem in A ′ is given by b′ = (max, max k+1 + max) with max = b k+1 + b . The reason for reserving twice as many bits in the second weight is that we need to save there two copies of the first weight. Figure 6 shows how to simulate one transition in A by a number of transitions in A ′ . From the newly added initial state q s we also add the transition q s ( 0 ,0) ----→ q 0 which inserts the separation strings '10' into the first weight. We shall now argue that the automaton A ′ faithfully simulates A. We will examine the effect of the sequence of transitions between q and q ′ added to the automaton A ′ (here numbered with (i), (ii), . . . , (ix) for convenience) and argue at the same time that the part of the run between q and q ′ in A ′ is uniquely determined. By construction, v [START_REF] Behrmann | Minimum-cost reachability for priced timed automata[END_REF] will be zero when entering q, and then the transition (i) adds the encoded weights of the original transition in A to v [START_REF] Alur | Optimal paths in weighted timed automata[END_REF]. Transition (ii) will add the upper bound to v [START_REF] Alur | Optimal paths in weighted timed automata[END_REF], hence before this, we need to take the loop with weight (-1, 1 + 1 k+1 ) until v [START_REF] Alur | Optimal paths in weighted timed automata[END_REF] equals zero, thereby copying twice the value of v [START_REF] Alur | Optimal paths in weighted timed automata[END_REF] to v [START_REF] Behrmann | Minimum-cost reachability for priced timed automata[END_REF] (first copy in the less significant bits, second copy in the more significant bits). After the transitions (ii) and (iii), v [START_REF] Alur | Optimal paths in weighted timed automata[END_REF] is then again at zero. Now transition (iv) wants to add the upper bound to the most significant bits of v [START_REF] Behrmann | Minimum-cost reachability for priced timed automata[END_REF], hence before this, we need to take the loop with weight (1, -1 k+1 ) until the value of the most significant bits in v [START_REF] Behrmann | Minimum-cost reachability for priced timed automata[END_REF] is copied to v [START_REF] Alur | Optimal paths in weighted timed automata[END_REF], thereby restoring the original weight in v [START_REF] Alur | Optimal paths in weighted timed automata[END_REF].

After the transitions (iv) and (v), we are in a situation where both coordinates in the accumulated weight store the same number, and we can afford to destroy the second copy during the verification phase for bound overflow/underflow performed by transitions (vi), the long loop, and transitions (vii), (viii) and (ix).

q q ′ ( w[1], . . . , w[k]) q q1 q2 q ′ • • • ( w[1], . . . , w[k]) (2 n , 2 n , . . . , 2 n ) (-2 n , -2 n , . . . , - 2 n )
(-1, 0, . . . , 0) (0, 0, . . . , -1) Fig. 7: Simulation of a transition in a LW game by a LU game This is identical to the construction in the previous proof (except for the extra coordinate v [START_REF] Alur | Optimal paths in weighted timed automata[END_REF] which is not updated). Provided that no violation of bounds was detected, we will reach q ′ with v [START_REF] Alur | Optimal paths in weighted timed automata[END_REF] encoding the weight vector of A at q ′ and v [START_REF] Behrmann | Minimum-cost reachability for priced timed automata[END_REF] equal to zero. Hence a transition between two states in A can be performed if and only if the sequence of transitions between q and q ′ in A ′ can be performed. As the reduction is clearly in polynomial time, this concludes the proof.

⊓ ⊔

The next theorem finishes our considerations about reductions between different variants of energy games. For the proof, the weak upper bound b = (b, . . . , b) is widened to (2 n +b, . . . , 2 n +b) (where again n is the size of the binary encoding of the game), and some extra transitions are added to ensure that the weights are truncated at b; see Figure 7.

Theorem 5. The problem GLW is polynomial time reducible to GLU, and ELW is polynomial time reducible to ELU.

Now, in combination with Theorems 3 and 4, we get the following corollary.

Corollary 1. The problems GLW and ELW are polynomial time reducible to GLU [START_REF] Alur | Optimal paths in weighted timed automata[END_REF] and ELU [START_REF] Behrmann | Minimum-cost reachability for priced timed automata[END_REF], respectively.

Summary of Complexity Results

The collection of complexity results and reductions between different types of energy games and automata enables us to draw the conclusions presented in Table 1. Notice that the LU problems are computationally easier than the L problems for an arbitrary number of weights, even though they are harder than the L problems in the 1-weighted case. The configuration space for the LU (and LW) problems is bounded (see Theorem 1), whereas the same a priori does not apply to the L problem.

Observe also that any universal problem with k weights can be solved by checking the same problem for each coordinate independently. If the k-weighted problem violates the bounds at some coordinate, so will do the 1-weighted problem projected on this coordinate. On the other hand, if some coordinate in the 1-weighted problem violates the bounds then so will do the k-weighted game, as the same run leading to the violation in one coordinate leads to a violation in the k-weighted game (unless the violation occurs in some other coordinate before that). As AL(1), ALW(1) and ALU(1) are decidable in P [START_REF] Bouyer | Infinite runs in weighted timed automata with energy constraints[END_REF], this implies polynomial upper bounds also for all the other k-weighted universal problems.

Parameterized Existential Problems

In this section we shall focus in more detail on the existential one-player energy games. So far we have studied decision problems where both the initial weight vector and the upper bound were given as a part of the input. We will now consider parameterized versions of the problems where, given a weighted automaton, we ask whether there is some initial weight vector v0 (and some upper bound b in case of ELU and ELW) such that the automaton has a run where the accumulated weight satisfies the constraints imposed by the respective variant of the problem. Recent work by Chatterjee et al. [START_REF] Chatterjee | Generalized mean-payoff and energy games[END_REF] proves that the parameterized version of the EL problem, asking if there is an initial weight vector such that the accumulated weight of some run in the automaton stays (component-wise) above zero, is decidable in polynomial time. Perhaps surprisingly, this result contrasts with our EXPSPACE-hardness result for the EL problem where the initial weight vector is fixed. An interesting fact, using Lemma 1, is that by the result of [START_REF] Chatterjee | Generalized mean-payoff and energy games[END_REF], it is also decidable in polynomial time whether there is an initial marking such that a given Petri net has an infinite run.

The situation can be, however, different when considering the problems ELU and ELW. Depending on whether the parameterized upper bound b is allowed to appear as a weight in transitions of the given weighted automaton (see Section 1 for an example where the upper bound appears as a weight), we shall show below that the problem is either decidable in polynomial time or undecidable.

We present first the positive result. Its proof is based on a polynomial time algorithm for zero-weight cycle detection in multiweighted automata by Kosaraju and Sullivan [START_REF] Kosaraju | Detecting cycles in dynamic graphs in polynomial time[END_REF], and we acknowledge [START_REF] Chatterjee | Generalized mean-payoff and energy games[END_REF] where we found a pointer to this result, which is mentioned there in connection with the parameterized EL problem. Theorem 6. The parameterized ELU and ELW problems where the upper bound parameter does not appear as a weight in the underlying weighted automaton are decidable in polynomial time.

However, if the uppper bound can appear as a weight, we get undecidability.

Theorem 7. The parameterized ELU [START_REF] Behrmann | Minimum-cost reachability for priced timed automata[END_REF] and ELW [START_REF] Bouyer | Infinite runs in weighted timed automata with energy constraints[END_REF] problems where the upper bound parameter can appear as a weight in the underlying weighted automaton are undecidable.

Proof. We provide a reduction from the undecidable halting problem of Minsky machines [START_REF] Minsky | Computation: Finite and Infinite Machines[END_REF] to ELU(3). Let 1 : inst 1 ; 2 : inst 2 ; . . . , n : inst n be a Minsky machine over the nonnegative counters c 1 and c 2 . We construct a 3-weighted automaton (Q, q 0 , -→) where Q = {q i , q ′ i | 0 ≤ i ≤ n} and where the initial weight vector v0 and the upper bound b are parameterized. The intuition is that the first and second coordinates will record the accumulated values of counters c 1 and c 2 , respectively, and the third coordinate will be used for counting the number of steps the machine performs. The transitions are of four types:

1. q 0 + b -→ q ′ 0 - b -→ q 1 2.
For each instruction i: c j := c j + 1; goto k, we add the transitions

-q i (+1,0,+1) ------→ q k if j = 1, and q i (0,+1,+1) ------→ q k if j = 2.
3. For each instruction i: if c j = 0 then goto k else (c j := c j -1; goto ℓ), we add the transitions

-q i (+ b[1],0,0) -------→ q ′ i (-b[1],0,+1)
--------→ q k and q i (-1,0,+1)

------→ q ℓ if j = 1, and

-q i (0,+ b[2],0) -------→ q ′ i (0,-b[2],+1)
--------→ q k and q i (0,-1,+1)

------→ q ℓ if j = 2. 4. Finally, we add the loop q n (0,0,0) ----→ q n . It is straightforward to argue that the constructed 3-weighted automaton has an infinite run iff the Minsky machine has an infinite computation. From Theorem 4 we get that ELU(3) is reducible to ELU(2), hence the parameterized existential problem is undecidable for vectors of dimension two. By Theorem 2 we can reduce ELU(2) to ELW(4), which implies the undecidability of the problem also for weak upper bound and weight vectors of size at least four.

⊓ ⊔

The parameterized problems ELU(1) and ELW(k) for 1 ≤ k ≤ 3 where the upper bound parameter can appear in the automata are open.

Extension to Timed Automata

It is natural to ask for extensions of the results presented in this article to multiweighted timed automata and games [START_REF] Alur | Optimal paths in weighted timed automata[END_REF][START_REF] Behrmann | Minimum-cost reachability for priced timed automata[END_REF]. For the case with one weight and one clock only, such extensions have been discussed in [START_REF] Bouyer | Timed automata with observers under energy constraints[END_REF][START_REF] Bouyer | Infinite runs in weighted timed automata with energy constraints[END_REF]. In [START_REF] Bouyer | Infinite runs in weighted timed automata with energy constraints[END_REF] it has been shown that the GLU(1) problem is already undecidable for one-clock multiweighted timed automata. By an adaptation of the technique introduced in [START_REF] Bouyer | Infinite runs in weighted timed automata with energy constraints[END_REF], we can prove that the existential problem ELU with two weights and one clock is also undecidable. As the reductions from Theorem 2 apply also to timed automata, we altogether get the following undecidability results. Theorem 8. The problems ELU [START_REF] Behrmann | Minimum-cost reachability for priced timed automata[END_REF], EL [START_REF] Bouyer | Infinite runs in weighted timed automata with energy constraints[END_REF] and ELW(4), and GLU [START_REF] Alur | Optimal paths in weighted timed automata[END_REF], GL [START_REF] Behrmann | Minimum-cost reachability for priced timed automata[END_REF] and GLW( 2) are undecidable for one-clock multiweighted timed automata.

Conclusion and Future Work

We have presented an extension of different types of energy games to a setting with multiple weights and established a comprehensive account of the complexity of these problems. To derive our results, we have demonstrated a close connection of these problems with infinite run problems in Petri nets, together with a number of reductions between different variants of multiweighted energy games. We have also studied a parameterized version of these problems and shown that depending on the precise statement of the problem, it is either solvable in polynomial time or undecidable. Finally, we have demonstrated that for the timed automata extension of energy games, the lower and upper bound existential problem is undecidable already for one clock and two weights.

There are two main problems left open. The first one deals with settling the complexity of the one-weight lower and upper bound existential problem, which is only known to be between NP and PSPACE. This is closely related to the lower bound and weak upper bound problems with a fixed number of weights. The second problem deals with the complexity of energy games with lower bound only, as the present upper complexity bound depends on the number of weights and does not have a matching lower bound.

Appendix

Remarks about Energy Games. We may without loss of generality assume an initial weight vector w0 different from 0. This is evident by adding a new fresh start state with one transition labeled with w0 pointing to the original start state. In addition we may assume that in any given upper bound or weak upper bound vector b we have b

[1] = b[2] = • • • = b[k].
This can be achieved by scaling every i'th coordinate of all weight vectors on transitions with b

[1]•...• b[k] b[i]
in order to obtain equality on the coordinates of b. Such a scaling implies only polynomial increase in the size (in binary encoding) of the upper bound constants.

Definition of Petri nets. We define the Petri net model with weighted arcs (that allow to consume more than one token from a given place).

A Petri net is a triple N = (P, T, W ) where P is a finite set of places, T is a finite set of transitions, and W : (P × T ) ∪ (T × P ) → ◆ 0 is a function assigning a weight to each arc in the net. A marking on N is a function M : P → ◆ 0 denoting the number of tokens present in the places. A marked Petri net is a pair (N, M 0 ) where N is a Petri net and M 0 is an initial marking on N . A transition t ∈ T is enabled in a marking M if M (p) ≥ W (p, t) for all p ∈ P . An enabled transition may fire. When a transition t fires, it produces a new marking M ′ obtained as M ′ (p) = M (p) -W (p, t) + W (t, p) for all places p ∈ P . Then we write M

t -→ M ′ . A marking M is reachable in N if M 0 -→ * M
where -→ = t∈T t -→. A marked Petri net is called 1-safe if for any reachable marking M the number of tokens in any place is at most one, i.e. M (p) ≤ 1 for all p ∈ P .

We say that a marked net (N, M 0 ) has an infinite run if there is a sequence of markings M 1 , M 2 , . . . and transitions t 1 , t 2 , . . .

such that M 0 t1 -→ M 1 t2 -→ M 2 t3
-→ . . . The infinite run problem for Petri nets (see e.g. [START_REF] Esparza | Decidability and complexity of Petri net problems -An introduction[END_REF]) is to decide whether a given Petri net has an infinite run. Lemma 1). We first prove the first part of the lemma. Given a Petri net N = (P, T, W ) where P = {p 1 , . . . , p k } we construct a k-weighted automaton A = (Q, q 0 , -→) such that Q = {q 0 } ∪ {q t | t ∈ T }. Now for every t ∈ T we add to A two transitions q 0 wt -→ q t and q t w+ t -→ q 0 where w- 2 for an example. The initial weight vector then corresponds to the initial marking of the net in the expected way.

Proof (of

t [i] = -W (p i , t) and w+ t [i] = W (t, p i ) for all i, 1 ≤ i ≤ k. Consult Figure
It follows from the construction that each transition firing can be simulated by two transitions in the constructed weighted automaton and vice versa. Observe that the reachable Petri net markings are represented as accumulated weight vectors in the automaton and hence are nonnegative in all coordinates. It is easy to verify that the net has an infinite run if and only if the EL problem has a solution. The reduction clearly runs in polynomial time.

For the second part, observe that if the net is 1-safe then by taking the upper bound b = (1, 1, . . . , 1) we have a reduction from the infinite run problem for 1-safe nets to ELU and ELW.

The reduction from k-weighted automata to Petri nets works in a similar way. Given a k-weighted automaton A = (Q, q 0 , -→) we construct a Petri net N = (P, T, W ) where P = {p 1 , . . . , p k } ∪ {p q | q ∈ Q} and T = {t (q, w,q ′ ) | q w -→ q ′ }. For each t (q, w,q ′ ) we set W (p q , t (q, w,q ′ ) ) = 1, W (t (q, w,q ′ ) , p q ′ ) = 1 and for all i, 3 for an example of the reduction. The initial marking corresponds to the initial weight vector in the natural way, and there is one extra token in the place p q0 representing the current state of the automaton.

1 ≤ i ≤ k, W (p i , t (q, w,q ′ ) ) = -w[i] if w[i] < 0 and W (t (q, w,q ′ ) , p i ) = w[i] if w[i] ≥ 0. See Figure
As before, it is easy to verify that the constructed Petri net has an infinite run if and only if the EL problem has a solution. The reduction clearly runs in polynomial time.

⊓ ⊔

Proof (of Theorem 2). Let G k = (Q 1 , Q 2 ,
q 0 , -→) be a k-weighted game and let b be a given upper bound vector for the GLU problem. We construct a 2k-weighted --------------------------→ q ′ in G 2k if and only if q w -→ q ′ in G k . We moreover add the initial transition q s w0 -→ q 0 where w0 [i] = 0 and w0 4 illustrates the construction on an example. Intuitively, every coordinate in the weight vector is duplicated and the duplicated coordinate gets initially the value from the vector b, while the original coordinate is 0. It is now easy to verify that during any run in G 2k all its configurations (q, v) satisfy the invariant v

game G 2k = (Q 1 ⊎ {q s }, Q 2 , q s , -→) where q ( w[1], w[2],..., w[k],-w[1],-w[2],...,-w[k])
[k + i] = b[i] for all i, 1 ≤ i ≤ k. Figure
[i]+ v[k + i] = b[i] for all i, 1 ≤ i ≤ k.
The upper bound check is hence replaced with a lower bound on the duplicate coordinates and hence the GLU problem is reduced to GL and also to GLW (by using the weak upper bound vector b), while the size of the weight vectors doubles. The reduction also clearly preserves the existential and universal variants of the problems.

⊓ ⊔ Proof (of Theorem 5). Let G = (Q 1 , Q 2 , q 0 , -→) be a k-weighted game and let b be a given upper bound vector for the GLW problem. We will construct a corresponding k-weighted game Each transition q w -→ q ′ in G is simulated by a number of transitions in G ′ as seen in Figure 7. Moving from q to q 1 adds w to the accumulated weights of G ′ in exactly the same way as in G. In q 1 Player 1 has the opportunity to decrement independently all weight coordinates with an arbitrary value. The two last transitions from q 1 to q ′ make sure that in all coordinates all weights are no more than b, otherwise the upper bound b′ is exceeded.

G ′ = (Q ′ 1 , Q ′ 2 , q 0 , -→) where Q ′ 1 = Q 1 ∪ {q 1 , q 2 | q ∈ Q 1 } and Q ′ 2 = Q 2 that
It is now clear that if Player 1 has a winning strategy in G, then it has a winning strategy also in G ′ by lowering all weights above b to exactly b in the state q 1 . On the other hand, if Player 1 does not have a winning strategy in G, then it cannot win in G ′ either. This can be observed by the fact that Player 1 is forced to decrement all weights to at least b, and the player cannot benefit from decrementing them to any lower number as this makes the position of Player 1 in the weak upper bound game only worse.

Since the reduction is clearly in polynomial time and it adds only existential (Player 1) states, this concludes the proof.

⊓ ⊔ Proof (of Theorem 6). We shall first focus on the ELU problem. Notice that a parameterized ELU problem has an infinite run (q 0 , v0 ), (q 1 , v1 ), . . . where 0 ≤ vi ≤ b for all i and some b if and only if there are two indices j < k such that (q j , vj ) = (q k , vk ). In other words, there is a cycle such that the accumulated weight on that cycle is exactly 0. A result in [START_REF] Kosaraju | Detecting cycles in dynamic graphs in polynomial time[END_REF] shows that the existence of such zero-weight cycle is decidable in polynomial time.

Assume without loss of generality that the given weighted automaton contains only states reachable (while disregarding the weights) from the initial state q 0 . It is now clear that if the weighted automaton contains a zero-weight cycle then the parameterized ELU problem has a solution by choosing an appropriate initial weight vector v0 and a sufficiently large upper bound b which enables us to execute the whole cycle plus reach the cycle from the initial pair (q 0 , v0 ). On the other hand, if there is no zero-weight cycle then the parameterized ELU does not have a solution, as for any choice of v0 and b, every run will eventually violate either the lower bound or the upper bound.

By similar arguments, it is easy to see that a parameterized ELW problem has a solution if and only if the weighted automaton contains a nonnegative-weight cycle. To check for the existence of such a cycle in polynomial time we can use the trick described in [START_REF] Chatterjee | Generalized mean-payoff and energy games[END_REF]. We simply add to each state in the automaton a number of self-loops with weights (-1, 0, . . . , 0), (0, -1, 0, . . . , 0), . . . (0, . . . , 0, -1) and then ask for the existence of a zero-weight cycle.

⊓ ⊔ Definition of Minsky two-counter machine. A Minsky machine with two nonnegative counters c 1 and c 2 is a sequence of labeled instructions 1 : inst 1 ; 2 : inst 2 ; . . . , n : inst n where inst n = HALT and each inst i , 1 ≤ i < n, is of one of the following forms:

(Inc) i: c j := c j + 1; goto k (Test-Dec) i: if c j = 0 then goto k else (c j := c j -1; goto ℓ) for j ∈ {1, 2} and 1 ≤ k, ℓ ≤ n. Instructions of type (Inc) are called increment instructions and of type (Test-Dec) are called test and decrement instructions.

A configuration is a triple (i, v 1 , v 2 ) where i is the current instruction and v 1 and v 2 are the values of the counters c 1 and c 2 respectively. A computation step between configurations is defined in the natural way. If starting from the initial configuration (1, 0, 0) the machine reaches the instruction HALT then we say it halts, otherwise it loops. It is well known that the problem whether a given Minsky machine halts is undecidable [START_REF] Minsky | Computation: Finite and Infinite Machines[END_REF].

Definition of k-weighted timed automaton. Let Φ(C) be the standard set of (diagonal-free) clock constraints over a finite set of clocks C given by conjunctions of constraints of the form x ⊲⊳ c with x ∈ C, c ∈ ), and ⊲⊳ any of the relations ≤, <, =, >, and ≥.

A k-weighted timed automaton is a tuple T = (L, ℓ 0 , C, E, r, w), where L is a finite set of locations, ℓ 0 ∈ L is the initial location, C is a finite set of clocks, E ⊆ L × Φ(C) × 2 C × L is a finite set of edges, and r : L → ) k , w : E → ) k assign weight vectors to locations and edges.

Note that we allow weight updates on edges here; as shown in [START_REF] Bouyer | Timed automata with observers under energy constraints[END_REF], this can have a significant influence on the complexity of the problems one wants to consider.

We also use the standard notation v |= g for the fact that a valuation v : -→ (ℓ, v + t) for all t ′ ∈ [0, t] (

C → | ≥0
-→ (ℓ ′ , v ′ ) for all e = (ℓ, g, R, ℓ ′ ) ∈ E s.t. v |= g and v ′ = v[R] (switch).

We recall the fact that weights on delay transitions may be non-integer real numbers; formally we have to change the definition of a k-weighted game to allow an infinite weighted transition relation -→ ⊆ Q × | k × Q. A run in a multiweighted timed automaton is a sequence of alternating switch and delay transitions in the corresponding multiweighted automaton. Theorem 8). We start by proving the case of ELU(2). The proof is by reduction from Minsky machines to multiweighted timed automata, based on the technique of the proof of Theorem 17 in [START_REF] Bouyer | Infinite runs in weighted timed automata with energy constraints[END_REF]. We construct a one-clock 2-multiweighted timed automaton T that simulates a Minsky machine such that the Minsky machine loops if and only if T is a positive instance of the ELU(2) problem.

Proof (of

The values c 1 , c 2 of the counters will be encoded by the accumulated weight vector w = (5 -2 -c1 , 5 -2 -c2 ) and T will start with an initial weight vector of v0 = (4, 4), and the upper bound vector is b = [START_REF] Brázdil | Reachability games on extended vector addition systems with states[END_REF][START_REF] Brázdil | Reachability games on extended vector addition systems with states[END_REF].

In order to simulate the instructions of the Minsky machine we now describe two different modules of T .

Increment and decrement: Figure 8 shows the general module used for incrementing and decrementing counter c 1 ; by interchanging the two weights one obtains the module for c 2 . Note that the second component w [START_REF] Behrmann | Minimum-cost reachability for priced timed automata[END_REF] of the weight

  Fig. 1: A lawn mower example

Fig. 5 :

 5 Fig. 5: Simulation of a transition in a k-weighted game by a 1-weighted game

  simulates G. As before we assume that the weak upper bound is b = (b, . . . , b) and that b is represented using at most n bits, hence 0 ≤ b < 2 n . The new upper bound for G ′ is given as b′ = (b ′ , . . . , b ′ ) where b ′ = 2 n + b (in binary the most significant bit 1 is appended to the binary encoding of b).

  satisfies the clock constraint g ∈ Φ(C), v + t for the valuation given by (v + t)(x) = v(x) + t, and v[R] for the valuation with clocks in R reset to value 0.The semantics of a k-weighted timed automaton is now given by a k-weightedautomaton with states Q = {(ℓ, v) | v |= I(ℓ)} ⊆ L × | C ≥0 and transitions (ℓ, v) t•r(ℓ)

  1 to an accumulated weight coordinate with full capacity and subtracting 11 . . . 1 from an accumulated weight coordinate that represents zero as showed in the following two examples. . . . 10 111 . . . 111 10 . . . + . . . 00 111 . . . 111 00 . . . . . . 11 111 . . . 110 10 . . . . . . 10 000 . . . 000 10 . . . -. . . 00 111 . . . 111 00 . . . . . . 01 000 . . . 001 10 . . .

Table 1 :

 1 Remark 5. The upper bound for GLU follows from Theorem 3 and the EXPTIME upper bound for GLU(1); the upper bound for GLW follows additionally from Theorem 5. The lower bound for GLU is obvious and for GLW it is by Theorem 2 and the EXPTIME-hardness result for GLU[START_REF] Alur | Optimal paths in weighted timed automata[END_REF].

	Weights Type Existential	Game
	One	L	∈ P [4]	∈ UP ∩ coUP [4]
		LW ∈ P [4]	∈ NP ∩ coNP [4]
		LU	NP-hard [4], ∈ PSPACE [4]	EXPTIME-complete [4]
	Fixed	L	NP-hard,	EXPTIME-hard,
	(k>1)		∈ k-EXPTIME [5] (Rem. 2)	∈ k-EXPTIME [5] (Rem. 3)
		LW NP-hard, ∈ PSPACE (Rem. 4)	EXPTIME-complete
			PSPACE-complete for k ≥ 4	(Rem. 5)
		LU	PSPACE-complete (Rem. 4) EXPTIME-complete (Rem. 5)
	Arbitrary L	EXPSPACE-complete	EXPSPACE-hard (from EL)
			(Thm. 1)	decidable [5]
		LW PSPACE-complete (Thm. 1) EXPTIME-complete (Rem. 5)
		LU	PSPACE-complete (Thm. 1) EXPTIME-complete (Rem. 5)

Complexity bounds; results obtained in this paper are in bold Remark 2. The problem ELU(1) is NP-hard, and Theorem 2 implies NPhardness for EL

[START_REF] Behrmann | Minimum-cost reachability for priced timed automata[END_REF]

. The upper bound follows from the game version of the problem (see also Remark 3).

Remark 3. The lower bound follows from EXPTIME-hardness of GLU(

1

) and Theorem 2. The upper bound is due to a result in

[START_REF] Brázdil | Reachability games on extended vector addition systems with states[END_REF]

showing (k-1)-EXPTIME containment for GL(k) but for games where weight updates are only +1, 0, and -1. We can reduce updates with arbitrary weights into this setting by standard techniques (introducing intermediate transitions which repeatedly add or subtract 1) but this causes an exponential blowup in the size of the system. Hence the complexity upper bound increases by one exponent to k-EXPTIME.

Remark 4. The PSPACE upper bound follows from the results for an arbitrary number of weights (Theorem 1). The PSPACE lower bound for ELU(2) is due to the reduction in Theorem 4 and PSPACE-hardness of ELU. By using Theorem 2 we get PSPACE-hardness for ELW(4) because ELU(2) is PSPACE-hard, and we also get NP-hardness of ELW(2) as ELU(1) is NP-hard.

⋆ Supported by the VKR Center of Excellence MT-LAB. ⋆⋆ Partially supported by Ministry of Education of Czech Republic, MSM 0021622419.

Fig. 9: The test-decrement module vector is not changed in the module, and we assume that w[1] = 5e when entering the module and 0 ≤ en ≤ 30. We now prove that when exiting the module, w[1] = 5 -en 6 . Any legal run must decrease w [START_REF] Alur | Optimal paths in weighted timed automata[END_REF] to value 0 while delaying in ℓ 1 (otherwise adding 5 to w [START_REF] Alur | Optimal paths in weighted timed automata[END_REF] in the following transition exceeds the upper bound), hence the clock x has the value 5-e 6 when leaving ℓ 1 . We cannot delay in the next location, as this would exceed the upper bound, hence we arrive in ℓ 2 with x = 5-e 6 and w [START_REF] Alur | Optimal paths in weighted timed automata[END_REF] = 0. We must delay in ℓ 2 until w [START_REF] Alur | Optimal paths in weighted timed automata[END_REF] has the value 5, otherwise the following transition would exceed the lower bound, hence the delay in ℓ 2 is precisely 1 /6 time units. Location ℓ 3 is thus entered with x = 1 -e 6 and w[1] = 5, and after delaying for e /6 time units, w[1] = 5 -en 6 . Hence instantiating n = 3 converts an input of w [START_REF] Alur | Optimal paths in weighted timed automata[END_REF] = 5e to w[1] = 5 -e 2 , thus incrementing counter c 1 . Likewise, for n = 12 counter c 1 is decremented.

The test-decrement module: We have shown how to implement a module which increments a counter, so we miss to construct a module performing the instruction if c 1 = 0 then goto k else (c 1 := c 1 -1; goto ℓ). This module is displayed in Figure 9; the construction for the corresponding c 2 module is symmetric.

We now argue that the module acts as claimed. If c 1 = 0 when entering, i.e. w[1] = 4, then the upper path can be taken, leading to Module m k with counter value c 1 = 0 (and c 2 unchanged). On the other hand, attempting to take the lower path exits the Dec module with a value w[1] = 3, hence the following transition leads to a violation of the lower bound.

If c 1 ≥ 1, i.e. w[1] ≥ 4.5, when entering the module, then the (1, 0) transition in the upper path will violate the upper bound. In the lower path, the Dec module is left with w[1] ≥ 4 and c 1 decreased by one, hence Module m ℓ is entered with the correct c 1 value.

We have shown how to faithfully simulate a Minsky machine by a one-clock 2-multiweighted timed automaton such that the Minsky machine has an infinite computation if and only if the timed automaton has an infinite alternating run.

By undecidability of the halting problem for Minsky machines, this concludes the proof for the case of ELU [START_REF] Behrmann | Minimum-cost reachability for priced timed automata[END_REF].

For the case of EL(4) and ELW(4) we observe that the construction in the proof of Theorem 2 can be adapted also to multiweighted timed automata. Given a k-weighted timed automaton T = (L, ℓ 0 , C, I, E, r, w) and an upper bound vector b, we construct a 2k-weighted timed automaton

Then T is a positive instance of the ELU problem with an upper bound vector b if and only if T ′ is a positive instance of the EL or ELW (with weak upper bound vector b) problems. The claim then follows from Theorem 8.

The results for the game versions of the problems follow from undecidability of GLU(1) [START_REF] Bouyer | Infinite runs in weighted timed automata with energy constraints[END_REF] together with Theorem 2.

⊓ ⊔


Sebastian S Bauer

Uli Fahrenberg

Line Juhl

Kim G Larsen

Axel Legay

Claus Thrane

Quantitative Refinement for Weighted Modal Transition Systems

Keywords: reducing complexity of design, modal specifications, quantitative reasoning

Specification theories as a tool in the development process of component-based software systems have recently attracted a considerable attention. Current specification theories are however qualitative in nature and hence fragile and unsuited for modern software systems. We propose the first specification theory which allows to capture quantitative aspects during the refinement and implementation process.

Introduction

Rigorous design of modern computer systems faces the major challenge that the systems are too complex to reason about [START_REF] Sifakis | A vision for computer science -the system perspective[END_REF]. Hence it is necessary to reason at the level of specification rather than at the one of implementations. Such specifications, which act as finite and concise abstractions for possibly infinite sets of implementations, allow not only to decrease the complexity of the design, but also permit to reason on subsystems independently.

Any reasonable specification theory is equipped with a satisfaction relation to decide whether an implementation matches the requirements of a specification, and a refinement relation that allows to compare specifications (hence sets of implementations). Moreover, the theory needs a notion of logical composition which allows to infer larger specifications as logical combinations of smaller ones. Another important ingredient is a notion of structural composition that allows to build overall specifications from subspecifications, mimicking at the implementation level e.g. the interaction of components in a distributed system. A partial inverse of this operation is given by the notion of quotient which allows to synthesize a subspecification from an overall specification and an implementation which realizes a part of the overall specification.

Over the years, there have been a series of advances on specification theories [START_REF] De | Interface-based design[END_REF][START_REF] Nyman | Modal Transition Systems as the Basis for Interface Theories and Product Lines[END_REF][START_REF] Chakrabarti | Synchronous and bidirectional component interfaces[END_REF][START_REF] Lynch | An introduction to input/output automata[END_REF]. The predominant approaches are based on modal logics and process algebras but have the drawback that they cannot naturally embed both logical and structural composition within the same formalism. Moreover, such formalisms do not permit to reason from specification to implementation through stepwise refinement.

In order to leverage those problems, the concept of modal transition systems was introduced [START_REF] Guldstrand | Automatic Verification Methods for Finite State Systems[END_REF]. In short, modal transition systems are labeled transition systems equipped with two types of transitions: must transitions which are mandatory for any implementation, and may transitions which are optional for implementations. It is well admitted that modal transition systems match all the requirements of a reasonable specification theory (see e.g. [START_REF] Raclet | Residual for component specifications[END_REF] for motivations). Also, practical experience shows that the formalism is expressive enough to handle complex industrial problems [START_REF]COMponent-Based Embedded Systems design Techniques[END_REF][START_REF] Speeds | SPEculative and Exploratory Design in Systems Engineering[END_REF].

In a series of recent work [START_REF] Bauer | Extending modal transition systems with structured labels[END_REF][START_REF] Juhl | Modal transition systems with weight intervals[END_REF], the modal transition system framework has been extended in order to reason on quantitative aspects, hence providing a new specification theory for more elaborated structures, with the objective to better meet practical needs. In this quantitative setting however, the standard Boolean satisfaction and refinement relations are too fragile. Indeed, either an implementation satisfies a specification or it does not. This means that minor and major modifications in the implementation cannot be distinguished, as both of them may reverse the Boolean answer. As observed by de Alfaro et al. for the logical framework of CTL [START_REF] Luca De Alfaro | Linear and branching system metrics[END_REF], this view is obsolete; engineers need quantitative notions on how modified implementations differ.

The main contribution of this paper is to mitigate the above problem by lifting the satisfaction and refinement relations into the quantitative framework, hence completing the quantitative approach to reason on modal transition systems. More precisely, and similarly to what has been proposed in the logical framework, we introduce a notion of distance between both specifications and implementations, which permits quantitative comparison. Given two implementations that do not necessarily satisfy a specification, we can decide through quantitative reasoning which one is the better match for the specification's requirements.

To facilitate this reasoning, we develop a notion of modal distance between specifications, which approximates the distances between their implementations. This preserves the relation between modal refinement and satisfaction checking in the Boolean setting. We show that computing distances between implementation sets is Exptime-hard, whereas modal distances are computable in NP ∩ co-NP (which is higher than for Boolean modal refinement). Akin to discounted games [START_REF] Zwick | The complexity of mean payoff games[END_REF] we can reason on behaviors in a discounted manner, giving more importance to differences that happen in the near future, while accumulating the amount by which the specifications fail to be compatible at each step. As for the games, the semantics of the outcome is considered application specific.

Modifying the semantic outcome of satisfaction has strong impact on operations between specifications. As a second contribution of this paper, we propose quantitative versions of structural composition and quotient which inherit the good properties from the Boolean setting. We also propose a new notion of relaxation, which is inherent to the quantitative framework and allows e.g. to calibrate the quotient operator.

However, there is no free lunch, and working with distances has a price: some of the properties of logical conjunction and determinization are not preserved in the quantitative setting. More precisely, conjunction is not the greatest lower bound with respect to refinement distance as it is in the Boolean setting, and deterministic overapproximation is too coarse. In fact we show that this is a fundamental limitation of any reasonable quantitative specification formalism.

Structure of the paper. We start out by introducing our quantitative formalism which has weighted transition systems as implementations and weighted modal transition systems as specifications. In Section 3 we introduce the distances we use for quantitative comparison of both implementations and specifications. Section 4 is devoted to a formalization of the notion of relaxation which is of great use in quantitative design. In the next section we see some inherent limitations of the quantitative approach, and Section 6 finishes the paper by showing that structural composition works as expected in the quantitative framework and links relaxation to quotients.

Acknowledgment. The authors wish to thank Jiří Srba for fruitful discussions during the preparation of this work.

Weighted Modal Transition Systems

In this section we present the formalism we use for implementations and specifications. As implementations we choose the model of weighted transition systems, i.e. labeled transition systems with integer weights at transitions. Specifications both have a modal dimension, specifying discrete behavior which must be implemented and behavior which may be present in implementations, and a quantitative dimension, specifying intervals of weights on each transition which an implementation must choose from.

Let ■ = [x, y] x ∈ ) ∪ {-∞}, y ∈ ) ∪ {∞}, x ≤ y be the set of closed extended-integer intervals and let Σ be a finite set of actions. Our set of specification labels is Spec = (Σ × ■) ∪ {⊥}, where the special symbol ⊥ models inconsistency. The set of implementation labels is defined as

Imp = Σ × [x, x] x ∈ ) ≈ Σ × ).
Hence a specification imposes labels and integer intervals which constrain the possible weights of an implementation.

We define a partial order on ■ (representing inclusion of intervals) by [x, y] ⊑ [x ′ , y ′ ] if x ′ ≤ x and y ≤ y ′ , and we extend this order to specification labels by (a, I) ⊑ (a ′ , I ′ ) if a = a ′ and I ⊑ I ′ , and ⊥ ⊑ (a, I) for all (a, I) ∈ Spec. The partial order on Spec is hence a refinement order; if k 1 ⊑ k 2 , then no more implementation labels are contained in k 1 than in k 2 .

Specifications and implementations are defined as follows:

Definition 1. A weighted modal transition system (WMTS) is a four-tuple (S, s 0 , , -→) consisting of a set of states S with an initial state s 0 ∈ S and must and may transition relations

-→ ⊆ ⊆ S × Spec × S. A WMTS is an implementation if -→ = ⊆ S × Imp × S.
A WMTS is finite if S and (and hence also -→) are finite sets, and it is deterministic if it holds that for any s ∈ S and a ∈ Σ, s, (a, I 1 ), t 1 , s, (a, I 2 ), t 2 ∈ imply I 1 = I 2 and t 1 = t 2 . Hence a deterministic specification allows at most one transition under each discrete action from every state. In the rest of the paper we will write s k s ′ for (s, k, s ′ ) ∈ and similarly for -→, and we will always write S = (S, s 0 , , -→) or S i = (S i , s 0 i , i , -→ i ) for WMTS and I = (I, i 0 , -→) for implementations. Note that an implementation is just a usual integer-weighted transition system.

The implementation semantics of a specification is given through modal refinement, as follows: A modal refinement of WMTS S 1 , S 2 is a relation R ⊆ S 1 × S 2 such that for any (s 1 , s 2 ) ∈ R and any may transition s 1

k 1 1 t 1 in S 1 , there exists s 2 k 2 2 t 2 in S 2 for which k 1 ⊑ k 2 and (t 1 , t 2 ) ∈ R, and for any must transition s 2 k 2 -→ 2 t 2 in S 2 , there exists s 1 k 1 -→ 1 t 1 in S 1 for which k 1 ⊑ k 2 and (t 1 , t 2 ) ∈ R.
Hence in such a modal refinement, behavior which is required in S 2 is also required in S 1 , no more behavior is allowed in S 1 than in S 2 , and the quantitative requirements in S 1 are refinements of the ones in S 2 . We write

S 1 ≤ m S 2 if there is a modal refinement relation R for which (s 0 1 , s 0 2 ) ∈ R.
The implementation semantics of a specification can then be defined as the set of all implementations which are also refinements:

Definition 2. The implementation semantics of a WMTS S is the set S = {I | I ≤ m S, I implementation}.
We say that a WMTS S is consistent if it has an implementation, i.e. if S = ∅. A useful over-approximation of consistency is local consistency: a WMTS S is said to be locally consistent if s k -→ t implies k = ⊥, i.e. if no ⊥-labeled must transitions appear in S. Local consistency implies consistency, but the inverse is not true; e.g. the WMTS s 0

S ⊥ = {s ∈ S | s ⊥ -→ t for some t ∈ S}. If s 0 / ∈ pre * (S ⊥ ), then the pruning ρ(S) = (S ρ , s 0 , ρ , -→ ρ ) is defined by S ρ = S \ pre * (S ⊥ ), ρ = ∩ S ρ × (Spec \ {⊥}) × S ρ and -→ ρ = -→ ∩ S ρ × (Spec \ {⊥}) × S ρ .
Note that if ρ(S) exists, then it is locally consistent, and if ρ(S) does not exist (s 0 ∈ pre * (S ⊥ )), then S is inconsistent. Also, ρ(S) ≤ m S and ρ(S) = S .

Thorough and Modal Refinement Distances

For the quantitative specification formalism we have introduced in the last section, the standard Boolean notions of satisfaction and refinement are too fragile. To be able to reason not only whether a given quantitative implementation satisfies a given quantitative specification, but also to what extent, we introduce a notion of distance between both implementations and specifications. We first define the distance between implementations; for this we introduce a distance on implementation labels by

i1 j1 k1 3 7 6 9 i2 j2 6 7 d(j1, j2) = 0 d(i1, j2) = ∞ d(j1, i2) = ∞ d(k1, j2) = ∞ d(k1, i2) = max{2 + .9 d(k1, i2), .9 0 d(j1, j2)} d(i1, i2) = max{3 + .9 d(j1, j2) 0 , .9 d(k1, i2)}
d Imp (a 1 , x 1 ), (a 2 , x 2 ) = ∞ if a 1 = a 2 , |x 1 -x 2 | if a 1 = a 2 .
(1)

In the rest of the paper, let λ ∈ | with 0 < λ < 1 be a discounting factor.

d(i 1 , i 2 ) = max        sup i1 k 1 -→1j1 inf i2 k 2 -→2j2 d Imp (k 1 , k 2 ) + λd(j 1 , j 2 ), sup i2 k 2 -→2j2 inf i1 k 1 -→1j1 d Imp (k 1 , k 2 ) + λd(j 1 , j 2 ).
We define d(I 1 , I 2 ) = d(i 0 1 , i 0 2 ). Except for the symmetrizing max operation, this is precisely the accumulating branching distance which is introduced in [START_REF] Thrane | Quantitative simulations of weighted transition systems[END_REF]; see also [START_REF] Fahrenberg | A quantitative characterization of weighted Kripke structures in temporal logic[END_REF][START_REF] Fahrenberg | Distances for weighted transition systems: Games and properties[END_REF] for a thorough introduction to linear and branching distances as we use them here. As the equations in the definition define a contraction, they have indeed a unique least fixed point; note that d(i 1 , i 2 ) = ∞ is also a fixed point, cf. [START_REF] Kim | Metrics for weighted transition systems: Axiomatization and complexity[END_REF].

We remark that besides this accumulating distance, other interesting system distances may be defined depending on the application at hand, but we concentrate here on this distance and leave a generalization to other distances for future work.

Example 1. Consider the two implementations I 1 and I 2 in Figure 1 with a single action (elided for simplicity) and with discounting factor λ = .9. The equations in the illustration have already been simplified by removing all expressions that evaluate to ∞. What remains to be done is to compute the least fixed point of the equation

d(k 1 , i 2 ) = max 2 + .9 d(k 1 , i 2 ), 0 which is d(k 1 , i 2 ) = 20. Hence d(i 1 , i 2 ) = max{3, .9 • 20} = 18.
To lift implementation distance to specifications, we need first to consider the distance between sets of implementations. Given implementation sets I 1 , I 2 , we define

d(I 1 , I 2 ) = sup I1∈I1 inf I2∈I2 d(I 1 , I 2 )
Note that in case I 2 is finite, we have that for all ε ≥ 0, d(I 1 , I 2 ) ≤ ε if and only if for each implementation I 1 ∈ I 1 there exists I 2 ∈ I 2 for which d(I 1 , I 2 ) ≤ ε, hence this is a natural notion of distance. Especially, d(I 1 , I 2 ) = 0 if and only if I 1 is a subset of I 2 up to bisimilarity. For infinite I 2 , we have the slightly more complicated property that d(I 1 , I 2 ) ≤ ε if and only if for all δ > 0 and any

I 1 ∈ I 1 , there is I 2 ∈ I 2 for which d(I 1 , I 2 ) ≤ ε + δ.
Note that in general, our distance on sets of implementations is asymmetric; we may well have d(I 1 , I 2 ) = d(I 2 , I 1 ). We lift this distance to specifications as follows:

Definition 5. The thorough refinement distance between WMTS S 1 and S 2 is defined as

d t (S 1 , S 2 ) = d S 1 , S 2 . We write S 1 ≤ ε t S 2 if d t (S 1 , S 2 ) ≤ ε.
Indeed this permits us to measure incompatibility of specifications; intuitively, if two specifications have thorough distance ε, then any implementation of the first specification can be matched by an implementation of the second up to ε. Also observe the special case where S 1 = I 1 is an implementation: then d t (I 1 , S 2 ) = inf I2∈ S2 d(I 1 , I 2 ), which measures how close I 1 is to satisfy the specification S 2 .

To facilitate computation and comparison of refinement distance, we introduce modal refinement distance as an overapproximation. We will show in Theorem 2 below that similarly to the Boolean setting [START_REF] Beneš | Checking thorough refinement on modal transition systems is EXPTIME-complete[END_REF], computation of thorough refinement distance is Exptime-hard, whereas modal refinement distance is computable in NP ∩ co-NP. First we generalize the distance on implementation labels from Equation (1) to specification labels so that for k, ℓ ∈ Spec we define d Spec (k, ℓ) = sup

k ′ ⊑k,k ′ ∈Imp inf ℓ ′ ⊑ℓ,ℓ ′ ∈Imp d Imp (k ′ , ℓ ′ ).
Note that d Spec is asymmetric, and that d Spec (k, ℓ) = 0 if and only if k ⊑ ℓ. Also, d Spec (k, ℓ) = d Imp (k, ℓ) for all k, ℓ ∈ Imp. Using the .

operation defined on integers by x 1 .

x 2 = max(x 1x 2 , 0), we can express d Spec as follows:

d Spec (a 1 , I 1 ), (a 2 , I 2 ) = ∞ if a 1 = a 2 d Spec (a, [x 1 , y 1 ]), (a, [x 2 , y 2 ]) = max(x 2 . -x 1 , y 1 . -y 2 ) d Spec ⊥, (a, I 2 ) = 0 d Spec (a, I 1 ), ⊥ = ∞ Definition 6. Let S 1 , S 2 be WMTS. The modal refinement distance d m : S 1 × S 2 → | ≥0 ∪ {∞} from states of S 1 to states of S 2 is the least fixed point of the equations d m (s 1 , s 2 ) = max        sup s1 k 1 1 t1 inf s2 k 2 2 t2 d Spec (k 1 , k 2 ) + λd m (t 1 , t 2 ), sup s2 k 2 -→2t2 inf s1 k 1 -→1t1 d Spec (k 1 , k 2 ) + λd m (t 1 , t 2 ).
We define d m (S 1 , S 2 ) = d m (s 0 1 , s 0 2 ), and we write The argument for existence and uniqueness of the least fixed point is exactly the same as for implementation distance in Definition 4. Like thorough refinement distance, modal refinement distance may be asymmetric.

S 1 ≤ ε m S 2 if d m (S 1 , S 2 ) ≤ ε. s1 S1 t1 a, [0, 1] s2 S2 t2 t3 a , [0 , 0 ] a , [1 , 1 ]
The next theorem shows that modal refinement distance indeed overapproximates thorough refinement distance, and that it is exact for deterministic WMTS. Note that nothing general can be said about the precision of the overapproximation in the nondeterministic case; as an example observe the two specifications in Figure 2 for which

d t (S 1 , S 2 ) = 0 but d m (S 1 , S 2 ) = ∞.
The fact that modal refinement only equals thorough refinement for deterministic specifications is well-known from the theory of modal transition systems [START_REF] Guldstrand | Automatic Verification Methods for Finite State Systems[END_REF], and the special case of S 1 locally consistent and S 2 deterministic is important, as it can be argued [START_REF] Guldstrand | Automatic Verification Methods for Finite State Systems[END_REF] that indeed, deterministic specifications are sufficient for applications.

Theorem 1. For WMTS S 1 , S 2 we have d t (S 1 , S 2 ) ≤ d m (S 1 , S 2 ). If S 1 is locally consistent and S 2 is deterministic, then d t (S 1 , S 2 ) = d m (S 1 , S 2 ).
The complexity results in the next theorem show that modal refinement distance can serve as a useful approximation of thorough refinement distance.

Theorem 2. For finite WMTS S 1 , S 2 and ε ≥ 0, it is Exptime-hard to decide whether S 1 ≤ ε t S 2 . The problem whether S 1 ≤ ε m S 2 is decidable in NP ∩ co-NP.

Relaxation

We introduce here a notion of relaxation which is specific to the quantitative setting. Intuitively, relaxing a specification means to weaken the quantitative constraints, while the discrete demands on which transitions may or must be present in implementations are kept. A similar notion of strengthening may be defined, but we do not use this here.

Definition 7. For WMTS S, S ′ and ε ≥ 0, S ′ is an ε-relaxation of S if S ≤ m S ′ and S ′ ≤ ε m S.
Hence the quantitative constraints in S ′ may be more permissive than the ones in S, but no new discrete behavior may be introduced. Also note that any implementation of S is also an implementation of S ′ , and no implementation of S ′ is further than ε away from an implementation of S. The following proposition relates specifications to relaxed specifications:

Proposition 1. If S ′
1 and S ′ 2 are ε-relaxations of S 1 and S 2 , respectively, then

d m (S 1 , S 2 ) -ε ≤ d m (S 1 , S ′ 2 ) ≤ d m (S 1 , S 2 ) and d m (S 1 , S 2 ) ≤ d m (S ′ 1 , S 2 ) ≤ d m (S 1 , S 2 ) + ε.
On the syntactic level, we can introduce the following widening operator which relaxes all quantitative constraints in a systematic manner. We write I ± δ = [xδ, y + δ] for an interval I = [x, y] and δ ∈ ◆. Definition 8. Given δ ∈ ◆, the δ-widening of a WMTS S is the WMTS S +δ with transitions s a,I±δ t in S +δ for all s a,I t in S, and s a,I±δ -→ t in S +δ for all s a,I -→ t in S.

Widening and relaxation are related as follows; note also that as widening is a global operation whereas relaxation may be achieved entirely locally, not all relaxations may be obtained as widenings.

Proposition 2. The δ-widening of any WMTS S is a (1λ) -1 δ-relaxation.

There is also an implementation-level notion which corresponds to relaxation:

Definition 9. The ε-extended implementation semantics, for ε ≥ 0, of a WMTS S is S +ε = I I ≤ ε m S, I implementation . Proposition 3. If S ′ is an ε-relaxation of S, then S ′ ⊆ S +ε .
It can be shown that there are WMTS S, S ′ such that S ′ is an ε-relaxation of S but the inclusion S ′ ⊆ S +ε is strict.

Limitations of the Quantitative Approach

In this section we turn our attention towards some of the standard operators for specification theories; determinization and logical conjunction. Quite surprisingly, we show that in the quantitative setting, there are problems with these notions which do not appear in the Boolean theory. More specifically, we show that there is no determinization operator which always yields a smallest deterministic overapproximation, and there is no conjunction operator which acts as a greatest lower bound. Theorem 3. There is no unary operator D on WMTS for which it holds that In the standard Boolean setting, there is indeed a determinization operator which satisfies properties similar to the above, and which is useful because it enables checking thorough refinement, cf. Theorem 1. Likewise, the greatestlower-bound property of logical conjunction in the Boolean setting ensures that the set of implementations of a conjunction of specifications is precisely the intersection of the implementation sets of the two specifications. Theorem 4. There is no partial binary operator ∧ on WMTS for which it holds that (4.1) S 1 ∧ S 2 ≤ m S 1 and S 1 ∧ S 2 ≤ m S 2 for all locally consistent WMTS S 1 , S 2 for which S 1 ∧ S 2 is defined, (4.2) for any locally consistent WMTS S and all deterministic and locally consistent WMTS S 1 , S 2 such that S ≤ m S 1 and S ≤ m S 2 , S 1 ∧ S 2 is defined and S ≤ m S 1 ∧ S 2 , (4.3) for any ε ≥ 0, there exist ε 1 ≥ 0 and ε 2 ≥ 0 such that for any locally consistent WMTS S and all deterministic and locally consistent WMTS S 1 , S 2 for which S 1 ∧S 2 is defined, S ≤ ε1 m S 1 and S ≤ ε2 m S 2 imply S ≤ ε m S 1 ∧S 2 . The counterexamples used in the proofs of Theorems 3 and 4 are quite general and apply to a large class of distances, rather than only to the accumulating distance discussed in this paper. Hence it can be argued that what we have exposed here is a fundamental limitation of any quantitative approach to modal specifications.

Structural Composition and Quotient

In this section we show that in our quantitative setting, notions of structural composition and quotient can be defined which obey the properties expected of such operations. In particular, structural composition satisfies independent implementability [START_REF] De | Interface-based design[END_REF], hence the refinement distance between structural composites can be bounded by the distances between their respective components.

First we define partial synchronization operators ⊕ and ⊖ on specification labels which will be used for synchronizing transitions. We let (a 1 , I 1 ) ⊕ (a 2 , I 2 ) and (a 1 , I 1 ) ⊖ (a 2 , I 2 ) be undefined if a 1 = a 2 , and otherwise

a, [x 1 , y 1 ] ⊕ a, [x 2 , y 2 ] = a, [x 1 + x 2 , y 1 + y 2 ] , (a, I 1 ) ⊕ ⊥ = ⊥ ⊕ (a, I 2 ) = ⊥; a, [x 1 , y 1 ] ⊖ a, [x 2 , y 2 ] = ⊥ if x 1 -x 2 > y 1 -y 2 , a, [x 1 -x 2 , y 1 -y 2 ] if x 1 -x 2 ≤ y 1 -y 2 , (a, I 1 ) ⊖ ⊥ = ⊥ ⊖ (a, I 2 ) = ⊥.
Note that we use CSP-style synchronization, but other types of synchronization can easily be defined. Also, defining ⊕ to add intervals (and ⊖ to subtract them) is only one particular choice; depending on the application, one can also e.g. let ⊕ be intersection of intervals or some other operation. It is not difficult to see that these alternative synchronization operators would lead to properties similar to those we show here.

Definition 10. Let S 1 and S 2 be WMTS. The structural composition of S 1 and

S 2 is S 1 S 2 = S 1 × S 2 , (s 0 1 , s 0
2 ), Spec, , -→ with transitions given as follows: The quotient of S 1 by S 2 is S 1 S 2 = ρ S 1 × S 2 ∪ {u}, (s 0 1 , s 0 2 ), Spec, , -→ with transitions given as follows:

s1 k 1 1 t1 s2 k 2 2 t2, k1 ⊕ k2 defined (s1, s2) k 1 ⊕k 2 (t1, t2) s1 k 1 -→1 t1 s2 k 2 -→2 t2 k1 ⊕ k2 defined (s1, s2) k 1 ⊕k 2 -→ (t1, t2) s1 t1 a, [0, 0] (a) S1 s2 t2 a, [0, 1] (b) S2 s3 t3 a, [0, 0] (c) S3 (s2, s3) (t2, t3) a, [0, 1] (d) S2 S3 (s1, s2) (e) S1 S2
s1 k 1 1 t1 s2 k 2 2 t2 k1 ⊖ k2 defined (s1, s2) k 1 ⊖k 2 (t1, t2) s1 k 1 -→1 t1 s2 k 2 -→2 t2 k1 ⊖ k2 defined (s1, s2) k 1 ⊖k 2 -→ (t1, t2) s1 k 1 -→1 t1 ∀s2 k 2 -→2 t2 : k1 ⊖ k2 undefined (s1, s2) ⊥ -→ (s1, s2) k ∈ Spec ∀s2 k 2 2 t2 : k ⊕ k2 undefined (s1, s2) k u k ∈ Spec u k u
Note that we ensure that the quotient S 1 S 2 is locally consistent by recursively removing ⊥-labeled must transitions using pruning, see Definition 3. The following theorem shows that structural composition is well-behaved with respect to modal refinement distance in the sense that the distance between the composed systems is bounded by the distances of the individual systems. Note also the special case in the theorem of S 1 ≤ m S 2 and S 3 ≤ m S 4 implying S 1 S 3 ≤ m S 2 S 4 .

Theorem 5 (Independent implementability). For WMTS S 1 , S 2 , S 3 , S 4 we have d m S 1 S 3 , S 2 S 4 ≤ d m (S 1 , S 2 ) + d m (S 3 , S 4 ).

The following theorem expresses the fact that quotient is a partial inverse to structural composition. Intuitively, the theorem shows that the quotient S 1 S 2 is maximal among all WMTS S 3 with respect to any distance S 2 S 3 ≤ ε m S 1 ; note the special case of S 3 ≤ m S 1 S 2 if and only if S 2 S 3 ≤ m S 1 .

Theorem 6 (Soundness and maximality of quotient). Let S 1 , S 2 and S 3 be locally consistent WMTS such that S 2 is deterministic and

S 1 S 2 is defined. If d m (S 3 , S 1 S 2 ) < ∞, then d m (S 3 , S 1 S 2 ) = d m (S 2 S 3 , S 1 ).
The example depicted in Figure 3 shows that the condition d m (S 3 , S 1 S 2 ) < ∞ in Theorem 6 is necessary. Here d m (S 2 S 3 , S 1 ) = 1, but d m (S 3 , S 1 S 2 ) = ∞ because of inconsistency between the transitions s 1 a,[0,0] 1 t 1 and s 2 a,[0,1] 2 t 2 for which k 1 ⊖ k 2 is defined.

As a practical application, we notice that relaxation as defined in Section 4 can be useful when computing quotients. The quotient construction in Definition 10 introduces local inconsistencies (which afterwards are pruned) whenever there is a pair of transitions s 1

k 1 1 t 1 , s 2 k 2 2 t 2 (or s 1 k 1 -→ 1 t 1 , s 2 k 2
-→ 2 t 2 ) for which k 1 ⊖ k 2 = ⊥. Looking at the definition of ⊖, we see that this is the case if k 1 = (a, [x 1 , y 1 ]) and k 2 = (a, [x 2 , y 2 ]) are such that x 1x 2 > y 1y 2 ; hence these local inconsistencies can be avoided by enlarging k 1 .

Enlarging quantitative constraints is exactly the intuition of relaxation, thus in practical cases where we get a quotient S 1 S 2 which is "too inconsistent", we may be able to solve this problem by constructing a suitable ε-relaxation S ′ 1 of S 1 . Theorems 5 and 6 can then be used to ensure that also S ′ 1 S 2 is a relaxation of S 1 S 2 .

Conclusion and Further Work

We have shown in this paper that within the quantitative specification framework of weighted modal transition systems, refinement and implementation distances provide a useful tool for robust compositional reasoning. Note that these distances permit us not only to reason about differences between implementations and from implementations to specifications, but they also provide a means by which we can compare specifications directly at the abstract level.

We have shown that for some of the ingredients of our specification theory, namely structural composition and quotient, our formalism is a conservative extension of the standard Boolean notions. We have also noted however, that for determinization and logical conjunction, the properties of the Boolean notions are not preserved, and that this is a fundamental limitation of any reasonable quantitative specification theory. The precise practical implications of this for the applicability of our quantitative specification framework are subject to future work.

a, 2 -→ s 1 a,9 s 2 ⊥-→ s 3 has an implementation i 0 a, 2 -→ i 1 .

 21221 Local inconsistencies may be removed recursively as follows: Definition 3. For a WMTS S, let pre : 2 S → 2 S be given by pre(B) = {s ∈ S | s k -→ t ∈ B for some k}, and let

Fig. 1 .

 1 Fig. 1. Two weighted transition systems with branching distance d(I1, I2) = 18.

Definition 4 .

 4 Let I 1 , I 2 be implementations (weighted transition systems). The implementation distance d : I 1 × I 2 → | ≥0 ∪ {∞} between the states of I 1 and I 2 is the least fixed point of the equations

Fig. 2 .

 2 Fig. 2. Incompleteness of modal refinement distance.

( 3 . 1 )

 31 D(S) is deterministic for any WMTS S, (3.2) S ≤ m D(S) for any WMTS S, (3.3) S ≤ ε m D implies D(S) ≤ ε m D for any WMTS S, any deterministic WMTS D, and any ε ≥ 0.

Fig. 3 .

 3 Fig. 3. WMTS for which dm(S3, S1 S2) = dm(S2 S3, S1).