Symbolic Approximation of Weighted Timed Games

Weighted timed games are zero-sum games played by two players on a timed automaton equipped with weights, where one player wants to minimise the accumulated weight while reaching a target. Weighted timed games are notoriously difficult and quickly undecidable, even when restricted to non-negative weights. For non-negative weights, the largest class that can be analysed has been introduced by Bouyer, Jaziri and Markey in 2015. Though the value problem is undecidable, the authors show how to approximate the value by considering regions with a refined granularity. In this work, we extend this class to incorporate negative weights, allowing one to model energy for instance, and prove that the value can still be approximated, with the same complexity. In addition, we show that a symbolic algorithm, relying on the paradigm of value iteration, can be used as an approximation schema on this class.


Introduction
The design of programs verifying some real-time specifications is a notoriously difficult problem, because such programs must take care of delicate timing issues, and are difficult to debug a posteriori. One research direction to ease the design of real-time software is to automatise the process. The situation may be modelled into a timed game, played by a controller and an antagonistic environment: they act, in a turn-based fashion, over a timed automaton [2], namely a finite automaton equipped with real-valued variables, called clocks, evolving with a uniform rate. A simple, yet realistic, objective for the controller is to reach a target location. We are thus looking for a strategy of the controller, that is a recipe dictating how to play so that the target is reached no matter how the environment plays. Reachability timed games are decidable [4], and EXPTIME-complete [19].
Weighted extensions of these games have been considered in order to measure the quality of the winning strategy for the controller [9,1]: when the controller has several winning strategies in a given reachability timed game, the quantitative version of the game helps choosing a good one with respect to some metrics. This means that the game now takes place over a weighted (or priced) timed automaton [5,3], where transitions are equipped with weights, and locations with rates of weights (the cost is then proportional to the time spent in this location, with the rate as proportional coefficient). While solving the optimal reachability problem on weighted timed automata has been shown to be PSPACE-complete [6] (i.e. the same complexity as the non-weighted version), weighted timed games are known to be undecidable [12]. This has led to many restrictions in order to regain decidability, the first and most interesting one being the class of strictly non-Zeno cost with only non-negative weights (in transitions and locations) [9]: this hypothesis requires that every execution of the timed automaton that follows a cycle of the region automaton has a weight far from 0 (in interval [1, +∞), for instance).
Negative weights are crucial when one wants to model energy or other resources that can grow or decrease during the execution of the system to study. In [16], we have recently extended the strictly non-Zeno cost restriction to weighted timed games in the presence of negative weights in transitions and/or locations. We have described there the class of divergent weighted timed games where each execution that follows a cycle of the region automaton has a weight far from 0, i.e. in (−∞, −1] ∪ [1, +∞). We were able to obtain a doubly-exponential-time algorithm to compute the values and almost-optimal strategies, while deciding the divergence of a weighted clocks of X is a conjunction of atomic constraints of the form x ⊲⊳ c, where ⊲⊳ ∈ { , <, =, >, } and c ∈ Q (we allow for rational coefficients as we will refine the granularity in the following). Guard g is the closed version of a satisfiable guard g where every open constraint x < c or x > c is replaced by its closed version x c or x c. A valuation ν : X → R 0 satisfies an atomic constraint x ⊲⊳ c if ν(x) ⊲⊳ c. The satisfaction relation is extended to all guards g naturally, and denoted by ν |= g. We let Guards(X) denote the set of guards over X. We rely on the crucial notion of regions, as introduced in the seminal work on timed automata [2]: intuitively, a region is a set of valuations that are all time-abstract bisimilar. We will need some refinement of regions, with respect to a granularity 1/N , with N ∈ N. Formally, with respect to the set X of clocks and a constant M , a 1/N -region r is a subset of valuations characterised by the vector (ι x ) x∈X = (min(M N, ⌊ν(x)N ⌋)) x∈X ∈ [0, M N ] X and the order of fractional parts of ν(x)N , given as a partition X = X 0 ⊎ X 1 ⊎ · · · ⊎ X m of clocks: a valuation ν is in this 1/N -region r if (i) ⌊ν(x)N ⌋ = ι x , for all clocks x ∈ X; (ii) ν(x) = 0 for all x ∈ X 0 ; (iii) all clocks x ∈ X i satisfy that ν(x)N have the same fractional part, for all 1 i m. We denote by Reg N (X, M ) the set of 1/N -regions, and we write Reg(X, M ) as a shorthand for Reg 1 (X, M ). We recover the traditional notion of region for N = 1. E.g., the figure on the right depicts regions Reg({x, y}, 2) as well as their refinement Reg 3 ({x, y}, 2). For any integer guard g, either all valuations of a given 1/N -region satisfy g, or none of them do. A 1/N -region r ′ is said to be a time successor of the 1/N -region r if there exist ν ∈ r, ν ′ ∈ r ′ , and d > 0 such that ν ′ = ν + d. Moreover, for Y ⊆ X, we let r[Y := 0] be the 1/N -region where clocks of Y are reset. On the left, a weighted timed game. Locations belonging to Min (resp. Max) are depicted by circles (resp. squares). The target location is ℓ3, whose output weight function is null. It is easy to observe that location ℓ1 (resp. ℓ5) has value +∞ (resp. −∞). As a consequence, the value in ℓ4 is determined by the edge to ℓ3, and depicted in blue on the right. In location ℓ2, the value associated with the transition to ℓ3 is depicted in red, and the value in ℓ2 is obtained as the minimum of these two curves. Observe the intersection in x = 2/3 requiring to refine the regions.
Weighted timed games. A weighted timed game (WTG) is then a tuple G = L = L Min ⊎ L Max , ∆, wt, L T , wt T where L Min and L Max are finite disjoint subsets of locations belonging to Min and Max, respectively, ∆ ⊆ L × Guards(X) × 2 X × L is a finite set of transitions, wt : ∆ ⊎ L → Z is the weight function, associating an integer weight with each transition and location, L T ⊆ L Min is a subset of target locations for player Min, and wt T : L T × R X 0 → R ∞ is a function mapping each target location and valuation of the clocks to a final weight of R ∞ = R ⊎ {−∞, +∞} (possibly 0, +∞, or −∞). The addition of target weights is not standard, but we will use it in the process of solving those games: anyway, it is possible to simply map each target location to the weight 0, allowing us to recover the standard definition. Without loss of generality, we suppose the absence of deadlocks except on target locations, i.e. for each location ℓ ∈ L\L T and valuation ν, there exists (ℓ, g, Y, ℓ ′ ) ∈ ∆ such that ν |= g, and no transitions start in L T .
The semantics of a WTG G is defined in terms of a game played on an infinite transition system whose vertices are configurations of the WTG. A configuration is a pair (ℓ, ν) with a location and a valuation of the clocks. Configurations are split into players according to the location. A configuration is final if its location is a target location of L T . The alphabet of the transition system is given by R 0 × ∆ and will encode the delay that a player wants to spend in the current location, before firing a certain transition. For every delay d ∈ R 0 , transition δ = (ℓ, g, Y, ℓ ′ ) ∈ ∆ and valuation ν, there is an edge (ℓ, ν) d,δ − − → (ℓ ′ , ν ′ ) if ν + d |= g and ν ′ = (ν + d)[Y := 0]. The weight of such an edge e is given by d × wt(ℓ) + wt(δ). An example is depicted on Figure 1.
A finite play is a finite sequence of consecutive edges ρ = (ℓ 0 , ν 0 ) − −− → · · · (ℓ k , ν k ). We denote by |ρ| the length k of ρ. The concatenation of two finite plays ρ 1 and ρ 2 , such that ρ 1 ends in the same configuration as ρ 2 starts, is denoted by ρ 1 ρ 2 . We let FPlays G be the set of all finite plays in G, whereas FPlays Min G (resp. FPlays Max G ) denote the finite plays that end in a configuration of Min (resp. Max). A play is then a maximal sequence of consecutive edges (it is either infinite or it reaches L T ).
A strategy for Min (resp. Max) is a mapping σ : FPlays Min A strategy σ is memoryless if for all finite plays ρ, ρ ′ ending in the same configuration, we have that σ(ρ) = σ(ρ ′ ). For all strategies σ Min and σ Max of players Min and Max, respectively, and for all configurations (ℓ 0 , ν 0 ), we let play G ((ℓ 0 , ν 0 ), σ Max , σ Min ) be the outcome of σ Max and σ Min , defined as the only play conforming to σ Max and σ Min and starting in (ℓ 0 , ν 0 ).
The objective of Min is to reach a target configuration, while minimising the accumulated weight up to the target. Hence, we associate to every finite play ρ = (ℓ 0 , ν 0 ) − −− → · · · (ℓ k , ν k ) its cumulated weight, taking into account both discrete and continuous costs: Then, the weight of a play ρ, denoted by wt G (ρ), is defined by +∞ if ρ is infinite (does not reach L T ), and wt Σ (ρ) + wt T (ℓ T , ν) if it ends in (ℓ T , ν) with ℓ T ∈ L T . Then, for all locations ℓ and valuation ν, we let Val G (ℓ, ν) be the value of G in (ℓ, ν), defined as Val G ((ℓ, ν)) = inf σ Min sup σ Max wt G (play((ℓ, ν), σ Max , σ Min )), where the order of the infimum and supremum does not matter, since WTGs are known to be determined 1 . We say that a strategy σ ⋆ Min of Min is ε-optimal if, for all (ℓ, ν), and all strategies σ Max of Max, wt G (play((ℓ, ν), σ Max , σ ⋆ Min )) Val G (ℓ, ν) + ε. It is said optimal if this holds for ε = 0. A symmetric definition holds for optimal strategies of Max. If the game is clear from the context, we may drop the index G from all previous notations.
As usual in related work [1,9,10], we assume that the input WTGs have guards where all constants are integers, and all clocks are bounded, i.e. there is a constant M ∈ N such that every transition of the WTG is equipped with a guard g such that ν |= g implies ν(x) M for all clocks x ∈ X. We denote by w L max (resp. w ∆ max , w e max ) the maximal weight in absolute values of locations (resp. of transitions, edges) of . We also assume that the output weight functions are piecewise linear with a finite number of pieces and are continuous on each region. Notice that the zero output weight function satisfies this property. Moreover, the computations we will perform in the following maintain this property as an invariant, and use it to prove their correctness.
Region and corner abstractions. The region automaton, or region game, R N (G) (abbreviated as R(G) when N = 1) of a game G = L = L Min ⊎ L Max , ∆, wt, L T , wt T is the WTG with locations S = L × Reg N (X, M ) and all transitions ((ℓ, r), g ′′ , Y, (ℓ ′ , r ′ )) with (ℓ, g, Y, ℓ ′ ) ∈ ∆ such that the model of guard g ′′ (i.e. all valuations ν such that ν |= g ′′ ) is a 1/N -region r ′′ , time successor of r such that r ′′ satisfies the guard g, and r ′ = r ′′ [Y := 0]. Distribution of locations to players, final locations and weights are taken according to G. We call path a finite or infinite sequence of transitions in this automaton, and we denote by π the paths. A play ρ in G is projected on a path π in R N (G), by replacing every edge (ℓ, ν) where r (resp. r ′ ) is the 1/N -region containing ν (resp. ν ′ ): we say that ρ follows the path π. It is important to notice that, even if π is a cycle (i.e. starts and ends in the same location of the region game), there may exist plays following it in G that are not cycles, due to the fact that regions are sets of valuations. By projecting away the region information of R N (G), we simply obtain: On top of regions, we will need the corner-point abstraction techniques introduced in [8]. A valuation v is said to be a corner of a 1/N -region r, if it belongs to the topological closure r and has coordinates multiple of 1/N (v ∈ (1/N )N X ). We call corner state a triple (ℓ, r, v) that contains information about a location (ℓ, r) of the region-game R N (G), and a corner v of the 1/N -region r. Every region has at most |X| + 1 corners. We now define the corner-point abstraction C N (G) of a WTG G as the WTG obtained as a refinement of R N (G) where guards on transitions are enforced to stay on one of the corners of the current 1/N -region: the locations of C N (G) are all corner states of R N (G), associated to each player accordingly, and transitions are all ((ℓ, r, v), g ′′ , Y, (ℓ ′ , r ′ , v ′ )) such that there exists t = ((ℓ, r), g, Y, (ℓ ′ , r ′ )) a transition of R N (G) such that the model of guard g ′′ is a corner v ′′ satisfying the guard g (recall that g is the closed version of g), v ′ = v ′′ [Y := 0], and there exist two valuations ν ∈ r, ν ′ ∈ r ′ such that ((ℓ, r), ν) the latter condition ensures that the transition between corners is not spurious). Because of this closure operation, we must also define properly the final weight function: we simply define it over the only valuation v reachable in location (ℓ, r, v) (with ℓ ∈ L T ) by wt T ((ℓ, r, v), v) = lim ν→v,ν∈r wt T (ℓ, ν) (the limit is well defined since wt T is piecewise linear with a finite number of pieces on region r).
The WTG C N (G) can be seen as a weighted game (with final weights), i.e. a WTG without clocks (which means that there are only weights on transitions), by removing guards, resets and rates of locations, and replacing the weights of transitions by the actual weight of jumping from one corner to another: a transition (((ℓ, r), v), g ′′ , Y, ((ℓ ′ , r ′ ), v ′ )) becomes an edge from ((ℓ, r), v) to ((ℓ ′ , r ′ ), v ′ ) with weight d × wt(ℓ) + wt(t) (for all possible values of d, which requires to allow for multi-edges 2 ). Note that delay d is necessarily a rational of the form α/N with α ∈ N, since it must relate corners of 1/N -regions. In particular, this proves that the cumulated weight wt Σ (ρ) of a finite play ρ in C N (G) is indeed a rational number with denominator N .
We will call corner play a play ρ in the corner-point abstraction C N (G): it can also be interpreted as a timed execution in G where all guards are closed (as explained in the definition above). It straightforwardly projects on a finite path π in the region game R N (G): in this case, we say again that ρ follows π. Figure 2 depicts a play, its projected path in the region game and one of its associated corner plays.

Fig. 2.
A play ρ (in blue), its projected path π in the region game (in red), and one of its associated corner plays ρ ′ (in green) Corner plays allow one to obtain faithful information on the plays that follow the same path: If π is a finite path in R N (G), the set {wt Σ (ρ) | ρ finite play following π} is an interval bounded by the minimum and the maximum values of the set {wt Σ (ρ) | ρ finite corner play of C N (G) following π}.
Value iteration. We will rely on the value iteration algorithm described in [1] for a WTG G.
If V represents a value function-i.e. a mapping from configurations of L × R X 0 to a value in R ∞ -we denote by V ℓ,ν the image V (ℓ, ν), for better readability, and by V ℓ the function mapping each valuation ν to V ℓ,ν . One step of the game is summarised in the following operator F mapping each value function V to a value function ranges over valid edges in G. Then, starting from V 0 mapping every configuration to +∞, except for the targets mapped to wt T , we let V i = F (V i−1 ) for all i > 0. The value function V i represents the value Val i G , which is intuitively what Min can guarantee when forced to reach the target in at most i steps.
More formally, we define wt i G (ρ) the weight of a maximal play ρ at horizon i, as wt G (ρ) if ρ reaches a target state in at most i steps, and +∞ otherwise. Using this alternative definition of the weight of a play, we can obtain a new game value The mappings V 0 ℓ are piecewise linear for all ℓ, and F preserves piecewise linearity over regions, so all iterates V i ℓ are piecewise linear with a finite number of pieces. In [1], it is proved that V i ℓ has a number of pieces (and can be computed within a complexity) exponential in i and in the size of G when wt T = 0. This result can be extended to handle negative weights in G and output weights wt T = 0.

Results
We consider the value problem that asks, given a WTG G, a location ℓ and a threshold α ∈ Z∪{−∞, +∞}, to decide whether Val G (ℓ, 0) α. In the context of timed games, optimal strategies may not exist. We generally focus on finding ε-optimal strategies, that guarantee the optimal value, up to a small error ε. Moreover, when the value problem is undecidable, we also consider the approximation problem that consists, given a precision ε ∈ Q >0 , in computing an ε-approximation of Val G (ℓ, 0). In the one-player case, computing the optimal value and an ε-optimal strategy for weighted timed automata is known to be PSPACE-complete [6]. In the two-player case, the value problem of WTGs (also called priced timed games in the literature) is undecidable with 3 clocks [12,10], or even 2 clocks in the presence of negative weights [15] (for the existence problem asking if a strategy of player Min can guarantee a given threshold). To obtain decidability, one possibility is to limit the number of clocks to 1: then, there is an exponential-time algorithm to compute the value as well as ε-optimal strategies in the presence of non-negative weights only [7,20,17], whereas the problem is only known to be PTIME-hard. A similar result can be lifted to arbitrary weights, under restrictions on the resets of the clock in cycles [13].
The other possibility to obtain a decidability result [9,16] is to enforce a semantical property of divergence (originally called strictly non-Zeno cost): it asks that every play following a cycle in the region automaton has weight far from 0. It allows the authors to prove that playing for only a bounded number of steps is equivalent to the original game, which boils down to the problem of computing the value of a tree-shaped weighted timed game G using the value iteration algorithm.
Other objectives, not directly related to optimal reachability, have been considered in [11] for weighted timed games, like mean-payoff and parity objectives. In this work, the authors manage to solve these problems for the so-called class of δ-robust WTGs that they introduce. This class includes the class we consider, but is decidable in 2-EXPSPACE.
In [16], we generalised the strictly non-Zeno cost property of [9,16] to weighted timed games with both positive and negative weights: we called them divergent weighted timed games. This article relaxes the divergence property, to introduce almost-divergent weighted timed games. We first define formally these classes of games. A cycle π of R(G) is said to be a positive cycle (resp. a 0-cycle, or a negative cycle) if every finite play ρ following π satisfies wt Σ (ρ) 1 (resp. wt Σ (ρ) = 0, or wt Σ (ρ) −1). A strongly connected component (SCC) S of R(G) is said to be positive (resp. negative) if every cycle π ∈ S is positive (resp. negative). An SCC S of R(G) is said to be non-negative (resp. non-positive) if every play ρ following a cycle in S satisfies either wt Σ (ρ) 1 or wt Σ (ρ) = 0 (resp. either wt Σ (ρ) −1 or wt Σ (ρ) = 0).

Definition 1.
A WTG G is divergent if every SCC of R(G) is either positive or negative. As a generalisation, a WTG G is almost-divergent when every SCC of R(G) is either non-negative or non-positive.
In [16], we showed that we can decide in 2-EXPTIME the value problem for divergent WTGs. Unfortunately, it is shown in [10] that this problem is undecidable for almost-divergent WTGs (already with non-negative weights only, where almost-divergent WTGs are called simple). They propose a solution to the approximation problem, again with non-negative weights only. Our first result is the following extension of their result: Theorem 1. Given an almost-divergent WTG G, a location ℓ and ε ∈ Q >0 , we can compute an ε-approximation of Val G (ℓ, 0) in time doubly-exponential in the size of G and polynomial in 1/ε.

Moreover, deciding if a WTG is almost-divergent is PSPACE-complete.
To obtain this result, we follow an approximation schema that we now outline. First, we will always reason on the region game R(G) of the almost-divergent WTG G. The goal is to compute an ε-approximation of Val R(G) (s 0 , 0) for some state s 0 = (ℓ 0 , r 0 ), with r 0 the region where every clock value is 0. As already recalled, techniques of [1] allow one to compute the (exact) values of a WTG played on a finite tree, using operator F . The idea is thus to decompose as much as possible the game R(G) in a WTG over a tree. First, we decompose the region game into SCCs (left of Figure 3).
During the approximation process, we must think about the final weight functions as the previously computed approximations of the values of SCCs below the current one. We will keep as an invariant that final weight functions are piecewise linear functions with a finite number of pieces, and are continuous on each region.
For an SCC of R(G) and an initial state s 0 of R(G) provided by the SCC decomposition, we show that the game on the SCC is equivalent to a game on a tree built from a semi-unfolding (see middle of Figure 3) of R(G) from s 0 of finite depth, with certain nodes of the tree being kernels. These kernels are some parts of R(G) that contain all cycles of weight 0. The semi-unfolding is stopped either when reaching a final location, or when some location (or kernel) has been visited for a certain fixed number of times: such locations deep enough are called stop leaves.
Our second result is a more symbolic approximation schema based on the value iteration only. It is more symbolic in the sense that it does not require the SCC decomposition, the computation of kernels nor the semi-unfolding of the game in a tree.
Then the sequence (Val k G ) k 0 converges towards Val G and for every ε ∈ Q >0 , we can compute an integer P such that Val P G is an ε-approximation of Val G for all configurations.
Remark 1. In a weighted-timed game, it is easy to detect the set of states with value +∞: these are all the states from which Min cannot ensure reachability of a target location ℓ ∈ L T with wt T (ℓ) < +∞. It can therefore be computed by an attractor computation, and is indeed a property constant on each region. In particular, removing those states from R(G) does not affect the value of any other state and can be done in complexity linear in |R(G)|. We will therefore assume that the considered WTG have no configurations with value +∞.

Kernels of an almost-divergent WTG
The approximation procedure described before uses the so-called kernels in order to group together all cycles of weight 0. We study those kernels and give a characterisation allowing computability. Contrary to the non-negative case, the situation is more complex in our arbitrary case, since weights of both locations and transitions may differ from 0 in the kernel. Moreover, it is not trivial (and may not be true in a non almost-divergent WTG) to know whether it is sufficient to consider only simple cycles, i.e. cycles without repetitions.
To answer these questions, let us first analyse the cycles of R(G) that we will encounter. Since we are in an almost-divergent game, by Lemma 2, all cycles π = t 1 · · · t n of R(G) (with t 1 , . . . , t n transitions of R(G)) are either 0-cycles, positive cycles or negative cycles. Additionally, in an SCC S of R(G), we cannot find both positive and negative cycles by definition. Moreover, we can classify a cycle by looking only at the corner plays following it.
Proof. If π is a 0-cycle, every such corner play ρ will have weight 0, by Lemma 2. Reciprocally, if such a corner play exists, all corner plays following π have weight 0: otherwise the set {wt Σ (ρ) | ρ play following π} would have non-empty intersection with the set (−1, 1) \ {0} which would contradict the almost-divergence.
An important result is that 0-cycles are stable by rotation. This is not trivial because plays following a cycle can start and end in different valuations, therefore changing the starting state of the cycle could a priori change the plays that follow it and their weights.
First, since there are finitely many corners, by constructing a long enough play following an iterate of π ′ π, we can obtain a corner play that starts and ends in the same corner. Formally, we define two sequences of region corners (v i ∈ first(π)) i and (v ′ i ∈ first(π ′ )) i . We start by choosing any v 0 ∈ first(π). Let v ′ 0 be a corner of first(π ′ ) such that v ′ 0 is accessible from v 0 by following π. For every i > 0, let v i be a corner of first(π) such that v i is accessible from v ′ i−1 by following π ′ , and let v ′ i be a corner of first(π ′ ) such that v ′ i is accessible from v i by following π. We stop the construction at the first l such that there exists This process is bounded since first(π) has at most |X| + 1 corners. For every 0 i l, let w i be the weight of a play ρ i from v i to v ′ i along π, and let w ′ i be the weight of a play ρ ′ i from v ′ i to v i+1 along π ′ . The concatenation of the two plays has weight w i + w ′ i = 0, since it follows the 0-cycle π 1 . Therefore, all corner plays from v i to v ′ i following π have the same weight w i , and the same applies for w ′ i . For every 0 i < l, the concatenation of Since π 2 is a cycle, and the game is almost-divergent, all possible values of w i+1 − w i have the same sign.
Finally, we can construct a corner play This implies that the terms w i+1 − w i , of constant sign, are all equal to 0. As a consequence, the concatenation of ρ ′ k and ρ k+1 is a corner play following π 2 of weight 0. By Lemma 3, we deduce that π 2 is a 0-cycle.
We will now construct the kernel K as the subgraph of R(G) containing all 0-cycles. Formally, let T K be the set of transitions of R(G) belonging to a simple 0-cycle, and S K be the set of states covered by T K . We define the kernel K of R(G) as the subgraph of R(G) defined by S K and T K . Transitions in T \T K with starting state in S K are called the output transitions of K. We define it using only simple 0-cycles in order to ensure its computability. However, we now show that this is of no harm, since the kernel contains exactly all the 0-cycles, which will be crucial in the approximation schema we present in Section 6.

Proposition 1. A cycle of R(G) is entirely in K if and only if it is a 0-cycle.
Proof. We prove that every 0-cycle is in K by induction on the length of the cycles. The initialisation contains only cycles of length 1, that are in K by construction. If we consider a cycle π of length n > 1, it is either simple or it can be rotated and decomposed into π ′ π ′′ , π ′ and π ′′ being smaller cycles. Let ρ be a corner play following π ′ π ′′ . We denote by ρ ′ the prefix of ρ following π ′ and ρ ′′ the suffix following π ′′ . It holds that wt Σ (ρ ′ ) = −wt Σ (ρ ′′ ), and in an almost-divergent SCC this implies wt Σ (ρ ′ ) = wt Σ (ρ ′′ ) = 0. Therefore, by Lemma 3 both π ′ and π ′′ are 0-cycles, and they must be in K by induction hypothesis. Note that this reasoning proves that every cycle contained in a longer 0-cycle is also a 0-cycle.
We now prove that every cycle in K is a 0-cycle. By construction, every transition t ∈ T K is part of a simple 0-cycle. Thus, to every transition t ∈ T K , we can associate a path π t such that tπ t is a simple 0-cycle (rotate the simple cycle if necessary). We can prove (using both Lemmas 3 and 4) the following property by relying on another pumping argument on corners: If t 1 · · · t n is a path in K, then t 1 t 2 · · · t n π tn · · · π t2 π t1 is a 0-cycle of R(G). Now, if π is a cycle of R(G) in K, there exists a cycle π ′ such that ππ ′ is a 0-cycle, therefore π is a 0-cycle.

Semi-unfolding of almost-divergent WTGs
Given an almost-divergent WTG G, we describe the construction of its semi-unfolding T (G) (as depicted in Fig. 3). This crucially relies on the absence of states with value −∞, so we explain how to deal with them first:

Lemma 5. In an SCC of R(G), the set of configurations with value −∞ is a union of regions computable in time linear in the size of R(G).
Proof (Sketch of proof). If the SCC is non-negative, the cumulated weight cannot decrease along a cycle, thus, the only way to obtain value −∞ is to jump in a final state with final weight −∞. We can therefore compute this set of states with an attractor for Min.
If the SCC is non-positive, we let S R f (resp. S −∞ f ) be the set of target states where wt T is bounded (resp. has value −∞). We also define T R f (resp. T −∞ f ), the set of transitions of R(G) whose end state belongs to S R f (resp. S −∞ f ). Notice that the kernel cannot contain target states since they do not have outgoing transitions. We can prove that a configuration has value −∞ iff it belongs to a state where player Min can ensure the LTL formula on transitions: . The procedure to detect −∞ states thus consists of four attractor computations, which can be done in time linear in |R(G)|.
We can now assume that no states of G have value −∞, and that the output weight function maps all configurations to R. Since wt T is piecewise linear with finitely many pieces, wt T is bounded. Let sup |wt T | denote the bound of |wt T |, ranging over all target configurations.
We now explain how to build the semi-unfolding T (G). We only build the semi-unfolding T (G) of an SCC of G starting from some state (ℓ 0 , r 0 ) ∈ S of the region game, since it is then easy to glue all the semi-unfoldings together to get the one of the full game. Since every configuration has finite value, we can prove that values of the game are bounded by |R(G)|w e max + sup |wt T |. As a consequence, we can find a bound γ linear in |R(G)|, w e max and sup |wt T | such that a play that visits some state outside the kernel more than γ times has weight strictly above |R(G)|w e max + sup |wt T |, hence is useless for the value computation. This leads to considering the semi-unfolding T (G) of G (nodes in the kernel are not unfolded, see Figure 3) such that each node not in the kernel is encountered at most γ times along a branch: the end of each branch is called a stop leaf of the semi-unfolding. In particular, the depth of T (G) is bounded by |R(G)|γ, and thus is polynomial in |R(G)|, w e max and sup |wt T |. Leaves of the semi-unfolding are thus of two types: target leaves that are copies of target locations of G for which we set the target weight as in G, and stop leaves for which we set their target weight as being constant to +∞ if the SCC G is non-negative, and −∞ if the SCC is non-positive.

Approximation of almost-divergent WTGs
Approximation of kernels. We start by approximating a kernel G by extending the region-based approximation schema of [10]. In their setting, all runs in kernels had weight 0, allowing a simple reduction to a finite weighted game. In our setting, we have to approximate the timed dynamics of runs, and therefore resort to the corner-point abstraction (as shown to the right of Fig. 3).
Since output weight functions are piecewise linear with a finite number of pieces and continuous on regions, they are Λ-Lipschitz-continuous 3 , for a given constant Λ 0. We let B = w L max |L||Reg(X, M )| + Λ. Let N be an integer. Consider the game C N (G) described in the preliminary section, with locations of the form (ℓ, r, v) with v a corner of the 1/N -region r. Two plays ρ of G and ρ ′ of C N (G) are said to be 1/N -close if they follow the same path π in R N (G). In particular, at each step the configurations (ℓ, ν) in ρ and (ℓ ′ , r ′ , v ′ ) in ρ ′ (with v ′ a corner of the 1/N -region r ′ ) satisfy ℓ = ℓ ′ and ν ∈ r ′ , and the transitions taken in both plays have the same discrete weights. Close plays have close weights, in the following sense: , with ν 0 ∈ r 0 , since both players have the ability to stay 1/N -close all along the plays, a bisimulation argument permits to obtain that the values of the two games are also close in (ℓ 0 , ν 0 ) and ((ℓ 0 , r 0 , v 0 ), v 0 ): Using this result, picking N an integer larger than B/ε, we can thus obtain |Val Recall that C N (G) can be considered as an untimed weighted game (with reachability objective). Thus we can apply the result of [14], where it is shown that the optimal values of such games can be computed in pseudo-polynomial time (i.e. polynomial time with weights encoded in unary, instead of binary). We then define an ε-approximation of Val G , named Val ′ N , on each 1/N -region by interpolating the values of its 1/N -corners in C N (G) with a piecewise linear function: therefore, we can control the Lipschitz constant of the approximated value for further use.

Lemma 8. Val ′
N is an ε-approximation of Val G , that is piecewise linear with a finite number of pieces and 2B-Lipschitz-continuous over regions.
Approximation of almost-divergent WTGs. We now explain how to approximate the value of an almost-divergent WTG G, thus proving Theorem 1. First, we compute a semi-unfolding T (G) as described in the previous section. Then we perform a bottom-up computation of the approximation. As already recalled, techniques of [1] allow us to compute exact values of a tree-shape WTG. In consequence, we know how to compute the value of a non-kernel node of T (G), depending of the values of its children. There is no approximation needed here, so that if all children are εapproximation, we can compute an ε-approximation of the node. Therefore, the only approximation lies in the kernels, and we explained before how to compute arbitrarily close an approximation of a kernel's value. We crucially rely on the fact that the value function is 1-Lipschitz-continuous 4 . This entails that imprecisions will sum up along the bottom-up computations, as computing an ε-approximation of the value of a game whose output weights are ε ′ -approximations yields an (ε + ε ′ )-approximation. Therefore we compute approximations with threshold ε ′ = ε/α for kernels in T (G), where α is the maximal number of kernels along a branch of T (G): α is smaller than the depth of T (G), which is bounded by Proposition 2.
The subregion granularity considered before for kernel approximation crucially depends on the Lipschitz constant of output weights. The growth of these constants is bounded for kernels in T (G) by Lemma 8. For non-kernel nodes of T (G), using a careful analysis of the algorithm of [1], we obtain the following bound: Lemma 9. If all the output weights of a WTG G are Λ-Lipschitz-continuous over regions (and piecewise linear, with finitely many pieces), then Val i G is ΛΛ ′ -Lipschitz-continuous over regions, with Λ ′ polynomial in w L max and |X| and exponential in i. The overall time complexity of this method is doubly-exponential in the size of the input game and polynomial in 1/ε.

Symbolic approximation algorithm
The previous approximation result suffers from several drawbacks. It relies on the SCC decomposition of the region automaton. Each of these SCCs have to be analysed in a sequential way, and their analysis requires an a priori refinement of the granularity of regions. This approach is thus not easily amenable to implementation. We instead prove in this section that the symbolic approach based on the value iteration paradigm, i.e. the computation of iterates of the operator F recalled in page 6, is an approximation schema. This is stated in Theorem 2, for which we now sketch a proof in this section.
Notice that configurations with value +∞ are stable through value iteration, and do not affect its other computations. Since Theorem 2 assumes the absence of configurations of value −∞, we will therefore consider in the following that all configurations have finite value in G.
Consider first a game G that is a kernel. By the results of Section 6, there exists an integer N such that solving the untimed weighted game C N (G) computes an ε/2-approximation of the value of 1/N corners. Using the results of [14] for untimed weighted games, we know that those values are obtained after a finite number of steps of (the untimed version of) the value iteration operator. More precisely, if one considers a number of iterations P = |L||Reg N (X, M )|(|X| + 1)(2(|L||Reg N (X, M )|(|X| + 1) − 1)w e max + 1), then Val P CN (G) ((ℓ, r, v), v) = Val CN (G) ((ℓ, r, v), v). From this observation, we deduce the following property of P :

Lemma 10. If G is a kernel with no configurations of infinite value, then |Val
Proof. We already know that Val P CN (G) ((ℓ, r, v), v) = Val CN (G) ((ℓ, r, v), v) for all configurations ((ℓ, r, v), v) of C N (G). Moreover, Section 6 ensures |Val G (ℓ, ν)−Val CN (G) ((ℓ, r, v), v)| ε/2 whenever ν is in the 1/N -region r. Therefore, we only need to prove that |Val P G (ℓ, ν) − Val P CN (G) ((ℓ, r, v), v)| ε/2 to conclude. This is done as for Lemma 7, since Lemma 6 (that we need to prove Lemma 7) does not depend on the length of the plays ρ and ρ ′ , and both runs reach the target state in the same step, i.e. both before or after the horizon of P steps.
Once we know that value iteration converges on kernels, we can use the semi-unfolding of Section 5 to prove that it also converges on non-negative SCCs when all values are finite.

Lemma 11. If G is a non-negative SCC with no configurations of infinite value, we can compute
The idea is to unfold every kernel of the semi-unfolding game T (G) according to its bound in Lemma 10. More precisely, let α be the maximum number of kernels along one of the branches of T (G). In a bottom-up fashion, we can find for each kernel K in T (G) a bound P K such that, for all configurations (ℓ, ν), |Val K (ℓ, ν) − Val P K K (ℓ, ν)| ε/α. We thus unfold K in T (G) with depth up to P K . After each kernel has been replaced this way, T (G) is no longer a semi-unfolding, it is instead a (complete) unfolding of R(G), of a certain bounded depth P + . This new bound P + is bounded by the former depth of T (G) to which is added α times the biggest bound P K we need for the kernels. Now, T (G) is a tree of depth P + whose value at its root is ε-close to the value of G. Finally, the value computed by Val P+ G is bounded between Val G and Val T (G) , which allows us to conclude.
The bound P K for a kernel K depends linearly in Λ, the Lipschitz constant of value functions on locations of T (G) reachable from K. Once K has been replaced by its unfolding of depth P K , the Lipschitz constant of the value function at the root of T (G) are thus bounded exponentially in Λ. This means that we ensure a bound for P + that is at most polynomial in 1/ε, and that is of the order of a tower of α exponentials.
Proving the same property on non-positive SCCs requires more work, because the semiunfolding gives output weight −∞ to stop leaves, which doesn't integrate well with value iteration (initialisation at +∞ on non-target states). However, by unfolding those SCCs slightly more (at most |R(G)| more steps), we can obtain the desired property with a similar bound P − . for all configurations (ℓ, ν) of G. Now, if we are given an almost-divergent game G and a precision ε, we can add the bounds for value iteration obtained from each SCC by Lemmas 11 and 12, and obtain a final bound P such that for all k P , Val k G is an ε-approximation of Val G . Discussion. Overall, this leads to an upper bound complexity that is polynomial in 1/ε and of the order of a tower of n exponentials, with n polynomial in the size of the input WTG. However, we argue that this symbolic procedure is more amenable to implementation than the previous approximation schema. First, it avoids the three already mentioned drawbacks (SCC decomposition, sequential analysis of the SCCs, and refinement of the granularity of regions) of the previous approximation schema. Then, it allows one to directly launch the value iteration algorithm on the game G, and we can stop the computation whenever we are satisfied enough by the approximation computed: however, there are no guarantees whatsoever on the quality of the approximation before the number of steps P given above. Finally, this schema allows one to easily obtain an almost-optimal strategy with respect to the computed value.

Lemma 12. If G is a non-positive SCC with no configurations of infinite value, we can compute
If G is not guaranteed to be free of configurations of value −∞, then we must first perform the SCC decomposition of R(G), and, as G is almost-divergent, identify and remove regions whose value is −∞, by Lemma 5. Then, we can apply the value iteration algorithm.
As a final remark, notice that our correctness proof strongly relies on Section 6, and thus would not hold with the approximation schema of [10] (which does not preserve the continuity on regions of the computed value functions, in turn needed to define output weights on 1/N -corners).

Conclusion
We have given an approximation procedure for a large class of weighted timed games with unbounded number of clocks and arbitrary integer weights that can be executed in doubly-exponential time with respect to the size of the game. In addition, we proved the correctness of a symbolic approximation schema, that does not start by splitting exponentially every region, but only does so when necessary (as dictated by [1]). We argue that this paves the way towards an implementation of value approximation for weighted timed games.
Another perspective is to extend this work to the concurrent setting, where both players play simultaneously and the shortest delay is selected. We did not consider this setting in this work because concurrent WTGs are not determined, and several of our proofs rely on this property for symmetrical arguments (mainly to lift results of non-negative SCCs to non-positive ones). Another extension of this work is the exploration of the effect of almost-divergence in the case of multiple weight dimensions, and/or with mean-payoff objectives.

A Proofs of Section 2
Proof (Proof of Lemma 2). The set {wt Σ (ρ) | ρ finite play following π} is an interval as the image of a convex set by an linear function (see [6,Sec. 3.2] for an explanation). The good properties of the corner-point abstraction allows us to conclude, since for every play ρ following π, one can find a corner play following π of smaller weight and one of larger weight, and for every corner play ρ following π and every ε > 0, one can find a play following π whose weight is at most ε away from wt Σ (ρ) [8].

A.1 Undecidability of value −∞
We prove that given a WTG G (not necessarily almost-divergent) and an initial location ℓ 0 , it is undecidable whether Val G (ℓ 0 , 0) = −∞. We reduce it to the existence problem on turn-based WTG: given a WTG G (without output weight function), an integer threshold α and a starting location ℓ 0 , does there exist a strategy for Min that can guarantee reaching the unique target location ℓ t from ℓ 0 with weight < α. In the non-negative setting, it is proved in [7] that the problem is undecidable for the comparison α. In the negative setting, formal proofs are given for all comparison signs in [15].
Consider G ′ the WTG built from G by adding a transition from ℓ t to ℓ 0 , without guards and resetting all the clocks, of discrete weight −α. We add a new target location ℓ ′ t , and add transitions of weight 0 from ℓ t to ℓ ′ t . Location ℓ t is then given to Min. Let us prove that Val G ′ (ℓ 0 , 0) = −∞ if and only if Min has a strategy to guarantee a weight < α in G.
Assume first Val G ′ (ℓ 0 , 0) = −∞. If Val G (ℓ 0 , 0) = −∞, we are done. Otherwise, Min must follow in G ′ the new transition from ℓ t to ℓ 0 to enforce a cycle of negative value, and thus enforce a play from (ℓ 0 , 0) to ℓ t with weight less than α. Therefore, there exists a strategy for Min in G that can guarantee a weight < α.
Reciprocally, if there exists a strategy for Min that can guarantee a weight < α, then Min can force a negative cycle play and Val G ′ (ℓ 0 , 0) = −∞.

A.2 Decision of the almost-divergence of a WTG
First, we state that a WTG G is not almost-divergent if and only if R(G) contains an SCC with either both a positive play following one of its cycles and a negative play following one of its cycles, or a play with weight in (−1, 0) ∪ (0, 1) following one of its cycles. We will now explain how we can test both of those properties (and thus if a game is not almost-divergent) in PSPACE.
A corner play following a cycle of the region game is said to be simple if it does not visit the same corner twice (but the first and last corners can be the same). A simple corner play following a cycle has length bounded by |S| × (|X| + 1). By Lemma 2, R(G) contains an SCC with either both a positive play following one of its cycles and a negative play following one of its cycles if and only if R(G) contains both a positive corner play following one of its cycles and a negative corner play following one of its cycles. We will extend this to simple corner plays.

Lemma 13. R(G) contains an SCC with either both a positive play following one of its cycles and a negative play following one of its cycles if and only if R(G) contains an SCC with both a positive simple corner play following one of its cycles and a negative simple corner play following one of its cycles.
Proof. All that is left to prove is that, in an SCC of R(G), if all simple corner plays following a cycle have non-negative weight (resp. non-positive weight), then all corner plays following a cycle have non-negative weight (resp. non-positive weight).
By contradiction, we consider ρ, the shortest corner play following a cycle π, such that wt Σ (ρ) < 0 (resp. wt Σ (ρ) > 0). Corner play ρ cannot be simple, so it must contain a simple loop. That loop is a simple corner play following a cycle of R(G), so it must have non-negative weight (resp. nonpositive weight). This means that ρ without that loop satisfies wt Σ (ρ) < 0 (resp. wt Σ (ρ) > 0), and therefore was not the shortest corner play with the desired property.
We can test the existence of such simple corner plays in a SCC of R(G) in NPSPACE, by guessing them corner after corner and by keeping the cumulated weight in memory. The check that both plays are in the same SCC is a reachability check in a timed automaton, which can be done in PSPACE. We described a similar procedure in [16] where we were testing the existence of a non-negative corner play and a non-positive one in the same SCC instead of a negative one and a positive one. Now, we will assume in this second part that this test failed, so every SCC of R(G) either satisfies that all plays following a cycle have non-negative weight or satisfies that they all have non-positive weight. We will now explain how to check if R(G) contains a play with weight in (−1, 0) ∪ (0, 1) following one of its cycles. Let B = (|S| × (|X| + 1)) 2 . Lemma 14. R(G) contains a play with weight in (−1, 0) ∪ (0, 1) following one of its cycles if and only if R(G) contains a cycle π of length at most B such that there is a corner play following π with weight zero and another one with non-zero weight.
Proof. By Lemma 2, R(G) contains a play with weight in (−1, 0) ∪ (0, 1) following one of its cycles if and only if that cycle satisfies that there is a corner play following it with weight zero and another one with non-zero weight.
We only need to show that if there are no such cycles of length at most B, then there are no such cycles of any length. Therefore, we assume that no cycle of length less than B allows a play with weight in (−1, 0) ∪ (0, 1). By contradiction, let π be the shortest cycle such that there exist two corner plays ρ and ρ ′ following π, with wt Σ (ρ) = 0 and wt Σ (ρ ′ ) = 0. Then |π| > B. Let v i be the i-th corner of ρ, and v ′ i be the i-th corner of ρ ′ . There are at most (|S| × (|X| + 1)) 2 different pairs (v i , v ′ i ), which implies that there must be two indexes, j and k, such that (v j , v ′ j ) = (v k , v ′ k ) and j < k. The portion of ρ between indexes j and k follows a cycle, and have opposite weight to the play constructed by considering ρ and removing the loop between indexes j and k. Since the sum of their weight is 0 and they both follow cycles of R(G) in the same SCC, both of those plays have weight 0. The portion of π between indexes j and k is a cycle shorter than π, and it contains a corner play of weight 0, therefore all of its corner plays have weight 0, and the portion of ρ ′ between indexes j and k has weight 0 too. But then the cycle defined by taking π and removing the loop between indexes j and k contains a corner play of weight 0 (derived from ρ), and a corner play of weight non-zero (derived from ρ ′ ), and that contradicts π being the shortest cycle with that property.
Once again, we can check the existence of such a cycle of length bounded by B in NPSPACE by guessing it and its two relevant corner plays on-the-fly and storing the cumulated weight of each. This imply that deciding if a game G is almost divergent is decidable in coNPSPACE = NPSPACE = PSPACE (using the theorems of Immerman-Szelepcsényi [18,22] and Savitch [21]).
Let us now show the PSPACE-hardness (indeed the coPSPACE, which is identical) by a reduction from the reachability problem in a timed automaton. We consider a timed automaton with a starting state and a different target state without outgoing transitions. We construct from it a weighted timed game by distributing all states to Min, and equipping all transitions with weight 0, and all states with weight 0. We also add a loop with weight 1 on the initial state, one with weight −1 on the target state, and a transition from the target state to the initial state with weight 0, all three resetting all clocks and with no guard. Then, the weighted timed game is not almost-divergent if and only if the target can be reached from the initial state in the timed automaton.
Proof. We prove the property by induction on n. For n = 1, the property is immediate since t 1 π t1 is a 0-cycle. Consider then n such that the property holds for n, and prove it for n + 1. We will exhibit two corner plays following t 1 · · · t n+1 π tn+1 · · · π t1 of opposite weight and conclude with Lemma 3.
Let v 0 be a corner of last(t n+1 ). Since t n+1 π tn+1 is a 0-cycle, there exists w ∈ Z, a corner play ρ 0 following t n+1 ending in v 0 with weight w and a corner play ρ ′ 0 following π tn+1 beginning in v 0 with weight −w. We name v ′ 0 the corner of last(t n ) where ends ρ ′ 0 . We consider any corner play ρ 1 following t n+1 from corner v ′ 0 . The corner play ρ ′ 0 ρ 1 follows the path π tn+1 t n+1 that is also a 0-cycle by Lemma 4, therefore ρ 1 has weight w. We denote by v 1 the corner where ends ρ 1 . By iterating this construction, we obtain some corner plays ρ 0 , ρ 1 , ρ 2 , . . . following t n+1 and ρ ′ 0 , ρ ′ 1 , ρ ′ 2 , . . . following π tn+1 such that ρ ′ i goes from corner v i to v ′ i , and ρ i+1 from corner v ′ i to v i+1 , for all i 0. Moreover, all corner plays ρ i have weight w and all corner plays ρ ′ i have weight −w. Consider the first index l such that v l = v k for some k < l, which exists because the number of corners is finite.
We apply the induction to find a corner play following t 1 · · · t n π tn · · · π t1 , going through the corner v ′ k in the middle: more formally, there exists w α , a corner play ρ α following t 1 · · · t n ending in v ′ k with weight w α and a corner play ρ ′ α following π tn · · · π t1 beginning in v ′ k with weight −w α . We apply the induction a second time with corner v ′ l−1 : there exists w β , a corner play ρ β following t 1 · · · t n ending in v ′ l−1 with weight w β and a corner play ρ ′ β following π tn · · · π t1 beginning in v ′ follows the cycle t 1 · · · t n t n+1 π tn+1 π tn · · · π t1 . Since the game is almost-divergent, and those two corner plays are in the same SCC, both have weight 0. The second corner play of weight 0 ensures that the cycle t 1 · · · t n+1 π tn+1 · · · π t1 is a 0-cycle, by Lemma 3.

C Proofs of the semi-unfolding (Section 5)
Proof (Proof of Lemma 5). We detail the case of non-negative SCCs. Let us prove that a configurations has value −∞ if and only if it belongs to a state where player Min can ensure the LTL formula on transitions: , then from s, Max must be able to avoid S −∞ f , and eventually enforce either S R f reachability or staying in K forever. In both cases, Max can ensure a value above −∞.

C.1 Semi-unfolding construction
In order to prove Proposition 2, we will construct the desired semi-unfolding T (G) of a (nonnegative or non-positive SCC) G.
If (ℓ, r) is in K, we let K ℓ,r be the part of K accessible from (ℓ, r) (note that K ℓ,r is an SCC as K is a disjoint set of SCCs). We define the output transitions of K ℓ,r as being the output transitions of K accessible from (ℓ, r). If (ℓ, r) is not in K, the output transitions of (ℓ, r) are the transitions of R(G) starting in (ℓ, r).
Formally, we define a tree T whose nodes will either be labelled by region graph states (ℓ, r) ∈ S\S K or by kernels K ℓ,r , and whose edges will be labelled by output transitions in R(G). The root of the tree T is labelled with (ℓ 0 , r 0 ), or K ℓ0,r0 (if (ℓ 0 , r 0 ) belongs to the kernel), and the successors of a node of T are then recursively defined by its output transitions. When a state (ℓ, r) is reached by an output transition, the child is labelled by K ℓ,r if (ℓ, r) ∈ K, otherwise it is labelled by (ℓ, r). Edges in T are labelled by the transitions used to create them. Along every branch, we stop the construction when either a final state is reached (i.e. a state not inside the current SCC) or the branch contains 3|R(G)|w e max + 2 sup |wt T | + 2 nodes labelled by the same state ((ℓ, r) or K ℓ,r ). Since R(G) has a finite number of states, T is finite. Leaves of T with a location belonging to L T are called target leaves, others are called stopped leaves.
We now transform T into a WTG T (G), by replacing every node labelled by a state (ℓ, r) by a different copy (l, r) of (ℓ, r). Those states are said to inherit from (ℓ, r). Edges of T are replaced by the transitions labelling them, and have a similar notion of inheritance. Every non-leaf node labelled by a kernel K ℓ,r is replaced by a copy of the WTG K ℓ,r , output transitions being plugged in the expected way. We deal with stopped leaves labelled by a kernel K ℓ,r by replacing them with a single node copy of (ℓ, r), like we dealt with node labelled by a state (ℓ, r). State partition between players and weights are inherited from the copied states of R(G). The only initial state of T (G) is the state denoted by (l 0 , r 0 ) inherited from (ℓ 0 , r 0 ) in the root of T (either (ℓ 0 , r 0 ) or K ℓ0,r0 ). The final states of T (G) are the states derived from leaves of T . If R(G) is a non-negative (resp. non-positive) SCC, the output weight function wt T is inherited from R(G) on target leaves and set to +∞ (resp. −∞) on stopped leaves.

C.2 Semi-unfolding correctness
We will now prove that Proposition 2 holds on this T (G).

Lemma 16. All finite plays in R(G) have cumulated weight (ignoring output weights) at least −|R(G)|w e
max in the non-negative case, and at most |R(G)|w e max in the non-positive case. Moreover, values of the game are bounded by |R(G)|w e max + sup |wt T |. Proof. Suppose first that R(G) is a non-negative SCC. Consider a play ρ following a path π. π can be decomposed into π = π 1 π c 1 · · · π n π c n such that every π c i is a cycle, and π 1 . . . π n is a simple path in R(G) (thus Proof. Note that by construction, all finite paths in T (G) from the initial state to a stopped leaf can be decomposed as π ′ π 1 · · · π 3|R(G)|w e max +2 sup |wtT |+1 with all π i being cycles. Additionally, those cycles cannot be 0-cycles by Proposition 1, since they take at least one transition outside of K. Therefore the restriction of ρ to π 1 · · · π 3|R(G)|w e max +1 has weight at least 3|R(G)|w e max + 2 sup |wt T | + 1 (in the non-negative case) and at most −3|R(G)|w e max − 2 sup |wt T | − 1 (in the nonpositive case). The beginning of the play, following π ′ , has cumulated weight at least −|R(G)|w e max (in the non-negative case) and at most |R(G)|w e max (in the non-positive case), by Lemma 16.
Two plays ρ = ((ℓ 1 , r 1 ), ν 1 ) and T (G), respectively, are said to mimic each other if every (l i , r i ) is inherited from (ℓ i , r i ) and every transitiont i is inherited from the transition δ i . Combining Lemmas 17 and 16, we obtain Lemma 18. If R(G) is a non-negative (resp. non-positive) SCC, every play from the initial state and with cumulated weight less than |R(G)|w e max +2 sup |wt T |+1 (resp. greater than −|R(G)|w e max − 2 sup |wt T | − 1) can be mimicked in T (G) without reaching a stopped leaf. Conversely, every play in T (G) reaching a target leaf can be mimicked in R(G).
Proof. We prove only the non-negative case. Let ρ be a play of R(G) with cumulated weight less than |R(G)|w e max + 2 sup |wt T | + 1. Consider the branch of the unfolded game it follows. If ρ cannot be mimicked in T (G), then a prefix of ρ reaches the stopped leaf of that branch when mimicked in T (G). In this situation, ρ starts by a prefix of weight at least 2|R(G)|w e max + 2 sup |wt T | + 1 by Lemma 17 and then ends with a suffix play of weight at least −|R(G)|w e max by Lemma 16, and that contradicts the initial assumption. The non-positive case is proved exactly the same way, and the converse is true by construction.
Then, the plays of R(G) starting in an initial configuration that cannot be mimicked in T (G) are not useful for value computation, which is formalised by Proposition 3: Proof. By Lemma 1, we already know that Val G (ℓ 0 , ν 0 ) = Val R(G) ((ℓ 0 , r 0 ), ν 0 ). Recall that we only left finite values in R(G) (in the final weight functions, in particular), and more precisely |Val R(G) ((ℓ 0 , r 0 ), ν 0 )| |R(G)|w e max + sup |wt T | by Lemma 16. We first show that the value is also finite in T (G). Indeed, if Val T (G) ((l 0 , r 0 ), ν 0 ) = +∞, since we assumed all output weights of R(G) bounded, we are necessarily in the non-negative case, and Max is able to ensure stopped leaves reachability. ((l 0 , r 0 ), ν 0 ) = +∞, then there are no winning strategies in R(G) for Min ensuring weight less than |R(G)|w e max + sup |wt T | + 1 from (ℓ 0 , r 0 ). Thus, we can obtain the contradiction Val R(G) ((ℓ 0 , r 0 ), ν 0 ) > |R(G)|w e max + sup |wt T |. Proof (Proof of Claim 1). By contradiction, consider a strategy σ Min of Min ensuring weight A |R(G)|w e max + sup |wt T | + 1 in R(G). Then, for all σ Max , the cumulated weight of play R(G) (((l 0 , r 0 ), ν 0 ), σ Min , σ Max ) (reaching target configuration (ℓ, ν)) is at most A − wt T (ℓ, ν) |R(G)|w e max + 2 sup |wt T | + 1, and by Lemma 18 this play does not reach a stopped leaf when mimicked in T (G), which is absurd.

Claim 2.If Val T (G)
Then, strategies and plays of T (G) starting from (l 0 , r 0 ) can be mimicked in R(G), therefore Val R(G) ((ℓ 0 , r 0 ), ν 0 ) Val T (G) (s 0 , ν 0 ): If R(G) is non-negative, for all ε > 0 we can fix an ε-optimal strategy σ Min for Min in T (G). It is a winning strategy, so every play derived from σ Min in T (G) reaches a target leaf, and can be mimicked in R(G) by Lemma 18. Therefore, σ Min can be mimicked in R(G), where it is also winning, with the same weight. From this we deduce Val R(G) ((ℓ 0 , r 0 s 0 , ν 0 ). If R(G) is non-positive, the same reasoning applies by considering an ε-optimal strategy for Max in T (G).
This proof not only holds on an SCC, but also on full almost-divergent WTGs, by simply stacking the semi-unfoldings of each SCC on top of each others.
Note that the semi-unfolding procedure of an SCC depends on sup |wt T |, where wt T can be the value function of an SCCs under the current one. Assuming all configurations have finite value, we can extend the reasoning of Lemma 16 and bound all values in the full game by |R(G)|w e max + sup |wt T |, which let us bound uniformly the unfolding depth of each SCC and gives us a bound on the depth of the complete semi-unfolding tree: |R(G)|(5|R(G)|w e max + 2 sup |wt T | + 2) + 1

D.1 Proofs of the approximation of kernels
Proof (Proof of Lemma 6). Since ρ and ρ ′ follow the same locations ℓ of G, one reaches a target location if and only if the other does. In the case where they do not reach a target location, both weights are infinite, and thus equal. We now look at the case where both plays reach a target location, moreover in the same step. Consider the region path π of the run ρ: π can be decomposed into a simple path with maximal cycles in it. The number of such maximal cycles is bounded by |L × Reg(X, M )| and the remaining simple path has length at most |L × Reg(X, M )|. Since all cycles of a kernel are 0-cycles, the parts of ρ that follow the maximal cycles have weight exactly 0.
Consider the same decomposition for the play ρ ′ . Cycles of π do not necessarily map to cycles over locations of C N (G), since the 1/N -regions could be distinct. However, Lemma 2 shows that, for all those cycles of π, there exists a sequence of finite plays of G whose weight tends to the weight of ρ ′ . Since all those finite plays follow a cycle of the region game R(G) (with G being a kernel), they all have weight 0. Hence, the parts of ρ ′ that follow the maximal cycles of π have also weight exactly 0. Therefore, the difference |wt G (ρ) − wt CN (G) (ρ ′ )| is concentrated on the remaining simple path of π: on each transition of this path, the maximal weight difference is 1/N × w L max since 1/N is the largest difference possible in time delays between plays that stay 1/N -close (since they stay in the same 1/N -regions). Moreover, the difference between the output weight functions is bounded by Λ/N , since the output weight function wt T is Λ-Lipschitz-continuous and the output weight function of C N (G) is obtained as limit of wt T . Summing the two contributions, we obtain as upper bound the constant B/N . Lemma 7). Let us prove that both Val G (ℓ, ν)

Proof (Proof of
Val CN (G) ((ℓ, r, v), v) + α and Val CN (G) ((ℓ, r, v), v) Val G (ℓ, ν) + α, with α = B/N . By definition and determinacy of turn-based WTG, this is equivalent to proving these two inequalities: play(((ℓ, r, v), v), σ ′ Max , σ ′ Min ))| α. To show the first inequality, it suffices to show that for all σ ′ Min , there exists σ Min such that for all σ Max , there is σ ′ Max verifying (β). For the second, it suffices to show that for all σ ′ Max , there exists σ Max such that for all σ Min , there is σ ′ Min verifying (β). We will detail the proof for the first, the second being syntactically the same, with both players swapped.
We build σ Min , f , and g by induction on the length n of plays, over prefixes of plays of length n− 1, n and n, respectively. For n = 0 (plays of length 0 are those restricted to a single configuration), we let f (ℓ, ν) = ((ℓ, r, v), v) and g ((ℓ, r, v), v) = (ℓ, ν), leaving the other values arbitrary (since we will not use them).
We then fix a strategy σ Max of Max in the game G, which determines a unique play play((ℓ, ν), σ Max , σ Min ). We construct a strategy σ ′ Max of Max in the game C N (G) by building the unique play play (((ℓ, r, v), v), σ ′ Max , σ ′ Min ) we will be interested in, such that each of its prefixes is in relation, via f or g, to the associated prefix of play((ℓ, ν), σ Max , σ Min ). Thus, we only need to consider a prefix of play ρ ′ ∈ FPlays Max CN (G) that starts in ((ℓ, r, v), v) and is consistent with σ ′ Min , and σ ′ Max built so far. Consider the play ρ = g(ρ ′ ), starting in (ℓ, ν) and consistent with σ Min , and σ Max (by assumption). For the decision (d, δ) = σ Max (ρ) (letting ρ + be the extended prefix), the definition of f and g ensures that there exists a decision (d ′ , δ ′ ) after ρ ′ that results in an extended play ρ ′ + that is 1/N -close, via f or g, with ρ + . We thus can choose σ ′ Max (ρ ′ ) = (d ′ , δ ′ ). We finally have built two plays play((ℓ, ν), σ Max , σ Min ) and play((ℓ ′ , ν ′ ), σ ′ Max , σ ′ Min ) that are 1/Nclose, as needed, which concludes this proof. Lemma 8). By construction, the approximated value is piecewise linear with one piece per 1/N -region. To prove the Lipschitz constant, it is then sufficient to bound the difference between Val CN (G) ((ℓ, r, v), v) and Val CN (G) ((ℓ, r, v ′ ), v ′ ), for v and v ′ two corners of a 1/N -region r. We can pick any valuation ν in r and apply Lemma 7 twice, between ν and v, and between ν and v ′ . We obtain |Val CN (G) ((ℓ, r, v)

D.2 Computing the value of an acyclic WTG
Note that for a piecewise linear functions with finitely many pieces, being Λ-Lipschitz-continuous over regions is equivalent to being continuous over regions and having all partial derivatives bounded by Λ in absolute value.

Lemma 19.
If for all ℓ ∈ L, V ℓ is piecewise linear with finitely many pieces that have all their partial derivatives bounded by Λ in absolute value, then for all ℓ ∈ L, F (V ) ℓ is continuous over regions and piecewise linear with finitely many pieces that have all their partial derivatives bounded by max(Λ, |wt(ℓ)| + (n − 1)Λ) in absolute value.
Proof. We will show that for every region r, F (V ) restricted to r has those properties. Note that they are transmitted over finite min and max operations. The continuity over regions is easy to prove because it is stable by inf and sup. We now use the notations and definitions of [1] to bound the partial derivatives.There exists a partition cost function (P, F ) that represents V , with P an ndimensional nested tube partition and F a mapping from the leaf nodes of P to linear expressions over variables in X. Intuitively, P defines a finite arborescence of convex spaces, defined by linear inequalities, whose root is the whole region r and whose leaves partition r into cells. A crucial property of those cells ( [1,Theorem 4]) is that, for a given valuation ν, the delays t that need to be considered in the sup or inf operation of F (V ) (ℓ,ν) correspond to the intersection points of the diagonal half line containing the time successors of ν and borders of cells (if ν b is such a valuation, t = ν b − ν ∞ is the associated delay). In particular, there is a finite number of such borders, and the final F (V ) ℓ function can be written as a finite nesting of finite min and max operations over linear terms, each corresponding to a choice of delay and a transition to take. Formally, there are several cases to consider to define those terms, depending on delay and transition choices. For each available transition δ, those terms can either be: 1. If a delay 0 is taken and all clocks in Y ⊆ X are reset by δ, then If a delay t > 0 (leading to valuation ν b on border B) is taken and the clocks in Y are reset by δ, then wt Σ ((ℓ, ν) In the first case, the resulting partial derivatives are 0 for clocks in Y , and the same as the partial derivatives in V ℓ ′ for all other clocks, which allows us to conclude that they are bounded by Λ. We now consider the second case. We argue that the second case could be decomposed as a delay followed by a transition of the first case, meaning that we can assume Y = ∅ without loss of generality.
There are again two cases: the border B being inside a region or on the frontier of a region. If the border is not the frontier of a region, it is the intersection points of two affine pieces of V ℓ ′ whose equations (in the space R n+1 whose n first coordinates are the clocks (x 1 , . . . , x n ) and the last coordinate correspond to the value V ℓ ′ (x 1 , . . . , x n )) can be written y = n i=1 a i x i + b (before the border) and y = n i=1 a ′ i x i + b ′ (after the border). Therefore, valuations of the borders all fulfil the equation Consider that ℓ is a location of Min (the very same reasoning applies to the case of a location of Max). Since F computes an infimum, we know that the function mapping the delay t to the weight obtained from reaching ν +t is decreasing before the border and increasing after. These functions are locally affine which implies that their slopes verify: We deduce from these two inequalities that A 0. The case where A = 0 would correspond to the case where the border contains a diagonal line, which is forbidden, and A > 0. Consider now a valuation of coordinates ν = (x 1 , . . . , x n ) and another valuation of coordinates ν ′ = (x 1 , . . . , x k−1 , x k + λ, x k+1 , . . . , x n ). The delays t and t ′ needed to arrive to the border starting from these two valuations are such that ν + t and ν ′ + t ′ both verify (2). We can then It is now possible to compute the partial derivative of F (V ) ℓ in the k-th coordinate using We may compute it by using the equations of the affine pieces before or after the border. We thus obtain In the case where a k a ′ k , the first equation, with (3), allows us to obtain that the partial derivative is at most a k . We may then lower wt(ℓ) by − n i=1 a ′ i to obtain that the partial derivative is at least a ′ k . Since a k and a ′ k are bounded in absolute value by Λ, so is the partial derivative. We get the same result by reasoning on the second equation if a ′ k a k . We now come back to the case where the border is on the frontier of a region. Then, it is a segment of a line of equation x k = c for some k and c. V ℓ ′ contains at most three values for points of B: The limit coming from before the border, the value at the border, and the limit coming from after the border. The computation of F (V ) computes values obtained from all three and takes the min (or the max). Now, let y = n i=1 a i x i + b be the equation defining the linear piece of V ℓ ′ before the border (resp. at the border, after the border). Consider now a valuation of coordinates ν = (x 1 , . . . , x n ) and another valuation of coordinates ν ′ = (x 1 , . . . , x j−1 , x j + λ, x j+1 , . . . , x n ). The delays t and t ′ needed to arrive to the border starting from these two valuations are such that ν + t and ν ′ + t ′ both verify x k = c. We can then deduce that t ′ − t = 0 if j = k and t ′ − t = −λ if j = k. It is now possible to compute the partial derivative of F (V ) ℓ in the j-th coordinate using We may compute it by using the equations of the linear piece before the border (resp. at the border, after the border). Then, Then, the partial derivatives are bounded, in absolute value, by |wt(ℓ)| + (n − 1)Λ.
As a corollary, we can now obtain Lemma 9, or more precisely: Lemma 20. Consider an acyclic WTG G of depth i with all the output weights being Λ-Lipschitzcontinuous over each region (and piecewise linear, with finitely many pieces). Then, A weighted timed game G with two clocks x and y, and the portion of its region game R(G) accessible from configuration (ℓ0, (0, 0)). Locations of Min (resp. Max) are depicted as circles (resp. squares). The states of R(G) are labeled by their associated region, location and weight, and transitions are labeled by a representation of their guards and resets. Since each location ℓ of G leads to a unique states (ℓ, r) of R(G), we will refer to states by their associated location label.
Therefore, R(G) only contains non-negative SCCs and is almost-divergent. Since all states are in the attractor of Min towards L T , all cycles are non-negative and the output weight function is bounded (on all reachable regions), there are no configurations in R(G) with value +∞ or −∞.
We let the kernel K be the sub-game of R(G) defined by π 2 , and we construct a semi-unfolding T (G) of R(G) of equivalent value. Following Appendix C, we should unfold the game until every stopped branch contains a state seen at least 3|R(G)|w e max + 2 sup |wt T | + 2 = 3 * 3 * 4 + 2 * 1 = 38 times. We will unfold with bound 4 instead of 38 for readability (it is enough on this example). Thus the infinite branch (ℓ 1 ℓ 2 ) ω is stopped when ℓ 1 is reached for the fourth time, as depicted in Figure 6. Fig. 6. The kernel K (with input state ℓ1), and a semi-unfolding T (G) such that ValG(ℓ0, (0, 0)) = Val T (G) (ℓ0, (0, 0)). We denote ℓi, ℓ ′ i and ℓ ′′ i the locations in K, K ′ and K ′′ .
Let us now compute an approximation of Val T (G) . Let us first remove the states of value +∞: ℓ ′′′ 1 and ℓ ′′ 2 . Then, we start at the bottom and compute an (ε/3)-approximation of the value of ℓ ′′ 1 in the game defined by K ′′ ℓ1 and its output transition to ℓ ′′ t . Following Section 6, we should use N 3(4 + 1)/ε and compute values in the 1/N -corners game C N (K ′′ ℓ1 ) in order to obtain an (ε/3)-approximation of the value function. For ε = 15 we will use N = 1 (in this case the computation happens to be exact and would also hold with a small ε) We construct this corner game, and obtain the finite (untimed) weighted game in Figure 7.
Following Section 6 one last time, we should use N 3(5+3)/ε and compute values in the 1/Ncorners game C N (K ℓ1 ). This time, let us use N = 3 to showcase an example where the computed value is not exact. We can construct a finite (untimed) weighted game as in Figure 7, and obtain a value for each 1/3-corner of state ℓ ′ 1 . From these results, we define a piecewise-linear function by interpolation, as depicted in Figure 9. .

D.4 Complexity analysis
We will express complexities according to several parameters: |L|, |X|, greatest guard constant M , greatest location and transition weight constants w L max and w ∆ max . We also need to keep track of the output weight functions' characteristics. Recall that the output weight functions must be piecewise linear with finitely many pieces and Lipschitz-continuous over regions. We define three parameters, its Lipschitz constant Λ, its number of linear pieces J and a bound U (that we call additive bound) on its additive constant, such that if (x 1 , . . . , x |X| ) → |X| i=1 a i x i + b defines one of those linear pieces, then |b| U and ∀1 i |X|, |a i | Λ.
Note that |L|, |X| and J are all polynomial in the size of the input, but M , w L max , w ∆ max , Λ and U are exponential in the size of the input if constants are encoded in binary.
We start with simple estimates: Tree Let us recall the complexity of the value iteration algorithm, used to compute the exact value of an acyclic WTG: Input: An acyclic game of depth i. Algorithm schema: Computes F i (V 0 ) = Val i = Val. Output: A Λ ′ -Lipschitz-continuous function with J ′ pieces and additive bound U ′ that is the game's value.
-Λ ′ is of the form Λ Λ ′′ with Λ ′′ polynomial in w L max and |X| and exponential in i. -J ′ is of the form J |X| J ′′ with J ′′ polynomial in M and |L| and exponential in |X| and i.
-U ′ is of the form U + U ′′ with U ′′ polynomial in M , w L max , w ∆ max and i.