Romain Brenguier
email: brenguier@ulb.ac.be

Franck Cassez
email: franck.cassez@nicta.com.au

Jean-François Raskin
email: jraskin@ulb.ac.be

Energy and Mean-payoff Timed Games *

In this paper, we study energy and mean-payoff timed games. The decision problems that consist in determining the existence of winning strategies in those games are undecidable, and we thus provide semi-algorithms for solving these strategy synthesis problems. We then identify a large class of timed games for which our semi-algorithms terminate and are thus complete. We also study in detail the relation between mean-payoff and energy timed games. Finally, we provide a symbolic algorithm to solve energy timed games and demonstrate its use on small examples using HyTech.

INTRODUCTION

Timed automata [START_REF] Alur | A theory of timed automata[END_REF], respectively timed games [START_REF] Maler | On the synthesis of discrete controllers for timed systems (an extended abstract)[END_REF][START_REF] Cassez | Efficient on-the-fly algorithms for the analysis of timed games[END_REF], are fundamental models to verify, respectively to synthesize controllers for, timed systems which have to enforce hard realtime constraints. Those models were introduced in the nineties and the underlying theory has since then been successfully implemented in efficient analysis tools such as Kronos [START_REF] Bozga | Kronos: A model-checking tool for real-time systems[END_REF] and UppAal [33] for verification, and UppAal-Tiga [START_REF] Behrmann | Uppaal-tiga: Time for playing games! In CAV[END_REF] for synthesis. The latter has been used to solve industrial case studies, e.g. [START_REF] Jessen | Guided controller synthesis for climate controller using Uppaal Tiga[END_REF][START_REF] Cassez | Automatic synthesis of robust and optimal controllers -an industrial case study[END_REF].

Recently, there has been an important research effort to lift verification and synthesis techniques from the Boolean case to the quantitative case, see [START_REF] Henzinger | Quantitative reactive modeling and verification[END_REF] and references therein. More specifically, lots of progress has been made recently on zero-sum two-player games played on weighted graphs, in which edges are decorated with costs or rewards, see for example [START_REF] Bouyer | Infinite runs in weighted timed automata with energy constraints[END_REF][START_REF] Chatterjee | A survey of stochastic games with limsup and liminf objectives[END_REF][START_REF] Chatterjee | Generalized mean-payoff and energy games[END_REF][START_REF] Brim | Faster algorithms for mean-payoff games[END_REF], with the objective of setting up a framework for the synthesis of optimal controllers (see also [START_REF] Tabuada | Controller synthesis for bisimulation equivalence[END_REF] for applications in linear control systems). Important examples of such games are mean-payoff and energy games [START_REF] Bouyer | Infinite runs in weighted timed automata with energy constraints[END_REF][START_REF] Brim | Faster algorithms for mean-payoff games[END_REF][START_REF] Chatterjee | Generalized mean-payoff and energy games[END_REF]. In those games, two players move a token along the edges of a weighted graph whose vertices are partitioned into vertices that belong to player 1, and player 2 respectively. In each round of the game, the player * Work supported by ERC Starting Grant inVEST (279499). that owns the vertex with the token chooses an outgoing edge and target vertex to move the token to. By playing in such a way, the two players form an infinite path through the graph. Player 1 wins the mean-payoff objective if the long-run average of the edge-weights along this path is nonnegative, and he wins the energy objective, if there exists a bound c ∈ Z such that the running sum of weights of the traversed edges along the infinite path never goes below c (this can model for example that the system never runs out of energy). As the games we consider are zero-sum, player 2 wins when he can enforce the complementary objectives. In the finite state case, the mean-payoff and energy objectives are inter-reducible, and this fact was used recently to provide algorithmic improvements to solve mean-payoff games [START_REF] Brim | Faster algorithms for mean-payoff games[END_REF].

Extensions of timed automata with costs and rewards have also been studied. In [START_REF] Alur | Optimal paths in weighted timed automata[END_REF][START_REF] Behrmann | Minimum-cost reachability for priced timed automata[END_REF], timed automata are extended with continuous variables that are used as observers, and allow for modeling accumulation of costs or rewards along executions. The main motivation for studying those extensions is to offer an extra modeling power while avoiding severe intractability of richer models like hybrid automata. Indeed, it has been shown that the reachability problem for weighted/priced timed automata remains decidable [START_REF] Alur | Optimal paths in weighted timed automata[END_REF][START_REF] Behrmann | Minimum-cost reachability for priced timed automata[END_REF], and more precisely PSPACE-c [START_REF] Bouyer | On the optimal reachability problem of weighted timed automata[END_REF], while the reachability problem is undecidable already for the class of stopwatch automata [START_REF] Cassez | The impressive power of stopwatches[END_REF] (a simple class of hybrid automata). Also the existence of executions in a weighted automaton that ensure a bound on the mean-payoff can also be decided in PSPACE [START_REF] Bouyer | Staying alive as cheaply as possible[END_REF]. In this paper, we consider timed extensions of the important classes of mean-payoff and energy games.

+3 [x ≤ 2]

-2

[x ≤ 2]
x ≥ 1, x ∶= 0

x ≥ 1, x ∶= 0 Example 1. Fig. 1 gives an example of an energy (turnbased) timed game. Eve (player 1) owns the left location and decides when to take the transition from left to right, while Adam (player 2) owns the right location and decides when to take the transition from right to left; x is a dense-time clock. Each transition resets the clock x, and when time elapses the energy level grows with derivative 3 in Eve's location and decreases with derivative 2 in Adam's location. In the remaining of this paper, we use the following conventions: plain (resp. dashed) arrows are Eve's (resp. Adam's) transitions; a location invariant is enclosed in brackets (e.g.

[x ≤ 2]) and must be satisfied by the valuation of the clocks when the control is in that location; when an edge weight is non zero, we attach it to the edge. Fig. 2, left, depicts the initial energy levels that are sufficient for Eve in order to have a winning strategy against any strategy of Adam, i.e. to ensure an infinite execution in which the energy level never falls below 0. For instance, if the infinite game starts in Eve's location, then if the value of clock x is less than 2 3 , an initial energy level 0 is sufficient; for x > 2 3 , the initial energy level should be larger than or equal to 3 ⋅ x -2. Similarly, the winning zone in Adam's location is depicted on the right hand side of Fig. 2. The main purpose of this article is to propose algorithmic methods to compute such information.

Unfortunately, for weighted extensions of timed games, even the cost bounded reachability problem is undecidable [START_REF] Brihaye | On optimal timed strategies[END_REF], and we show here that both mean-payoff and energy games are undecidable. This is unfortunate as such cost extensions of timed games are very natural and well-suited to model optimality problems in embedded control [START_REF] Cassez | Automatic synthesis of robust and optimal controllers -an industrial case study[END_REF]. Nevertheless, we believe that the undecidability result should not be an end to the story and we study in this paper semialgorithms (completeness and/or termination is not guaranteed) to solve those two synthesis problems. We also identify a large class of timed games where our semi-algorithms are complete. To the best of our knowledge, there are the first positive results for those objectives on timed automata. There are related works in the literature but they apply to orthogonal classes of games, or to other objectives. Indeed, in [START_REF] Bouyer | Average-price and reachability-price games on hybrid automata with strong resets[END_REF], it is shown that mean-payoff games are decidable for O-minimal hybrid automata, this class is different from the one identified here as timed automata are not O-minimal hybrid automata. In [START_REF] Jurdzinski | Average-time games[END_REF], the authors study the average time per transition problem for turn-based timed games; their results do not apply to mean-payoff, nor to energy objectives.

Contributions. Our contribution is threefold. First, we study the relation between mean-payoff and energy timed games. As we already mentioned, in the finite state case, the mean-payoff and energy objectives are inter-reducible [START_REF] Brim | Faster algorithms for mean-payoff games[END_REF]: given a weighted game G, Eve wins the mean-payoff objective if, and only if, she wins the energy objective. We show here that the relationship between the two types of games is more complex in the timed case. We identify conditions under which it is possible to transfer winning strategies for one objective into winning strategies for the other objective, and we show that those conditions are also necessary. Those results are formalized by Thm. 1 and Thm. 2. Second, Thm. 3 establishes the undecidability of the decision problems associated with energy and mean-payoff timed games. This result is unfortunate but not surprising (it was already conjectured in [START_REF] Bouyer | From qualitative to quantitative analysis of timed systems -Mémoire d'habilitation à diriger des recherches[END_REF], see page 89). This negative result motivates the main contribution of this paper: we propose two semi-algorithms for synthesizing winning strategies. We first consider a cycle forming game (in the spirit of [START_REF] Björklund | Memoryless determinacy of parity and mean payoff games: a simple proof[END_REF]) on the region graph associated with the underlying weighted timed game: the two players move a token on the region graph and the game is stopped as soon as a cycle is formed. In Sect. 3.5, we partition the set of simple cycles of the region graph into those that are good for Eve, those that are good for Adam, and those that are neither good for Eve nor for Adam. If the formed cycle belongs to the first set then Eve is declared winner of the cycle forming game, if the cycle belongs to the second then Adam is the winner, otherwise it is a draw. Thm. 4 establishes that if Eve wins the cycle forming game then she has also a winning strategy in associated energy games, and Thm. 5 proves a similar result for Adam. Then, we identify a class of weighted timed games, that we call robust, for which this reduction to the cycle forming game on the region graph is complete: in this case the good cycles for Eve and the good cycles for Adam partition the set of simple cycles of the region graph. This class covers the class of timed games where costs appear on edges only. Thm. 11 establishes the decidability of the membership problem for the class of robust weighted timed games.

Finally, as the cycle forming game is defined on the region graph, it does not lead to a practical algorithmic solution. This is why we propose in addition a symbolic semialgorithm to solve energy timed games. In Thm. [START_REF] Bouyer | Lower-bound constrained runs in weighted timed automata[END_REF], we show that our symbolic algorithm is also complete on the class of robust weighted timed games. In order to show the feasibility of our approach, we have implemented this algorithm as a script for HyTech [START_REF] Henzinger | Hytech: A model checker for hybrid systems[END_REF] and ran it on small examples.

Our main theorems and their relation with the different classes of games we consider are depicted in Fig. 3 and4.

Structure of the paper. In Sect. 2, we define the meanpayoff and energy timed games. In Sect. 3, we develop semialgorithms based on reductions to cycle games played on the region graph. In Sect. 4, we identify a class robust games, for which the reduction to cycle games is complete. In Sect. 5, we propose a symbolic semi-algorithm which is also complete for robust games.

PRELIMINARIES

In this section, we first recall the definition of concurrent games. Then we review a useful result from [START_REF] Jurdziński | Deciding the winner in parity games is in UP and in co-UP[END_REF] that defines a canonical decomposition of infinite paths in a graph into simple cycles. Next, we introduce weighted timed games, the semantics of which is given in term of infinite concurrent games. Starting from the notion of weight (or cost/reward), we define mean payoff and energy objectives. We close the section with a study of the relationships that exist between

Mean payoff Energy

Unknown credit

Cycle forming

Thm. 1

Thm. 4

Thm. 4

Thm. 9 Thm. 9 We let N be the set of natural numbers, Z the set of integers, R the set of reals and R+ the set of non-negative reals.

Concurrent Games

Definition 1. ( [START_REF] Alur | Alternating-time temporal logic[END_REF]) A concurrent game between two players Eve and Adam is a tuple C = ⟨St, ι, Act, Mov, Tab, Ω⟩, where:

• St is the set of states;

• ι ∈ St is the initial state;

• Act is the set of actions;

• Mov ∶ St × {Eve, Adam} ↦ 2 Act ∖ {∅} gives for a state and a player the set of allowed actions, we let A round of the game consists in Eve and Adam to choose independently and simultaneously some actions, say a∃ and a∀ respectively, such that a∃ ∈ Mov(s, Eve) and a∀ ∈ Mov(s, Adam).

Mov(s) = {(a, b) a ∈ Mov(s, Eve), b ∈ Mov(s, Adam)}; • Tab ∶ St × Act × Act ↦ St is the transition function; • Ω ⊆ (St ⋅ (Act × Act))
The pair m = (a∃, a∀) is an allowed move i.e. m ∈ Mov(s). By playing finitely (resp. infinitely) many rounds from state s ∈ St, the players build a finite (resp. infinite) path. Formally, a path is a finite or infinite sequence s0 ⋅ m0 ⋅ s1 ⋅ m1⋯s k ⋅ m k ⋯ of alternating states and moves, such that ∀i ≥ 0, mi ∈ Mov(si) and si+1 = Tab(si, mi). We also write a path as s0

m 0 → s1 m 1 → ⋯. The length, ρ , of an infinite path
ρ is ∞ and the length of a finite path ρ with n moves (ending in sn) is n and last(ρ) = sn. We write ρn, n ≤ ρ , for sn, the n + 1-th state in ρ, and first(ρ

) = ρ0 = s0. Given a path ρ = s0 m 0 → s1 m 1
→ ⋯, we write ρ≤n, n ≤ ρ for the prefix of ρ up to sn that is the finite path s0

m 0 → ⋯ m n-1 → sn.
A play is an infinite path in (St ⋅ (Act × Act)) ω , and a history is a finite path in (St ⋅ (Act × Act)) * ⋅ St. The set of plays from s is Play(C, s) and Play(C) = Play(C, ι). A play is winning for Eve if it belongs to the objective Ω.

Definition 2. (Strategies) A strategy for Eve (resp. Adam) is a function which associates with a history h an Eve-action in Mov(last(h), Eve) (resp. an Adam-action). A pair of strategies (σ∃, σ∀) forms a strategy profile. Given a strategy profile, its outcome from state s, written Outs(σ∃, σ∀), is the unique play ρ such that: ρ0 = s and ∀n ≥ 0, ρn+1 = Tab(ρn, σ∃(ρ≤n), σ∀(ρ≤n)). Given a strategy σ∃ of Eve, its outcomes from state s, written Outs(σ∃), are the set of plays ρ for which there is a strategy σ∀ of Adam, such that ρ = Outs(σ∃, σ∀). A strategy σ∃ of Eve is winning, if for all strategies σ∀ of Adam, Outι(σ∃, σ∀) ∈ Ω; strategy σ∀ of Adam is winning, if for all strategies σ∃ of Eve, Outι(σ∃, σ∀) ∈ Ω.

Decomposition in Simple Cycles

In the sequel we will reduce energy and mean payoff games to games played on the region with cycles objectives. In this paragraph we recall the key results [START_REF] Jurdziński | Deciding the winner in parity games is in UP and in co-UP[END_REF] related to the decomposition of a play into simple cycles.

A history h = s0 ⋅ m0 ⋅ s1 ⋅ m1⋯sn is a cycle if s0 = sn, n ≥ 1. A simple cycle
is a cycle such that for all i and j, 0 ≤ i < j < n, si ≠ sj. We write C(C) (C when C is clear from the context) for the set of simple cycles in the concurrent game C.

Every history h of a finite game can be uniquely decomposed into a sequence of simple cycles, except for a finite part. The decomposition process maintains a stack, st(h), of distinct states and moves. We write the stack content s1 ⋅ m1 ⋅ s2 ⋅ ⋯ ⋅ mn-1 ⋅ sn where s1 is at the bottom of the stack and sn the top. We use the notation s ∈ st(h) for s ∈ {s1, s2, ⋯, sn}. The decomposition, dec(h), is a set of simple cycles. We define dec(h) and st(h) inductively as follows:

• for the single state history s, dec(s) = ∅ and st(s) = s.

• let h ′ = h ⋅ m ⋅ s, m a move, s ∈ St, be a history.

-If s ∈ st(h), and st(h) = α ⋅ s ⋅ β, then st(h ′ ) = pop(st(h), β ) and dec(h ′ ) = dec(h)∪{s⋅β ⋅m⋅s}.

else dec(h ′ ) = dec(h), st(h ′ ) = push(st(h), m⋅s).

Note that the stack always contains distinct elements, therefore only simple cycles are added to the decomposition. The elements in the stack from the bottom to the top, form a history s0 ⋅ m0 ⋅ s1 ⋅ m1 ⋯ sn, where n + 1 is the height of the stack. The decomposition of a play is the union of the decompositions of the finite prefixes of the play.

Weighted Timed Games

Let X be a finite set of variables called clocks. A clock valuation is a mapping v ∶ X → R+. We let R X + be the set of clock valuations over X. We let 0 X be the zero valuation where all the clocks in X are set to 0 (we use 0 when X is clear from the context). Given δ ∈ R+, v + δ denotes the valuation defined by (v + δ)(x) = v(x) + δ. We let C(X) be the set of convex constraints on X which is the set of conjunctions of constraints of the form x ⋈ c with c ∈ N and ⋈ ∈ {≤, <, =, >, ≥}. Given a constraint g ∈ C(X) and a valuation v, we write

v ⊧ g if g is satisfied by v. Given Y ⊆ X and a valuation v, [Y ← 0]v is the valuation defined by ([Y ← 0]v)(x) = v(x) if x ∈ Y and ([Y ← 0]v)(x) = 0 otherwise.
Definition 3. A weighted timed game [START_REF] La Torre | Optimal-reachability and control for acyclic weighted timed automata[END_REF] (WTG for short) is a tuple T = ⟨L, ℓι, X, T∃, T∀, Inv, w⟩, where:

• L is the (finite) set of locations and ℓι is the initial location;

• X is a finite set of clocks;

• T∃, T∀ ⊆ L × C(X) × 2 X × L are the set of transitions belonging to Eve and Adam respectively, and we let T = T∃∪T∀; An element of T∃ (resp. T∀) is an Eve-transition (resp. Adam-transition).

• Inv∶ L → C(X) defines the invariants of each location; Similarly for a∀. We assume that from any reachable state of the game, at least one player has a legal action, hence the pair ( , ) is never proposed.

• w∶ L ∪ T → Z
To determine the effect of a joint action, we select the player p that chooses the shortest delay dp. In case both players choose the same delay, the convention is that Adam is selected (this is without loss of generality and other policies can be accommodated for). These informal game rules are formalized in the next section.

Semantics of Timed Games

Given a timed action (d, e) ∈ R+ × T with e = (ℓ, g, Y, ℓ ′ ), a state (ℓ, v), the successor state in the WTG is

(ℓ ′ , v ′ ) if: 1. ∀0 ≤ δ ≤ d, v + δ ⊧ Inv(ℓ);
2. and v + δ ⊧ g;

3. and [Y ← 0](v + d) ⊧ Inv(ℓ ′ ).
We denote this transition (ℓ, v)

(d,e)
→ (ℓ ′ , v ′ ) which accounts for a combined delay transition of d time units followed by the discrete step firing edge e. The duration of this transition is d((ℓ, v)

(d,e) → (ℓ ′ , v ′ )) = d. Its reward (or weight) is w((ℓ, v) (d,e) → (ℓ ′ , v ′ )) = d ⋅ w(ℓ) + w(e).
Given an objective Ω ⊆

(L × R X + ) ⋅ ((R+ × T∃) × (R+ × T∀)) ω ,
the semantics of the WTG T is the (infinite) concurrent game C(T , Ω) = (St, ι, Act, Mov, Tab, Ω) defined by:

• the set of states is St = L × R X + and the initial state is ι = (ℓι, 0);

• the set of actions is Act = Act∃ ∪ Act∀, where Act∃ = R+ × T∃ are the actions for Eve and Act∀ = R+ × T∀ are the actions for Adam; if a∃ = (resp. a∀ = ) then Adam (resp. Eve) is selected and Mov(a∃, a∀) = a∀ (resp. Mov(a∃, a∀) = a∃);

• Mov(s, Eve) ∈ 2 Act ∃ ∖ {∅} ∪ { }
otherwise a∃ = (d∃, e∃) and a∀ = (d∀, e∀) and:

1. if d∃ < d∀, Mov(a∃, a∀) = a∃; 2. if d∀ ≤ d∃ then Mov(a∃, a∀) = a∀;

• Given two actions a∃ and a∀, Tab((ℓ, v), a∃, a∀)

= (ℓ ′ , v ′ ) if (ℓ, v) Mov(a ∃ ,a ∀ ) → (ℓ ′ , v ′ ). Let h = s0 a ∃ 1 ,a ∀ 1 → s1 ⋯ sn-1 a ∃ n-1 ,a ∀ n-1
→ sn⋯ be a finite or infinite path in C(T , Ω). The duration and reward of h are respectively: → Tab((ℓ, v), a∃, a∀) ≤ D.

d(h) = h -1 k=0 d s k Mov(a ∃ k ,a ∀ k ) → s k+1 w(h) = h -1 k=0 w s k Mov(a ∃ k ,a ∀ k ) → s k+1 A play ρ is said non-Zeno if (d(
-1

0 0 < x Figure 5: WTG B. 0 0 x = 0 -1 0 x < 1

Mean-payoff and Energy Objectives

The mean payoff (per time unit) of a play is defined as the long-run average of reward per time unit. Formally, the mean payoff of a play ρ is:

MP(ρ) = lim inf n→∞ w(ρ≤n) d(ρ≤n)
.

Definition 4. We consider the following types of games:

• The mean payoff game TMP associated with a WTG T , is the game played on T where the objective (for Eve) is to obtain a non-negative mean payoff: i.e. TMP = C(T , ΩMP) where ΩMP = {ρ ∈ Play(C) MP(ρ) ≥ 0}. • Given an initial credit c ≥ 0, the c-energy game T E(c) associated to a WTG T , is the game played on T where the objective Ω(c) is to maintain the reward of every prefix of every play above -c: i.e. T E(c) = C(T , Ω(c))

where Ω(c) = {ρ ∈ Play(C) ∀n ∈ N. c + w(ρ≤n) ≥ 0}.

• The energy game associated with a WTG T , is the game C(T , Ω E ) where the objective is Ω E = ∪c≥0Ω(c).

Decision problems. For each type of games, we define the associated decision problem:

• Mean-payoff : Given a mean payoff game TMP, is there a winning strategy for Eve in TMP? • c-energy: Given a c-energy game T E(c) , is there a winning strategy for Eve in T E(c) ?

• Energy: Given an energy game T E , is there a winning strategy for Eve in T E ?

We also consider the following related problem:

• Unknown initial credit: Given a WTG T , is there a credit c such that Eve has a winning strategy in T E(c) ?

We also consider these problems from Adam's point of view.

To conclude this section we study the relations between mean payoff and energy games and state that all decision problems we have defined are undecidable for WTG.

Relations Between Mean-payoff and Energy Objectives

Obviously, if for some c the c-energy game is won by Eve, then the energy game is also won. In the other direction, if

Adam has a winning strategy for the energy game then it is also winning for any c-energy game. In the finite state case the problem of energy and unknown initial credit are equivalent [START_REF] Brim | Faster algorithms for mean-payoff games[END_REF]: if Eve has a winning strategy for the energy game she has a memoryless one, and there is a bound on the maximum energy consumed by the outcomes of that strategy. This is not the case in general for WTG as demonstrated by the WTG B of Fig. 5, for which Eve wins the mean-payoff game and the energy game, but no c-energy game.

While energy and mean-payoff objectives are inter-reducible in the finite state case [START_REF] Brim | Faster algorithms for mean-payoff games[END_REF], the relationships between the two classes of objectives, formalized in the next two theorems, is more subtle for weighted timed games.

Theorem 1. Let T be a WTG. If Eve has a winning strategy σ∃ in the energy game T E and σ∃ is immune from Zenoness, then σ∃ is a winning strategy in the mean payoff game TMP.

Proof. Let σ∃ be a strategy for Eve in T E . Let σ∀ be a strategy for Adam, and ρ = Out (ℓ 0 ,0) (σ∃, σ∀). We know that ∃c. ∀n. c + w(ρ≤n) ≥ 0. As ρ is non-Zeno, 1. for n sufficiently large, d(ρ≤n) > 0 and 2. limn→∞ d(ρ≤n) = ∞.

Hence for n sufficiently large, w(ρ≤n) d(ρ≤n) ≥ -c d(ρ≤n) and the limits are in the same order, this means that MP(ρ) ≥ 0. Therefore σ∃ is also winning in the mean-payoff game.

Example 2. The following example shows that if we do not have immunity from Zenoness, the property no longer holds. In the game of Fig. 6, any play is winning for Eve in the c-energy game if c > 1. However, the total delay of a play is always smaller or equal to 1, hence the mean-payoff is smaller than -1, which means that Eve is losing.

We let T +δ be the game T in which we increase the weights of all locations by δ ∈ R. Formally T +δ is the WTG ⟨L, ℓι, X, T∃, T∀, Inv, w +δ ⟩, where:

1. w +δ (ℓ) = w(ℓ) + δ if ℓ ∈ L; 2. w +δ (t) = w(t) if t ∈ T .
Theorem 2. Let T be a WTG. If there exists δ > 0, such that Adam has a winning strategy σ∀ in the energy game T +δ E which is immune from Zenoness, then σ∀ is a winning strategy in the mean payoff game TMP.

Proof. Let σ∀ be a strategy which is winning the energy game T +δ E and immune from Zenoness. Let σ∃ be a strategy for Eve and ρ be the outcome Out (ℓι,0) (σ∃, σ∀). We know that ∀c. ∃n. c+w +δ (ρ≤n) < 0, so ∀c. ∃n. c+w(ρ≤n)+d(ρ≤n)⋅δ < 0. We define the sequence (n k ) k∈N by n0 = 0 and given n k we choose n k+1 such that writing

c k = max{-w(ρ≤n) -d(ρ≤n) ⋅ δ n ≤ n k } we have that c k + w(ρ≤n k+1 ) + d(ρ≤n k+1 ) ⋅ δ < 0.
Notice that the sequence n k is strictly increasing. Since σ∀ is immune from Zenoness, after for k big enough, d(ρ≤n k ) > 0.

We have that

w(ρ≤n k ) d(ρ≤n k ) < -c k d(ρ≤n k ) -δ.
Hence lim infn→∞ w(ρ≤n) d(ρ≤n) ≤ -δ. This means that MP(ρ) < 0, therefore τ∀ is also winning in the mean-payoff game T .

Example 3. The following example shows that if we do not add this δ to the weight of locations, the property no longer holds. In the game of Fig. 7, for any initial credit c, Adam wins the c-energy game T E(c) . However Eve has a winning strategy in the mean-payoff game TMP. She has to choose a delay which increases fast enough so that the weight of the play is small compared to its duration. For instance, if at the n-th step of the game, she chooses to delay for n 2 time units, the average weight of the play will be greater than -1 n . Hence it converges towards 0 and the mean-payoff is 0. Notice that if we add a small positive δ to the weight of each location, then following the same strategy, Eve also wins the c-energy game T E(c) for c greater than 1 δ .

0 0 x = 0 -1 0 x ← 0 Figure 7: A WTG T . 1 2 1 2 x = 0 -1 0 x ← 0 Figure 8: WTG T + 1 2 .
As already announced in the introduction, all the decisions problems that we have defined on weighted timed games are undecidable. The following theorem can be established using variants of techniques used in [START_REF] Brihaye | On optimal timed strategies[END_REF][START_REF] Bouyer | Lower-bound constrained runs in weighted timed automata[END_REF]:

Theorem 3.
The mean-payoff, c-energy, energy and unknown initial credit problems are undecidable for WTG.

Proof. The c-energy problem was already proven undecidable in [START_REF] Bouyer | Lower-bound constrained runs in weighted timed automata[END_REF] for one player (i.e. Adam does not control any transition). However in the one player case, [START_REF] Bouyer | Lower-bound constrained runs in weighted timed automata[END_REF] also proves that the unknown initial credit is in PSPACE. We will adapt the proof of undecidability of the c-energy problem for the other problems, making use of the extra player Adam.

We encode linear constraints for two clocks x and y which stay between 0 and 1 as illustrated by the example of Fig. 12.

A play entering the module y ≤ 2x, in Fig. 11 has a reward of 2xy each times it comes back to the first module +x. Hence it is winning for Eve for the energy objective only if y ≤ 2x. It is easy to adapt this module to encode constraints of the type a ⋅ y ≤ b ⋅ x with a, b ∈ N.

We will then use these linear constraints to encode a twocounter machine. We use two clocks x1 and y1 for counter c1 and two clocks x2 and y2 for counter c2. The value of counter c1 is encoded by 1 2 x 1 and c2 by 1 2 x 2 . Clocks y1 and y2 are used to remember the value of clocks x1 and x2 before they are updated by increments and decrements so that we (i.e. Adam) can check that the operation was performed correctly. Eve has to choose when to reset x1 to 0. In the second state Adam can choose to check if x1 = y 1 2 . Therefore Eve loses if she does not divide the valuation of x1 by two, which means adding 1 to c1. In the last state, we reset x1 and y1 at the same time so that the property x1 = y1 is satisfied when entering the next module.

0 1 z = 0 x = 1; x ← 0 z = 1; z ← 0 y = 1; y ← 0 y = 1; y ← 0 Figure 9: Module +x 1 0 z = 0 x = 1; x ← 0 z = 1; z ← 0 y = 1; y ← 0 y = 1; y ← 0 Figure 10: Module +(1 -x) +x +x +(1 -y) z = 0 -1 Figure 11: Module y ≤ 2x 0 y ≤ 2x y ≥ 2x z = 0
Once the accepting state is reached, the weight of the play no longer decreases. Therefore if the machine terminates, there is a strategy for Eve that reaches this final state, and wins for the c-energy game where c is the number of execution steps of the machine times 2. This strategy is also winning for the mean payoff and the energy game.

Conversely if the machine does not terminate, either:

• the game stays in the states that encode the different instruction of the machine, like the one in Fig. 14, in that case there is a reward of -1 at each time step;

-1 -1 2 ⋅ x1 = y1 -1 t = 0 q1 x1 ← 0 y1 = 1; y1 ← 0 y2 = 1; y2 ← 0 x2 = 1; x2 ← 0 t = 1; t ← 0 t = 0 t = 0 x1 = 1; x1 ← 0; y1 ← 0 y2 = 1; y2 ← 0 x2 = 1; x2 ← 0 t = 1; t ← 0 q2

→ q2

• or Eve has to "cheat" at some point which is the occasion for Adam to punish this by taking the edge going to a module that check the values of the clocks, like the one in Fig. 12.

Therefore Eve has no winning strategy in the energy game.

Moreover the strategy of Adam we described is also winning in the mean-payoff game.

A SEMI-PROCEDURE USING REGIONS

In this section, starting from the classical notion of regions [START_REF] Alur | A theory of timed automata[END_REF], we define a finite concurrent game that exploits the relationship between timed paths and their projections in the region graph. We identify simple cycles in the region graph that are good for Eve (they roughly correspond to fragments of timed paths with positive reward), and others that are good for Adam (they roughly correspond to fragments of timed paths with negative reward). Thm. 4 tells us that if Eve can force to visit only her good cycles in the region graph then she has a winning strategy in the original energy timed game, and Thm. 5 is a symmetric result for Adam. To formalize those results, we need the notion of quasi-path: when we decompose a timed path according to simple cycles of the region graph, we introduce jumps inside regions because we remove a fragment of a timed path that starts inside a region and ends up in a possibly different state of the same region. Finally, we show how to solve the cycle forming game. This reduction is not complete: there are games which have winning strategies for Eve (or Adam) that our procedure will not find. However, we identify in Section 4 a class of games for which this reduction is complete.

Regions

We first recall the classical notion of regions [START_REF] Alur | A theory of timed automata[END_REF]. If k ∈ N, we write C k (X) for the set of constraints in C(X) in which constants are integers within the interval ⟦0; k⟧. Let T be a WTG, and let M = max{c x ∼ c is a constraint in T }.

For δ ∈ R+, we write ⌊δ⌋ the integral part of δ and fr(δ) its fractional part. The equivalence relation ≡ X,M over R X + ×R X + by v ≡ X,M v ′ if, and only if:

1. for all clocks x ∈ X, either ⌊v(x)⌋ and ⌊v ′ (x)⌋ are the same, or both v(x) and v(x) exceed M ;

2. for all clocks x, y ∈ X with v(x) ≤ M and v(y) ≤ M , fr(v(x)) ≤ fr(v(y)) if, and only if, fr(v ′ (x)) ≤ fr(v ′ (y));

3. for all clocks x ∈ X with v(x) ≤ M , fr(v(x)) = 0 if, and only if, fr(v ′ (x)) = 0;

This equivalence relation naturally induces a partition R X,M of R X + . We write [v] X,M ([v] when X and M are fixed) for the equivalence class of v ∈ R X

+ . An equivalence class is called a region. It is well known that this partition has the following properties:

1. it is compatible with the constraints in C M (X), i.e.

for every r ∈ R X,M , and constraint g ∈ C M (X) either all valuations in r satisfy the clock constraint g, or no valuation in r satisfies it;

2. it is compatible with time elapsing, i.e. if there is v ∈ r and t ∈ R+ such that v + t ∈ r ′ , then for all v ′ ∈ r there is

t ′ such that v ′ + t ′ ∈ r ′ ; 3. it is compatible with resets, i.e. if Y ⊆ X then if [Y ← 0]r ∩ r ′ ≠ ∅ then [Y ← 0]r ⊆ r ′ .
A region r is said to be time-elapsing, if for any v ∈ r there is t > 0 such that v + t ∈ r. We write Succ(r) the successors of r by time elapsing, it is defined by

r ′ ∈ Succ(r) if there is v ∈ r and t ≥ 0 such that v + t ∈ r ′ .
The number of region is bounded by X ! ⋅ (4M + 4) X , note that this is exponential both in the number of clocks in X and in the size of the binary encoding of the maximal constant.

Region Game

Given an objective Ω ⊆ ((L × R X,M ) ⋅ Act) ω , the region game associated with a WTG T = ⟨L, ℓ0, X, T∃, T∀, Inv, w⟩ is the concurrent game R(T , Ω) = ⟨St, ι, Act, Mov, Tab, Ω⟩ where:

• St = L × R X,M and ι = (ℓι, 0) is the initial state;
• Act is the set of actions. They are either or of the form (r, e, a) where r ∈ R X,M , e ∈ T∃ ∪ T∀ is a transition, and a ∈ {head; tail}; intuitively, an action is a target region (abstract delay) and a discrete transition. The extra component in {head; tail} is needed to determine who plays first when the two players choose the same abstract delay (target region).

• Let s = (ℓ, r). Action (r ′ , e, a) belongs to Mov(s, Eve) (resp. Mov(s, Adam)), if:

1. ∃(ℓ, g, Y, ℓ ′ ) ∈ T∃ (resp. T∀); 2. r ′ ∈ Succ(r); 3. r ′ ⊆ Inv(ℓ); 4. r ′ ∩ g ≠ ∅;
5. and

[Y ← 0]r ′ ⊆ Inv(ℓ ′ ).
If there are no such action then only is allowed and this is the only situation in which is allowed.

• Let s = (ℓ, r) and (r∃, e∃, a∃) ∈ Mov(s, Eve), (r∀, e∀, a∀) ∈ Mov(s, Adam). s ′ = Tab(s, (r∃, e∃, a∃), (r∀, e∀, a∀)) is defined as follows:

if r∃ ≠ r∀, one region is a strict (time abstract) predecessor of the other (as they are both successors of r). If r∃ is a strict predecessor of r∀, Eve's action (r∃, e∃, a∃) is selected and otherwise Adam's action (r∀, e∀, a∀) is selected.

otherwise r∃ = r∀ and two cases arise:

1. either r∃ is not a time-elapsing region: in this case Adam's move is selected; 2. or r∃ is a time-elapsing region; which move is selected then depends on the extra components a∃, a∀ ∈ {head; tail}: if a∃ = a∀ then Eve's move is selected and otherwise Adam's move is selected.

Once an action (r ′ , e, a) with e = (ℓ, g, Y, ℓ ′ ) is selected, the resulting state is

s ′ = (ℓ ′ , r ′′ ) with r ′′ = [Y ← 0]r ′ .
Remark 1. In case T is turn-based, then in each state of R(T , Ω) only one player has a choice. The region game can then be seen as a (classical) turn-based finite game.

Example 4. We want to reduce the problem of finding winning strategies in a WTG to an equivalent problem in the region game. To illustrate the need for the extra component in the actions (i.e. a ∈ {head; tail}) consider the example of Fig. 15. In the WTG (left), Eve has no winning strategy to win the mean payoff game: Adam can always choose a delay shorter than her from ℓ0 to enforce location ℓ2. For the same reason Adam has also no winning strategy. In the region game (right), we abstract away from the actual delays Eve and Adam can propose: they have only one possible choice which is to propose to delay up-to region 0 < x < 1. To reproduce the possibility that either Eve or Adam are able to propose the smallest delay, we use the choices of both players in {head, tail}.

ℓ0, w = 0 [x < 1] ℓ1, w = 1 ℓ2, w = -1 0 < x < 1 0 < x < 1 ℓ0, r0 ℓ1, r1 ℓ2, r1
head, head tail, tail head, tail tail, head

Game Simulation

In this part, we show that the region game is a game simulation of the WTG.

Definition 5. Let C and C ′ be two games. A relation R is a game simulation between C and

C ′ if for all states s ∈ St, s ′ ∈ St ′ if s R s ′ then: ∀a∃ ∈ Mov(s, Eve). ∃b∃ ∈ Mov ′ (s ′ , Eve). ∀b∀ ∈ Mov ′ (s ′ , Adam). ∃a∀ ∈ Mov(s, Adam).
Tab(s, a∃, a∀) R Tab ′ (s ′ , b∃, b∀)

We say that C ′ simulates C if there exists such a relation R with ι R ι ′ , where ι (resp. ι ′ ) is the initial state of C (resp. C ′ ). When a∃ and b∃ are witness of the above property we say that action b∃ simulates action a∃ in s. When the inverse relation is a game simulation between C ′ and C, it is called a game bisimulation.

The following proposition shows that R(T , Ω) simulates T .

Proposition 1. The relation ⊏ defined by (ℓ, v) ⊏ (ℓ ′ , r) ⇔ ℓ = ℓ ′ ∧ v ∈ r is a game bisimulation.
We decompose the proposition in two lemmas.

Lemma 1. The relation ⊏ is a simulation. Proof. Let (ℓ, v) ⊏ (ℓ, r), we have that r = [v]. Let a∃ ∈ Mov((ℓ, v), Eve).
If a∃ = , then take b∃ = . Otherwise let (d, e) = a∃. We define b∃ to be (r ′ , e, head) such that v + d ∈ r ′ . This action is allowed in T , since r ′ is a successor of [v] satisfying the invariant of ℓ, the guard of e and the invariant of the target of e after reset.

We now show that: ∀b∀ ∈ Mov ′ ((ℓ, r), Adam). ∃a∀ ∈ Mov((ℓ, v), Adam).

Tab ′ ((ℓ, r), b∃, b∀) ⊏ Tab((ℓ, v), a∃, a∀).

• If b∀ = then we set a∀ = , as it is the only action allowed for Adam in (ℓ, v).

Tab ′ (b∃, ) = (r ′ [z ← 0], ℓ ′′ )
where b∃ = (r ′ , e, head) and e = (ℓ, g, z, ℓ ′′ ). By definition, v

+ d ∈ r ′ . Hence v + d∃[z ← 0] ∈ r ′ [z ← 0] and Tab((ℓ, v), a∃, ) ∈ Tab ′ ((ℓ, r), b∃, ). • If b∃ = then a∃ = . Take a∀ = (d, e∀) such that v + d ∈ r ′ .
By the same reasoning Tab((ℓ, v), , a∀) ⊏ Tab ′ ((ℓ, r), , b∀).

Otherwise let (r∃, e∃, a∃) = b∃ and (r∀, e∀, a∀) = b∀. We set a∀ = (d∀, e∀) such that v + d∀ ∈ r∀ and if e∃ is selected then d∃ < d∀ and otherwise d∃ ≥ d∀. This is possible because if e∃ is selected then either r∀ is a (strict) successor of r∃ or r∀ = r∃ and it is a time elapsing region; and if e∀ is selected either r∀ is a successor of r∃ or r∀ = r∃. Then the same transition is applied, and therefore Tab((ℓ, v), a∃, a∀) ⊏ Tab ′ ((ℓ, r), b∃, b∀).

We define the inverse relation

⊐, by a ⊐ b ⇔ b ⊏ a. Lemma 2. The relation ⊐ is a simulation. Proof. Let (ℓ, v) ⊏ (ℓ, r), we have that r = [v].
Let a∃ ∈ Mov ′ ((ℓ, r), Eve). If a∃ = , then take b∃ = . Otherwise let (r ′ , e, a) = a∃. We define b∃ to be (d, e) such that v+d ∈ r ′ . Such a d exists since r ′ has to be a successor of [v]. Moreover this action is allowed in T .

We now show that: ∀b∀ ∈ Mov((ℓ, v), Adam). ∃a∀ ∈ Mov ′ ((ℓ, r), Adam).

Tab((ℓ, v), b∃, b∀) ⊏ Tab ′ ((ℓ, r), a∃, a∀).

• If b∀ = then we set a∀ = , as it is the only action allowed for Adam in s. Tab(b∃,

) = (v + d∃[Y ← 0], ℓ ′′ )
where b∃ = (d∃, e) and e = (ℓ, g, Y, ℓ ′′ ). By definition, v + d∃ ∈ r ′ where a∃ = (r ′ , e, a).

Hence v + d∃[Y ← 0] ∈ r ′ [Y ← 0]
and Tab((ℓ, v), b∃, ) ⊏ Tab ′ ((ℓ, r), a∃, ). • If b∃ = then a∃ = . Take a∀ = (r ′ , e∀, a) such that v + d∀ ∈ r ′ . By the same reasoning than the first point Tab((ℓ, v), , b∀) ⊏ Tab ′ ((ℓ, r), , a∀).

Otherwise let (d∃, e∃) = b∃ and (d∀, e∀) = b∀. We set a∀ = (r∀, e∀, a∀) such that v + d∀ ∈ r∀ and if e∃ is selected then a∃ = a∀ and otherwise a∃ = a∀.

• If [v + d∃] is not a successor of [v + d∀], then r∃ < r∀.
Hence in both cases e∃ is selected.

• If [v + d∀] is not a successor of [v + d∃], then r∀ < r∃.
Hence in both cases e∀ is selected.

Otherwise [v+d∃] = [v+d∀], then the player selected depends on whether a∃ = a∀. Since a∀ have been chosen to make the player selected coincide, the same transition is applied.

We say that a path

ρ ′ = s ′ 0 m ′ 0 → s ′ 1 m ′ 1 → ⋯ simulates a play ρ = s0 m 0 → s1 m 1 → ⋯, if for all i, s ′ i simulates si.
Lemma 3. Let C and C ′ be two games, s0 a state of C and s ′ 0 a state of C ′ . If C ′ simulates C and s ′ 0 simulates s0 then for all strategies σ∃ in C there is a strategy σ ′ ∃ in C ′ such that for all outcome ρ ′ of σ ′ ∃ from s ′ 0 there is an outcome ρ of σ∃ from s0 such that ρ ′ simulates ρ.

Proof. We define σ ′ ∃ inductively. Assume we have defined it for all histories of length k, and that for all prefixes of length k of outcomes of σ ′ ∃ , there is a prefix of an outcome of σ∃ that is simulated by it. Given a history h ′ of length k, we choose h that is simulated by h ′ , and choose σ ′ ∃ (h ′ ) to simulate σ∃(h). Now σ ′ ∃ (h ′ ) simulates σ∃(h), hence there exists an action of Adam such that Tab(h, σ∃(h), a∀) is simulated by Tab ′ (h, σ ′ ∃ (h), σ ′ ∀ (h ′ )). This way the property will be verified for length k + 1. This way, given ρ ′ = Outs(σ ′ ∃ , σ ′ ∀ ) for some strategy σ ′ ∀ , we can construct ρ outcome of σ∃ which is simulated by ρ ′ This shows that an outcome of σ∃ is simulated by ρ ′ .

Quasi Paths

A quasi path in a WTG is a sequence of states and transitions ρ = (ℓ0, v0)τ0(ℓ1, v1)τ1⋯τn-1(ℓn, vn) such that for all 0 ≤ i ≤ n -1 either:

1. τi is a move (a∃, a∀) and (ℓi, vi)

Mov(a ∃ ,a ∀ ) → (ℓi+1, vi+1); 2. or ℓi = ℓi+1 and [vi] = [vi+1].
In that case τi is called a jump. We will denote jumps by ↷.

A quasi cycle is a quasi path such that (ℓn, [vn]) = (ℓ0, [v0]).

In order to extend the reward to quasi paths, we need a weight function δ ∶ L × R X,M ↦ R which attributes a weight to jumps according to the region in which they happen. We define w δ the reward for each transition τi, depending on its type:

1. if τi is a move (a∃, a∀) and (ℓi, vi)

Mov(a ∃ ,a ∀ ) → (ℓi+1, vi+1), then w δ ((ℓi, vi)τi(ℓi+1, vi+1)) = d ⋅ w(ℓi) + w(e)
where (d, e) = Mov(a∃, a∀);

2. otherwise τi =↷, then w δ ((ℓi, vi) ↷ (ℓi+1, vi+1)) = δ([ℓi, vi]).
The reward for the quasi path ρ is then

w δ (ρ) = ∑ i< ρ w δ ((ℓi, vi)τi(ℓi+1, v
We define a projection from quasi paths to paths in the region game by forgetting jumps and projecting each state to its associated region. Formally, the projection π is defined inductively:

1. π((ℓ, v)) = (ℓ, [v]); 2. π(h ↷ (ℓ, v)) = π(h); 3. π h ⋅ (ℓ, v) a ∃ ,a ∀ → (ℓ, v ′ ) = π(h ⋅ (ℓ, v)) b ∃ ,b ∀ → (ℓ ′ , [v ′ ])
where ap = (dp, ep) for p ∈ {Eve, Adam}, b∃ = ([v + d∃], e∃, head), and b∀ = ([v + d∀], e∀, head) if d∃ < d∀ and b∀ = ([v + d∀], e∀, tail) otherwise.

It is naturally extended from histories to plays: ρ ′ is the projection of ρ if for all finite prefixes h of ρ, π(h) is a prefix of ρ ′ . If h is a path in the region game, the path ρ is said compatible with h if π(ρ) = h, and we write γ(h) for the set of path compatible with h.

We now associate to histories of WTG quasi paths by forgetting simple cycle like we did in the simple cycle decomposition. It is compatible with the stack of the projection on regions but contains more information.

Definition 6. (Timed Stack)

The timed stack tst of a history is defined inductively as a quasi path. We set tst(ε) = ε. Given a history h ′ = h a ∃ ,a ∀ → (ℓ, v), and assuming tst has been defined for h:

1. if there is i ≤ h such that tst(h)i = (ℓ, v ′ ) with v ′ ∈ [v],
then we consider the greatest such i and set

tst(h ′ ) = tst(h)≤i ↷ (ℓ, v); 2. otherwise tst(h ′ ) = tst(h) a ∃ ,a ∀ → (ℓ, v).
Notice that the timed stack can contain several states of the same region, hence i is not always unique. However, the states of the same region are all linked by jumps.

Lemma 4. For any history h, tst(h) is compatible with st(π(h)).

Proof. We prove this by induction on the size of h. This is obvious when h only contains one state. We now assume the property is true for h and all its prefixes. We write

st(π(h)) = r0 m 0 → ⋯ m k-1 → r k . Consider now some history h a ∃ ,a ∀ → s.
• if for all i ∈ ⟦0, k⟧, s ∈ ri, then by induction hypothesis on h, there is no index i such that hi belongs to the same region than s. Then tst(h

a ∃ ,a ∀ → s) = tst(h) a ∃ ,a ∀ → s is a quasi path that is compatible with st(π(h a ∃ ,a ∀ → s)). • otherwise there is i, n ′ such that st(π(h ≤n ′ )) = r0 m 0 → ⋯ri and s ∈ ri. tst(h a ∃ ,a ∀ → s) = tst(h)≤i ↷ s = tst(h ≤n ′ ) ↷ s. Since π(s) = ri, st(π(h a ∃ ,a ∀ → s) = r0 m 0 → ⋯ri. By induction hypothesis, tst(h ≤n ′ ) is compatible with st(π(h ≤n ′ )), hence π(tst(h ≤n ′ ) ↷ s) = r0 m 0 → ⋯ri. Which shows that tst(h a ∃ ,a ∀ → s) is compatible with st(π(h a ∃ ,a ∀ → s)).

Reduction to the Region Game

Given a weight function δ ∶ L × R X,M ↦ R, we will write C + δ for the set of simple cycles in the region game that only correspond to quasi cycles rewarding more than δ if δ is positive and more than 0 otherwise. Formally1 :

C + δ = {c ∈ C ∀ρ ∈ γ(c). w δ (ρ) ≥ max{δ(first(c)), 0}}
. Given a real number ε > 0, we write C -ε δ for the simple cycles of the region game that correspond to quasi cycles with weight lower than δ and lower than -ε. Formally2 :

C -ε δ = {c ∈ C ∀ρ ∈ γ(c). w δ (ρ) ≤ min{δ(first(c)), -ε}}.
The winning condition of the region game will be given by cycle objectives. The intuition behind the definition of these objectives, is that if Eve can force the play to see only cycles with positive reward (i.e. in C + δ ), the accumulated weight will be positive, except for a finite part. Which means she is winning the c-energy game, if c is big enough to cover the loss of energy in this finite part.

In the region game, we will consider the cases where the objective of Eve is given by Ω + δ = {ρ dec(ρ) ⊆ C + δ }. That is, she wins for plays whose decomposition in simple cycles only contains positive cycles.

We will prove in the next lemma that the remaining finite part in the cycle decomposition cannot have arbitrary big weight.

Given δ, we write δ + (resp. δ -) the weight function δ where we replaced all the negative (resp. positive) value by 0, i.e. δ + (r) = max{0, δ(r)} (resp. δ -(r) = min{0, δ(r)}).

Lemma 5. Let ρ ∈ Play(T ), if dec(π(ρ)) ⊆ C + δ then there is a bound W ∈ Z such that for all n, w δ + (tst(ρ≤n)) ≥ W . Similarly if dec(π(ρ)) ⊆ C -ε δ then there is a bound W ∈ Z such that for all n, w δ -(tst(ρ≤n)) ≤ W .
Note that this is trivial when the game has only bounded transitions, but non-obvious in the general case.

Proof. The prove the result for C + δ ; the result for C -ε δ can be proved the same way.

First notice that in the quasi paths of the form tst(ρ≤n), the number of transitions that are not jumps is bounded, because the same region cannot appear twice unless it follows a jump. Moreover all the jumps have positive rewards (w.r.t. w δ + ) since all the values of δ + are greater or equal to 0. The only solution left to have weights arbitrarily far below 0, is that there is a sequence of transitions in ρ whose weights grow arbitrarily big negatively. We write ρ = (ℓ0, v0)

m 0 → (ℓ1, v1) m 1 → . . . .

Toward a contradiction, assume

∀i. ∃ni. w((ℓn i , vn i )

mn i → (ℓn i +1, vn i +1)) ≤ -i. (1)
Then since the number of region is finite, there is a transition in the region game (ℓ, r)

m → (ℓ ′ , r ′ ), such that π ρn i mn i → ρn i +1 = (ℓ, r) m → (ℓ ′ , r ′ ) for an infinite number of i's. Since (ℓ, r) m → (ℓ ′ , r ′ ) is appears more than once in the projection of ρ, there is a simple cycle c ∈ dec(π(ρ)) such that (ℓ, r) m → (ℓ ′ , r ′ ) ap- pears in c, i.e. c = c1 ⋅ (ℓ, r) m → (ℓ ′ , r ′ ) ⋅ c2 for some path c1 ⋅ (ℓ, r) and (ℓ ′ , r ′ ) ⋅ c2 in the region game. Let ρ ′ ∈ γ(c), ρ ′ = ρ 1 ⋅ (ℓ, v) m ′ → (ℓ ′ , v ′ ) ⋅ ρ 2 with π (ℓ, v) m ′ → (ℓ ′ , v ′ ) = (ℓ, r) m → (ℓ ′ , r ′ ). Then ρ ′′ = ρ 1 ⋅ (ℓ, v) ↷ (ℓm p , vm p ) mp → (ℓm p +1, vm p +1) ↷ (ℓ ′ , v ′ ) ⋅ ρ 2 ∈ γ(c)
, where we take mp to be such that (ℓm p , vm p ) mp → (ℓm p +1, vm p +1) has weight strictly

smaller than -w(ρ 1 ⋅ (ℓ, v)) -δ(ℓ, r) -δ(ℓ ′ , r ′ ) -w((ℓ ′ , v ′ ) ⋅ ρ 2 ) + δ(first(c))
, this is possible because of hypothesis (1). We then have that w(ρ ′′ ) < δ(first(c)). Since ρ ′′ ∈ γ(c), this contradicts the fact that all the quasi cycle compatible with c are greater than δ(first(c)).

Given a WTG T , let W T = min t∈T {w(t)} ∪ {0} and WL = min ℓ∈L {w(ℓ)} ∪ {0}. Theorem 4. Let T be a WTG, if Eve has a winning strategy in R(T , Ω + δ ) then:

1. she has a winning strategy τ∃ in the energy game T E ;

2. if T has bounded transitions, τ∃ is a winning strategy in the energy game T E(c) for the initial credit c = L × R X,M ⋅ (WL ⋅ D + W T );

3. if τ∃ is immune from Zenoness, then it is winning in the mean payoff game TMP.

Proof. Let σ∃ be a winning strategy of Eve for the condition given by C + δ from (ℓι, [v0]). Thanks to Lem. 2 and 3 there is a strategy τ∃ such that for all outcome ρ of τ∃, π(ρ) is an outcome of σ∃.

We show that for all outcomes ρ of τ∃, there is a value c0 such that all the prefixes of ρ have a weight greater than -c0. Let ρ = (ℓ0, v0)

m 0 → (ℓ1, v1) m 1
→ ⋯ be an outcome of τ∃.

We write (dn, en) = Mov(mn). We show by induction over n that w δ + (tst(ρ≤n)) ≤ w(ρ≤n). This is obviously true if n = 0. Assuming this is true for some n ≥ 0, we show this is true for n + 1.

• if π(ρn+1) does not appear in the stack st(π(ρ≤n)), then:

w δ + (tst(ρ≤n+1)) = w δ + (
m ′ 0 → s1 m ′ 1 → ⋯sj mn → ρn+1)} so π(ρi m ′ 0 → ⋯sj mn → ρn+1) is in dec(π(ρ)).
Since σ∃ is a winning strategy, π(ρ) is a winning play in the region game, therefore π(ρi

m ′ 0 → ⋯sj mn → ρn+1) ∈ C + δ . ρi m ′ 0 → ⋯sj mn → ρn+1 ∈ γ(π(ρi m ′ 0 → ⋯sj mn → ρn+1)) so: w δ (ρi m ′ 0 → ⋯sj mn → ρn+1) ≥ δ + ([ρi]) (2)
Now we can write:

w δ + (tst(ρ≤n+1)) = w δ + (tst(ρ≤i) ↷ ρn+1) = w δ + (tst(ρ≤i)) + δ + ([ρn+1]) ≤ w δ + (tst(ρ≤i)) + w δ (ρi m ′ 0 → ⋯sj mn → ρn+1) by equation (2) ≤ w δ + (tst(ρ≤i) m ′ 0 → ⋯ m ′ j-1 → ρn) + w(ρn mn → ρn+1) ≤ w(ρ≤n) + w(ρn mn → ρn+1) by induction hypothesis ≤ w(ρ≤n+1)
Now notice that in the quasi paths of the form tst(ρ≤n), the number of transitions that are not jumps is bounded, because the same region cannot appear twice unless it follows a jump. Moreover all the jumps have positive rewards since all the value of δ + are greater or equal to 0.

In the case where T has bounded transition, the total weight of the play is greater or equal to L × R X,M ⋅ (WL ⋅ D + W T ).

Therefore the strategy τ∃ is winning the energy game T E(c) for the initial credit c = L × R X,M ⋅ (WL ⋅ D + W T ).

In the other case, Lem. 5 shows that there is a bound W such that for all n, w δ + (tst(ρ≤n)) ≥ W . Hence for all n, w(ρ≤n) ≥ W , and therefore ρ is in Ω(-W ). This being true for all outcomes of τ∃, τ∃ is a winning strategy in the energy game.

Point 3 in Thm. 4 is a direct consequence of point 1 Thm. 4 and Thm. 1.

Remark 2. We made the hypothesis that there exists a bound on the duration of transitions in order to get the result for the unknown initial credit. Consider the example of Fig. 5. In this game, Eve is winning in the region game for Ω + δ , and therefore by Thm. 4 she also wins in the energy game T E , by Thm. 1 she also wins the mean-payoff game TMP if we consider a strategy that is immune from Zenoness. However, the transition going out of ℓ0 can be taken by Adam at any moment, its duration is not bounded. Indeed, whatever the initial credit is, Adam can force a play which costs more than this credit, by delaying the transition for long enough. Therefore Eve has no winning strategy for any fixed initial credit and the answer to the unknown initial credit problem is negative.

We now consider the objective for Eve:

Ω -ε δ = {ρ dec(ρ) ⊆ C -ε δ }.
That is, she wins if the decomposition in simple cycle contains at least on simple cycle that is not below -ε.

Theorem 5. Let T be a WTG, if Adam has a winning strategy in R(T , Ω -ε δ ) then 1. he has a winning strategy in the energy game T E ;

2. if T has bounded transitions, then Adam has a winning strategy in the mean payoff game TMP.

Proof. The proof is very similar to the proof of Thm. 4. The main difference is that instead of proving that for all outcomes ρ of τ∃, and all n, w δ + (tst(ρ≤n)) ≤ w(ρ≤n), we prove that for all outcomes ρ of τ∀, and all n:

w(ρ≤n) ≤ w0(tst(ρ≤n)) - n -tst(ρ≤n) m + 1 -1 ⋅ ε.
where w0 assign weight 0 to all regions, m = L ⋅ R X,M , and q is the number of distinct elements in the timed stack. This is proven by induction, it holds for n = 0 and assuming it holds for n ≥ 0, we write ρ = (ℓ0, v0)

m 0 → (ℓ1, v1) m 1 → . . .
and (dn, en) = Mov(mn):

• if π(ρn+1) does not appear in the stack st(π(ρ≤n)), then:

w(ρ≤n+1) = w(ρn) + dn ⋅ w(ℓn) + w(en) ≤ w0(tst(ρn)) -n-tst(ρ≤n) m+1 -1 ⋅ ε + dn ⋅ w(ℓn) + w(en) ≤ w0(tst(ρn+1)) -n-tst(ρ≤n) m+1 -1 ⋅ ε ≤ w0(tst(ρn+1)) -n+1-tst(ρ ≤n+1 ) m+1 -1 ⋅ ε • otherwise there is i such that [ρi] = [ρn+1] and tst(ρ≤n) = tst(ρ≤i) m 1
→ s1⋯sj and sj = ρn.

w(ρ≤n+1)

= w(ρn) + dn ⋅ w(ℓn) + w(en) ≤ w0(tst(ρn)) -n-tst(ρ≤n)

m+1 -1 ⋅ ε + dn ⋅ w(ℓn) + w(en) ≤ w0(tst(ρi t 1 → . . . t j-1 → ρn)) + dn ⋅ w(ℓn) + w(en) -n-tst(ρ≤n) m+1 -1 ⋅ ε ≤ w0(tst(ρi)) -ε -n-tst(ρ≤n) m+1 -1 ⋅ ε ≤ w0(tst(ρi)) -ε -n+1-tst(ρ ≤n+1 ) m+1 ⋅ ε ≤ w0(tst(ρn+1)) -n+1-tst(ρ ≤n+1 ) m+1 -1 ⋅ ε
We then use Lem. 5 to conclude that τ∀ is a winning strategy.

Point 2 in Thm. 5 is a direct consequence of point 1 of Thm. 5 and Thm. 2.

Solving the Region Game

We now show how to solve a finite game with objective of the form Ω = {ρ ∀c ∈ dec(ρ).c ∈ C W } or Ω = {ρ ∃c ∈ dec(ρ).c ∈ C W }. We can then apply this technique to solve the region game. To do so we unravel the game, and stop as soon as a cycle is formed. The play is then winning if the cycle formed belong to C W . This technique is adapted from [START_REF] Björklund | Memoryless determinacy of parity and mean payoff games: a simple proof[END_REF].

Definition 7. Let G = ⟨St, ι, Act, Mov, Tab, Ω⟩ be a concurrent game with Ω = {ρ ∀c ∈ dec(ρ).c ∈ C W } or Ω = {ρ ∃c ∈ dec(ρ).c ∈ C W }. The unraveling of G, written U (G), is the tuple ⟨St ′ , ι, Act, Mov ′ , Tab ′ , Ω ′ ⟩:

• the set of states is St ′ = {h ∈ (St ⋅ (Act × Act)) * ⋅ St ∀i, j ≠ i. hi ≠
hj} ∪ {↑, ↓}, the set of histories of the original game where all states appear at most once; with the addition of a winning state ↑ and a loosing state ↓ for Eve;

• Mov ′ (h, p) = Mov(last(h), p);

• for an history h and a move (a∃, a∀), let s = Tab(last(h), a∃, a∀): Then, from ↑ and ↓, there are only self loops, thus Tab ′ (x, a∃, a∀) = x for x ∈ {↑, ↓}.

• the objective is to reach

↑, i.e. Ω ′ = (St ′ ⋅ (Act × Act)) * ⋅ (↑ ⋅(Act × Act)) ω .
Theorem 6. Let G be a concurrent game and U (G) its unraveling. Then Eve has a winning strategy in the unraveled game U (G) if, and only if, she has a winning strategy in G.

In the following we will call objectives of the form {ρ ∀c ∈ dec(ρ). c ∈ C W } universal cycle objective and objectives of the {ρ ∃c ∈ dec(ρ). c ∈ C W } existential cycle objective.

We show the following lemma wich implies Thm. 6. Lemma 6. Let G be a concurrent game and U (G) its unraveling. The three following properties are equivalent:

1. Eve has a winning strategy in the unraveled game U (G);

2. Eve has a winning strategy in G for the existential cycle objective;

3. Eve has a winning strategy in G for the universal cycle objective;

The implication from universal cycle objective to the existential one is obvious. We decompose the remaining of the proof in two lemmas as represented in Fig. 16.

Lemma 7. If Eve has a winning strategy in G for the existential cycle condition C W , she has a winning strategy in the unraveled game U (G).

Proof. We will show that if Eve has no winning strategy in U (G), then she has none in G, by considering the attractor of ↑. The idea is that if the stack of the play in G is not in this attractor, then Eve cannot enforce the next simple cycle in the decomposition to be positive. The attractor of ↑, written Attr∃(↑) is defined as Attr∃(↑) = {h ∈ St * ∃σ∃. ∀σ∀. ∃n. Outs(σ∃, σ∀)n =↑}. This attractor set can be constructed iteratively, consider Attr 0 ∃ (↑) =↑ and Attr k+1 ∃ (↑ ) = {h ∈ St * ∃a∃. ∀a∀. h ⋅ Tab(last(h), a∃, a∀) ∈ Attr k ∃ (↑)}, a fixed point is reached after n ≤ St number of steps, and Attr n ∃ (↑) = Attr∃(↑). Assuming that Eve has no winning strategy in U (G), the initial state is not in the attractor.

Fix a strategy σ∃ in G, let h be a history in G and l = last(h). Notice that if st(h) ∈ Attr∃(↑) then there is an action a∀ such that writing s = Tab(ℓ, σ∃(h), a∀), we have that st(h

σ ∃ (h),a ∀ → s) ∈ Attr∃(↑) and if there is i such that st(h)i = s, then st(h)≥i σ ∃ (h),a ∀ → s ∈ C W .
We construct a strategy σ∀, that for all history h such that st(h) ∈ Attr∃(↑), chose an action a∀ witness of the previous property.

It is easy to show by induction that the outcome of (σ∃, σ∀) stays outside the attractor: this is because the initial state is outside of it and when a cycle is formed, the stack comes back to a prefix of the current one, and since (by induction hypothesis) along the history no state of the attractor has been seen, we are still outside the attractor. Therefore in the decomposition of the outcome, all the simple cycles are in C ∖ C W . This contradicts the fact that the strategy of Eve is winning in G for the existential cycle condition. Proof. Let ν∃ be a winning strategy in the unraveling. We define a strategy σ∃ in the original game by simply forgetting cycles. It therefore plays according to the element that are in the stack of the decomposition process: σ∃(h) = ν∃(st(h)). Let ρ be an outcome of σ∃, we show that it is winning. Let c be a cycle appearing in the decomposition in simple cycles of ρ. Let k be the first index such that last(dec(ρ ≤k )) = c.

We write st(ρ ≤k-1 ) = s0 m 0 → ⋯s k , and we will prove by induction over n ∈ ⟦0, k⟧ that the sequence of states in the stack forms a history compatible with ν∃. For the case s0 this is simply because the initial state will never disappear from the stack. We now assume that the property holds until some index n ∈ ⟦0, k -1⟧. We write i the last occurrence of sn in ρ before position k, that is i = max{j ≤ k -1 ρj = sn}.

We show that ρi+1 = sn+1. Since i + 1 ≤ k, state ρi+1 is added to the stack and will only disappear before index k if a cycle is formed with some state sj with j ≤ n + 1:

• if j < n then sn is also removed from the stack and since it does not appear after i this contradicts the fact that sn is still present on the stack of ρ ≤k ; • j = n contradicts the fact that i was the last appearance of sn before position k; • otherwise j = n + 1, and in that case, the same state ρi+1 is still on top of the stack once the cycle has been removed. Therefore sn+1 = ρi+1. Now, since ρ is an outcome of σ∃, there is some a∀ such that Tab(ρi, σ∃(ρ≤i), a∀) = ρi+1. By definition, σ∃(ρ≤i) = ν∃(st(ρ≤i)) and then:

Tab ′ (s0 m 0 → ⋯sn, ν∃(s0 m 0 → ⋯sn), a∀) = Tab(sn, σ∃(ρ≤i), a∀) = ρi+1 = sn+1 Hence s0 m 0 → ⋯sn+1 is an outcome of ν∃.
This proves that st(ρ ≤k-1 ) is an outcome of ν∃. We now have to complete the cycle. There is a∀ such that:

Tab(ρ k-1 , σ∃(ρ ≤k-1 ), a∀) = ρ k .
And ρ k appears in st(ρ ≤k-1 ) to form the cycle c. Since ν∃(st(ρ ≤k-1 )) = σ∃(ρ ≤k-1 ), we have that:

Tab ′ (st(ρ ≤k-1 ), ν∃(st(ρ ≤k-1 )), a∀) = ↑ if c ∈ C W ↓ otherwise .
Since ν∃ is a winning strategy the final state is necessarily ↑, meaning that c belongs to C W . This shows that σ∃ is a winning strategy in G.

We are now ready to give an algorithm that solves game with cycle objectives. Its complexity depends on the way we represent the cycle objective, as an explicit representation can be exponentially larger than the size of the game. To be as general as possible, we assume that we have an algorithm to tell us if a cycle is in C W , which works using space at most p( St + Act ) where p is a function from N to N.

Theorem 7. Given a concurrent game G with (existential or universal) cycle objective C W , we can decide in space O( St ⋅ Act 2 )+p( St+Act ) whether Eve has a winning strategy.

Proof. The algorithm proceeds by an exploration of the unraveling. We give an inductive procedure win. Given a state of the unraveling h:

• if h contains a cycle c,
Ω = {ρ ∀c ∈ dec(ρ).c ∈ C W } or Ω = {ρ ∃c ∈ dec(ρ).c ∈ C W }
where C W is given by an automaton, deciding if Eve has a winning strategy is PSPACE-complete.

We assume that the set of cycles is given by an (non-deterministic) automaton A whose language is C W .

Proof. We use the algorithm of Thm. 7. Determining if a cycle is accepted by A can be done in polynomial space by doing a subset construction on the fly. The problem is therefore in PSPACE.

The hardness proof is an encoding of QBF. Assume we are given a formula φ = ∃x1. ∀x2. . . . ∀xn. C1 ∧ ⋯Cm with for all j, Cj = (lj,1 ∨ lj,2 ∨ lj,3) and li,j is of the form x k or ¬x k for some k. We describe a game G. In state s0, Eve chooses to go to either state x1 or state ¬x1, then we go to s1 and Adam chooses to go to either x2 or ¬x2, and we repeat this until sn, then Adam chooses a clause Cj and we come back to s0. This forms a cycle s0 ⋅ l1 ⋅ s1 ⋅ l2⋯ln ⋅ sn ⋅ Cj ⋅ s0 where li = xi or ¬xi. Notice that in this proof we only write states of the path and not moves, this is in order to simplify the notations. The objective C W for Eve is given as the language:

⋃ j∈⟦1,m⟧ ⋃ i∈⟦1,3⟧ St * ⋅ li,j ⋅ St * ⋅ Cj.
This can be described by a non-deterministic automaton of polynomial size. Then Eve has a winning strategy in G if, and only if, the formula φ is valid.

ROBUST GAMES

The reduction to the cycle forming game in the region graph is complete when there exists a weight function δ, that partitions the set of simple cycles of the region into good ones for Eve and good ones for Adam.

Definition 8. (Robust game) A WTG is said δ-robust if C = C + δ ∪ C -ε
δ for some ε. We simply call a WTG robust when there exists δ ∶ R X,M ↦ R such that it is δ-robust. Remark 3. Note that a WTG G where all the costs are discrete (i.e. ∀ℓ ∈ L. w(ℓ) = 0) is robust for δ = 0 and ε < 1. The results of this section implies decidability of the energy problem and mean payoff problem for this class.

Remark 4. If T is robust, then the leafs of U (R(T )) are partitioned between winning for Eve and winning for Adam. If, in addition, this game is turn-based, then it is determined. By Thm. 4 and Thm. 10, we can conclude that if T is robust and turn-based then the energy game T E is determined. Now, we establish that in a robust WTG, we can decide if Eve can win the energy game. This is a consequence of the following theorem which complements Thm. 4. A symmetric result also holds for Adam. Theorem 9. Let T be a δ-robust WTG:

1. if Eve has a winning strategy in the energy game T E then she has a winning strategy in U (R(T , Ω + δ ));

2. if T has bounded transitions and Eve has a winning strategy in the mean payoff game TMP then she has a winning strategy in U (R(T , Ω + δ )).

Proof. Let τ∃ be a strategy in T . Thanks to Lem. 1 and 3, there is a strategy σ∃ such that for any outcome ρ of σ∃ there is an outcome ρ ′ of τ∃ such that π(ρ ′ ) = ρ.

We will prove that Eve has no winning strategy in U (R(T , Ω + δ )), then she has none in the energy game T E ; and in the case where T has bounded transitions she has no winning strategy in the mean payoff game TMP either.

Assume that Eve has no winning strategy in U (R(T , Ω + δ )), according to Lem.7, she has no winning strategy for the existential cycle objective C + δ . Therefore there is an outcome ρ of τ∃, such that dec(π(ρ)) only contains cycles of

C ∖ C + δ . As T is robust, C ∖ C + δ = C -ε
δ , and each cycle decreases the weight of at least ε. Therefore for all index n:

w(ρ ′ ≤n ) ≤ w δ + (tst(ρ ′ ≤n )) -ε ⋅ n L ⋅ R X,M -1 .
Thanks to Lem. 5, w δ + (tst(ρ≤n)) is bounded, so the weight of ρ decreases infinitely low. This contradicts the fact that τ∃ is a winning strategy in T E .

Assuming now that T has bounded transitions, the bound D is such that:

w(ρ≤n) dρ≤n ≤ w δ + (tst(ρ≤n)) dρ≤n -ε ⋅ 1 D ⋅ L ⋅ R X,M - 1 n .
Thanks to Lem. 5,

w δ + (tst(ρ≤n)) d (ρ≤n)
+ ε n converges to 0. The mean payoff is therefore strictly below 0, this contradicts that τ∃ is a winning strategy for the mean payoff game TMP.

Theorem 10. Let T be a δ-robust WTG:

1. if Adam has a winning strategy in the energy game T E , then he has a winning strategy in U (R(T , Ω -ε δ )); 2. if T has bounded transitions and Adam has a winning strategy in the mean payoff game TMP, then he has a winning strategy in U (R(T , Ω -ε δ )).

Proof. Similarly to Thm. 9, we assume that Adam has no winning strategy in U (R(T , Ω -ε δ )), and prove that he has none in the energy game T E ; and in the case where T has bounded transitions he has no winning strategy in the mean payoff game TMP either. Let τ∀ be a strategy of Adam. Using the same arguments than for Thm. 9, there is an outcome ρ of τ∀ such that dec(π(ρ)) only contains cycles of C + δ . We therefore have that for all n, w(ρ≤n) ≥ w δ -(tst(ρ≤n)). We showed in Lem. 5 that w δ -(tst(ρ≤n)) cannot go arbitrarily far below 0. Hence τ∀ is not winning the energy game

T E . Now, if T has bounded transitions, w(ρ≤n) d(ρ≤n) ≥ w δ + (tst(ρ≤n)) ⋅ D n .
The mean payoff is therefore greater or equal to 0. This means that τ∀ is not winning the mean payoff game T M .

Given a weighted timed game, it is decidable whether this game is robust or not.

Theorem 11. The membership problem for the class of robust game is decidable.

To solve the membership problem, we encode the condition on simple cycles as a formula of the theory of real closed fields, for which there is a decision procedure in EXPSPACE [START_REF] Ben-Or | The complexity of elementary algebra and geometry[END_REF]. The size of the formula we obtain can be doubly exponential, and therefore our algorithm is 3EXPSPACE.

Theorem 12. Deciding if a WTG T is robust can be done in 3EXPSPACE.

For a weight function δ, we will denote the weight δ(ℓ, r) by the variable δ ℓ,r .

Given a simple cycle c = (ℓ0, r0)

(r 0 ∃ ,e 0 ∃ ,a 0 ∃ ),(r 0 ∀ ,e 0 ∀ ,a 0 ∀ ) → (ℓ1, r1) p 1 → ⋯(ℓn, rn) of the region game, a quasi path h ∈ γ(c) is of the form (ℓ0, v 0 0 ) ↷ ⋯ ↷ (ℓ0, v j 0 0 ) (d 0 ∃ ,e 0 ∃ ),(d 0 ∀ ,e 0 ∀ ) → (ℓ1, v 0 1 )⋯(ℓn, v jn n ).
Where for all i ∈ ⟦1, n⟧, ji is the number of jumps in the region ri, and for all j ∈ ⟦0, ji⟧, v j i is in the region ri. We write

(di, ei) = Mov((d 0 ∃ , e 0 ∃ ), (d 0 ∀ , e 0 ∀ )).
We have the constraint on the number of jumps:

ψi = ji ≥ 0 ∧ v 0 i (x) ≠ v j i i (x) ⇒ ji ≥ 1 .
The fact that the correct transition is selected at each step is expressed by:

ςi = d i ∃ < d i ∀ ∧ di = d i ∃ if Eve is selected in (r i ∃ , e i ∃ , a i ∃ ), (r i ∀ , e i ∀ , a i ∀ ) d i ∃ < d i ∀ ∧ di = d i ∃ otherwise
The transition is correctly applied if

[z ← 0]v j i i + di = v 1 i+1
. This is expressed by:

ξi = ⋀ x∈X v j i i (x) + di = v 1 i+1 (x) if x ∈ z v 1 i+1 (x) = 0 otherwise Let g ∈ C(X), it is of the form x1 ⋈ c1 ∧ ⋅ ⋅ ⋅ ∧ x k ⋈ c k . The fact that a valuation v + d (v ∈ R X and d ∈ R) satisfies the guard g is expressed by the formula φ(v, d, g) = vx 1 + d ⋈ c1 ∧ ⋅ ⋅ ⋅ ∧ vx k + d ⋈ c k . Each transition is allowed if v j i i + di ⊧ Inv(ℓi), v j i i + di ⊧ g and v 0 i+1 + di ⊧ Inv(ℓi+1)
. This is expressed by the conjunction:

φi = φ v j i i , di, Inv(ℓi) ∧ φ v j i i , di, g ∧ φ v 0 i+1 , 0, Inv(ℓi+1) .
The weight of this path is expressed by the polynomial pc

= j1 ⋅ δ ℓ 1 ,r 1 + d1 ⋅ w(ℓ1) + w(e1) + ⋅ ⋅ ⋅ + jn ⋅ δ ℓn,rn .
To each region is associated set of constraints on clocks that are satisfied exactly by the valuation belonging to that region. We can translate them to a formula χ(r, v). The fact that the history is compatible with c is expressed by for all i and j ∈ ⟦1, ji⟧: χ(ri, v j i ). Note that for j ≠ 1, ji the variables v j i have not appeared yet and it is therefore unnecessary to put constraint on these. We therefore write

χi = χ(ri, v 0 i )∧χ(ri, v j i i )∧χ(ri, v j i i )∧χ(r i ∃ , v j i +d i ∃ )∧χ(r i ∀ , v j i +d i ∀ ).
The following formula characterizes the quasi paths that are compatible with c: κc = ⋀ i∈⟦1,n-1⟧ ψi ∧ φi ∧ ςi ∧ ξi ∧ χi

The algorithm proceeds as follows: we look at all the possible partition of C into two sets G + and G -there are a triply exponential number of possible partitions; G + and G - potentially correspond to C + δ and C -ε δ for some δ and ε; we consider the formula: ∃ ℓ∈L,r∈R X,M δ ℓ,r . ∃ε.

⋀ c∈G + ∀ i∈⟦1, c ⟧ di, ji. ∀ x∈X v 0 i (x), v j i i (x). (κc ⇒ pc ≥ 0) ⋀ c∈G - ∀ i∈⟦1, c ⟧ di, ji. ∀ x∈X v 0 i (x), v j i i (x). (κc ⇒ pc < -ε)
we then check that the formula has a solution. The size of the formula is at most doubly exponential, the algorithm we described is therefore 3EXPSPACE.

Theorem 13. If δ and ε are given then deciding if T is δ, ε-robust can be done in 2EXPSPACE.

Proof. This is because in that case, the formula we considered can be translated to an existential formula, which has size doubly exponential in the input. We know that the existential theory of the reals is decidable in PSPACE [START_REF] Basu | Existential theory of the reals[END_REF]. Therefore the global algorithm is 2EXPSPACE. We encode the circuit by having two clocks gi and ḡi for each gate gi. They represent whether the gate output should be true: in that case gi = 1 and ḡi = 0; in the other case gi = 0 and ḡi = 1.

Proposition 2. Deciding if a game is δ, ε-robust is co- NEXP-hard.
We assume the gates are ordered g1, g2, . . . , g G such that if i < j implies that gi does not take gj as input, it is always possible to find such an order as Boolean circuits are acyclic.

Gates are encoded as represented in Fig. 21 for a ∧-gate. For the ∧-gate, if both inputs, from g1 and g2 are true, then the valuation of the clocks is such that g1 = g2 = 1. The first transition can be taken, and g3 is set to 1. This encodes the fact that the output of gate g3 is positive. x ← 1 Notice that in the definition of WTG, we assumed that there always is a player that can play an action, which is not the case here, but we can add an edge in each state to go to a sink state. This does not change the fact that the game is robust, but we do not include this edges to make the presentation clearer.

. . . t = 1 c1 = 2; c1 ← 0 c2 = 2; c2 ← 0 c k = 2; c k ← 0 c1 = 1 c2 = 1 c k = 1 t = 1; t ← 0 Figure 17: Module X ← 1 -X. Where X = {c1, . . . , c k }. X ← 1 -X X ← 1 -X x ← 0 Figure 18: Module x ← 1. x ← 1 x ← 0 t = 0
y = 1 y = 0; x ← 0 t = 0
The global game, represented in Fig. 24, is played as follows:

1. we start with a weight of 2-2 N +1 and the initial state i is encoded by a valuation of 0 for all variables x1, ⋯, xn;

2. Eve can choose a successor j by choosing the valuations of y1, ⋯, yn;

3. the play can traverse the module Edge only if there is a edge between nodes i and j;

4. we replace the valuation of x1, ⋯, xn by that of y1, ⋯, yn, i.e. we now consider that j is the current state;

5. either we go back to step 2 with a reward of 2 or to the module MIX.

If there is a Hamiltonian path in the graph succinctly represented, then following it, until j is the initial state, will give a weight of 0. Then entering MIX, can give simple cycle that are either positive or negative, while all traverse the same regions. Hence the game is not robust for any δ and ε.

If there is a simple cycle in the region game, that can correspond to both positive and negative cycle, then: it goes through the module MIX since it is the only place where the weight can depend on the valuations; it must have been 2 N -1 times through the Edge module, so that we can have a weight around 0; the valuations each time must have encoded different states, since otherwise this cycle is not a simple one. Thus it describes an Hamiltonian path.

Finally, we can characterize the complexity of deciding the energy problem for robust weighted timed games:

Theorem 14. The energy problem for robust games is in EXPSPACE and is EXP-hard.

Proof Sketch. The algorithm proceeds by constructing the region game and then solving it using the algorithm of Thm. 8. This is correct because of Thm. 4, 6 and 9.

Proof. We consider the region game, which has at most exponential size. Deciding if a simple cycle is winning for Eve is easy since we only need to check one arbitrary path in the WTG whose projection on the regions corresponds to the simple cycle we consider. If its weight is greater or equal to 0, the cycle is in C + δ . This can be done using polynomial space (w.r.t. the size of the simple cycle). Using the algorithm of Thm. 7 we obtain a global procedure which is in EXPSPACE. EXP-hardness already holds for reachability objectives in timed games.

FIXPOINT ALGORITHM

While the reduction to the cycle forming game in the region graph is elegant and allows us to identify a large and natural class of weighted timed games with decidable properties, this reduction does not lead directly to a practical semialgorithm. In this section, we design a valuation iteration algorithm that can be implemented symbolically using polyhedra, which can be executed on any weighted timed game, and find winning strategies for Eve when it terminates successfully. We also show that termination is guaranteed on robust weighted timed games.

Value Iteration Algorithm

Our value iteration algorithm is an adaptation of the solution for the finite state case described in [START_REF] Brim | Faster algorithms for mean-payoff games[END_REF] to the setting of WTG. It computes successive approximations of the minimal energy level that Eve needs to win the energy game.

Essentially, the semi-algorithm is based on the iteration of an operator that computes successive approximations of the energy level/credit that is necessary for Eve to maintain the energy level positive for k rounds in the energy timed game, where k increases along with the iterations. Most importantly, our algorithm is parameterized by a value c ∈ N, that represents a maximal energy level that we want to track: if the energy level necessary to stay alive from a given state (l, v) for k rounds is larger than c then (ℓ, v) is considered as loosing. This is a sound approximation when looking for winning strategies. This parameter is important to enforce termination of the analysis. If a fixed point is reached, then it contains enough information to identify winning states (those that are not mapped to +∞ by the operator) and construct winning strategies. If the analysis is negative (no winning strategy found) then this value can be increased. Furthermore, we show that for robust weighted timed games, there is a finite value c which is computable and sufficient to detect winning strategies for Eve.

In this section, we assume the WTG is fixed and transitions, weight functions, etc . . . refer to this game. Given c ∈ N, we write a ⊖c b for max(0, ab) if ab ≤ c and +∞ otherwise. Notice that for all a, b ∈ R ∪ {+∞}:

a -b ≤ a ⊖c b (3)
In the sequel we consider mappings in S = [St ↦ R+ ∪{+∞}] that associate with each state an element in R+ ∪ {+∞}. Given f, g ∈ S, we write f ⪯ g if ∀s ∈ St, f (s) ≤ g(s).

Given c ∈ N, the operator liftc ∶ S ↦ S is defined by:

∀s ∈ St, liftc(f )(s) = inf a ∃ sup a ∀ f (s ′ ) ⊖c w(s a ∃ ,a ∀ → s ′ ) Remark 5. The operator lift c is monotonic, i.e. f ⪯ g ⇒ lift c (f ) ⪯ lift c (g).
We let f c 0 ∶ St ↦ R+ ∪ {+∞} be the mapping defined by ∀s ∈ St, f c 0 (s) = 0. We then inductively define f c k+1 , for k ≥ 0 to be liftc(f c k ). Notice that the sequence (f c n ) n∈N forms an increasing sequence. Thus, f c n (s) represents the initial energy level that is needed by Eve to keep the energy level positive for n steps from s. If more than c is needed then f c n (s) is set to be +∞ (c being the maximal energy level that we want to track). This is formalized in Lem. 9.

Lemma 9. For all state s, index n, credit c, ε > 0:

fn(s) ≥ -sup σ ∃ inf σ ∀ w c (Outs(σ∃, σ∀)≤n) .
where for a history h = h0

m 0 → h1⋯ mn → hn, w c (h) = -∞ if ∃i. w(hi m i → hi+1) < -c -ε and w(h) otherwise.
Proof. We prove the property by induction over n, it is obvious for n = 0. Now assuming this holds for n we show it for n + 1. Let ε > 0, we define a strategy σ∃. We select σ∃(s) that is ε 2 close to the optimal of inf

a ∃ sup a ∀ f c n (s ′ ) ⊖c w(s a ∃ ,a ∀ → s ′ )
if this value is different from +∞ (otherwise the result is obvious). Hence for all action a∀:

f c n (s ′ ) ⊖c w(s σ ∃ (s),a ∀ → s ′ ) ≤ f c n+1 (s) + ε 2 f c n (s ′ ) -w(s σ ∃ (s),a ∀ → s ′ ) ≤ f c n+1 (s) + ε 2 (by remark (3)) w(s σ ∃ (s),a ∀ → s ′ ) ≥ f c n (s ′ ) -f c n+1 (s) - ε 2
where Tab(s, σ∃(s), a∀) = s ′ .

For the remaining of the proof, we introduce the notation σ∃ ○ (s m → s ′ ) for the strategy that associate to a history h, the action σ∃(s m → h). We select σ∃ ○ (s → s ′ ) to be at most → ρi+1 , then:

• if i = 0, then inf a ∃ sup a ∀ f c n (s ′ ) ⊖c w(s a ∃ ,a ∀ → s ′ ) > -c
because we chose σ∃(s) to be ε 2 close to the optimal. This means that f c n+1 (s) = +∞ and the property is verified;

• otherwise i > 0, because we chose σ∃ ○ (s → s ′ ) to be close to the optimal, and using the induction hypothesis, f c n (s ′ ) = +∞. This shows sup

a ∀ f c n (s ′ ) ⊖c w(s σ ∃ (s),a ∀ → s ′ ) = +∞
Since σ∃(s) was also selected to be close to the optimal, this means that f c n+1 (s) = +∞.

In the other case:

w c (ρ≤n+1) = w(ρ≤n+1) = w(s σ ∃ (s),σ ∀ (s) → s ′ ) + Out s ′ (σ∃ ○ (s σ ∃ (s),σ ∀ (s) → s ′ )≤n, σ∀ ○ (s σ ∃ (s),σ ∀ (s) → s ′ )) ≥ f c n (s ′ ) -f c n+1 (s) - ε 2 + sup σ ∃ inf σ ∀ w c (Out s ′ (σ∃, σ∀)≤n) - ε 2 ≥ f c n (s ′ ) -f c n+1 (s) - ε 2 -f c n (s ′ ) - ε 2 (induction hypothesis) ≥ -f c n+1 (s) -ε This means that inf σ ∀ (w c (Outs(σ∃, σ∀)≤n)) ≥ -f c n+1 (s) -ε
and since we have such a strategy σ∃ for any ε > 0:

sup σ ∀ inf σ ∀ (w c (Outs(σ∃, σ∀)≤n)) ≥ -f c n+1 (s)
Which proves the property for fn+1.

Lemma 10. For all state s, index n, credit c, ε > 0:

sup

σ ∃ inf σ ∀ w + c (Outs(σ∃, σ∀)≤n) ≥ fn(s).
where for a history h = h0

m 0 → h1⋯ m n-1 → hn, w + c (h) = -∞ if ∃i, j. w(hi m i → hi+1 m i+1 → ⋯hj) < -c + ε and w(h) otherwise.
Proof. The proof is quite similar to that Lem. 9, we do it by induction over n and the property is obvious for n = 0. Let σ∃ be a strategy of Eve and ε > 0. In order to prove the property for rank n+1, we construct a strategy σ∀ such that w + c (Outs (σ∃, σ∀)≤n+1) ≤ -f c n+1 + ε.

Let a∀ be ε 2 close to the optimal of sup

a ∀ f c n (s ′ ) ⊖c w(s σ ∃ (s),a ∀ → s ′ ) if it is different from +∞ and such that f c n (s ′ )⊖c w(s σ ∃ (s),a ∀ → s ′ ) = +∞ otherwise. Let s ′ = Tab(s, σ∃ (
s), a∀) and σ ′ ∀ be such that:

w + c Out s ′ (σ∃ ○ (s σ ∃ (s),a ∀ → s ′ ), σ ′ ∀ )≤n ≥ -f c n (s ′ ) - ε 2 ; if f c n (s ′ ) ≠ +∞ and such that w + c Out s ′ (σ∃ ○ (s σ ∃ (s),a ∀ → s ′ ), σ ′ ∀ )≤n = -∞
otherwise. This is possible thanks to the induction hypothesis.

We define strategy σ∀ by:

σ∀ = ⎧ ⎪ ⎪ ⎨ ⎪ ⎪ ⎩ s ↦ a∀ s σ ∃ (s),a ∀ → h ↦ σ ′ ∀ (h) Let h = h0 m 0 → h1⋯ mn → hn+1 = Outs(σ∃, σ∀)≤n+1. If there is i, j such that w(hi m i → hi+1 m i+1 → ⋯hj) < -c then w + c (h) = -∞
and the property is obviously verified. Otherwise, lets look at the weight of the outcome:

w (h) = w(h0 m 0 → h1) + w(h≥1) = w(s σ ∃ (s),a ∀ → s ′ ) + w + c (h≥1) If f c n (s ′ ) = +∞ then w + c (
h≥1) = +∞, which contradicts the fact that there is no i, j such that w(hi

m i → hi+1 m i+1 → ⋯hj) < -c. Therefore f c n (s ′ ) ≠ +∞ and: w (h) ≥ w(s σ ∃ (s),a ∀ → s ′ ) -f c n (s ′ ) - ε 2 • If f c n (s ′ ) -w(s σ ∃ (s),a ∀ → s ′ ) ≥ c then w(s σ ∃ (s),a ∀ → s ′ ) + w(h≥1) ≥ c -ε 2 . Hence w + c (h) = +∞. • Otherwise w (h) ≥ -f c n (s ′ ) ⊖c w(s σ ∃ (s),a ∀ → s ′ ) - ε 2 ≥ -f c n+1 (s) -ε
Theorem 15 (Correctness). If there exists n ≥ 0 such that fn+1 = fn, and f c n (ι) ≠ +∞, then for any ε > 0, Eve has a winning strategy for the c ′ -energy game T E(c ′ ) with initial credit c ′ = f c n (ι) + ε.

Proof. We define a strategy σ∃ for Eve, that for a history h and a state s, select an action a∃ that is ε 2 h +1 close to the optimal. That is σ∃(h ⋅ s) = a∃ such that:

sup a ∀ f c n (s ′ ) ⊖c w(s a ∃ ,a ∀ → s ′ ) ≤ f c n (s) + ε 2 h +1 . This is possible since f c n (s) = f c n+1 (s) = infa ∃ sup a ∀ f c n (s ′ ) ⊖cw(s a ∃ ,a ∀ → s ′ ) . Consider now an outcome ρ = ρ0 m 0 → ρ1 m 1 → ⋯ of σ∃ such that ρ0 = s. We show by induction that for all k, f c n (ρ0) + ε ⋅ (1 -1 2 k ) ≥ f c n (ρ k ) -w(ρ ≤k )
. This is true for k = 0 since w(ρ≤0) = 0. Assume now that the property holds for some integer k. By the definition of σ∃, we have:

f c n (ρ k ) + ε 2 k+1 ≥ f c n (ρ k+1 ) ⊖c w(ρ k m k → ρ k+1 ) f c n (ρ k ) + ε 2 k+1 ≥ f c n (ρ k+1 ) -w(ρ k m k → ρ k+1 ) (by rem. (3)) f c n (ρ k ) + ε 2 k+1 ≥ f c n (ρ k+1 ) -(w(ρ ≤k+1 ) -w(ρ ≤k )) f c n (ρ k ) -w(ρ ≤k ) + ε 2 k+1 ≥ f c n (ρ k+1 ) -w(ρ ≤k+1 )
Using the induction hypothesis, we obtain:

f c n (ρ0) + ε ⋅ (1 - 1 2 k ) + ε 2 k+1 ≥ f c n (ρ k+1 ) -w(ρ ≤k+1 ) f c n (ρ0) + ε ⋅ (1 - 1 2 k+1 ) ≥ f c n (ρ k+1 ) -w(ρ ≤k+1 )
Which proves the property for k+1. Hence for all k, f c n (ρ0)+ ε + w(ρ ≤k ) ≥ 0. This shows that from s, σ∃ is a winning strategy for the initial credit f c n (s).

Remark 6. Note that winning strategies do not necessarily exist for the initial credit f c n (s) we compute for each state as this is an infimum. However, given any ε > 0, ε-optimal strategies i.e. winning strategies with initial credit f c n (s) + ε are guaranteed to exist. This is illustrated in Fig. 25 where for all ε > 0, Eve can win for the initial credit ε, but she cannot win for (limit) initial credit 0. In the case of robust game, we show that we can stop the algorithm after a finite number of iterations.

Theorem 16 (Termination). Let T be a WTG and c a fixed credit. If T is δ, ε-robust and f c n 0 (ℓι, 0) ≠ +∞ for n0 ≥ c⋅( L ⋅ R X,M +1) ε + 1 ⋅ L ⋅ R X,M then Eve has a winning strategy in the energy game.

Proof. We show in fact, the equivalent property that if Eve has no winning strategy for the energy game T , then f c n 0 (ℓι, 0) = +∞.

We use the correspondence with the region game. Assuming Eve has no winning strategy for the energy game T , by Thm. 4, she has no winning strategy in R(T , Ω + δ ), and by Lem. 8, she has no winning strategy in U (R(T , Ω + δ )). According to Lem.7 she has no winning strategy in R(T ) for the existential cycle objective C + δ . Once a strategy σ∃ for Eve is fixed, Adam has a strategy σ∀ such that the simple cycles in the decomposition of the projection of the outcome are never in C + δ . Since the game is robust, all these simple cycles have a weight smaller than -ε.

We have that:

sup σ ∃ w c (Outs(σ∃, σ ′ ∀ )≤n) ≤ -ε⋅ n L ⋅ R X,M -1 +c⋅ L ⋅ R X,M . Let n0 ≥ c⋅( L ⋅ R X,M +1) ε + 1 ⋅ L ⋅ R X,M
. Using Lem. 9 we have that fn 0 (s) > c, hence f c n 0 (s) = +∞.

If moreover the game has bounded transition, the algorithm is complete.

Theorem 17 (Completeness for robust games). Let T be a robust WTG, which has bounded transitions, and c = L×R X,M ⋅(WL ×D +W T )+1. Eve has a winning strategy in the energy game T E(c) if, and only if, f c n 0 ≠ +∞.

Proof. Thanks to Thm. 9, we know that in such a game, if Eve has a winning strategy, then a credit of c -1 is enough to win. Lem. 10, ensures that f n c will never go higher than c in the initial state. Reciprocally Thm. 16, ensures that if Eve has no winning strategy, then +∞ is reached within n0 steps.

Symbolic Algorithm

We have implemented the previous value iteration algorithm in HyTech [START_REF] Henzinger | Hytech: A model checker for hybrid systems[END_REF]. The implementation is based on the symbolic controllable timed predecessors operator defined in [START_REF] Bouyer | Optimal Strategies in Priced Timed Game Automata[END_REF] and first implemented in HyTech for cost optimal reachability games [START_REF] Bouyer | Synthesis of Optimal Strategies Using HyTech[END_REF]. The choice of HyTech compared to state-of-the-art hybrid systems' analyzers like PHAVer [START_REF] Frehse | PHAVer: algorithmic verification of hybrid systems past HyTech[END_REF] or SpaceEx [START_REF] Frehse | SpaceEx: Scalable Verification of Hybrid Systems[END_REF] is motivated by the fact that HyTech has a built-in script language in which we can define the symbolic controllable predecessors operator easily. The symbolic algorithm/program in HyTech for the example of Fig. 1 is given in Appendix E. The result of the computation for the value iteration algorithm with c = 4 is depicted on Fig. 2 and show the winning zones for Eve in locations Eve and Adam.

The value iteration algorithm is implemented as the iterative computation of the fixpoint of a safety hybrid game. The hybrid game has a special variable E, the energy variable which is the only variable that is not a clock. Each location ℓ of the original WTG has a counterpart location ℓ H in the hybrid game. If w(ℓ) = k ∈ Z then the derivative of E in ℓ H is given by dE dt = k; each discrete transition (ℓ, g, z, ℓ ′ ) of the WTG also has a counterpart transition (ℓ, g, z∧E ∶= E+k, ℓ ′ ) if w(ℓ, g, z, ℓ ′ ) = k.

A state of the hybrid game is thus defined by ((ℓ, v), E) where (ℓ, v) is a state of the original WTG. The existence of a winning strategy for the c-energy game T is reduced to the existence of a winning strategy in the associated hybrid game for the safety objective E ≥ 0 (in each location.) Let Safe = {((ℓ, v), E) 0 ≤ E ≤ c}, where the upper bound c is the one used in the lift function from subsection 5.1. We define the winning states of the safety hybrid game as the greatest fixpoint of: X = Safe ∩ Predt(Up(cPred(X)), uPred(X))

where cPred (controllable predecessor), uPred (uncontrollable predecessor), Predt (temporal predecessor) are defined as in [START_REF] Bouyer | Optimal Strategies in Priced Timed Game Automata[END_REF][START_REF] Bouyer | Synthesis of Optimal Strategies Using HyTech[END_REF] and Up(Y ) = {((ℓ, v), e ′ ) ∃((ℓ, v), e) ∈ Y ∧ e ′ ≥ e}.

The Up operator captures in our symbolic implementation the role of the bound c in the liftc operator: indeed, while the set Xi contains only triples ((ℓ, v), e) where e ≤ c, it is clear that we must include in Xi+1 triples ((ℓ ′ , v ′ ), e ′ ) from which Eve can force in one round the upward closure (for the energy level) of safe states in i steps. This is because if Eve can win from (ℓ, v) with a given energy level then she can win from that state with any greater energy level.

Example 5. In Fig. 26, plain (resp. dashed) arrows are controllable (resp. uncontrollable) edges. In location ℓ0, no task is scheduled and the (battery) energy is recharging at rate +3. There is a background task B to be run at least every 2 t.u. if the other task has not arrived (and actually running in location ℓ1) and a sporadic task S (interrupt) that can happen any time. The task B can be scheduled from location ℓ0 (this is controllable) and we can stop to run it after at least 1 t.u. (measured by clock x.) The background task B has less priority than S and if S happens it is scheduled and B preempted. If we schedule the background task B, we are rewarded by +2 energy units. In locations ℓ0, ℓ1, the sporadic task S can occur (uncontrollable) and in this case it must be scheduled (going to ℓ2) which consumes energy at rate -α. The execution time of S is at most 1 t.u. (measured by clock x) and successive occurrences of S must be separated by at least 2 t.u. (measured by clock y.) ℓ0, +3

[x ≤ 2] ℓ1, -1 [x ≤ 3] ℓ2, -α [x ≤ 1]
x ∶= 0, +2 y ≥ 2, y ∶= 0, x ∶= 0 x ≥ 1, x ∶= 0 y ≥ 2, y ∶= 0, x ∶= 0

x ≤ 1, x ∶= 0 On this example, our symbolic algorithm terminates. If α = 3, the HyTech program (Appendix E) gives a minimal initial energy level of 3 to be able to win the game (notice that we start with y = 2 and thus the sporadic task can arrive at the initial instant.) The optimal strategy from the point of view of Adam is to trigger the sporadic task S as often as possible. While a winning strategy for Eve (scheduler) is to wait in location ℓ0 as long as possible. If the sporadic task arrives again, it is not before 1 t.u. and thus we are rewarded by at least 3 energy credits. If the sporadic does not occur before x = 2, we get 6 energy credits, and we can switch to ℓ1 which increases energy by 2. This ensures winning the energy game, see Fig. 27 for a graphical representation of the winning region. The set of winning state computed by the HyTech program can be used to determine the minimal initial credit for each possible initial state: for example energy ≥ 3 is necessary for the initial condition x = 0, y = 2.)

Now assume α = 4. The previous strategy is not winning any more. However, the result of the HyTech program is now: energy > 4 (for x = 0, y = 2 as initial state.) In this case, while the minimal (infimum) initial credit is 4, there is no strategy realizing this value; the game cannot be won with an initial credit of 4 but rather with any value strictly above 4. Note that this information is collected by our symbolic algorithm but not by the operator liftc as this operator is defined using inf, sup operators.

Figure 1 :

 1 Figure 1: Turn-Based Energy Timed Game A.

en er gy = 3 ⋅ x - 2 +3 4 Figure 2 :

 3242 Figure 2: Winning Zones for Timed Game A.

Figure 3

 3 Figure 3: Winning strategies for Eve

Figure 4 :

 4 Figure 4: Winning strategies for Adam

Figure 6 :

 6 Figure 6: WTG D.

Figure 12 :Figure 13 :

 1213 Figure 12: Game for checking y = 2x

Figure 14 :

 14 Figure 14: Module to encode an increment instruction q1 c 1 ++

Figure 15 :

 15 Figure 15: A WTG T and its associated region game.

1 →

 1 tst(ρn)) + dn ⋅ w(ℓn) + w(en) ≤ w(ρ≤n) + dn ⋅ w(ℓn) + w(en) (by induction hyp.) ≤ w(ρ≤n+1) • otherwise there is i such that [ρi] = [ρn+1] and tst(ρ≤n) = tst(ρ≤i) ⋯sj and sj = ρn. dec(π(ρ≤n+1)) = dec(π(ρ≤i)) ∪ {π(ρi

Lemma 8 .

 8 If Eve has a winning strategy in the unraveling of G from s, she has a winning strategy in G for the universal cycle condition C W .

Proof.

  We show hardness of the problem by a reduction from the Succinct Hamilton Cycle problem: Given a Boolean circuit C with 2N inputs, does the graph on 2N nodes with edge relation encoded by C have a Hamiltonian cycle? This problem is known to be NEXP-complete [35]. We will construct a WTG of polynomial size, which is robust if, and only, if there is no Hamiltonian cycle in the succinctly represented graph. Thus showing that the problem is co-NEXP-hard Variables representing nodes of the graph are encoded by clocks x1 . . . x N and y1 . . . y N . Variables xi being for the current node and yi for the successor node, i.e. xi are the first N inputs of the circuit and yi the N last.

Figure 19 :

 19 Figure 19: Module Choose(x).

Figure 20 := 0 g3 ← 1 t = 0 g1 = 1 ∧Figure 21 :

 2010121 Figure 20: Module x ← y.

Figure 22 : 1 Figure 23 :+2Figure 24 :

 2212324 Figure 22: Module MIX introducing weight around 0

  Out s ′ (σ∃, σ∀)≤n) Consider now a strategy σ∀ and ρ the outcome of σ∃ and σ∀. If there is i such that w ρi σ ∃ (ρ ≤i ),σ ∀ (ρ ≤i )

Figure 25 :

 25 Figure 25: WTG with no optimal strategy.

Figure 26 :

 26 Figure 26: Scheduling Example

Figure 27 :

 27 Figure 27: Winning Strategy for Eve, α = 4.

  1. if s does not appear in h then Tab ′ (h, a∃, a∀) = h Figure 16: Winning strategies of Eve.

	a ∃ ,a ∀ → s; 2. otherwise, let i be such that hi = s, and c = h≥i a ∃ ,a ∃ cycle Lem. 7	Unraveling	∀ cycle Lem. 8

∀

→ s (notice that such a i is unique): if c belongs to C W then Tab ′ (h, a∃, a∀) =↑ and otherwise Tab ′ (h, a∃, a∀) =↓.

  The depth of the computation is at most St + 1 and each step is done using space bounded by O( Act 2 ), except at the leafs where we use space p( St + Act ). Hence our algorithm works in space O( St ⋅ Act 2 ) + p( St + Act ).

	Theorem 8. Given a finite concurrent game G with ob-jective

we ask if c ∈ C W and answer true if it does and false otherwise; this is done in space p( St + Act ); • otherwise we successively compute win for each history h ⋅ s with s = Tab(last(h), a∃, a∀) where a∃ ∈ Mov(last(h), Eve) and a∀ ∈ Mov(last(h), Adam), and keep only the result each time; now we check that: ∃a∃. ∀a∀. win (h ⋅ Tab(last(h), a∃, a∀)) ; This can be done in space O( Act 2 ).

Note, that this definition is inductive: as a jump in the region (ℓ, r) gives a reward of δ(ℓ, r), we make sure that a (quasi)-cycle on that region always provides a reward larger than or equal to this value.

Note, that the definition for the good cycles of Adam is symmetric but slightly stronger as we require that the weight of (quasi)-cycles to be ε-bounded away from zero.

uncontrollable predecessors leading to winning states