# Playing Stochastically in Weighted Timed Games to Emulate Memory

Benjamin Monmege, Julie Parreaux, Pierre-Alain Reynier

► To cite this version:

Benjamin Monmege, Julie Parreaux, Pierre-Alain Reynier. Playing Stochastically in Weighted Timed Games to Emulate Memory. Logical Methods in Computer Science, 2025, 21 (1), 10.46298/lmcs-21(1:19)2025 . hal-04973633

HAL Id: hal-04973633

https://hal.science/hal-04973633v1

Submitted on 3 Mar 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# PLAYING STOCHASTICALLY IN WEIGHTED TIMED GAMES TO EMULATE MEMORY

BENJAMIN MONMEGE ◦ª, JULIE PARREAUX ◦ᵇ, AND PIERRE-ALAIN REYNIER ◦ª

**ABSTRACT.** Weighted timed games are two-player zero-sum games played in a timed automaton equipped with integer weights. We consider optimal reachability objectives, in which one of the players, that we call Min, wants to reach a target location while minimising the cumulated weight. While knowing if Min has a strategy to guarantee a value lower than a given threshold is known to be undecidable (with two or more clocks), several conditions, one of them being divergence, have been given to recover decidability. In such weighted timed games (like in untimed weighted games in the presence of negative weights), Min may need finite memory to play (close to) optimally. This is thus tempting to try to emulate this finite memory with other strategic capabilities. In this work, we allow the players to use stochastic decisions, both in the choice of transitions and of timing delays. We give a definition of the expected value in weighted timed games. We then show that, in divergent weighted timed games as well as in (untimed) weighted games (that we call shortest-path games in the following), the stochastic value is indeed equal to the classical (deterministic) value, thus proving that Min can guarantee the same value while only using stochastic choices, and no memory.

## 1. INTRODUCTION

Game theory is now an established model in the computer-aided design of correct-by-construction programs. Two players, the controller and an environment, are fighting one against the other in a zero-sum game played on a graph of all possible configurations. A winning strategy for the controller results in a correct program, while the environment is a player modelling all uncontrollable events that the program must face. Many possible objectives have been studied in such two-player zero-sum games played on graphs: reachability, safety, repeated reachability, and even all possible ω-regular objectives [GTW02].

*Key words and phrases:* weighted timed games, algorithmic game theory, timed automata, stochastic strategies.

We thank the reviewers of the various versions of this article that helped us greatly improve the quality of the results and the writing. This work has been partly funded by the QuaSy project (ANR-23-CE48-0008), and the NCN grant 2019/35/B/ST6/02322.

<figure><img src="image_2.png" /></figure>

<footnote>ª Aix Marseille Univ, CNRS, LIS, Marseille, France
*e-mail address:* benjamin.monmege@univ-amu.fr, pierre-alain.reynier@univ-amu.fr</footnote>

<footnote>ᵇ University of Warsaw, Poland
*e-mail address:* j.parreaux@uw.edu.pl</footnote>
<figure><img src="image_3.png" /><figcaption>Figure 1: On the left, an SPG, where Min requires memory to play optimally. In the middle, the Markov Decision Process obtained when letting Min play at random, with a parametric probability $p \in (0, 1)$. On the right, the Markov Chain obtained when Max plays along a memoryless randomised strategy, with a parametric probability $q \in [0, 1]$.</figcaption></figure>

Apart from such qualitative objectives, more quantitative ones are useful in order to select a particular strategy among all the ones that are correct with respect to a qualitative objective. Some metrics of interest, mostly studied in the quantitative game theory literature, are mean-payoff, discounted-payoff, or total-payoff. All these objectives have in common that both players have strategies using no memory or randomness to win or play optimally [GZ05].

Combining quantitative and qualitative objectives, in order to select a good strategy among the valid ones for the selected metrics, often leads to the need of memory to play optimally. One of the simplest combinations showing this consists in the shortest-path games (SPGs) combining a reachability objective with a total-payoff quantitative objective (studied in [KBB+08, BGHM17] under the name of min-cost reachability games). Another case of interest is the combination of a parity qualitative objective (modelling every possible $\omega$-regular condition), with a mean-payoff objective (aiming for a controller of good quality in the average long-run), where controllers need memory, and even infinite memory, to play optimally [CHJ05].

It is often crucial to enable randomisation in the strategies. For instance, Nash equilibria are only ensured to exist in matrix games (like rock-paper-scissors) when players can play at random [Nas50]. In the context of games on graphs, a player may choose, depending on the current history, the probability distribution on the successors. In contrast, strategies that do not use randomisation are called *deterministic* (we sometimes say *pure*).

An example of SPG is depicted on the left of Figure 1. The objective of Min is to reach vertex $\C$, while minimising the cumulated weight. Let us consider the vertex $\ell_{\text{Min}}$ as initial. Player Min could reach directly $\C$, thus leading to a weight of 0. But Min can also choose to go to $\ell_{\text{Max}}$, in which case Max either jumps directly to $\C$ (leading to a beneficial payoff $-10$), or comes back to $\ell_{\text{Min}}$, but having already capitalised a total payoff $-1$. We can continue this way *ad libitum* until Min is satisfied (at least 10 times) and jumps to $\C$. This guarantees a value at most $-10$ for Min when starting in $\ell_{\text{Min}}$. Reciprocally, Max can guarantee a value at least $-10$ by directly jumping into $\C$ when playing for the first time. Thus, the optimal value is $-10$ when starting from $\ell_{\text{Min}}$ or $\ell_{\text{Max}}$. However, Min cannot achieve this optimal value by playing *without memory* (we sometimes say *positionally*), since it either results in a total-payoff 0 (directly going to the target) or Max has the opportunity to keep Min in the negative cycle for ever, thus never reaching the target. Therefore, Min needs memory to play optimally. He can do so by playing a *switching strategy*, looping in the negative cycle long enough so that no matter how he reaches the target finally, the value he gets is lower than
the optimal value. This strategy uses pseudo-polynomial memory with respect to the weights of the game graph. It can be described by two memoryless strategies *A* and *B*, following *A* for a given number of terms (to loop in negative cycles long enough) before switching to *B* (to ensure reaching 😊).

In this example, such a switching strategy can be mimicked using randomisation only (and no memory), *Min* deciding to go to $\ell_{Max}$ with high probability $p < 1$ and to go to the target vertex with the remaining low probability $1 - p > 0$ (we enforce this probability to be positive, in order to reach the target with probability 1, no matter how the opponent is playing). The resulting *Markov Decision Process (MDP)* is depicted in the middle of Figure 1. The shortest path problem in such MDPs has been thoroughly studied in [BT91], where it is proved that *Max* does not require memory to play optimally. Denoting by *q* the probability that *Max* jumps in its memoryless strategy, we obtain the *Markov chain (MC)* on the right of Figure 1. We can compute (see Example 7.7) the expected value in this MC, as well as the best strategy for both players: in the overall, the optimal value remains $-10$, even if *Min* no longer has an optimal strategy. He rather has an $\varepsilon$-optimal strategy, consisting in choosing $p = 1 - \varepsilon/10$ that ensures a value at most $-10 + \varepsilon$.

A first aim of this article is thus to study the trade-off between memory and randomisation in strategies of SPGs. The study is only interesting in the presence of both positive and negative weights, since both players have optimal memoryless deterministic strategies when the graph contains only non-negative weights [KBB+08]. The trade-off between memory and randomisation has already been investigated in many classes of games where memory is required to win or play optimally. This is for instance the case for qualitative games like Street or Müller games thoroughly studied (with and without randomness in the arena) in [CdAH04]. The study has been extended to timed games [CHP08] where the goal is to use as little information as possible about the precise values of real-time clocks. Memory or randomness is also crucial in multi-dimensional objectives [CRR14]: for instance, in mean-payoff parity games, if there exists a deterministic finite-memory winning strategy, then there exists a randomised memoryless almost-sure winning strategy. We show in this article that deterministic memory and memoryless randomisation provide the same power to *Min* in SPGs.

Another aim of this article is to extend this study to the case of weighted games on timed automata. *Timed automata* [AD94] extend finite-state automata with timing constraints, providing an automata-theoretic framework to model and verify real-time systems. While this has led to the development of mature verification tools, the design of programs verifying some real-time specifications remains a notoriously difficult problem. In this context, *timed games* have been explored, with an objective of reaching a target as quickly as possible: they are decidable [AM99], and *EXPTIME*-complete [JT07]. As in the untimed setting of SPGs, timed games have been extended with quantitative objectives, in the form of *weighted or (priced) timed games* (WTGs for short) [BCFL04, ABM04].

While solving the optimal reachability problem on weighted timed automata has been shown to be PSPACE-complete [BBBR07] (i.e. the same complexity as the non-weighted version), WTGs are known to be undecidable [BBR05]. Many restrictions have then been considered 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) [BCFL04]: 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, +\infty)$, for instance). This setting has been extended in the presence of negative weights in transitions and locations
[BMR17]: in the so-called *divergent WTGs*, each execution that follows a cycle of the region automaton has a weight in $(−∞, −1] ∪ [1, +∞)$. A triply-exponential-time algorithm allows one to compute the values and almost-optimal strategies, while deciding the divergence of a WTG is *PSPACE*-complete.

When studying optimal reachability objectives with both positive and negative weights, it is known that strategies of player Min require memory to play optimally (see [BGHM17] for the case of finite games). More precisely, the memory needed is pseudo-polynomial (i.e. polynomial if constants are encoded in unary). For WTGs, the memory needed even becomes exponential. An important challenge is thus to find ways to avoid using such complex strategies, e.g. by proposing alternative classes of strategies that are more easily amenable to implementation.

We thus use the same ideas as developed before for SPGs, introducing stochasticity in strategies. A first important challenge is to analyse how to play stochastically in WTGs. To our knowledge, this has not been studied before. Starting from a notion of stochastic behaviours in a timed automaton considered in [BBB$^{+}$14] (for the one-player setting), we propose a new class of stochastic strategies. Compared with [BBB$^{+}$14], our class is larger in the sense that we allow Dirac distributions for delays, which subsumes the setting of deterministic strategies. However, in order to ensure that strategies yield a well-defined probability distribution on sets of executions, we need measurability properties stronger than the one considered in [BBB$^{+}$14] (we actually provide an example showing that their hypothesis was not strong enough).

Then, we turn our attention towards the expected cumulated weight of the set of plays conforming to a pair of stochastic strategies. We first prove that under the previous measurability hypotheses, this expectation is well-defined when restricting to the set of plays following a finite sequence of transitions. In order to have the convergence of the global expectation, we identify another property of strategies of Min, which intuitively ensures that the set of target locations is reached quickly enough. This allows us to define a notion of stochastic value (resp. memoryless stochastic value) of the game, i.e. the best value Min can achieve using stochastic strategies (resp. memoryless stochastic strategies), when Max uses stochastic strategies (resp. memoryless stochastic strategies) too.

Our main contribution is to show that in divergent WTGs and in SPGs, the stochastic value and the (stochastic) memoryless value are determined (i.e. it does not matter which player chooses first their strategy), and the stochastic, memoryless and deterministic values are equal: when allowing players to play with memory, no players benefit from using also randomisation; moreover Min can emulate memory using randomisation, and vice versa.

**Outline.** We will recall the model of WTGs in Section 2. We present in Section 3 the notion of stochastic strategy and ground mathematically the associated definitions of expected weight and stochastic value. We adapt the notion of deterministic value to restrict deterministic strategies to be *smooth* (in order for them to be considered as particular stochastic strategies). We relate in Section 4 the new deterministic value and the stochastic value in all WTGs: as a technical tool, also used afterwards, we show that the player Max always has a deterministic best-response against any strategy of player Min in all WTGs. We then recall in Section 5 the notion of divergence in WTGs, and show new results on the form of almost-optimal (deterministic and smooth) strategies for both players. Section 6 then contains the proof of the possible trade-off between memory and randomisation in strategies in divergent WTGs. We then focus on the special case of SPGs (i.e. WTGs without clocks) in Section 7, where
<figure><img src="image_4.png" /><figcaption>Figure 2: On the left, a (one-clock) weighted timed game. On the right, the value function of location $\ell_2$, with respect to the value of clock $x$, is obtained as the minimum of two curves.</figcaption></figure>

we are also able to obtain the previous trade-off, as well as characterising the existence of an
optimal deterministic (or memoryless) strategy.

This article is an extended version of the two conference articles [MPR20, MPR21], showing respectively the results in untimed, and timed games. With respect to these works, we have tried to uniformise the notations and techniques, and obtained the results about the stochastic value and the determinacy results shown in this article.

## 2. WEIGHTED TIMED GAMES

We let $\mathcal{X}$ be a finite set of variables called clocks. A valuation is a mapping $\nu: \mathcal{X} \to \mathbb{R}_{\ge 0}$ to the set $\mathbb{R}_{\ge 0}$ of non-negative real numbers. For a valuation $\nu$, a delay $t \in \mathbb{R}_{\ge 0}$ and a subset $Y \subseteq \mathcal{X}$ of clocks, we define the valuation $\nu+t$ as $(\nu+t)(x) = \nu(x)+t$, for all $x \in \mathcal{X}$, and the valuation $\nu[Y := 0]$ as $(\nu[Y := 0])(x) = 0$ if $x \in Y$, and $(\nu[Y := 0])(x) = \nu(x)$ otherwise. A (non-diagonal) guard on clocks of $\mathcal{X}$ is a conjunction of atomic constraints of the form $x \bowtie c$, where $\bowtie \in \{\leq, <, =, >, \geq\}$ and $c \in \mathbb{N}$. A valuation $\nu$ satisfies an atomic constraint $x \bowtie c$ if $\nu(x) \bowtie c$. The satisfaction relation is extended to all guards $g$ naturally, and denoted by $\nu \models g$. We let **Guards**($\mathcal{X}$) denote the set of guards over $\mathcal{X}$. For all $a \in \mathbb{R}_{\ge 0}$, $\lfloor a \rfloor \in \mathbb{N}$ denotes the integral part of $a$, and **fract**($a) \in [0, 1)$ its fractional part, such that $a = \lfloor a \rfloor + \text{fract}(a)$.

**Definition 2.1.** A weighted timed game (WTG) is a tuple $\mathcal{G} = \langle L_{\text{Min}}, L_{\text{Max}}, L_T, \Delta, \text{wt} \rangle$ where $L_{\text{Min}}, L_{\text{Max}}, L_T$ are finite disjoint subsets of Min locations, Max locations, and target locations, respectively (we let $L = L_{\text{Min}} \uplus L_{\text{Max}} \uplus L_T$), $\Delta \subseteq L \times \text{Guards}(\mathcal{X}) \times 2^{\mathcal{X}} \times L$ is a finite set of transitions, **wt**: $\Delta \uplus L \to \mathbb{Z}$ is the weight function.

An example of WTGs is depicted on the left of Figure 2. Locations belonging to Min (resp. Max) are depicted by circles (resp. squares). The target location is $\ell_3$. Weights of transitions and locations are depicted in bold font.

The semantics of a WTG $\mathcal{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 $(\ell, \nu)$ with a location $\ell$ and a valuation $\nu$ 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 $\Delta \times \mathbb{R}_{\ge 0}$: a pair $(\delta, t)$ encodes the delay $t$ that a player wants to spend in the current location, before firing transition $\delta$. For every delay $t \in \mathbb{R}_{\ge 0}$, transition $\delta = (\ell, g, Y, \ell') \in \Delta$ and valuation $\nu$, there is an edge $\delta = (\ell, \nu) \xrightarrow{\delta,t} (\ell', \nu')$ if
$\nu + t \models g$ and $\nu' = (\nu + t)[Y := 0]$. Without loss of generality, we suppose the absence of deadlocks except on target locations, i.e. for each location $\ell \in L \setminus L_T$ and valuation $\nu$, there exists $(\ell, g, Y, \ell') \in \Delta$ and a delay $t \in \mathbb{R}_{\ge 0}$ such that $\nu + t \models g$, and no transitions start in $L_T$. This is generally not true on the examples we draw in this article (the example seen above) because we will bound the clocks later, but the automaton can always be completed to allow for a useless move reaching a sink vertex. A finite play is a finite sequence of consecutive edges $\rho = (\ell_0, \nu_0) \xrightarrow{\delta_0, t_0} (\ell_1, \nu_1) \xrightarrow{\delta_1, t_1} \cdots (\ell_k, \nu_k)$. We denote by $|\rho|$ the length $k$ of $\rho$. The concatenation of two finite plays $\rho_1$ and $\rho_2$, such that $\rho_1$ ends in the same configuration as $\rho_2$ starts, is denoted by $\rho_1\rho_2$. We denote by $I(\rho, \delta)$ the interval<fnref n="1" /> of delays $t$ such that the play $\rho$ can be extended with the edge $\xrightarrow{\delta, t}$. This extended play is denoted by $\rho[\delta, t]$. In particular, we sometimes denote a play $\rho$ by $(\ell_0, \nu_0)[\delta_0, t_0] \cdots [\delta_{k-1}, t_{k-1}]$, since intermediate locations and valuations are uniquely defined by the initial configuration and the sequence of transitions and delays. We let FPlays be the set of all finite plays, whereas FPlays<sub>Min</sub> (resp. FPlays<sub>Max</sub> and TPlays) denote the finite plays that end in a configuration of Min (resp. Max and $L_T$). We let TPlays<sub>ρ</sub> (resp. TPlays<sub>ρ</sub><sup>n</sup>) be the subset of TPlays that start in the last configuration of the finite play $\rho$ (resp. containing $n$ transitions without taking into account the size of $\rho$). A play is then a maximal sequence of consecutive edges (it is either infinite or it reaches $L_T$).

We call *path* a finite or infinite sequence $\pi$ of transitions of $\mathcal{G}$. As for finite plays, the concatenation of two finite paths $\pi_1$ and $\pi_2$, such that $\pi_1$ ends in the same location as $\pi_2$ starts, is denoted by $\pi_1\pi_2$. Each play $\rho$ of $\mathcal{G}$ is associated with a unique path $\pi$ (by projecting away everything but the transitions): we say that $\rho$ *follows* the path $\pi$. A *target path* is a finite path ending in the target set $L_T$. We denote by *TPaths* the set of target paths. We let *TPaths*<sub>ρ</sub> (resp. *TPaths*<sub>ρ</sub><sup>n</sup>) the subset of target paths that start from the last location of the finite play $\rho$ (resp. containing $n$ transitions without taking into account the size of $\rho$). A path is said to be *maximal* if it is infinite or if it is a target path.

A deterministic strategy for Min (resp. Max) is a mapping $\sigma: FPlays_{Min} \to \Delta \times \mathbb{R}_{\ge 0}$ (resp. $\tau: FPlays_{Max} \to \Delta \times \mathbb{R}_{\ge 0}$) such that for all finite plays $\rho \in FPlays_{Min}$ (resp. $\rho \in FPlays_{Max}$) ending in (non-target) configuration $(\ell, \nu)$, there exists an edge $(\ell, \nu) \xrightarrow{\sigma(\rho)} (\ell', \nu')$. We let $dStrat_{Min}$ and $dStrat_{Max}$ denote the set of deterministic strategies in $\mathcal{G}$ for players Min and Max, respectively. A play or finite play $\rho = (\ell_0, \nu_0)[\delta_0, t_0][\delta_1, t_1] \cdots$ conforms to a deterministic strategy $\sigma$ of Min (resp. Max) if for all $k$ such that $(\ell_k, \nu_k)$ belongs to Min (resp. Max), we have that $(\delta_k, t_k) = \sigma((\ell_0, \nu_0)[\delta_0, t_0] \cdots [\delta_{k-1}, \delta_{k-1}])$. For all deterministic strategies $\sigma$ and $\tau$ of players Min and Max, respectively, and for all configurations $(\ell_0, \nu_0)$, we let $Play((\ell_0, \nu_0), \sigma, \tau)$ be the outcome of $\sigma$ and $\tau$, defined as the unique maximal play conforming to $\sigma$ and $\tau$ and starting in $(\ell_0, \nu_0)$.

The objective of Min is to reach a target configuration, while minimising the cumulated weight up to the target. Hence, we associate with every finite play $\rho = (\ell_0, \nu_0) \xrightarrow{\delta_0, t_0} (\ell_1, \nu_1) \xrightarrow{\delta_1, t_1} \cdots (\ell_k, \nu_k)$ its cumulated weight, taking into account both discrete and continuous costs:

$$ \text{wt}\Sigma(\rho) = \sum_{i=0}^{k-1} [t_i \times \text{wt}(\ell_i) + \text{wt}(\delta_i)]. $$

<footnote n="1">¹It is an interval since guards are conjunctions of inequality constraints on clocks. More precisely, for each constraint given by an inequality over the valuation of one clock adequate delays are described by an (possibly empty) interval. Then, $I(\rho, \delta)$ is defined by the intersection of these intervals.</footnote>
Then, the weight of a maximal play $\rho$, denoted by $wt(\rho)$, is defined by $+\infty$ if $\rho$ is infinite, i.e. it does not reach $L_T$, and $wt_{\Sigma}(\rho)$ if it ends in $(\ell_T, \nu)$ with $\ell_T \in L_T$.

A deterministic strategy $\sigma \in d\text{Strat}_{\text{Min}}$ guarantees a certain value, against all possible strategies of the opponent: for all locations $\ell$ and valuations $\nu$, we let

$$d\text{Val}_{\ell, \nu}^{\sigma} = \sup_{\tau \in d\text{Strat}_{\text{Max}}} \text{wt}(\text{Play}((\ell, \nu), \sigma, \tau)).$$

Then, for all locations $\ell$ and valuations $\nu$, we define the deterministic value from $(\ell, \nu)$ under the point of view of Min by

$$\overline{d\text{Val}}_{\ell, \nu} = \inf_{\sigma \in d\text{Strat}_{\text{Min}}} \sup_{\tau \in d\text{Strat}_{\text{Max}}} \text{wt}(\text{Play}((\ell, \nu), \sigma, \tau)).$$

Similarly, we define the deterministic value from $(\ell, \nu)$ under the point of view of Max by

$$\underline{d\text{Val}}_{\ell, \nu} = \sup_{\tau \in d\text{Strat}_{\text{Max}}} \inf_{\sigma \in d\text{Strat}_{\text{Min}}} \text{wt}(\text{Play}((\ell, \nu), \sigma, \tau)).$$

Since WTGs are known to be determined [BGH$^{+}$15], i.e. $\underline{d\text{Val}}_{\ell, \nu} = \overline{d\text{Val}}_{\ell, \nu}$, we note by $d\text{Val}_{\ell, \nu}$ the deterministic value, for all configurations $(\ell, \nu)$.

In the example of Figure 2, location $\ell_1$ (resp. $\ell_5$) has deterministic value $+\infty$ (resp. $-\infty$). As a consequence, the value in $\ell_4$ is determined by the edge to $\ell_3$, and depicted in blue on the right of Figure 2. In location $\ell_2$, the deterministic value associated with the transition to $\ell_3$ is depicted in red, and the deterministic value in $\ell_2$ is obtained as the minimum of these two curves.

Finally, we say that a deterministic strategy $\sigma$ of Min is $\varepsilon$-optimal wrt the deterministic value if $d\text{Val}_{\ell, \nu}^{\sigma} \le d\text{Val}_{\ell, \nu} + \varepsilon$ for all $(\ell, \nu)$. It is said optimal if this holds for $\varepsilon = 0$.

Seminal works in weighted timed games [ABM04, BCFL04] have assumed that clocks are *bounded*. This is known to be without loss of generality for (weighted) timed automata [BFH$^{+}$01, Theorem 2]: it suffices to replace transitions with unbounded delays with self-loop transitions periodically resetting the clocks. We do not know if it is the case for the weighted timed games defined above. Indeed, the technique of [BFH$^{+}$01] cannot be directly applied. This would give too much power to player Max that would then be allowed to loop in a location where an unbounded delay could originally be taken before going to the target. In [BCFL04], the situation is simpler since the game is *concurrent*, and thus Min always has a chance to move outside of such a situation. Trying to detect and avoid such situations in our turn-based case seems difficult in the presence of negative weights, since the opportunities of Max crucially depend on the configurations of value $-\infty$ that Min could control afterwards: the problem of detecting such configurations is undecidable [Bus19, Prop. 9.2], which is an additional evidence to motivate the decision to focus only on bounded weighted timed games. We thus suppose from now on that all clocks are bounded by a constant $M \in \mathbb{N}$, i.e. every transition of the WTG is equipped with a guard $g$ such that $\nu \models g$ implies $\nu(x) < M$ for all clocks $x \in \mathcal{X}$.

We denote by $w_{\text{max}}^{L}$ (resp. $w_{\text{max}}^{\Delta}$, $w_{\text{max}}^{e}$) the maximal weight in absolute values of locations (resp. of transitions, edges) of $\mathcal{G}$, i.e. $w_{\text{max}}^{L} = \max_{\ell \in L} |\text{wt}(\ell)|$ (resp. $w_{\text{max}}^{\Delta} = \max_{\delta \in \Delta} |\text{wt}(\delta)|$, $w_{\text{max}}^{e} = Mw_{\text{max}}^{L} + w_{\text{max}}^{\Delta}$).

In the following, we rely on the crucial notion of regions, as introduced in the seminal work on timed automata [AD94]. Formally, with respect to the set $\mathcal{X}$ of clocks and the upper bound $M$ on the valuation of clocks, we denote by $\text{Reg}(\mathcal{X}, M)$ the set of regions bounded by $M$. The regions partition the set $[0, M)^{\mathcal{X}}$ of valuations. Each such region is characterised by a pair $(\iota, \beta)$ where $\iota: \mathcal{X} \to [0, M) \cap \mathbb{N}$ and $\beta$ is a partition of $\mathcal{X}$ into subsets $\beta_0 \uplus \beta_1 \uplus \cdots \uplus \beta_m$
(with $m \ge 0$), where $\beta_0$ can be empty but $\beta_i \ne \emptyset$ for $1 \le i \le m$. A valuation $\nu$ of $[0, M)^X$ belongs to the region characterised by $(\iota, \beta)$ if

* for all $x \in \mathcal{X}$, $\iota(x) = \lfloor \nu(x) \rfloor$;

* for all $x \in \beta_0$, $\text{fract}(\nu(x)) = 0$;

* for all $0 \le i \le m$, for all $x, y \in \beta_i$, $\text{fract}(\nu(x)) = \text{fract}(\nu(y))$;

* for all $0 \le i < j \le m$, for all $x \in \beta_i$ and all $y \in \beta_j$, $\text{fract}(\nu(x)) < \text{fract}(\nu(y))$.

The set of valuations contained in a region $r$ characterised by $(\iota, \beta)$ with $\beta = \beta_0 \uplus \beta_1 \uplus \cdots \uplus \beta_m$ can be described by the guard $g_0 \wedge g_1 \wedge \cdots \wedge g_m$ with

$$g_0 = \bigwedge_{x \in \beta_0} (x = \iota(x)), \quad g_1 = \bigwedge_{x, y \in \beta_1} (0 < x - \iota(x) = y - \iota(y) < 1)$$

and for $i \in \{2, \dots, m\}$,

$$g_i = \bigwedge_{x, y \in \beta_i} (z - \iota(z) < x - \iota(x) = y - \iota(y) < 1)$$

where $z$ is any clock of $\beta_{i-1}$.

If $r$ is a region, then the time successors of valuations in $r$ form a finite union of regions. Formally, a region $r'$ is said to be a time successor of the region $r$ if there exist $\nu \in r$, $\nu' \in r'$, and $t > 0$ such that $\nu' = \nu + t$. Moreover, the reset $r[Y := 0]$ of $Y \subseteq \mathcal{X}$, containing all valuations of $r$ where clocks of $Y$ have been reset, is also a region.

A game $\mathcal{G}$ can be populated with the region information, without loss of generality, as described formally in [BMR17]. Letting $\text{Reg}(\mathcal{X}, M)$ be the set of regions for the set of clocks $\mathcal{X}$ bounded by $M$, the region automaton, or region game, $\mathcal{R}(\mathcal{G})$ is thus the WTG with locations $S = L \times \text{Reg}(\mathcal{X}, M)$ and all transitions $((\ell, r), g'', Y, (\ell', r'))$ with $(\ell, g, Y, \ell') \in \Delta$ such that the model of the guard $g''$ (i.e. all valuations $\nu$ such that $\nu \models g''$) is a region $r''$, time successor of $r$ such that $r''$ satisfies the guard $g$, and $r'$ is the region obtained from $r''$ by resetting all clocks of $Y$. Distribution of locations to players, final locations, and weights are inherited from $\mathcal{G}$. We call region path a finite or infinite sequence of transitions in this automaton, and we again denote by $\pi$ such paths. A play $\rho$ in $\mathcal{G}$ is projected on a region path $\pi$, with a similar definition as the projection on paths: we again say that $\rho$ follows the region path $\pi$. It is important to notice that, even if $\pi$ is a cycle (i.e. starts and ends in the same location of the region game), there may exist plays following it in $\mathcal{G}$ that are not cycles, due to the fact that regions are sets of valuations.

As shown in previous works [BCFL04, BMR17], knowing whether $\text{dVal}_{\ell, \nu} = +\infty$ for a certain configuration $(\ell, \nu)$ is a purely qualitative problem that can be decided easily by using the region game: indeed, $\text{dVal}_{\ell, \nu} = +\infty$ if and only if Min has no strategies that guarantee that a target of $L_T$ is reached. This is thus a reachability objective, where weights are useless. Moreover, Max has a strategy that guarantees that no plays reach the target $L_T$ from any configuration $(\ell, \nu)$ such that $\text{dVal}_{\ell, \nu} = +\infty$. In this situation, considering stochastic choices is not interesting. **We thus rule out this case by supposing in the following that no configurations of $\mathcal{G}$ have a deterministic value $+\infty$: such configurations can be removed in the region game by strengthening the guards on transitions.**

### 3. PLAYING STOCHASTICALLY IN WTGS

Our first contribution consists in allowing both players to use stochastic choices in their strategies. From a game theory point of view, this seems natural: it is necessary to find Nash
equilibria in finite strategic games [Nas50]. From a controller synthesis point of view, we claim that using stochastic choices is natural too in WTGs, especially because player Min may require exponential memory to play optimally in WTGs. This is already the case even without clocks (such games are then sometimes called *shortest-path games*) as in Figure 1. We aim at proving that the memory required by Min could be traded for stochastic choices instead (and vice versa). Before doing so, we must introduce stochastic strategies in the context of WTGs, which has never been explored until now, as far as we are aware of. We will however strongly rely on a recent line of works aiming at studying *stochastic timed automata* [BBB+14, BBCM16, BBBC18, BBR+20], thus extending the results in the context of two-player games (instead of model-checking) and with weights, which indeed represents the main challenge in order to give a meaning to the expected payoff.

Naturally, deterministic strategies for Min are extended to more general stochastic strategies. We let $Dist(S)$ be the set of all probability distributions over a set $S$ (equipped with an underlying $\sigma$-algebra). Stochastic strategies are then mappings $\eta: \text{FPlays}_{\text{Min}} \to \text{Dist}(\Delta \times \mathbb{R}_{\ge 0})$ where each finite play is associated to a probability distribution over the set of pairs of transition and delay. Since $\Delta$ is a finite set, we choose to decouple the distribution on pairs of $\Delta \times \mathbb{R}_{\ge 0}$ by first selecting a transition and then delay, whereas authors of [BBB+14] consider independent choices, the one on transitions being described by some weights on transitions (depending on the current region). Thus, the strategy $\eta$ can be decoupled as first choosing a transition via $\eta_{\Delta}: \text{FPlays}_{\text{Min}} \to \text{Dist}(\Delta)$, and then, knowing the chosen transition, choosing a delay via $\eta_{\mathbb{R}+}: \text{FPlays}_{\text{Min}} \times \Delta \to \text{Dist}(\mathbb{R}_{\ge 0})$, the support of the distribution $\eta_{\mathbb{R}+}(\rho, \delta)$, denoted by $\text{supp}(\eta_{\mathbb{R}+}(\rho, \delta))$, being included in the interval $I(\rho, \delta)$ of valid delays. Similar definitions hold for Max whose stochastic strategies will be denoted by $\theta$.

Notice that deterministic strategies are a special case of stochastic strategies, where the distributions are chosen to be Dirac distributions. Another useful restriction over strategies is the non-use of memory: a strategy $\eta$ is *memoryless* if for all finite plays $\rho, \rho'$ ending in the same configuration, we have that $\eta(\rho) = \eta(\rho')$. A similar definition holds for Max. Finally, we let $\text{FPlays}_{\rho}^{\eta, \theta}$ be the set of plays reaching $L_T$ from $\rho$ (without containing $\rho$) conforming to $\eta$ and $\theta$.

**3.1. Probability measure on plays.** We fix a strategy $\eta$ and $\theta$ for each player, and an initial configuration $(\ell_0, \nu_0)$. Our goal is to define a probability measure on plays. To do so, and following the contribution of [BBB+14] for stochastic timed automata, the set of plays of a WTG $\mathcal{G}$ starting from $(\ell_0, \nu_0)$ and conforming to $\eta$ and $\theta$ that we denote by $\text{Plays}_{\ell_0, \nu_0}^{\eta, \theta}$ can be equipped with a structure of $\sigma$-algebra generated by cylinders, that are all subsets of plays that start with a finite prefix following the same finite path $\pi$ (remember that paths are sequences of transitions, with no information on the delayed time) with some Lebesgue-measurable constraints on the delays taken along $\pi$. The idea is thus to define a probability measure $\mathbb{P}_{\ell_0, \nu_0}^{\eta, \theta}$ on the algebra generated by such cylinders (i.e. the closure of cylinders by finite union and complement) which extends uniquely as a probability measure over the whole $\sigma$-algebra (i.e. the closure of cylinders by countable union and complement), by Carathéodory's extension theorem. First, we formally define the notion of cylinders, generalising the single configuration $(\ell_0, \nu_0)$ by a finite play $\rho_0$ to later take into account the possible use of memory in strategies of both players.
In the setting of [BBB$^{+}$14], the strategy in $\ell_1$ can be obtained by first choosing a delay similarly as ours, and then choosing transition $\delta_2$ with either probability 1/2 or 1 depending on whether transition $\delta_3$ is fireable after letting the chosen delay elapse: authors of [BBB$^{+}$14] would describe this by putting weight 1 on both transitions $\delta_2$ and $\delta_3$ in the stochastic timed automaton. The intricate formulas above for the transitions are thus simply a way to mimic their setting in ours. Let us try to compute the probability of the cylinder $\text{Cyl}_{\ell_0,0}(\delta_1\delta_2)$: its probability with respect to $\mathbb{P}_{\ell_0,0}^{\eta}$ is

$$ \mathbb{P}_{\ell_0,0}^{\eta}(\delta_1\delta_2) = \int_{I((\ell_0,0),\delta_1)} \eta_{\Delta}(\ell_0,0)(\delta_1) \times \mathbb{P}_{(\ell_0,0)[\delta_1,t_1]}^{\eta}(\delta_2) \, d\eta_{\mathbb{R}^+}((\ell_0,0),\delta_1)(t_1) $$

Moreover, since $\delta_1$ is the only transition from $\ell_0$, then $\eta_{\Delta}(\ell_0,0)(\delta_1) = 1$ and

$$ \mathbb{P}_{\ell_0,0}^{\eta}(\delta_1\delta_2) = \int_{0}^{1} \mathbb{P}_{(\ell_0,0)[\delta_1,t_1]}^{\eta}(\delta_2) \, dt_1 $$

that requires $h: t_1 \mapsto \mathbb{P}_{(\ell_0,0)[\delta_1,t_1]}^{\eta}(\delta_2)$ to be a measurable function on $[0,1]$ to be well-defined. For $t_1 \in [0,1) \cap A$,

$$ h(t_1) = \int_{I((\ell_1,t_1),\delta_1)} \eta_{\Delta}(\ell_1,t_1)(\delta_2) \times 1 \, d\eta_{\mathbb{R}^+}((\ell_1,t_1),\delta_2)(t_2) = \int_{0}^{2-t_1} f(t_1) \frac{dt_2}{2-t_1} = f(t_1). $$

Similarly, if $t_1 \in [0,1) \cap \bar{A}$, $h(t_1) = g(t_1)$. Functions $f$ and $g$ are measurable and never match over $[0,1)$. Thus, if $h$ is measurable, so would be $(h-g)/(f-t)$ that is equal to the characteristic function of $A$: this contradicts the non-measurability of $A$. And thus, it is not possible to define the probability $\mathbb{P}_{\ell_0,0}^{\eta}(\delta_1\delta_2)$.

From this example, we see the importance to moreover enforce that the distributions $\eta_{\Delta}(\rho_0)$ and $\eta_{\mathbb{R}^+}(\rho_0, \delta)$ are “measurable wrt the sequence of delays along the play $\rho_0$”. This is easy to define for the transition part. For delays, since we want deterministic strategies to be a subset of stochastic strategies, we must be able to choose delays by using Dirac distributions, and by extension discrete distributions (that are not absolutely continuous, as [BBB$^{+}$14] requires). We restrict ourselves to discrete distributions whose cumulative distribution functions (CDF) are a finite linear combination of translated Heaviside functions. Precisely, we let the Heaviside function $H$ denote the mapping from $\mathbb{R}$ to $[0,1]$ such that $H(t) = 0$ if $t < 0$ and $H(t) = 1$ otherwise. Recall that it is the CDF of the Dirac distribution choosing $t = 0$. This results in the following hypothesis:

**Hypothesis 3.3** (smooth strategies). A strategy $\xi$ is said to be smooth if for all finite plays $\rho_0 = (\ell_0, \nu_0)[\delta_0, t_0] \cdots [\delta_{k-1}, t_{k-1}]$ and transitions $\delta$,

(1) the mapping $(t_0, \dots, t_{k-1}) \mapsto \xi_{\Delta}(\rho_0)(\delta)$ is Lebesgue-measurable; and

(2) the probability distribution $\xi_{\mathbb{R}^+}(\rho_0, \delta)$ (of the random variable $t$) is described by a CDF of the form

$$ t \mapsto G(\rho_0, \delta)(t) + \sum_{i=0}^{n} \alpha_i(\rho_0, \delta)H(t - a_i(\rho_0, \delta)) $$

where $G(\rho_0, \delta)$ is an absolutely continuous function, $\alpha_i(\rho_0, \delta) \in [0,1]$ and $a_i(\rho_0, \delta) \in \mathbb{R}_{\ge 0}$, for all $i \in \{0, \dots, n\}$.

Moreover, the mappings

$$ (t_0, \dots, t_{k-1}, t) \mapsto G(\rho_0, \delta)(t), \quad (t_0, \dots, t_{k-1}) \mapsto \alpha_i(\rho_0, \delta), \quad \text{and} \quad (t_0, \dots, t_{k-1}) \mapsto a_i(\rho_0, \delta) $$
must be Lebesgue-measurable.

By default, all stochastic strategies considered in the rest of this article are smooth. We thus let $\mathbf{Strat}_{\text{Min}}$ and $\mathbf{Strat}_{\text{Max}}$ be the sets of smooth (stochastic) strategies of each player, as well as $\mathbf{mStrat}_{\text{Min}}$ and $\mathbf{mStrat}_{\text{Max}}$ be their respective subsets of memoryless strategies.

However, not all deterministic strategies are smooth (Example 3.2 can be modified to build non-smooth deterministic strategies), and we will thus recall the smoothness of them when we need it: we let $\mathbf{sdStrat}_{\text{Min}}$ and $\mathbf{sdStrat}_{\text{Max}}$ be the respective subsets of smooth deterministic strategies.

**Remark 3.4.** In divergent WTGs (that will be in studied in Section 5), we will show in Corollary 5.9 that there exists, for both players, $\varepsilon$-optimal smooth deterministic strategies with respect to the deterministic value.

Under the smooth hypothesis, we prove that the integral in (3.1) is always well-defined:

**Lemma 3.5.** For all finite plays $\rho_0 = (\ell_0, \nu_0)[\delta_0, t_0] \cdots [\delta_{k-1}, t_{k-1}]$, finite paths $\pi$ starting in $\ell_0$ (such that $|\pi| \ge k$), and Lebesgue-measurable sets $C$ of $\mathbb{R}_{\ge 0}^{|\pi|}$,

(1) the mapping $(t_0, \dots, t_{k-1}) \mapsto \mathbb{P}_{\rho_0}^{\eta, \theta}(\pi, C)$ is Lebesgue-measurable;

(2) $0 \le \mathbb{P}_{\rho_0}^{\eta, \theta}(\pi, C) \le 1$.

*Proof.* We reason by induction on the length of $\rho_0$. If $|\rho_0| = |\pi|$, then (by its definition), the mapping $(t_0, \dots, t_{k-1}) \mapsto \mathbb{P}_{\rho_0}^{\eta, \theta}(\pi, C)$ is equal to 1 if and only if $\pi = \delta_0\delta_1 \cdots \delta_{k-1}$ and $(t_0, \dots, t_{k-1}) \in C$ (otherwise it is equal to 0). In particular, in case $\pi = \delta_0\delta_1 \cdots \delta_{k-1}$, this mapping is equal to the characteristic function of $C$ (regarding to delays) which is Lebesgue-measurable by definition of a cylinder. Thus, $(t_0, \dots, t_{k-1}) \mapsto \mathbb{P}_{\rho_0}^{\eta, \theta}(\pi, C)$ is Lebesgue-measurable. Otherwise, we suppose that the property holds for all finite plays of length $k+1 \le |\pi|$ and we consider a finite play $\rho_0$ of length $k$. Letting $\xi$ be the strategy $\eta$ or $\theta$ according as $\rho_0 \in \mathbf{FPlays}_{\text{Min}}$, or $\rho_0 \in \mathbf{FPlays}_{\text{Max}}$, then by using the notations of (3.1) and Hypothesis 3.3.(2), we can decompose $\mathbb{P}_{\rho_0}^{\eta, \theta}(\pi, C)$ as $\xi_{\Delta}(\rho_0)(\delta)(A+B)$ where

$$A = \int_{I(\rho_0, \delta) \cap C^k} \mathbb{P}_{\rho_0[\delta, t]}^{\eta, \theta}(\pi, C) \times G(\rho_0, \delta)(t) \, dt \quad (3.2)$$

and

$$B = \sum_{i=0}^{\infty} \alpha_i(\rho_0, \delta) \times \mathbb{P}_{\rho_0[\delta, a_i(\rho_0, \delta)]}^{\eta, \theta}(\pi, C). \quad (3.3)$$

We start by studying (3.2). In particular, by induction hypothesis applied to the finite play $\rho_0[\delta, t]$, we know that the mapping $(t_0, \dots, t_{k-1}, t) \mapsto \mathbb{P}_{\rho_0[\delta, t]}^{\eta, \theta}(\pi, C)$ is Lebesgue-measurable. Therefore, the mapping $(t_0, \dots, t_{k-1}, t) \mapsto \mathbb{P}_{\rho_0[\delta, t]}^{\eta, \theta}(\pi, C) \times G(\rho_0, \delta)(t)$ is Lebesgue-measurable. Since it is also non-negative and upper-bounded by 1, and the interval $I(\rho_0, \delta)$ is bounded, the integral exists. Moreover, by Fubini Theorem<fnref n="2" />, the resulting integral is Lebesgue-measurable wrt the delays in $\rho$, i.e. (3.2) is Lebesgue-measurable wrt $(t_0, \dots, t_{k-1})$.

We focus on (3.3). By composition of the Lebesgue-measurable mappings $(t_0, \dots, t_{k-1}, t) \mapsto \mathbb{P}_{\rho_0[\delta, t]}^{\eta, \theta}(\pi, C)$ (by induction hypothesis applied on $\rho_0[\delta, t]$) and $(t_0, \dots, t_{k-1}) \mapsto a_i(\rho_0, \delta)$ (by

<footnote n="2">²The dependency on $\rho_0$ in the interval $I(\rho_0, \delta) \cap C^k$ of integration can be replaced by the full space $[0, M]$ since clocks are bounded by $M$, and the characteristic function of $t \in I(\rho_0, \delta) \cap C^k$ which is measurable wrt $(t_0, \dots, t_{k-1}, t)$.</footnote>
Hypothesis 3.3.(2)), the mapping $(t_0, \dots, t_{k-1}) \mapsto \mathbb{P}_{\rho_0[\delta, a_i(\rho, \delta)]}^{\eta, \theta}(\pi, \mathcal{C})$ is Lebesgue-measurable. Then, thanks to Hypothesis 3.3.(2), the countable sum of (3.3) absolutely converges. Thus, by countable sum of Lebesgue-measurable functions, (3.3) is Lebesgue-measurable wrt $(t_0, \dots, t_{k-1})$.

Finally, by using Hypothesis 3.3.(1), $(t_0, \dots, t_{k-1}) \mapsto \xi_{\Delta}(\rho_0)(\delta)$ is Lebesgue-measurable. Thus, $(t_0, \dots, t_{k-1}) \mapsto \mathbb{P}_{\rho_0}^{\eta, \theta}(\pi, \mathcal{C})$ is Lebesgue-measurable as a linear combination of Lebesgue-measurable functions. Moreover, by using the fact that $\xi_{\Delta}(\rho_0)$ is a probability distribution and the induction hypothesis bounding the probabilities between 0 and 1, we obtain, from the definition,

$$0 \le \mathbb{P}_{\rho_0}^{\eta, \theta}(\pi, \mathcal{C}) \le \int_{I(\rho, \delta)} d\xi_{\mathbb{R}^+}(\rho_0, \delta)(t) = 1$$

since $\xi_{\mathbb{R}^+}(\rho_0, \delta)$ is a probability measure.

Under the smoothness hypothesis, we want to prove that $\mathbb{P}_{\rho_0}^{\eta, \theta}$ can be extended as a probability distribution over the set $\text{Plays}_{\rho_0}^{\eta, \theta}$ of maximal plays starting in the last configuration of $\rho_0$, and conforming to $\eta$ and $\theta$, equipped with the $\sigma$-algebra $\Sigma_{\rho_0}$ generated by the cylinders $\text{Cyl}_{\rho_0}(\pi, \mathcal{C})$, following a similar proof as [BBB$^+$14, Proposition 3.2]. The complete proof is given in Appendix A.

**Proposition 3.6.** If $\eta$ and $\theta$ are smooth strategies, then, for all finite plays $\rho_0$, there exists a probability measure $\mathbb{P}_{\rho_0}^{\eta, \theta}$ over $(\text{Plays}_{\rho_0}^{\eta, \theta}, \Sigma_{\rho_0})$.

3.2. **Expected payoff of plays.** We now define the expected weight over the maximal plays starting from the last configuration of a finite play $\rho_0$. We denoted it by $\mathbb{E}_{\rho_0}^{\eta, \theta}$ instead of $\mathbb{E}_{\rho_0}^{\eta, \theta}(\text{wt})$, since we only consider the expectation of the weight wt:

$$\mathbb{E}_{\rho_0}^{\eta, \theta} = \int_{\rho} \text{wt}(\rho) \, d\mathbb{P}_{\rho_0}^{\eta, \theta}(\rho) \qquad (3.4)$$

This definition of the expectation makes sense by the following result:

**Lemma 3.7.** The mapping $\rho \mapsto \text{wt}(\rho)$ is a $\mathbb{P}_{\rho_0}^{\eta, \theta}$-measurable function.

*Proof.* By using the results of [BBBR07, Section 3.2], we know that given a finite path $\pi$ ending in a target location of $L_T$ and an open interval of possible weights $I_{\text{wt}}$ (that is a basic Lebesgue-measurable set of $\mathbb{R}$), the set of maximal plays following $\pi$ and with a weight in $I_{\text{wt}}$ is defined by constraints over the delays taken along the play. More precisely, this set of plays can be defined by a set of delays $(t_i)_{0 \le i \le |\pi|-1}$ that satisfy a linear program where the constraints are over partial sums $\sum_{i=j}^k t_i$. Thus, the set of maximal plays with a weight in $I_{\text{wt}}$ is a (countable) union of cylinders, defined by finite maximal paths reaching the target and constraints on delays described by a linear program (and thus a Lebesgue-measurable set of $\mathbb{R}_{\ge 0}^{\pi}$).

Even if the integral $\mathbb{E}_{\rho_0}^{\eta, \theta}$ always exists, it may be infinite. In particular, it is finite only if the probability to reach a target location is equal to 1, since otherwise there is a non-zero probability to not reach the target location, the weight of all such plays being $+\infty$, leading to an infinite expectation. We thus now require that $\mathbb{P}_{\rho_0}^{\eta, \theta}(\text{TPlays}_{\rho_0}) = 1$ (i.e. the probability to follow an infinite path is 0) that is possible since $\text{TPlays}_{\rho_0}$ is a $\mathbb{P}_{\rho_0}^{\eta, \theta}$-measurable set as a
<figure><img src="image_5.png" /><figcaption>Figure 4: A WTG where Min has a strategy reaching the target with probability 1 but with an expected weight equal to +∞.</figcaption></figure>

countable union of cylinders generated by all finite maximal paths ending in $L_T$. However, this is not a sufficient condition to ensure that the expected weight is finite.

**Example 3.8.** We consider the WTG of Figure 4, where only Min plays, and the memoryless strategy $\eta$ defined as follows. For all $t \le 1$, $\eta_\Delta(\ell, t)(\delta_0) = t$, $\eta_\Delta(\ell, t)(\delta_1) = 1 - t$, and, for all $i \ge 2$ and $\delta \in \{\delta_0, \delta_1\}$, $\eta_{\mathbb{R}^+}((\ell, 1 - \frac{1}{i}), \delta)$ is the Dirac distribution selecting the delay $t = \frac{1}{i} - \frac{1}{i+1}$. Notice that we can extend the delay distribution (continuously for instance) so that this strategy is smooth. For all $i \ge 1$, there is a unique play conforming to $\eta$ of length $i$ that reaches the target from configuration $(\ell, \frac{1}{2})$: it has a weight $i$ and a probability $\frac{1}{i+1} \prod_{j=2}^i (1 - \frac{1}{j}) = \frac{1}{i(i+1)}$. In particular, $\mathbb{P}_{\ell, \frac{1}{2}}^\eta(\text{TPlays}_{\ell, \frac{1}{2}}) = \sum_{i \ge 1} \frac{1}{i(i+1)} = 1$. Moreover, by the previous computation, we can deduce that

$$ \mathbb{E}_{\ell, \frac{1}{2}}^{\eta, \theta} = \int_{\rho} \mathrm{wt}(\rho) \, d\mathbb{P}_{\ell, \frac{1}{2}}^{\eta, \theta}(\rho) = \sum_{i} \int_{\rho} \mathrm{wt}(\rho) \chi_{\text{TPlays}_{\ell, \frac{1}{2}}^{i}}(\rho) \, d\mathbb{P}_{\ell, \frac{1}{2}}^{\eta, \theta}(\rho) $$

where $\text{TPlays}_{\ell, \frac{1}{2}}^i$ is a subset of $\text{TPlays}_{\ell, \frac{1}{2}}$ that contains all plays of length $i$. The expected weight would thus be $\mathbb{E}_{\ell, \frac{1}{2}}^{\eta, \theta} = \sum_{i \ge 1} i \times \frac{1}{i(i+1)} = \sum_{i \ge 1} \frac{1}{i+1}$, which is a diverging series. This example can easily be adapted to only consider continuous distributions on the delays (instead of Dirac ones).

Even smooth deterministic strategies of Min that guarantee that a target location is reached may not ensure that the expected payoff is finite (see Appendix B). We thus need a stronger hypothesis to ensure that the expectation is finite in all cases. We adopt here an asymmetrical point of view, relying only on a hypothesis on the strategy $\eta$ of Min. Our choice is grounded in our controller synthesis view, Min being the controller desiring to reach a target location with minimum expected weight, while Max is an uncontrollable environment.

On top of ensuring that the strategy of Min reaches the target set of locations with probability 1, we ask the strategies of Min to fulfil the following hypothesis, by separating two cases. For deterministic strategies, we simply ask that the expected payoff is finite, as we indeed want. For non-deterministic strategies, we ask a more demanding condition (and prove afterwards that it is sufficient), which will be helpful in our later proofs: not only Min must reach the target almost surely, but must do it quickly enough so that the expectation converges.

**Hypothesis 3.9 (proper strategies).** A strategy $\eta \in \text{Strat}_\text{Min}$ of Min is said to be proper if:

* either it is a smooth deterministic strategy and for all finite plays $\rho_0$ and strategies $\theta \in \text{Strat}_\text{Max}$, $\mathbb{P}_{\rho_0}^{\eta, \theta}(\text{TPlays}_{\rho_0}) = 1$ and $\mathbb{E}_{\rho_0}^{\eta, \theta}$ is finite;

* or there exist $m \in \mathbb{N}$ and $\alpha \in (0, 1)$ such that for all finite plays $\rho_0$ and strategies $\theta \in \text{Strat}_\text{Max}$,

$$ \mathbb{P}_{\rho_0}^{\eta, \theta} \left( \bigcup_{n \le m} \text{TPlays}_{\rho_0}^n \right) \ge \alpha. $$
We let $\text{Strat}_{\text{Min}}^{\text{P}}$ be the set of proper (smooth) strategies of Min. We let $\text{mStrat}_{\text{Min}}^{\text{P}}$ be the set of proper (smooth) memoryless strategies of Min. Finally, we let $\text{sdStrat}_{\text{Min}}^{\text{P}}$ be the set of proper smooth deterministic strategies of Min.

In the non-deterministic case, Hypothesis 3.9 formalises the idea that Min guarantees that the play reaches a target quickly enough since we can exponentially bound the probability of each cylinder according to its length. The complete proof of the following result is in Appendix C.

**Lemma 3.10.** Let $\eta \in \text{Strat}_{\text{Min}}^{\text{P}}$ be a strategy of Min satisfying the second condition of Hypothesis 3.9 for the bounds $\alpha$ and $m$. Let $\theta \in \text{Strat}_{\text{Max}}$ be a strategy of Max and $\rho_0 \in \text{FPlays}$ be a finite play following a finite path $\pi_0$. For all $n$, we have

$$ \sum_{\pi \in \text{TPaths}_{\rho_0}^n} \mathbb{E}_{\rho_0}^{\eta, \theta}(\pi_0 \pi) \le (1 - \alpha)^{\lfloor n/m \rfloor}. $$

In particular, this hypothesis is indeed a sufficient condition for the expected payoff to be finite:

**Proposition 3.11.** All proper strategies of Min are such that for all finite plays $\rho_0$ and strategies $\theta \in \text{Strat}_{\text{Max}}$, $\mathbb{E}_{\rho_0}^{\eta, \theta}$ is finite.

The proof is trivial, by definition, in the case of smooth deterministic strategies. For the other case, the main idea of the proof is to decompose the expectation $\mathbb{E}_{\rho_0}^{\eta, \theta}$ according to the size of maximal plays such that we can bound their weight by an affine function and their probabilities by the exponential function seen in Lemma 3.10. A natural choice is to decompose the expectation with cylinders (as for probability). Thus, we need to define the expected weight of a cylinder. We will not need to consider specific constraints on the delays and thus only consider cylinders of the form $\text{Cyl}_{\rho_0}(\pi)$ (with the set of constraints $\mathbb{R}_{\ge 0}^{[\pi]}$).

**Definition 3.12.** Let $\rho_0$ be a finite play and $\pi$ be a finite path. If the cylinder $\text{Cyl}_{\rho_0}(\pi)$ is non empty, the *expected weight* $\mathbb{E}_{\rho_0}^{\eta, \theta}(\pi)$ of plays that are in $\text{Cyl}_{\rho_0}(\pi)$ is defined by induction on the length of $\rho_0$. If $|\rho_0| = |\pi|$, we let $\mathbb{E}_{\rho_0}^{\eta, \theta}(\pi) = 0$, meaning that there are no more steps to take into account in the expected weight. Otherwise, letting $\delta = (\ell, g, Y, \ell')$ be the $(|\rho_0|+1)$-th transition of $\pi$, and $\xi$ be the strategy $\eta$ or $\theta$ depending if $\rho_0 \in \text{FPlays}_{\text{Min}}$ or $\rho_0 \in \text{FPlays}_{\text{Max}}$, we let

$$ \mathbb{E}_{\rho_0}^{\eta, \theta}(\pi) = \int_{I(\rho_0, \delta)} \xi_{\Delta}(\rho_0)(\delta) \left[ (t \text{wt}(\ell) + \text{wt}(\delta)) \mathbb{E}_{\rho_0[\delta, t]}^{\eta, \theta}(\pi) + \mathbb{E}_{\rho_0[\delta, t]}^{\eta, \theta}(\pi) \right] d\xi_{\mathbb{R}^+}(\rho_0, \delta)(t). $$

For the sake of completeness, if the cylinder $\text{Cyl}_{\rho_0}(\pi)$ is empty, we let $\mathbb{E}_{\rho_0}^{\eta, \theta}(\pi) = 0$.

By adapting the proof of Lemma 3.5, the smooth hypothesis is sufficient to show that all expectations $\mathbb{E}_{\rho_0}^{\eta, \theta}(\pi)$ are finite:

**Lemma 3.13.** For all finite plays $\rho_0 = (\ell_0, \nu_0)[\delta_0, t_0] \cdots [\delta_{k-1}, t_{k-1}]$, we let $\pi_0 = \delta_0 \delta_1 \cdots \delta_{k-1}$. For all finite paths $\pi$ starting in the last location of $\pi_0$, $\eta \in \text{Strat}_{\text{Min}}$ and $\theta \in \text{Strat}_{\text{Max}}$:

(1) $\mathbb{E}_{\rho_0}^{\eta, \theta}(\pi_0 \pi)$ exists;

(2) $|\mathbb{E}_{\rho_0}^{\eta, \theta}(\pi_0 \pi)| \le \mathbb{E}_{\rho_0}^{\eta, \theta}(\pi_0 \pi) |\pi| w_{\text{max}}^e$ (so $\mathbb{E}_{\rho_0}^{\eta, \theta}(\pi_0 \pi)$ is finite);

(3) the mapping $(t_0, \dots, t_{k-1}) \mapsto \mathbb{E}_{\rho_0}^{\eta, \theta}(\pi_0 \pi)$ is Lebesgue-measurable.
**Proof.** We start by proving (1) and (2) by induction on the length $k$ of $\rho_0$. Since $\rho_0$ follows $\pi_0$, the result is immediate when $k = |\pi_0\pi|$ (i.e. $|\pi| = 0$). Otherwise, we suppose that the property holds for all finite plays of length $k+1$ and we consider a finite play $\rho_0$ of length $k$. We let $\xi$ be the strategy $\eta$ or $\theta$ according if $\rho_0 \in \text{FPlays}_{\text{Min}}$ or $\rho_0 \in \text{FPlays}_{\text{Max}}$, $\delta = (\ell, g, Y, \ell')$ be a transition with $\ell$ the last location of $\rho_0$ and $\pi'$ be a finite path starting in $\ell'$. We also let $\pi = \delta\pi'$. By definition of the expectation, we have

$$ \mathbb{E}_{\rho_0}^{\eta, \theta}(\pi_0\pi) = \int_{I(\rho_0, \delta)} \xi_{\Delta}(\rho_0)(\delta) \left[ (t \text{wt}(\ell) + \text{wt}(\delta)) \mathbb{P}_{\rho_0[\delta, t]}^{\eta, \theta}(\pi_0\pi) + \mathbb{E}_{\rho_0[\delta, t]}^{\eta, \theta}(\pi_0\pi) \right] d\xi_{\mathbb{R}^+}(\rho_0, \delta)(t). $$

By induction hypothesis for all finite plays $\rho_0[\delta, t]$, we know that $\mathbb{E}_{\rho_0[\delta, t]}^{\eta, \theta}(\pi_0\pi)$ exists and is a measurable function of $t$. Therefore, the mapping

$$ t \mapsto (t \text{wt}(\ell) + \text{wt}(\delta)) \mathbb{P}_{\rho_0[\delta, t]}^{\eta, \theta}(\pi_0\pi) + \mathbb{E}_{\rho_0[\delta, t]}^{\eta, \theta}(\pi_0\pi) $$

is measurable (by Lemma 3.5). Thus, since $(t_0, \dots, t_{k-1}) \mapsto \xi_{\Delta}(\rho)(\delta)$ is Lebesgue-measurable (by Hypothesis 3.3.(1)), $\mathbb{E}_{\rho_0}^{\eta, \theta}(\pi_0\pi)$ exists, i.e. (1) holds. Moreover, by triangular inequality, we have

$$ |\mathbb{E}_{\rho_0}^{\eta, \theta}(\pi_0\pi)| \le \int_{I(\rho_0, \delta)} \xi_{\Delta}(\rho_0)(\delta) \left[ |t \text{wt}(\ell) + \text{wt}(\delta)| \mathbb{P}_{\rho_0[\delta, t]}^{\eta, \theta}(\pi_0\pi) + |\mathbb{E}_{\rho_0[\delta, t]}^{\eta, \theta}(\pi_0\pi)| \right] d\xi_{\mathbb{R}^+}(\rho_0, \delta)(t). $$

By definition of $w_{\max}^e$ and induction hypothesis applied to $\rho_0[\delta, t]$,

$$ |t \text{wt}(\ell) + \text{wt}(\delta)| \le w_{\max}^e \quad \text{and} \quad |\mathbb{E}_{\rho_0[\delta, t]}^{\eta, \theta}(\pi_0\pi)| \le \mathbb{P}_{\rho_0[\delta, t]}^{\eta, \theta}(\pi_0\pi) |\pi'| w_{\max}^e. $$

By properties of the integral, we deduce that

$$ \begin{aligned} |\mathbb{E}_{\rho_0}^{\eta, \theta}(\pi_0\pi)| & \le \underbrace{(|\pi'| + 1) w_{\max}^e}_{=|\pi|} \underbrace{\int_{I(\rho_0, \delta)} \xi_{\Delta}(\rho_0)(\delta) \mathbb{P}_{\rho_0[\delta, t]}^{\eta, \theta}(\pi_0\pi) d\xi_{\mathbb{R}^+}(\rho_0, \delta)(t)}_{=\mathbb{P}_{\rho_0}^{\eta, \theta}(\pi_0\pi)} \\ & = \mathbb{P}_{\rho_0}^{\eta, \theta}(\pi_0\pi) \end{aligned} $$

and (2) holds.

To conclude the proof, we remark that by (2) and Fubini theorem, $\mathbb{E}_{\rho_0}^{\eta, \theta}(\pi_0\pi)$ is Lebesgue-measurable wrt the delays in $\rho_0$, i.e. $(t_0, \dots, t_{k-1}) \mapsto \mathbb{E}_{\rho_0}^{\eta, \theta}(\pi_0\pi)$ is Lebesgue-measurable. In particular, (3) holds. $\square$

Now, we give the link between the expected weight and the expected weight restricted to a cylinder. In particular, we prove that the expected weight can be decomposed over cylinders.

**Lemma 3.14.** Let $\eta \in \text{Strat}_{\text{Min}}$, $\theta \in \text{Strat}_{\text{Max}}$, and $\rho_0$ be a finite play following the path $\pi_0$, then

$$ \mathbb{E}_{\rho_0}^{\eta, \theta} = \sum_{\pi \in \text{TPaths}_{\rho_0}} \mathbb{E}_{\rho_0}^{\eta, \theta}(\pi_0\pi). $$

**Proof.** By property of the integral, we can split the integral into cylinders and obtain that<fnref n="3" />

$$ \mathbb{E}_{\rho_0}^{\eta, \theta} = \sum_{\pi \in \text{TPaths}_{\rho_0}} \underbrace{\int_{\rho} \text{wt}(\rho) \chi_{\text{Cyl}_{\rho_0}(\pi_0\pi)}(\rho) d\mathbb{P}_{\rho_0}^{\eta, \theta}(\rho)}_{=A} $$

<footnote n="3">³The definition of $A$ could correspond to that of $\mathbb{E}_{\rho_0}^{\eta, \theta}(\pi)$. However, in the following, we need the inductive formula given by Definition 3.12.</footnote>
To conclude the proof, we prove by induction on the length of $\rho_0$ that $A = \mathbb{E}_{\rho_0}^{\eta,\theta}(\pi_0\pi)$. If $|\rho_0| = |\pi_0\pi|$, since $\pi \in \text{TPaths}_{\rho_0}$, then $wt(\rho) = 0$ for all $\rho \in \text{Cyl}_{\rho_0}(\pi_0\pi)$. Thus, the property holds in this case. Otherwise, we suppose that the property holds for all finite plays of length $k+1$ and we consider a finite play $\rho_0$ of length $k$, $\delta = (\ell, g, Y, \ell') \in \Delta$ the first transition of $\pi$, and we let $\xi$ be a strategy $\eta$ or $\theta$ according if $\rho_0$ ends in a configuration of Min or Max. In particular, we obtain that $A$ is equal to

$$ \int_{I(\rho_0, \delta)} \xi_{\Delta}(\rho_0)(\delta) \left( \int_{\rho} (t \, wt(\ell) + wt(\delta) + wt(\rho)) \chi_{\text{Cyl}_{\rho_0[\delta,t]}(\pi_0\pi)}(\rho) \, d\mathbb{P}_{\rho_0[\delta,t]}^{\eta,\theta}(\rho) \right) d\xi_{\mathbb{R}^+}(\rho_0, \delta)(t). $$

In particular, by linearity of the integral, $A$ can be rewritten as

$$ \begin{aligned} & \int_{I(\rho_0, \delta)} \xi_{\Delta}(\rho_0)(\delta) \left[ (t \, wt(\ell) + wt(\delta)) \underbrace{\int_{\rho} \chi_{\text{Cyl}_{\rho_0[\delta,t]}(\pi_0\pi)}(\rho) \, d\mathbb{P}_{\rho_0[\delta,t]}^{\eta,\theta}(\rho) +}_{= \mathbb{P}_{\rho_0[\delta,t]}^{\eta,\theta}(\pi_0\pi)} \right. \\ & \qquad \left. \qquad \qquad \int_{\rho} wt(\rho) \chi_{\text{Cyl}_{\rho_0[\delta,t]}(\pi_0\pi)}(\rho) \, d\mathbb{P}_{\rho_0[\delta,t]}^{\eta,\theta}(\rho) \right] d\eta_{\mathbb{R}^+}(\rho_0, \delta)(t). \end{aligned} $$

By hypothesis of induction applying on $\rho_0[\delta, t]$, we have

$$ \int_{\rho} wt(\rho) \chi_{\text{Cyl}_{\rho_0[\delta,t]}(\pi_0\pi)}(\rho) \, d\mathbb{P}_{\rho_0[\delta,t]}^{\eta,\theta}(\rho) = \mathbb{E}_{\rho_0[\delta,t]}^{\eta,\theta}(\pi_0\pi) $$

so that $A$ can be rewritten as

$$ A = \int_{I(\rho_0, \delta)} \xi_{\Delta}(\rho_0)(\delta) \left[ (t \, wt(\ell) + wt(\delta)) \mathbb{P}_{\rho_0[\delta,t]}^{\eta,\theta}(\pi_0\pi) + \mathbb{E}_{\rho_0[\delta,t]}^{\eta,\theta}(\pi_0\pi) \right] d\eta_{\mathbb{R}^+}(\rho_0, \delta)(t) $$

that is the definition of $\mathbb{E}_{\rho_0}^{\eta,\theta}(\pi_0\pi)$.

<figure><img src="image_6.png" /></figure>

Finally, we can conclude the proof of Proposition 3.11.

*Proof of Proposition 3.11.* Let $\eta \in \text{Strat}_{\text{Min}}$ be a strategy satisfying the second condition of Hypothesis 3.9 with the bounds $\alpha$ and $m$. Let $\theta \in \text{Strat}_{\text{Max}}$, and $\rho_0 \in \text{FPlays}$ following a path $\pi_0$.

We first show that $\mathbb{P}_{\rho_0}^{\eta,\theta}(\text{TPlays}_{\rho_0}) = 1$. The probability not to reach the target can be obtained as the limit

$$ \lim_{n \to \infty} \sum_{\pi \in \text{TPaths}_{\rho_0}^n} \mathbb{P}_{\rho_0}^{\eta,\theta}(\pi_0\pi) $$

By Lemma 3.10, this limit is 0, so that the probability to reach the target is indeed 1.

We then show that the infinite sum $\mathbb{E}_{\rho_0}^{\eta,\theta} = \sum_{\pi \in \text{TPaths}_{\rho_0}} \mathbb{E}_{\rho_0}^{\eta,\theta}(\pi_0\pi)$ (given by Lemma 3.14) converges. Notice that this sum can be decomposed as

$$ \mathbb{E}_{\rho_0}^{\eta,\theta} = \sum_{n=0}^{\infty} \sum_{\pi \in \text{TPaths}_{\rho_0}^n} \mathbb{E}_{\rho_0}^{\eta,\theta}(\pi_0\pi) \quad (3.5) $$

Since $\text{TPaths}_{\rho_0}^n$ is a finite set, only the first sum must be shown to be converging. We prove that it is absolutely converging by bounding $\sum_{\pi \in \text{TPaths}_{\rho_0}^n} |\mathbb{E}_{\rho_0}^{\eta,\theta}(\pi_0\pi)|$ with respect to $n$. By Lemmas 3.13.(2) and 3.10, it is bounded by $n(1-\alpha)^{\lfloor n/m \rfloor} w_{\text{max}}^e$, which is the general term of a convergent series since $0 < \alpha < 1$. □

<figure><img src="image_7.png" /></figure>
Now that we have associated an expected payoff with each convenient pair of strategies, we are able to mimic the classical definitions of *values* to stochastic strategies. Let $\ell$ be a location and $\nu$ be a valuation. For all $\eta \in \text{Strat}_{\text{Min}}^{\text{P}}$ and $\theta \in \text{Strat}_{\text{Max}}$, we let

$$ \text{Val}_{\ell, \nu}^{\eta} = \sup_{\theta \in \text{Strat}_{\text{Max}}} \mathbb{E}_{\ell, \nu}^{\eta, \theta} \quad \text{and} \quad \text{Val}_{\ell, \nu}^{\theta} = \inf_{\eta \in \text{Strat}_{\text{Min}}^{\text{P}}} \mathbb{E}_{\ell, \nu}^{\eta, \theta}. $$

This definition can be generalised by replacing configurations $(\ell, \nu)$ by finite plays $\rho_0$: we let $\text{Val}_{\rho_0}^{\eta} = \sup_{\theta \in \text{Strat}_{\text{Max}}} \mathbb{E}_{\rho_0}^{\eta, \theta}$ and $\text{Val}_{\rho_0}^{\theta} = \sup_{\eta \in \text{Strat}_{\text{Min}}^{\text{P}}} \mathbb{E}_{\rho_0}^{\eta, \theta}$ be the generalised versions. Then, we let $\overline{\text{Val}}_{\ell, \nu}$ and $\underline{\text{Val}}_{\ell, \nu}$ be the upper- and lower-values of $\mathcal{G}$ in $(\ell, \nu)$, defined as the best expected payoff Min and Max can hope for, respectively:

$$ \overline{\text{Val}}_{\ell, \nu} = \inf_{\eta \in \text{Strat}_{\text{Min}}^{\text{P}}} \text{Val}_{\ell, \nu}^{\eta} \quad \text{and} \quad \underline{\text{Val}}_{\ell, \nu} = \sup_{\theta \in \text{Strat}_{\text{Max}}} \text{Val}_{\ell, \nu}^{\theta}. $$

We also define the *memoryless values* $\text{mVal}_{\ell, \nu}^{\eta}$, $\text{mVal}_{\ell, \nu}^{\theta}$, $\overline{\text{mVal}}_{\ell, \nu}$, and $\underline{\text{mVal}}_{\ell, \nu}$, where all strategies are moreover taken memoryless. We finally define the *smooth deterministic values* $\text{sdVal}_{\ell, \nu}^{\eta}$, $\text{sdVal}_{\ell, \nu}^{\theta}$, $\overline{\text{sdVal}}_{\ell, \nu}$, and $\underline{\text{sdVal}}_{\ell, \nu}$, where all strategies are moreover taken (smooth) deterministic. As usual, for all configurations $(\ell, \nu)$, we always have

$$ \underline{\text{Val}}_{\ell, \nu} \le \overline{\text{Val}}_{\ell, \nu}, \quad \underline{\text{mVal}}_{\ell, \nu} \le \overline{\text{mVal}}_{\ell, \nu} \quad \text{and} \quad \underline{\text{sdVal}}_{\ell, \nu} \le \overline{\text{sdVal}}_{\ell, \nu}. $$

We have introduced the (stochastic) values to generalize the deterministic one. However, to ensure the existence of mathematical objects like the measure of probabilities or the expectation (against all strategies for Max), we need to constraint deterministic strategies and defined new deterministic values. In particular, we do not have tools to prove that smooth deterministic values are determined, and are equal to the deterministic value. An idea to prove it will be proving the existence of an $\varepsilon$-optimal proper smooth deterministic for the deterministic value, intuitively it consists on proving some smooth properties on the deterministic value function as well as the capability of Min to ensure the deterministic value by enough quickly going to a target location. Moreover, unlike in the case of the deterministic value, we do not know that WTGs are determined under smooth deterministic strategies.

Our main contribution, presented in details in Sections 6 and 7, is to compare the memoryless (stochastic) values, the (smooth) deterministic values and the stochastic values, showing their equality for two fragments of WTGs.

**3.3. Discrete strategies.** Between deterministic and stochastic strategies, we define a new class of strategies that we call *discrete strategies*. Intuitively, discrete strategies generalise deterministic strategies by only allowing discrete probabilities for both transitions and delays. We will later use such particular strategies and thus study them here.

**Definition 3.15.** A smooth strategy $\xi$ is *discrete* if for all $\rho \in \text{FPlays}$ and $\delta \in \Delta$, $\xi_{\mathbb{R}^+}(\rho, \delta)$ is a piecewise-constant function, i.e. there exist $\alpha_0, \dots, \alpha_n \in (0, 1]$, and $a_0, \dots, a_n \in \mathbb{R}_{\ge 0}$ such that, for all $t \in I(\rho, \delta)$,

$$ \xi_{\mathbb{R}^+}(\rho, \delta)(t) = \sum_{i=0}^{n} \alpha_i(\rho, \delta)H(t - a_i(\rho, \delta)) $$

Under a discrete strategy, the current player chooses a delay on a finite set of possible choices (i.e. pairs of transitions and delays). In a certain way, discrete strategies discretize the time in WTG. However, even if a discrete strategy for Min only uses Dirac distributions for delays, and verifies that the probability to reach the target (against all strategies of
Max) is 1, the expectation may not exist. Thus, to ensure the existence of the expectation, strategies of Min must moreover be proper (i.e. satisfy Hypothesis 3.9).

We consider $\eta \in \text{Strat}_{\text{Min}}^{\mathbb{P}}$ and $\theta \in \text{Strat}_{\text{Max}}$ two discrete strategies (with $\eta$ being moreover proper), and we will rewrite the expectation they induce. Intuitively, since $\eta$ and $\theta$ only use discrete distributions for transitions and delays, a single play reaching a target and conforming to both strategies forms a $\mathbb{P}_{\rho_0}^{\eta, \theta}$-measurable set. Moreover, when we consider a finite path conforming to both discrete strategies, the number of finite plays following it is countable. Thus, we prove that $\mathbb{P}_{\rho_0}^{\eta, \theta}$ is a discrete measure and we obtain a simpler formula for the expectation.

**Lemma 3.16.** Let $\eta \in \text{Strat}_{\text{Min}}^{\mathbb{P}}$ and $\theta \in \text{Strat}_{\text{Max}}$ be two discrete strategies. For all finite plays $\rho_0$, we have

$$ \mathbb{E}_{\rho_0}^{\eta, \theta} = \sum_{\rho \in \text{TPlays}_{\rho_0}^{\eta, \theta}} \text{wt}(\rho) \times \mathbb{P}_{\rho_0}^{\eta, \theta}(\rho) $$

where $\text{TPlays}_{\rho_0}^{\eta, \theta}$ is the $\mathbb{P}_{\rho_0}^{\eta, \theta}$-measurable set of plays starting in the last configuration of $\rho_0$, conforming to $\eta$ and $\theta$ and ending in the target.

*Proof.* Since $\eta$ is proper, the probability measure of the set of plays that do not reach the target is 0. By definition of the expectation, we thus have

$$ \mathbb{E}_{\rho_0}^{\eta, \theta} = \int_{\rho} \text{wt}(\rho) \, d\mathbb{P}_{\rho_0}^{\eta, \theta}(\rho) = \int_{\rho} \text{wt}(\rho) \chi_{\text{TPlays}_{\rho_0}^{\eta, \theta}}(\rho) \, d\mathbb{P}_{\rho_0}^{\eta, \theta}(\rho) $$

We conclude by showing that $\text{TPlays}_{\rho_0}^{\eta, \theta}$ is countable. To do so, notice that the number of finite maximal paths from the last location of $\rho_0$ is countable (as we restrict ourselves to plays that reach the target). Moreover, since the distributions on delays have a finite support, for each finite path, the number of possible delays consistent with strategies is finite. Thus, along a finite path, at each step, the current player can extend the play with a finite number of choices. In total, $\text{TPlays}_{\rho_0}^{\eta, \theta}$ only contains a countable number of plays. $\square$

## 4. PROBABILITIES ARE USELESS IN THE PRESENCE OF MEMORY

Our first result is to show that the combination of stochastic choices and memory in strategies does not bring more power than just the memory, i.e. that the stochastic values are bounded by the smooth deterministic ones.

**Theorem 4.1.** In all WTGs, for all locations $\ell$ and valuations $\nu$,

$$ \underline{\text{sdVal}}_{\ell, \nu} \leq \underline{\text{Val}}_{\ell, \nu} \leq \overline{\text{Val}}_{\ell, \nu} \leq \overline{\text{sdVal}}_{\ell, \nu}. $$

The rest of this section is devoted to the proof of this result. The main ingredient for the proof is the fact that when Min plays with a proper strategy, Max always has a best response strategy that is (smooth) deterministic:

**Lemma 4.2.** Let $\eta \in \text{Strat}_{\text{Min}}^{\mathbb{P}}$ and $\varepsilon > 0$. There exists a smooth deterministic strategy $\tau \in \text{sdStrat}_{\text{Max}}$ such that for all finite plays $\rho$, $\mathbb{E}_{\rho}^{\eta, \tau} \geq \text{Val}_{\rho} - \varepsilon$. If $\eta \in \text{mStrat}_{\text{Min}}^{\mathbb{P}}$ is memoryless, then there exists a smooth deterministic strategy $\tau \in \text{sdStrat}_{\text{Max}}$ such that for all configurations $(\ell, \nu)$, $\mathbb{E}_{\ell, \nu}^{\eta, \tau} \geq \text{mVal}_{\ell, \nu} - \varepsilon$.
A useful tool for the proof is a Bellman-like fixpoint equation fulfilled by the expected payoff. To state it, we pack all expectations following a pair $(\eta, \theta)$ of strategies in a single mapping $\mathbb{E}^{\eta,\theta}: \rho \in \text{FPlays} \mapsto \mathbb{E}_{\rho}^{\eta,\theta} \in \mathbb{R}$. The Bellman-like fixpoint operator $\mathcal{H}$ is a function relating mappings $X: \text{FPlays} \to \mathbb{R}$ such that $\mathcal{H}^{\eta,\theta}: (\text{FPlays} \to \mathbb{R}) \to (\text{FPlays} \to \mathbb{R})$ is partially defined for $X: \text{FPlays} \to \mathbb{R}$, and $\rho \in \text{FPlays}$ by

$$ \left\{ \begin{array}{ll} 0 & \text{if } \rho \text{ ends in } L_T \\ \sum_{\delta} \int_{I(\rho, \delta)} \eta_{\Delta}(\rho)(\delta) (t \operatorname{wt}(\ell) + \operatorname{wt}(\delta) + X(\rho[\delta, t])) d\eta_{\mathbb{R}^+}(\rho, \delta)(t) & \text{if } \rho \in \text{FPlays}_{\text{Min}} \\ \sum_{\delta} \int_{I(\rho, \delta)} \theta_{\Delta}(\rho)(\delta) (t \operatorname{wt}(\ell) + \operatorname{wt}(\delta) + X(\rho[\delta, t])) d\theta_{\mathbb{R}^+}(\rho, \delta)(t) & \text{if } \rho \in \text{FPlays}_{\text{Max}} \end{array} \right. \quad (4.1) $$

This operator is only partially defined since it makes sense only for functions $X$ that are measurable wrt delays along the finite play. In the following, we prove that, when $\eta$ is not-deterministic but satisfies the second item of Hypothesis 3.9 (this is the only case where we will need a non-trivial proof for Lemma 4.2), $\mathbb{E}^{\eta,\theta}$ is a function for which $\mathcal{H}^{\eta,\theta}$ is well defined, and it is a fixpoint of $\mathcal{H}^{\eta,\theta}$.

**Lemma 4.3.** Let $\eta \in \text{Strat}_{\text{Min}}^p \setminus \text{sdStrat}_{\text{Min}}^p$ and $\theta \in \text{Strat}_{\text{Max}}$. The mapping $\mathbb{E}^{\eta,\theta}: \rho \in \text{FPlays} \mapsto \mathbb{E}_{\rho}^{\eta,\theta}$ is a fixpoint of the operator $\mathcal{H}^{\eta,\theta}: (\text{FPlays} \to \mathbb{R}) \to (\text{FPlays} \to \mathbb{R})$.

*Proof.* Let $\eta$ and $\theta$ be two strategies, and $\rho_0 \in \text{FPlays}$. If $\rho_0$ ends in $L_T$, then $\mathcal{H}^{\eta,\theta}(\mathbb{E}^{\eta,\theta})(\rho_0) = 0 = \mathbb{E}_{\rho_0}^{\eta,\theta}$.

Otherwise, we let $\xi$ be the strategy $\eta$ or $\theta$ depending on whether $\rho_0 \in \text{FPlays}_{\text{Min}}$ or $\rho_0 \in \text{FPlays}_{\text{Max}}$ and $\pi_0$ be the path that $\rho_0$ follows. By Lemma 3.14, $\mathbb{E}_{\rho_0}^{\eta,\theta} = \sum_{\pi \in \text{TPaths}_{\rho_0}} \mathbb{E}_{\rho_0}^{\eta,\theta}(\pi_0 \pi)$. In particular, by decomposing the path (that is possible, since $\rho_0$ does not end in $L_T$), we have $\mathbb{E}_{\rho_0}^{\eta,\theta} = \sum_{\delta} \sum_{\pi|\delta\pi \in \text{TPaths}_{\rho_0}} \mathbb{E}_{\rho_0}^{\eta,\theta}(\pi_0 \delta\pi)$. Thus, by definition of the expectation of a path, $\mathbb{E}_{\rho_0}^{\eta,\theta}$ is equal to

$$ \sum_{\delta} \sum_{\pi|\delta\pi \in \text{TPaths}_{\rho_0}} \int_{I(\rho_0, \delta)} \xi_{\Delta}(\rho_0)(\delta) [(t \operatorname{wt}(\ell) + \operatorname{wt}(\delta)) \mathbb{P}_{\rho_0[\delta, t]}^{\eta,\theta}(\pi_0 \delta\pi) + \mathbb{E}_{\rho_0[\delta, t]}^{\eta,\theta}(\pi_0 \delta\pi)] d\xi_{\mathbb{R}^+}(\rho_0, \delta)(t). $$

Since $\eta$ is not smooth deterministic, yet proper, it satisfies the second item of Hypothesis 3.9 for bounds $\alpha$ and $m$. Then by Lemma 3.10 and Lemma 3.13.(2) we obtain that

$$ \mathbb{E}_{\rho_0[\delta, t]}^{\eta,\theta}(\pi_0 \delta \pi) \le (1-\alpha)^{\lfloor \pi \rfloor / m} |\pi| w_{\max}^e $$

and

$$ (t \operatorname{wt}(\ell) + \operatorname{wt}(\delta)) \mathbb{P}_{\rho_0[\delta, t]}^{\eta,\theta}(\pi_0 \delta \pi) \le (1-\alpha)^{\lfloor \pi \rfloor / m} w_{\max}^e $$

In particular, $(t \operatorname{wt}(\ell) + \operatorname{wt}(\delta)) \mathbb{P}_{\rho_0[\delta, t]}^{\eta,\theta}(\pi_0 \delta \pi) + \mathbb{E}_{\rho_0[\delta, t]}^{\eta,\theta}(\pi_0 \delta \pi)$ is bounded by $(1-\alpha)^{\lfloor \pi \rfloor / m}$ ($|\pi| + 1) w_{\max}^e$. Thus, by dominated convergence theorem, again by Lemma 3.14, and by definition of $\mathcal{H}^{\eta,\theta}$, we obtain

$$ \mathbb{E}_{\rho_0}^{\eta,\theta} = \sum_{\delta} \int_{I(\rho_0, \delta)} \xi_{\Delta}(\rho_0)(\delta) (t \operatorname{wt}(\ell) + \operatorname{wt}(\delta) + \mathbb{E}_{\rho_0[\delta, t]}^{\eta,\theta}) d\xi_{\mathbb{R}^+}(\rho_0, \delta)(t) = \mathcal{H}^{\eta,\theta}(\mathbb{E}^{\eta,\theta})(\rho_0). $$

Thus, $\mathbb{E}^{\eta,\theta}$ is a fixpoint of $\mathcal{H}^{\eta,\theta}$.

<figure><img src="image_8.png" /></figure>

With this fixpoint equation in mind, we are equipped to prove Lemma 4.2: $\text{Max}$ has a deterministic best-response strategy against a proper strategy of $\text{Min}$.
*Proof of Lemma 4.2.* To do so, we first consider a (stochastic) strategy $\theta$ of Max such that for all finite plays $\rho_0$, $E_{\rho_0}^{\eta, \theta} \ge \text{Val}_{\rho_0}^{\eta} - \varepsilon/2$, for a fixed $\varepsilon > 0$, which exists by definition of the (stochastic) value. We show the existence of a smooth deterministic strategy $\tau \in \text{sdStrat}_{\text{Max}}$ for Max such that for all finite plays $\rho_0$, we have $E_{\rho_0}^{\eta, \tau} \ge E_{\rho_0}^{\eta, \theta} - \varepsilon/2^{|\rho|}$, which allows us to conclude that $E_{\rho_0}^{\eta, \tau} \ge \text{Val}_{\rho_0}^{\eta} - \varepsilon$.

To do that, we distinguish the cases where $\eta$ is deterministic or is not. First, suppose $\eta \in \text{sdStrat}_{\text{Min}}^p$. By contradiction, we suppose that for all $\tau \in \text{sdStrat}_{\text{Max}}$, $\text{wt}(\text{Play}(\rho_0, \eta, \tau)) \le E_{\rho_0}^{\eta, \theta} - \varepsilon/2^{|\rho_0|}$. Thus, by definition of the expectation,

$$E_{\rho_0}^{\eta, \theta} = \int_{\rho} \text{wt}(\rho) d\mathbb{P}_{\rho_0}^{\eta, \theta} \le E_{\rho_0}^{\eta, \theta} - \varepsilon/2^{|\rho_0|}$$

We obtain a contradiction.

Now, we suppose that $\eta$ is not in $\text{sdStrat}_{\text{Min}}^p$. In this case, we will use the $\text{argsup}^\varepsilon$ operator defined for all mappings $f: A \to \mathbb{R}$ and $B \subseteq A$ by $\text{argsup}_B^\varepsilon f = \{a \in B \mid f(a) \ge \sup_B f - \varepsilon\}$. For all $\rho \in \text{FPlays}_{\text{Max}}$ ending in $(\ell, \nu)$, we let

$$\tau(\rho) \in \text{argsup}_{(\ell, \nu) \xrightarrow{\delta, t} (\ell', \nu')}^{\varepsilon/2^{|\rho|+1}} (t \text{wt}(\ell) + \text{wt}(\delta) + \mathbb{E}_{\rho[\delta, t]}^{\eta, \theta})$$

We can use the Kuratowski and Ryll-Nardzewski measurable selection theorem [KRN65] to ensure that $\tau$ can be chosen in $\text{sdStrat}_{\text{Max}}$. This theorem states that if $\psi$ is a mapping from a measurable space taking values in the set of non empty closed subsets of a Borel set (for us, pairs $(\delta, t)$ of transitions and real delays) that is weakly measurable, then $\psi$ has a selection, i.e. a measurable mapping $\tau$ such that for all elements $\omega$ of the measurable space, $\tau(\omega) \in \psi(\omega)$. Weak measurability amounts to saying that for every open subset $U$, we have that $\{\omega \mid \psi(\omega) \cap U \ne \emptyset\}$ is measurable.

Indeed, the mapping $\psi$ defined for all plays $\rho$ by

$$\psi(\rho) = \{(\delta, t) \in \mathbb{R} \mid t \text{wt}(\ell) + \text{wt}(\delta) + \mathbb{E}_{\rho[\delta, t]}^{\eta, \theta} \ge K - \varepsilon\}$$

where $K$ is the supremum of the function $t \mapsto t \text{wt}(\ell) + \text{wt}(\delta) + \mathbb{E}_{\rho[\delta, t]}^{\eta, \theta}$ can be shown to be weakly measurable: for all open set $U$ of $\mathbb{R}$, the set $\{\rho \mid \psi(\rho) \cap U \ne \emptyset\}$ can be generated by a countable union of cylinders, since we have a countable number of paths and delays are constrained by $U$ (which is measurable) and a supremum (which is also measurable). The selection theorem thus allows us to define a measurable strategy $\tau \in \text{sdStrat}_{\text{Max}}$.

We also define, for all $i \in \mathbb{N}$, the (smooth) strategy $\xi_i \in \text{Strat}_{\text{Max}}$ consisting in playing $\tau$ during the first $i$ steps of the play, and $\theta$ for the remaining ones: since $\tau$ and $\theta$ are smooth, the combination $\xi_i$ does too. When $i$ increases, strategy $\xi_i$ looks more and more like $\tau$. In particular, for all finite plays $\rho_0$, $E_{\rho_0}^{\eta, \xi_i}$ tends to $E_{\rho_0}^{\eta, \tau}$ when $i$ tends to $+\infty$. To prove it formally, we decompose the sum given for the expectation in Lemma 3.14 according to the length of the path, we have

$$|\mathbb{E}_{\rho_0}^{\eta, \xi_i} - \mathbb{E}_{\rho_0}^{\eta, \tau}| = \left| \sum_{j=0}^{\infty} \sum_{\pi \in \text{TPaths}_{\rho}^j} \mathbb{E}_{\rho_0}^{\eta, \xi_i}(\pi_0 \pi) - \sum_{j=0}^{\infty} \sum_{\pi \in \text{TPaths}_{\rho}^j} \mathbb{E}_{\rho_0}^{\eta, \tau}(\pi_0 \pi) \right|$$

where $\pi_0$ is the path followed by $\rho_0$. Letting $k_i = \max(0, i - |\rho_0|)$ be the number of steps after $\rho_0$ where $\xi_i$ and $\tau$ are equal, and noticing that $\xi_i$ and $\tau$ behave the same until the step
$k_i$ from $\rho_0$, we deduce that

$$ \begin{aligned} |\mathbb{E}_{\rho_0}^{\eta, \xi_i} - \mathbb{E}_{\rho_0}^{\eta, \tau}| &= \left| \sum_{j=k_i+1}^{\infty} \sum_{\pi \in \text{TPaths}_{\rho_0}^j} \mathbb{E}_{\rho_0}^{\eta, \xi_i}(\pi_0 \pi) - \sum_{j=k_i+1}^{\infty} \sum_{\pi \in \text{TPaths}_{\rho_0}^j} \mathbb{E}_{\rho_0}^{\eta, \tau}(\pi_0 \pi) \right| \\ &\le \sum_{j=k_i+1}^{\infty} \sum_{\pi \in \text{TPaths}_{\rho_0}^j} (|\mathbb{E}_{\rho_0}^{\eta, \xi_i}(\pi_0 \pi)| + |\mathbb{E}_{\rho_0}^{\eta, \tau}(\pi_0 \pi)|). \end{aligned} $$

Thus, by Lemma 3.13.(2) and Lemma 3.10, we have (with $\alpha$ and $m$ given by the property of being proper)

$$ |\mathbb{E}_{\rho_0}^{\eta, \xi_i} - \mathbb{E}_{\rho_0}^{\eta, \tau}| \le \sum_{j=k_i+1}^{\infty} 2j w_{\max}^e (1-\alpha)^{\lfloor j/m \rfloor}. $$

Moreover, since $x \mapsto (1-\alpha)^x$ is decreasing, we obtain that

$$ |\mathbb{E}_{\rho_0}^{\eta, \xi_i} - \mathbb{E}_{\rho_0}^{\eta, \tau}| \le \sum_{j=k_i+1}^{\infty} 2j w_{\max}^e (1-\alpha)^{j/m+1}. $$

Noticing that the formal power series $\sum x\beta^{x-1}$ is the formal derivative of the formal power series $\sum \beta^x$, whose sum we can compute, we conclude that

$$ |\mathbb{E}_{\rho_0}^{\eta, \xi_i} - \mathbb{E}_{\rho_0}^{\eta, \tau}| \le 2 w_{\max}^e \frac{(1-\alpha)^{(k_i+2)/m} (k_i(1-(1-\alpha)^{1/m}) + 1)}{(1-(1-\alpha)^{1/m})^2} $$

that tends to 0 when $i$ (and thus $k_i$) tends to $+\infty$.

Independently, we relate strategies $\xi_i$ and $\theta$, by showing that

$$ \forall i \in \mathbb{N} \quad \forall \rho_0 \in \text{FPlays} \quad \mathbb{E}_{\rho_0}^{\eta, \xi_i} \ge \mathbb{E}_{\rho_0}^{\eta, \theta} - \frac{\varepsilon}{2^{|\rho_0|}} \quad (4.2) $$

When taking the limit when $i$ tends to $+\infty$, we obtain that for all finite plays $\rho_0$, $\mathbb{E}_{\rho_0}^{\eta, \tau} \ge \mathbb{E}_{\rho_0}^{\eta, \theta} - \frac{\varepsilon}{2^{|\rho_0|}}$. In particular, $\mathbb{E}_{\rho_0}^{\eta, \tau} \ge \text{Val}_{\rho_0}^{\eta} - \varepsilon$. In the case where $\eta$ is memoryless, since memoryless strategies of Max are stochastic strategies of Max, we have, for all configurations $(\ell, \nu)$, $\text{Val}_{\ell, \nu}^{\eta} \ge \text{mVal}_{\ell, \nu}^{\eta}$. Thus, by applying the previous result in case where $\rho$ is only a configuration, we deduce that $\mathbb{E}_{\ell, \nu}^{\eta, \tau} \ge \text{Val}_{\ell, \nu}^{\eta} - \varepsilon \ge \text{mVal}_{\ell, \nu}^{\eta} - \varepsilon$.

To conclude the proof, we need to show (4.2). First, we notice that this inequality trivially holds when $|\rho_0| \ge i$, since then strategies $\xi_i$ and $\theta$ coincide for the rest of the play. It remains to show that the property holds for all $i$ and plays $\rho_0$ such that $|\rho_0| \le i$. We proceed by induction on $i - |\rho_0|$. If $i - |\rho_0| = 0$, we have said before that the inequality trivially holds. Otherwise, we distinguish three cases according to the last location of $\rho_0$. If $\rho_0$ ends in $L_T$, we have $\mathbb{E}_{\rho_0}^{\eta, \xi_i} = 0 \ge 0 - \frac{\varepsilon}{2^{|\rho_0|}} = \mathbb{E}_{\rho_0}^{\eta, \theta} - \frac{\varepsilon}{2^{|\rho_0|}}$.

If $\rho_0 \in \text{FPlays}_{\text{Min}}$, by Lemma 4.3,

$$ \mathbb{E}_{\rho_0}^{\eta, \xi_i} = \mathcal{H}^{\eta, \xi_i}(\mathbb{E}^{\eta, \xi_i})(\rho_0) = \sum_{\delta} \int_{I(\rho_0, \delta)} \eta_{\Delta}(\rho_0)(\delta) [t \text{wt}(\ell) + \text{wt}(\delta) + \mathbb{E}_{\rho_0[\delta, t]}^{\eta, \xi_i}] \, d\eta_{\mathbb{R}^+}(\rho_0, \delta)(t) $$

By induction hypothesis, we deduce that

$$ \mathbb{E}_{\rho_0}^{\eta, \xi_i} \ge \sum_{\delta} \int_{I(\rho_0, \delta)} \eta_{\Delta}(\rho_0)(\delta) (t \text{wt}(\ell) + \text{wt}(\delta) + \mathbb{E}_{\rho_0[\delta, t]}^{\eta, \theta} - \frac{\varepsilon}{2^{|\rho_0|+1}}) \, d\eta_{\mathbb{R}^+}(\rho_0, \delta)(t). $$
Thus, by linearity of the integral, we have

$$ \mathbb{E}_{\rho_0}^{\eta, \xi_i} \geq \sum_{\delta} \int_{I(\rho_0, \delta)} \eta_{\Delta}(\rho_0)(\delta) (t \operatorname{wt}(\ell) + \operatorname{wt}(\delta) + \mathbb{E}_{\rho_0[\delta, t]}^{\eta, \theta}) \, d\eta_{\mathbb{R}^+}(\rho_0, \delta)(t) \\ - \frac{\varepsilon}{2|\rho_0|+1} \sum_{\delta} \int_{I(\rho_0, \delta)} \eta_{\Delta}(\rho_0)(\delta) \, d\eta_{\mathbb{R}^+}(\rho_0, \delta)(t). $$

Since $\eta$ is a distribution, we obtain that

$$ \mathbb{E}_{\rho_0}^{\eta, \xi_i} \geq \mathcal{H}^{\eta, \theta}(\mathbb{E}^{\eta, \theta})(\rho_0) - \frac{\varepsilon}{2|\rho_0|+1} \times 1 \geq \mathcal{H}^{\eta, \theta}(\mathbb{E}^{\eta, \theta})(\rho_0) - \frac{\varepsilon}{2|\rho_0|}. $$

If $\rho_0 \in \text{FPlays}_{\text{Max}}$, Lemma 3.14 gives again

$$ \mathbb{E}_{\rho_0}^{\eta, \xi_i} = \sum_{\delta} \sum_{\pi | \delta \pi \in \text{TPaths}_{\rho_0}} \mathbb{E}_{\rho_0}^{\eta, \xi_i}(\pi_0 \delta \pi). $$

Since $|\rho_0| \le i$, the next step for Max is dictated by the strategy $\tau$, that is deterministic. Letting $(\delta_0, t_0) = \tau(\rho_0)$, we thus have

$$ \mathbb{E}_{\rho_0}^{\eta, \xi_i} = (t_0 \operatorname{wt}(\ell) + \operatorname{wt}(\delta_0)) \sum_{\pi | \delta_0 \pi \in \text{TPaths}_{\rho_0}} \mathbb{P}_{\rho_0[\delta_0, t_0]}^{\eta, \xi_i}(\pi_0 \delta_0 \pi) + \sum_{\pi | \delta_0 \pi \in \text{TPaths}_{\rho_0}} \mathbb{E}_{\rho_0[\delta_0, t_0]}^{\eta, \xi_i}(\pi_0 \delta_0 \pi) $$

Moreover, since $\eta$ is proper, we know that $\sum_{\pi | \delta_0 \pi \in \text{TPaths}_{\rho_0}} \mathbb{P}_{\rho_0[\delta_0, t_0]}^{\eta, \xi_i}(\text{TPaths}_{\rho_0}[\delta_0, t_0]) = 1$, and we deduce that

$$ \mathbb{E}_{\rho_0}^{\eta, \xi_i} = t_0 \operatorname{wt}(\ell) + \operatorname{wt}(\delta_0) + \mathbb{E}_{\rho_0[\delta_0, t_0]}^{\eta, \xi_i} $$

By the induction hypothesis, we obtain that

$$ \mathbb{E}_{\rho_0}^{\eta, \xi_i} \geq t_0 \operatorname{wt}(\ell) + \operatorname{wt}(\delta_0) + \mathbb{E}_{\rho_0[\delta_0, t_0]}^{\eta, \theta} - \frac{\varepsilon}{2|\rho_0|+1} $$

Thus, by definition of $\tau$ and letting $(\ell, \nu)$ the last configuration of $\rho_0$, we get

$$ \mathbb{E}_{\rho_0}^{\eta, \xi_i} \geq \sup_{(\ell, \nu) \xrightarrow{\delta, t} (\ell', \nu')} (t \operatorname{wt}(\ell) + \operatorname{wt}(\delta) + \mathbb{E}_{\rho_0[\delta, t]}^{\eta, \theta}) - \frac{\varepsilon}{2|\rho_0|+1} - \frac{\varepsilon}{2|\rho_0|+1}. $$

Since $\theta$ is a distribution, we have

$$ \begin{aligned} \mathbb{E}_{\rho_0}^{\eta, \xi_i} &\geq \sum_{\delta} \int_{I(\rho_0, \delta)} \theta_{\Delta}(\rho_0)(\delta) (t \operatorname{wt}(\ell) + \operatorname{wt}(\delta) + \mathbb{E}_{\rho_0[\delta, t]}^{\eta, \theta}) \, d\theta_{\mathbb{R}^+}(\rho_0, \delta)(t) - \frac{\varepsilon}{2|\rho_0|} \\ &= \mathcal{H}^{\eta, \theta}(\mathbb{E}^{\eta, \theta})(\rho_0) - \frac{\varepsilon}{2|\rho_0|}. \end{aligned} $$

We conclude in all cases, by Lemma 4.3:

$$ \mathbb{E}_{\rho_0}^{\eta, \xi_i} \geq \mathcal{H}^{\eta, \theta}(\mathbb{E}^{\eta, \theta})(\rho_0) - \frac{\varepsilon}{2|\rho_0|} = \mathbb{E}_{\rho_0}^{\eta, \theta} - \frac{\varepsilon}{2|\rho_0|}. \quad \square $$

We are now able to come back to the proof of Theorem 4.1, separated into two inequalities. The first one shows that the stochastic values are at most equal to the smooth deterministic upper-value:

**Lemma 4.4.** In all WTGs $\mathcal{G}$, for all locations $\ell$ and valuations $\nu$, $\overline{\text{Val}}_{\ell, \nu} \le \overline{\text{sdVal}}_{\ell, \nu}$. □
Proof. Let $\sigma$ be a proper smooth deterministic strategy for Min. Let $\varepsilon > 0$. By Lemma 4.2, there exists $\tau \in \text{sdStrat}_{\text{Max}}$ such that $\text{wt}(\text{Play}((\ell, \nu), \sigma, \tau)) = \mathbb{E}_{\ell, \nu}^{\sigma, \tau} \geq \text{Val}_{\ell, \nu}^{\sigma} - \varepsilon$. Therefore

$$ \sup_{\tau \in \text{sdStrat}_{\text{Max}}} \text{wt}(\text{Play}((\ell, \nu), \sigma, \tau)) \geq \text{Val}_{\ell, \nu}^{\sigma} - \varepsilon. $$

Since this holds for all $\varepsilon$, we have

$$ \sup_{\tau \in \text{sdStrat}_{\text{Max}}} \text{wt}(\text{Play}((\ell, \nu), \sigma, \tau)) \geq \text{Val}_{\ell, \nu}^{\sigma}. $$

By considering the infimum over all proper smooth deterministic strategies, we obtain

$$ \overline{\text{sdVal}}_{\ell, \nu} = \inf_{\sigma \in \text{sdStrat}_{\text{Min}}^{p}} \sup_{\tau \in \text{sdStrat}_{\text{Max}}} \text{wt}(\text{Play}((\ell, \nu), \sigma, \tau)) \geq \inf_{\sigma \in \text{sdStrat}_{\text{Min}}^{p}} \text{Val}_{\ell, \nu}^{\sigma}. $$

Since $\text{sdStrat}_{\text{Min}}^{p} \subseteq \text{Strat}_{\text{Min}}^{p}$, the infimum over all proper strategies of Min is at most the infimum over deterministic strategies:

$$ \overline{\text{sdVal}}_{\ell, \nu} \geq \inf_{\eta \in \text{Strat}_{\text{Min}}^{p}} \text{Val}_{\ell, \nu}^{\eta} = \overline{\text{Val}}_{\ell, \nu}. \quad \square $$

The second one shows that smooth deterministic lower-value is at most equal to the stochastic values.

**Lemma 4.5.** In all WTGs $\mathcal{G}$, for all locations $\ell$ and valuations $\nu$, $\underline{\text{sdVal}}_{\ell, \nu} \leq \overline{\text{Val}}_{\ell, \nu}$.

Proof. Let $\varepsilon > 0$. If $\underline{\text{sdVal}}_{\ell, \nu} = -\infty$, the result is trivial. Otherwise, by definition, Max has a deterministic $\varepsilon$-optimal strategy $\tau$ for the smooth deterministic lower-value. Against any proper smooth deterministic strategy of Min, from $(\ell, \nu)$, it guarantees a weight at least $\underline{\text{sdVal}}_{\ell, \nu} - \varepsilon$.

Let $\eta$ be any proper strategy of Min. Every play conforming to $\eta$ and $\tau$ has a weight at least $\underline{\text{sdVal}}_{\ell, \nu} - \varepsilon$ (since it is conforming to $\tau$), so that, by definition of the expectation,

$$ \mathbb{E}_{\ell, \nu}^{\eta, \tau} = \int_{\rho} \text{wt}(\rho) d\mathbb{P}_{\ell, \nu}^{\eta, \tau}(\rho) \geq \underline{\text{sdVal}}_{\ell, \nu} - \varepsilon $$

Since this inequality holds for all proper strategies of Min, we deduce that

$$ \inf_{\eta \in \text{Strat}_{\text{Min}}^{p}} \mathbb{E}_{\ell, \nu}^{\eta, \tau} \geq \underline{\text{sdVal}}_{\ell, \nu} - \varepsilon. $$

By taking the supremum over all strategies of Max (that contain the smooth deterministic strategy $\tau$), we have

$$ \sup_{\theta \in \text{Strat}_{\text{Max}}^{p}} \inf_{\eta \in \text{Strat}_{\text{Min}}^{p}} \mathbb{E}_{\ell, \nu}^{\eta, \theta} \geq \underline{\text{sdVal}}_{\ell, \nu} - \varepsilon. $$

In particular, $\underline{\text{sdVal}}_{\ell, \nu} \geq \overline{\text{Val}}_{\ell, \nu} - \varepsilon$. To conclude, we remark that this inequality holds for all $\varepsilon > 0$, and thus also when $\varepsilon$ is set to 0. $\square$

Combined with the fact that $\underline{\text{sdVal}}_{\ell, \nu} \leq \overline{\text{Val}}_{\ell, \nu}$, we indeed proved the equalities of Theorem 4.1.

It remains to study the memoryless values, and compare them with the (smooth) deterministic value(s). Unfortunately, we cannot hope for a similar result as the one above, showing the equality of the memoryless values with the deterministic one. Indeed, the following example shows that WTGs are not determined with respect to the memoryless value.
<figure><img src="image_9.png" /><figcaption>Figure 5: A one-clock WTG where $\overline{mVal}_{\ell_0,0} > mVal_{\ell_0,0}$.</figcaption></figure>

**Example 4.6.** We consider the one-clock WTG depicted in Figure 5, and show that $\overline{mVal}_{\ell_0,0} = 0 > -9 \ge mVal_{\ell_0,0}$.

To do so, consider a proper memoryless strategy $\eta$ of Min. First, we remark that there exists $p \in [0, 1)$ such that $\eta_\Delta(\ell_0, 0) = p \times \text{Dirac}_{\delta_1} + (1-p) \times \text{Dirac}_{\delta_4}$. Moreover, since $\ell_0$ and $\ell_1$ are always reached after a reset, i.e. with the valuation 0, $\eta$ always chooses the same delay in $\ell_0$ that does not impact the next choice of the memoryless strategy of Max. Formally, let $t \in (0, 1)$ be the expected delay in $\ell_0$ (from the valuation 0) according to $\eta_{\mathbb{R}^+}(\ell_0, 0)(\delta_1)$, and we define the discrete strategy $\eta'$ by

$$ \eta'(\ell_0, 0) = p \times \text{Dirac}_{\delta_1, t} + (1-p) \times \text{Dirac}_{\delta_4, 0} $$

For all memoryless strategies $\theta$ of Max, $\mathbb{E}_{\ell_0,0}^{\eta,\theta} = \mathbb{E}_{\ell_0,0}^{\eta',\theta}$. Now, we consider the smooth deterministic memoryless strategy $\tau$ of Max defined by $\tau(\ell_1, 0) = (\delta_2, (1+t)/2)$. Then

$$ \mathbb{E}_{\ell_0,0}^{\eta',\tau} = \sum_{i=0}^{+\infty} \frac{1-t}{2} ip^i = \frac{1-t}{2} \frac{p}{(1-p)^2} \ge 0 $$

and this expectation is null when $p=0$, thus $\overline{mVal}_{\ell_0,0} = 0$.

By a similar reasoning, all (smooth) memoryless strategies $\theta$ of Max are equivalent to a discrete strategy $\theta'$ described by the probability $q = \theta_\Delta(\ell_1, 0) \in [0, 1)$ and the expected delay $t \in (0, 1)$ spent in $\ell_1$ (from the valuation 0) according to $\theta_{\mathbb{R}^+}(\ell_1, 0)(\delta_2)$: we have

$$ \theta'(\ell_1, 0) = q \times \text{Dirac}_{\delta_2, t} + (1-q) \times \text{Dirac}_{\delta_3, 0}. $$

We define a proper memoryless strategy $\eta$ for Min by letting

$$ \eta(\ell_0, 0) = p \times \text{Dirac}_{\delta_1, (1+t)/2} + (1-p) \times \text{Dirac}_{\delta_4, 0}. $$

By Lemma 4.3, we have $\mathbb{E}_{\ell_0,0}^{\eta,\theta'} = (\mathbb{E}_{\ell_1,0}^{\eta,\theta'} - (1+t)/2) \times p$ and $\mathbb{E}_{\ell_1,0}^{\eta,\theta'} = -10 \times (1-q) + (t+\mathbb{E}_{\ell_0,0}^{\eta,\theta'}) \times q$. In particular, we deduce that

$$ \mathbb{E}_{\ell_0,0}^{\eta,\theta'} = \left( -10(1-q) + (\mathbb{E}_{\ell_0,0}^{\eta,\theta'} + t)q - \frac{1+t}{2} \right) p $$

which resolves into

$$ \mathbb{E}_{\ell_0,0}^{\eta,\theta'} = \left( -10(1-q) - \frac{t(1-2q)+1}{2} \right) \frac{p}{1-pq}. $$
<figure><img src="image_10.png" /><figcaption>Figure 6: One-clock WTG where $dVal_{\ell_1,0} \neq \overline{mVal}_{\ell_1,0} = \underline{mVal}_{\ell_1,0}$.</figcaption></figure>

First, we suppose that $q = 1$, i.e. $\theta'$ is a deterministic strategy such that $\theta'(\ell_1, 0) = (\delta_2, t)$. In this case, we have

$$E_{\ell_0,0}^{\eta,\theta'} = -\frac{1-t}{2} \frac{p}{1-p}.$$

Now, as we control the strategy of Min, we can fix $p = \frac{18}{19-t} < 1$ (since $t < 1$), and we obtain

$$E_{\ell_0,0}^{\eta,\theta'} = -\frac{1-t}{2} \frac{18}{(19-t)(1-\frac{18}{19-t})} = -\frac{1-t}{2} \frac{18}{1-t} = -9.$$

Otherwise, we suppose that $0 \le q < 1$, we deduce that $t(1 - 2q) + 1 \ge 0$ (since $t \in (0, 1]$). Thus,

$$E_{\ell_0,0}^{\eta,\theta'} \le -10(1-q) \frac{p}{1-pq}.$$

Again, as we control the strategy of Min, we can fix $p = \frac{9}{10-q} < 1$ (since $q < 1$), and

$$E_{\ell_0,0}^{\eta,\theta'} \le -10(1-q) \frac{9}{(10-q)(1-\frac{9}{10-q}q)} = -10(1-q) \frac{9}{10(1-q)} = -9.$$

We deduce that $\underline{mVal}(\ell_0, 0) \le -9$. Thus, we conclude that $\underline{mVal}(\ell_0, 0) \le -9 < 0 = \overline{mVal}(\ell_0, 0)$ as expected.

Moreover, even if we wanted to restrict our study to one of the memoryless values (upper or lower-values), the following example shows a case where memoryless lower and upper-values are equal, but different from the deterministic value.

**Example 4.7.** We consider the one-clock WTG depicted in Figure 6. We explain why $dVal_{\ell_1,0} \neq \overline{mVal}_{\ell_1,0} = \underline{mVal}_{\ell_1,0}$. Since Min has a way to obtain the weight 0 by using transition $\delta_2$ (and thus with a memoryless and deterministic strategy), all values $dVal_{\ell_1,0}$, $\overline{mVal}_{\ell_1,0}$, $\underline{mVal}_{\ell_1,0}$ are non-positive.

We consider the deterministic strategy $\tau$ for Max defined, for all plays $\rho$ with $(\ell_0, \nu)$ as last configuration, by

$$\tau(\rho) = \begin{cases} (\delta_1, \frac{\varepsilon}{2|\rho|}) & \text{if } \nu = 0 \\ (\delta_1, 0) & \text{if } \nu > 0 \end{cases}$$

Since each iteration of the cycle gives a cumulated weight of at most $-\frac{\varepsilon}{2|\rho|}$, then $dVal_{\ell_1,0}^{\tau} \ge -\varepsilon$ for all $\varepsilon > 0$. In particular, $dVal_{\ell_1,0}$ is also non-negative, which implies that $dVal_{\ell_1,0} = 0$. Notice that the strategy $\tau$ uses memory, to compute the length $|\rho|$ of the current play.

Now, we consider the memoryless strategy for Min such that, for $p \in (0, 1)$, chooses transition $\delta_0$ with delay 0 with probability $1-p$ and transition $\delta_2$ with delay 0 with probability $p$. When Max follows a memoryless strategy, each time we pass through the configuration $(\ell_0, 0)$, the same choice is always made that is to delay for a small amount of time before taking transition $\delta_1$. In particular, the two memoryless strategies combined allows one to expect $1/(1-p)$ turns in the cycle, each turn having a fixed negative weight. Thus, Min can
secure a weight as little as possible, by making $p$ approach 1. Thus $\overline{mVal}_{\ell_1,0} = -\infty$. And since $\overline{mVal}_{\ell_1,0} \le \overline{mVal}_{\ell_1,0}$, we also have $\overline{mVal}_{\ell_1,0} = -\infty$.

We will be able to obtain a result comparing the memoryless values and the deterministic one, in a fragment of WTGs that we present in the next section.

## 5. DIVERGENT WEIGHTED TIMED GAMES

Interesting fragments of WTGs have been designed, in order to regain decidability of the problem of determining whether the value of a WTG is below a certain threshold. One such fragment is obtained by enforcing a semantical property of divergence (originally called strictly non-Zeno cost when only dealing with non-negative weights [BCFL04]): it asks that every play following a cycle in the region automaton has a weight far from 0. We will consider this restriction in the following, since it allows for a large class of decidable WTGs, with no limitations on the number of clocks. Formally, a cyclic region path $\pi$ of $\mathcal{R}(\mathcal{G})$ is said to be a positive cycle (resp. a negative cycle) if every finite play $\rho$ following $\pi$ satisfies $\text{wt}\Sigma(\rho) \ge 1$ (resp. $\text{wt}\Sigma(\rho) \le -1$).

**Definition 5.1** [BMR17]. A WTG is divergent if every cyclic region path is positive or negative.

In [BMR17], it is shown that this definition is equivalent to requiring that for all strongly connected components (SCC) $S$ of the graph of $\mathcal{R}(\mathcal{G})$, either every cycle $\pi$ inside $S$ is positive (we say that the SCC is positive), or every cycle $\pi$ inside $S$ is negative (we say that the SCC is negative). The best computability result in this setting is:

**Theorem 5.2** [BMR17]. The deterministic value of a divergent WTG can be computed in triply-exponential-time.

We explain how to recover from Theorem 5.2 the needed shape of $\varepsilon$-optimal strategies, since this is one of the new technical ingredients we need afterwards.

**5.1. Switching strategies for Min.** Theorem 5.2 is obtained in [BMR17] by using a value iteration algorithm (originally described in [ABM04] for acyclic timed automata). If $V$ represents a value function, i.e. a mapping $L \times \mathbb{R}_{\ge 0}^\chi \to \mathbb{R}_\infty$, we denote by $V_{\ell,\nu}$ the image $V(\ell, \nu)$, for better readability. One step of the game is summarised in the following operator $\mathcal{F}$ mapping each value function $V$ to the value function defined for all $(\ell, \nu) \in L \times \mathbb{R}_{\ge 0}^\chi$ by

$$ \mathcal{F}(V)_{\ell,\nu} = \begin{cases} 0 & \text{if } \ell \in L_T \\ \sup_{(\ell,\nu) \xrightarrow{\delta,t} (\ell',\nu')} [t \times \text{wt}(\ell) + \text{wt}(\delta) + V_{\ell',\nu'}] & \text{if } \ell \in L_{\text{Max}} \\ \inf_{(\ell,\nu) \xrightarrow{\delta,t} (\ell',\nu')} [t \times \text{wt}(\ell) + \text{wt}(\delta) + V_{\ell',\nu'}] & \text{if } \ell \in L_{\text{Min}} \end{cases} $$

where $(\ell, \nu) \xrightarrow{\delta,t} (\ell', \nu')$ ranges over valid edges in $\mathcal{G}$. Then, starting from $V^0$ mapping every configuration to $+\infty$, except for the targets mapped to 0, we let $V^i = \mathcal{F}(V^{i-1})$ for all $i > 0$. The value function $V^i$ is intuitively what Min can guarantee when forced to reach the target in at most $i$ steps.

The value computation of Theorem 5.2 is then obtained in two steps. First, configurations $(\ell, \nu)$ of value $\text{dVal}_{\ell,\nu} = -\infty$ are found by using a decomposition of the region game $\mathcal{R}(\mathcal{G})$ into SCCs. Indeed, in divergent WTGs, configurations of value $-\infty$ are all the
ones from which Min has a strategy to visit infinitely many times configurations of a single location $(\ell, r)$ of $\mathcal{R}(\mathcal{G})$ contained in a negative SCC. This is thus a Büchi objective on the region game, that can easily be solved with some attractor computations. Notice that if a configuration $(\ell, \nu)$ has value $-\infty$, this implies that all configurations $(\ell, \nu')$ with $\nu'$ in the same region as $\nu$ have value $-\infty$. As we explained at the end of Section 2 for the values $+\infty$, we can then remove configurations of value $-\infty$ by strengthening the guards on transitions, while letting unchanged other finite values.

Then, the (finite) deterministic value $\mathbf{dVal}$ is obtained as an iterate $V^H$ of the previous operator, with $H$ polynomial in the size of the region game and the maximal weights of $\mathcal{G}$. This means that playing for only a bounded number of steps is equivalent to the original game. In particular, at horizon $H$, we have that $\mathcal{F}(V^H) = V^{H+1} = \mathbf{dVal}$ so that $\mathbf{dVal}$ is a fixpoint of $\mathcal{F}$. As a side effect, this allows one to decompose the clock space $\mathbb{R}^{\ge 0}$ into a finite number $\alpha$ of cells (a refinement of the classical regions) such that $\mathbf{dVal}$ is affine on each cell.

**Lemma 5.3** [BMR17]. Let $(\ell, \nu)$ be a configuration. Then $\mathbf{dVal}_{\ell, \nu}$ is a fixpoint of $\mathcal{F}$, i.e. $\mathcal{F}(\mathbf{dVal}_{\ell, \nu}) = \mathbf{dVal}_{\ell, \nu}$.

Based on this, we can construct good strategies for Min that have a special form, the so-called switching strategies (introduced in [BGHM17] in the untimed setting, further extended in the timed setting with only one-clock in [BGH$^+$15]).

**Definition 5.4.** A switching strategy $\sigma$ is described by two deterministic memoryless strategies $\sigma^1$ and $\sigma^2$, as well as a switching threshold $K$. The strategy $\sigma$ then consists in playing strategy $\sigma^1$ until either we reach a target location, or the finite play has length at least $K$, in which case we switch to strategy $\sigma^2$.

Our new contribution is as follows:

**Theorem 5.5.** In a divergent WTG, for all $\varepsilon > 0$ and $N \in \mathbb{N}$, there exists a switching strategy $\sigma \in \text{sdStrat}_{\text{Min}}^{\mathbb{P}}$ for Min, for which the two components $\sigma^1$ and $\sigma^2$ are smooth, such that for all configurations $(\ell, \nu)$, $\mathbf{dVal}_{\ell, \nu}^{\sigma} \le \max(-N, \mathbf{dVal}_{\ell, \nu}) + \varepsilon$.

In particular, if all configurations have a finite deterministic value, there exists an $\varepsilon$-optimal proper smooth switching strategy wrt the deterministic value. In the presence of a configuration with a deterministic value $-\infty$, we build from Theorem 5.5 a family of proper smooth switching strategies (indexed by the parameter $N$) whose value tends to $-\infty$.

The proof of Theorem 5.5 requires to build both (smooth) strategies $\sigma^1$ and $\sigma^2$, as well as a switching threshold $K$. The second strategy $\sigma^2$ only consists in reaching the target and is thus obtained as a deterministic memoryless strategy from a classical attractor computation in the region game $\mathcal{R}(\mathcal{G})$. It is easy to choose $\sigma^2$ smooth (so that it fulfils Hypothesis 3.3). In contrast, the first strategy $\sigma^1$ requires more care. We build it so that it fulfils two properties, that we summarise in saying that $\sigma^1$ is fake-$\varepsilon$-optimal wrt the deterministic value:

(1) each finite play conforming to $\sigma^1$ from $(\ell, \nu)$ and reaching the target has a cumulated weight at most $\mathbf{dVal}_{\ell, \nu} + |\rho|\varepsilon$ (in particular, if $\mathbf{dVal}_{\ell, \nu} = -\infty$, no such plays should exist);

(2) each finite play conforming to $\sigma^1$ following a long enough cycle in the region game $\mathcal{R}(\mathcal{G})$ has a cumulated weight at most $-1$.

Here, “fake” means that $\sigma^1$ is not obliged to guarantee that the target is reached, but if it does so, it must do it with a cumulated weight close to $\mathbf{dVal}_{\ell, \nu}$, the error term depending linearly on the size of the play. The second property ensures that playing long enough $\sigma^1$ without reaching the target results in diminishing the cumulated weight. Then, if the switch
happens at horizon $K$ big enough, ($K = (w_{\max}^e |\mathcal{R}(\mathcal{G})|(|L|\alpha + 2) + N)(|\mathcal{R}(\mathcal{G})|(|L|\alpha + 1) + 1)$ suffices for instance), Min is sure that the cumulated weight so far is low enough so that the rest of the play to reach a target location (following $\sigma^2$ only) will not make the weight increase too much. In the absence of values $-\infty$ in dVal, the first property allows one to obtain a $K\epsilon$-optimal strategy even in the case where the switch does not occur (because we reach the target prematurely). The construction of a fake-$\epsilon$/K-optimal strategy $\sigma^1$ (the linear dependency on the length of the play in the first property of fake-optimality is thus taken care by a division by $K$ here) relies on the fact that $\mathcal{F}(dVal) = dVal$ (by Lemma 5.3) to play almost-optimally at horizon 1. More formally:

* For all configurations of value $-\infty$, $\sigma^1$ is built as a winning strategy for the Büchi objective "visit infinitely often configurations of a location $(\ell, r)$ of $\mathcal{R}(\mathcal{G})$ contained in a negative SCC". By definition, all cyclic paths following $\sigma^1$ will be inside a negative SCC, and thus be of cumulated weight at most $-1$, by divergence of the WTG. Moreover, no plays conforming to $\sigma^1$ from such a configuration of value $-\infty$ will reach a target location, since the chosen negative SCC is a trap controlled by Min. It is easy to choose $\sigma^1$ smooth (so that it fulfils Hypothesis 3.3).

* For the remaining configurations of finite deterministic value, we rely upon operator $\mathcal{F}$, letting $\sigma^1$ choose a decision that minimises the deterministic value at horizon 1. However, because of the guards on clocks, infimum/supremum operators in $\mathcal{F}$ are not necessarily minima/maxima, and we thus need to allow for a small error at each step of the strategy: this is the main difference with the untimed setting, which by the way explains why our definition of switching strategy needed to be adapted. We will use the $\text{arginf}_B^\epsilon$ operator defined for all mappings $f: A \to \mathbb{R}$ and $B \subseteq A$ by $\text{arginf}_B^\epsilon f = \{a \in B \mid f(a) \le \inf_B f + \epsilon\}$. Then, for all configurations $(\ell, \nu) \in L_{\text{Min}} \times \mathbb{R}_{\ge 0}^\chi$, we choose $\sigma^1(\ell, \nu)$ as a pair $(\delta, t)$ such that

$$ \sigma^1(\ell, \nu) \in \underset{(\ell, \nu) \to (\ell', \nu')}{\operatorname{arginf}}_{\epsilon/K} (t \operatorname{wt}(\ell) + \operatorname{wt}(\delta) + \operatorname{dVal}_{\ell', \nu'}) \quad (5.1) $$

This set is non empty since dVal is a fixpoint of operator $\mathcal{F}$ in this case. Moreover, knowing that the mapping $\text{dVal}_\ell$ is piecewise affine by the results shown in [BMR17], it is possible to choose $\sigma^1$ so that it fulfils the measurability (even piecewise continuity) conditions of Hypothesis 3.3. More precisely, we can consider it to take the same kind of decision for all configurations of a same cell: same transition, and either no delay or a delay jumping to the same border of cell.

The strategy $\sigma^1$ thus built makes a small error wrt the optimal at each step. But once again strongly relying on the divergence of the WTG, we can nevertheless show that $\sigma^1$ is fake-$\epsilon$/K-optimal wrt the deterministic value.

**Lemma 5.6.** The strategy $\sigma^1$ of Min is fake-$\epsilon$/K-optimal wrt the deterministic value, i.e.

(1) each finite play $\rho$ conforming to $\sigma^1$ from $(\ell, \nu)$ and reaching the target has a cumulated weight at most $\text{dVal}_{\ell,\nu} + |\rho|\epsilon/K$: in particular, if $\text{dVal}_{\ell,\nu} = -\infty$, no such play exists;

(2) each finite play conforming to $\sigma^1$ following a cycle in the region game $\mathcal{R}(\mathcal{G})$ of length at least $|L|\alpha + 1$ has a cumulated weight at most $-1$.

*Proof.* We show independently the two properties.

(1) If $\text{dVal}_{\ell,\nu} = -\infty$, we have already seen before that no such play exists. We thus restrict ourselves to considering configurations of value different from $-\infty$ in the following. We
then reason by induction on the length of the plays $\rho$. If $|\rho| = 0$, $\ell \in L_T$ and

$$ \mathrm{wt}(\rho) = 0 = \mathrm{dVal}_{\ell,\nu} \le \mathrm{dVal}_{\ell,\nu} + 0 \times \frac{\varepsilon}{K}. $$

If $|\rho| = n > 0$, we write $\rho = (\ell, \nu) \xrightarrow{\delta, t} (\ell', \nu') \dots$, and let $\rho'$ be the play following $\rho$ from $(\ell', \nu')$. By definition, we have $\mathrm{wt}(\rho) = t \mathrm{wt}(\ell) + \mathrm{wt}(\delta) + \mathrm{wt}(\rho')$. By induction hypothesis, we obtain

$$ \mathrm{wt}(\rho) \le t \mathrm{wt}(\ell) + \mathrm{wt}(\delta) + \mathrm{dVal}_{\ell',\nu'} + (n-1)\frac{\varepsilon}{K} \quad (5.2) $$

First, we suppose that $\ell \in L_{\mathrm{Max}}$, then we can rewrite (5.2) (by applying the supremum) as

$$ \mathrm{wt}(\rho) \le \sup_{(\ell, \nu) \xrightarrow{\delta, t} (\ell', \nu')} (t \mathrm{wt}(\ell) + \mathrm{wt}(\delta) + \mathrm{dVal}_{\ell', \nu'}) + (n-1)\frac{\varepsilon}{K}. $$

Moreover, since $\mathrm{dVal}$ is a fixpoint of $\mathcal{F}$ (by Lemma 5.3), then

$$ \mathrm{wt}(\rho) \le \mathrm{dVal}_{\ell,\nu} + (n-1)\frac{\varepsilon}{K} \le \mathrm{dVal}_{\ell,\nu} + n\frac{\varepsilon}{K}. $$

Otherwise, we suppose that $\ell \in L_{\mathrm{Min}}$, then, using the definition of $\sigma^1$ given in (5.1), we can rewrite (5.2) as

$$ \mathrm{wt}(\rho) \le \inf_{(\ell, \nu) \xrightarrow{\delta, t} (\ell', \nu')} (t \mathrm{wt}(\ell) + \mathrm{wt}(\delta) + \mathrm{dVal}_{\ell', \nu'}) + \frac{\varepsilon}{K} + (n-1)\frac{\varepsilon}{K} $$

We conclude, since $\mathrm{dVal}$ is a fixpoint of $\mathcal{F}$ (by Lemma 5.3), that $\mathrm{wt}(\rho) \le \mathrm{dVal}_{\ell,\nu} + n\frac{\varepsilon}{K}$.

(2) The second property is trivial (and already discussed before) when the strategy $\sigma^1$ is chosen according to the case of values $-\infty$. We therefore once again suppose that there are no remaining configurations of value $-\infty$ in this proof.

We first show that, for all edges $(\ell, \nu) \xrightarrow{\delta, t} (\ell', \nu')$ conforming to $\sigma^1$, we have

$$ \mathrm{dVal}_{\ell,\nu} \ge t \mathrm{wt}(\ell) + \mathrm{wt}(\delta) + \mathrm{dVal}_{\ell',\nu'} - \frac{\varepsilon}{K} \quad (5.3) $$

If $\ell \in L_{\mathrm{Min}}$, since $\mathrm{dVal}$ is a fixpoint of $\mathcal{F}$ (by Lemma 5.3), we have

$$ \mathrm{dVal}_{\ell,\nu} = \inf_{(\ell, \nu) \xrightarrow{\delta_1, t_1} (\ell_1, \nu_1)} (t_1 \mathrm{wt}(\ell) + \mathrm{wt}(\delta_1) + \mathrm{dVal}_{\ell_1, \nu_1}). $$

Then, by definition of $(\delta, t)$ chosen by $\sigma^1$,

$$ \mathrm{dVal}_{\ell,\nu} \ge t \mathrm{wt}(\ell) + \mathrm{wt}(\delta) + \mathrm{dVal}_{\ell',\nu'} - \frac{\varepsilon}{K}. $$

If $\ell \in L_{\mathrm{Max}}$, since $\mathrm{dVal}$ is a fixpoint of $\mathcal{F}$ (by Lemma 5.3), we have

$$ \mathrm{dVal}_{\ell,\nu} = \sup_{(\ell, \nu) \xrightarrow{\delta_1, t_1} (\ell_1, \nu_1)} (t_1 \mathrm{wt}(\ell) + \mathrm{wt}(\delta_1) + \mathrm{dVal}_{\ell_1, \nu_1}). $$

In particular, for the pair $(\delta, t)$ chosen in $\rho$, we have

$$ \mathrm{dVal}_{\ell,\nu} \ge t \mathrm{wt}(\ell) + \mathrm{wt}(\delta) + \mathrm{dVal}_{\ell',\nu'} \ge t \mathrm{wt}(\ell) + \mathrm{wt}(\delta) + \mathrm{dVal}_{\ell',\nu'} - \frac{\varepsilon}{K}. $$

Then, let $\pi$ be a cyclic path in $\mathcal{R}(\mathcal{G})$ of length at least $|L|\alpha + 1$, and $\rho$ a finite play following $\pi$ and conforming to $\sigma^1$. It goes through only states of a single SCC of $\mathcal{R}(\mathcal{G})$, that is either positive or negative, by divergence of the WTG $\mathcal{G}$. We show that this SCC is necessarily negative, therefore proving $\mathrm{wt}_{\Sigma}(\rho) \le -1$. Suppose, in the contrary, that the SCC is positive.
First, since $\pi$ has length at least $|L|\alpha + 1$, it must go through the same pair of location and cell of dVal (remember that dVal is piecewise affine, and we have called cell each piece where it is affine) at least twice. Consider the cycle $\pi'$ (of length at most $|L|\alpha$) obtained by considering the part of $\pi$ between these two occurrences, and $\rho'$ a corresponding finite play starting in a configuration $(\ell, \nu)$, ending in $(\ell, \nu')$ (with $\nu$ and $\nu'$ in the same cell). Since the SCC is positive, $\rho'$ has weight at least 1. By the definition of $\sigma^1$ taking a uniform decision on each cell, we can mimic this loop once again from $(\ell, \nu')$, for $2\lceil\beta\rceil$ times, where $\beta$ is the maximum over the cells $c$ (where dVal is not $-\infty$) of the differences $\sup_c dVal - \inf_c dVal$, that is finite since each cell is compact. The obtained play $\rho''$ has weight at least $2\lceil\beta\rceil$ (since it is decomposed as $2\lceil\beta\rceil$ cycles in a positive SCC), and length at most $2\lceil\beta\rceil|L|\alpha$.

By summing up all the inequalities given by (5.3) along the play $\rho''$ (from $(\ell, \nu)$ to $(\ell, \nu'')$), and by simplifying the result, we obtain that

$$ \mathrm{wt}_{\Sigma}(\rho'') \leq \mathrm{dVal}_{\ell,\nu} - \mathrm{dVal}_{\ell,\nu''} + \frac{\varepsilon}{K}|\rho''| \leq \mathrm{dVal}_{\ell,\nu} - \mathrm{dVal}_{\ell,\nu''} + \frac{\varepsilon}{K}2\lceil\beta\rceil|L|\alpha. $$

However, by definition of $\beta$ (the maximum difference of values in a cell), we obtain

$$ \mathrm{wt}_{\Sigma}(\rho'') \leq \lceil\beta\rceil\left(1 + \frac{\varepsilon}{K}2|L|\alpha\right) \leq \lceil\beta\rceil(1 + 2\varepsilon) < 2\lceil\beta\rceil $$

since $K \geq 2|L|\alpha$ and $\varepsilon < 1/2$. This contradicts the fact that $\rho''$ has weight at least $2\lceil\beta\rceil$, and concludes the proof of the second item. $\square$

Now, we conclude the proof of Theorem 5.5.

*Proof of Theorem 5.5.* We start by showing that the switching strategy $\sigma$ defined above by the triplet $(\sigma^1, \sigma^2, K)$ is a proper smooth deterministic strategy. First, $\sigma$ is a smooth deterministic strategy since $\sigma^1$ and $\sigma^2$ satisfy Hypothesis 3.3 by construction. Now, $\sigma$ is also proper (by Proposition 3.11) since it satisfies the second condition of Hypothesis 3.9: by letting $m = K + |\mathcal{R}(G)| + 1$, the probability to reach a target location in at most $m$ steps is 1.

Now, we prove that for all configurations $(\ell, \nu)$, we have

$$ \mathrm{dVal}_{\ell,\nu}^{\sigma} \leq \max(-N, \mathrm{dVal}_{\ell,\nu}) + \varepsilon. $$

Let $\rho$ be a play conforming to $\sigma$ from $(\ell, \nu)$ that reaches the target $(\ell_t, \nu_t)$. We distinguish two cases according to the length of $\rho$. First, we suppose that $|\rho| \leq K$, then $\rho$ is only conforming to $\sigma^1$ which is a fake-$\varepsilon/K$-optimal strategy. Moreover, as $\rho$ reaches the target, $\mathrm{dVal}_{\ell,\nu}$ is finite. Indeed if $\mathrm{dVal}_{\ell,\nu} = -\infty$, $\sigma^1$ is built with a Büchi objective and cannot reach the target. In particular, $\mathrm{wt}_{\Sigma}(\rho) \leq \mathrm{dVal}_{\ell,\nu} + |\rho|^{\varepsilon/K}$, and we conclude since $|\rho| \leq K$

$$ \mathrm{wt}_{\Sigma}(\rho) \leq \mathrm{dVal}_{\ell,\nu} + \varepsilon \leq \max(-N, \mathrm{dVal}_{\ell,\nu}) + \varepsilon. $$

Otherwise, we suppose that $|\rho| \geq K$, then we can decompose $\rho$ as $\rho_1$ conforming to $\sigma^1$, and followed by $\rho_2$ conforming to $\sigma^2$ with $|\rho_1| = K$. As $\rho_2$ is conforming to $\sigma^2$, an attractor strategy on the region game $\mathcal{R}(G)$, it is acyclic in $\mathcal{R}(G)$, so $|\rho_2| \leq |\mathcal{R}(G)|$. In particular,

$$ \mathrm{wt}_{\Sigma}(\rho_2) \leq w_{\max}^{e}|\mathcal{R}(G)|. $$

As $|\rho_1| = K$, by definition of $K = (w_{\max}^e|\mathcal{R}(G)|(|L|\alpha + 2) + N)(|\mathcal{R}(G)|(|L|\alpha + 1) + 1)$, $\rho_1$ goes at least $(w_{\max}^e|\mathcal{R}(G)|(|L|\alpha + 2) + N)(|L|\alpha + 1)$ times through the same pair of location and region, and thus contains at least $w_{\max}^e|\mathcal{R}(G)|(|L|\alpha + 2) + N$ region cycles of length at least $|L|\alpha + 1$. Moreover, all of them are conforming to $\sigma^1$ that is a fake-$\varepsilon/K$-optimal strategy. In
particular, each cycle has a weight at most $-1$, and the weight of all cycles of $\rho_1$ is therefore at most $-w_{\max}^e |\mathcal{R}(\mathcal{G})|(|L|\alpha + 2) - N$. Moreover, $\rho_1$ has at most $|\mathcal{R}(\mathcal{G})|(|L|\alpha + 1)$ remaining edges (otherwise it would contain a region cycle of length at least $|L|\alpha + 1$), once the region cycles are removed. The weight of one of these edges is at most $w_{\max}^e$, so the weight of this set of edges is at most $w_{\max}^e |\mathcal{R}(\mathcal{G})|(|L|\alpha + 1)$. We can deduce that

$$ \mathrm{wt}_{\Sigma}(\rho_1) \le -w_{\max}^e |\mathcal{R}(\mathcal{G})|(|L|\alpha + 2) - N + w_{\max}^e |\mathcal{R}(\mathcal{G})|(|L|\alpha + 1) = -w_{\max}^e |\mathcal{R}(\mathcal{G})| - N. $$

So, we can deduce that

$$ \mathrm{wt}_{\Sigma}(\rho) = \mathrm{wt}_{\Sigma}(\rho_1) + \mathrm{wt}_{\Sigma}(\rho_2) \le -w_{\max}^e |\mathcal{R}(\mathcal{G})| - N + w_{\max}^e |\mathcal{R}(\mathcal{G})| = -N. $$

In particular, we obtain that $\mathrm{wt}_{\Sigma}(\rho) \le \max(-N, \mathrm{dVal}_{\ell,\nu}) + \varepsilon$. To conclude the proof, we remark that $\rho$ is a play reaching the target, so $\mathrm{wt}(\rho) = \mathrm{wt}_{\Sigma}(\rho) \le \max(-N, \mathrm{dVal}_{\ell,\nu}) + \varepsilon$. $\square$

**5.2. Memoryless strategies for Max.** In a divergent WTG, we can prove that Max has an $\varepsilon$-optimal memoryless smooth deterministic strategy for all $\varepsilon > 0$. To make this proof, we take the point of view of Max; looking for good strategies for this other player. This is possible since all WTGs are determined with respect to the deterministic value. We may thus associate a deterministic value with any deterministic strategy $\tau$ of Max:

$$ \mathrm{dVal}_{\ell,\nu}^{\tau} = \inf_{\sigma \in \mathrm{dStrat}_{\mathrm{Min}}} \mathrm{wt}(\mathrm{Play}((\ell, \nu), \sigma, \tau)). $$

Then, the deterministic strategy $\tau$ is $\varepsilon$-optimal wrt the deterministic value if $\mathrm{dVal}_{\ell,\nu}^{\tau} \ge \mathrm{dVal}_{\ell,\nu} - \varepsilon$ for all configurations $(\ell, \nu)$.

As Max does not wish to go to the target, we show that no switch is necessary to play $\varepsilon$-optimally: memoryless strategies are sufficient to guarantee a value as close as wanted to the deterministic value. For a configuration with a value equal to $-\infty$, all the deterministic strategies for Max are equivalent, that is, they are all equally bad. Without loss of generality, we can therefore suppose that there are no configurations in $\mathcal{G}$ with a value equal to $-\infty$. Then, it is shown in [BMR17] that remaining values are bounded in absolute value by $w_{\max}^e |\mathcal{R}(\mathcal{G})|$, since optimal plays have no cycles. We use that fact to build a memoryless deterministic strategy $\tau$ analogous to strategy $\sigma^1$ before:

**Theorem 5.7.** In a divergent WTG, there exists a memoryless smooth deterministic $\varepsilon$-optimal strategy for player Max wrt the deterministic value.

Once again, Max will use the fact that $\mathrm{dVal}$ is a fixpoint of operator $\mathcal{F}$ (once removed configurations of value $-\infty$). We must still accomodate small errors at each step, because of the guards on clocks. Similarly to the switching parameter $K$ for the switching strategy (with $N = 0$), we let $K = w_{\max}^e |\mathcal{R}(\mathcal{G})|(|L|\alpha + 2)(|\mathcal{R}(\mathcal{G})|(|L|\alpha + 1) + 1)$. We use the $\mathrm{argsup}^\varepsilon$ operator, analogously to $\mathrm{arginf}^\varepsilon$, defined for all mappings $f: A \to \mathbb{R}$ and $B \subseteq A$ by $\mathrm{argsup}_B^\varepsilon f = \{a \in B | f(a) \ge \mathrm{sup}_B f - \varepsilon\}$. Then, for all configurations $(\ell, \nu) \in L_{\mathrm{Max}} \times \mathbb{R}_{\ge 0}^\chi$, we choose $\tau(\ell, \nu)$ as a pair $(\delta, t)$ such that

$$ \tau(\ell, \nu) \in \mathrm{argsup}_{(\ell, \nu) \xrightarrow{\delta, t} (\ell', \nu')}^{\varepsilon/K} (t \mathrm{wt}(\ell) + \mathrm{wt}(\delta) + \mathrm{dVal}_{\ell', \nu'}) \quad (5.4) $$

with similar smooth assumptions as for $\sigma^1$ before. In a completely symmetrical way as for Lemma 5.6, we show that $\tau$ satisfies the following useful properties:

**Lemma 5.8.** The strategy $\tau$ satisfies the following properties:
(1) each finite play $\rho$ conforming to $\tau$ from $(\ell, \nu)$ and reaching the target has a cumulated weight at least $\mathrm{dVal}_{\ell,\nu} - |\rho|\varepsilon/K$;

(2) each finite play conforming to $\tau$, that follows a cycle in the region game $\mathcal{R}(\mathcal{G})$ of length at least $|L|\alpha + 1$, has a cumulated weight at least 1.

Now, we have tools to prove that $\tau$ is an $\varepsilon$-optimal strategy for Max with respect to the deterministic value from $(\ell, \nu)$. In other words, we show that $\mathrm{dVal}_{\ell,\nu}^\tau \ge \mathrm{dVal}_{\ell,\nu} - \varepsilon$.

*Proof of Theorem 5.7.* Let $\rho$ be a play conforming to $\tau$ from $(\ell, \nu)$. We distinguish two cases according to the length of $\rho$. First, we suppose that $|\rho| \le K$, then, by Lemma 5.8.1, we have

$$ \mathrm{wt}(\rho) \ge \mathrm{dVal}_{\ell,\nu} - \frac{\varepsilon}{K} |\rho| \ge \mathrm{dVal}_{\ell,\nu} - \varepsilon. $$

Otherwise, we suppose that $|\rho| > K$, then by definition of $K = w_{\max}^e|\mathcal{R}(\mathcal{G})|(|L|\alpha + 2)(|\mathcal{R}(\mathcal{G})|(|L|\alpha + 1) + 1)$, $\rho$ contains at least $w_{\max}^e|\mathcal{R}(\mathcal{G})|(|L|\alpha + 2)$ cycles of length at least $|L|\alpha + 1$ in $\mathcal{R}(\mathcal{G})$. By Lemma 5.8.(2), all of these cycles have a cumulated weight at least 1. So, the cumulated weight of $\rho$ induced by the cycles in $\mathcal{R}(\mathcal{G})$ is at least $w_{\max}^e|\mathcal{R}(\mathcal{G})|(|L|\alpha + 2)$. Moreover, $\rho$ has at most $|\mathcal{R}(\mathcal{G})|(|L|\alpha + 1)$ remaining edges, once the region cycles are removed. The weight of each of these edges is at least $-w_{\max}^e$, so the weight of this set of edges is at least $-w_{\max}^e|\mathcal{R}(\mathcal{G})|(|L|\alpha + 1)$. So, we can deduce that

$$ \mathrm{wt}(\rho) \ge w_{\max}^e |\mathcal{R}(\mathcal{G})|(|L|\alpha + 2) - w_{\max}^e |\mathcal{R}(\mathcal{G})|(|L|\alpha + 1) = w_{\max}^e |\mathcal{R}(\mathcal{G})| \ge \mathrm{dVal}_{\ell,\nu}. $$

In particular, we obtain that $\mathrm{wt}(\rho) \ge \mathrm{dVal}_{\ell,\nu} - \varepsilon$.

<figure><img src="image_11.png" /></figure>

With the existence of the (proper) smooth deterministic $\varepsilon$-optimal strategies for both players with respect to the deterministic value, we can deduce that divergent WTGs are determined with respect to the smooth deterministic value and this value is equal to the deterministic one. Finally, we will deduce that divergent WTGs are determined with respect to the stochastic value, and the stochastic and (smooth) deterministic values are equal:

**Corollary 5.9.** In all divergent WTGs, for all $(\ell, \nu)$,

$$ \mathrm{dVal}_{\ell,\nu} = \underline{\mathrm{dVal}}_{\ell,\nu} = \overline{\mathrm{dVal}}_{\ell,\nu} = \underline{\mathrm{Val}}_{\ell,\nu} = \overline{\mathrm{Val}}_{\ell,\nu}. $$

*Proof.* Let $\varepsilon > 0$, there exists $\sigma \in \mathrm{sdStrat}_{\mathrm{Min}}^{\mathrm{p}}$ and $\tau \in \mathrm{sdStrat}_{\mathrm{Max}}$ such that

$$ \mathrm{dVal}_{\ell,\nu}^{\sigma} - \varepsilon \le \mathrm{dVal} \le \mathrm{dVal}_{\ell,\nu}^{\tau} + \varepsilon $$

by Theorem 5.5 and Theorem 5.7. First, since $\mathrm{sdStrat}_{\mathrm{Max}} \subseteq \mathrm{dStrat}_{\mathrm{Max}}$, we deduce that

$$ \overline{\mathrm{dVal}}_{\ell,\nu} \le \sup_{\tau \in \mathrm{sdStrat}_{\mathrm{Max}}} \mathrm{wt}(\mathrm{Play}((\ell, \nu), \sigma, \tau)) \le \sup_{\tau \in \mathrm{dStrat}_{\mathrm{Max}}} \mathrm{wt}(\mathrm{Play}((\ell, \nu), \sigma, \tau)) = \mathrm{dVal}_{\ell,\nu}^{\sigma} - \varepsilon. $$

Next, with the same reasoning, since $\mathrm{sdStrat}_{\mathrm{Min}}^{\mathrm{p}} \subseteq \mathrm{dStrat}_{\mathrm{Min}}$, we deduce that

$$ \mathrm{dVal}_{\ell,\nu}^{\tau} - \varepsilon = \inf_{\sigma \in \mathrm{dStrat}_{\mathrm{Min}}} \mathrm{wt}(\mathrm{Play}((\ell, \nu), \sigma, \tau)) \le \inf_{\sigma \in \mathrm{sdStrat}_{\mathrm{Min}}^{\mathrm{p}}} \mathrm{wt}(\mathrm{Play}((\ell, \nu), \sigma, \tau)) \le \underline{\mathrm{dVal}}_{\ell,\nu}. $$

Thus, $\underline{\mathrm{dVal}}_{\ell,\nu} = \overline{\mathrm{dVal}}_{\ell,\nu}$, since $\underline{\mathrm{dVal}}_{\ell,\nu} \le \overline{\mathrm{dVal}}_{\ell,\nu}$. Finally, we conclude the proof by applying Theorem 4.1:

$$ \underline{\mathrm{dVal}}_{\ell,\nu} \le \underline{\mathrm{Val}}_{\ell,\nu} \le \overline{\mathrm{Val}}_{\ell,\nu} \le \underline{\mathrm{sdVal}}_{\ell,\nu} = \underline{\mathrm{dVal}}_{\ell,\nu}. $$

<figure><img src="image_12.png" /></figure>
## 6. MEMORYLESS VALUE IN DIVERGENT WEIGHTED TIMED GAMES

We finally study the memoryless values of divergent WTGs showing that memory can be fully emulated with stochastic choices, and vice versa. Moreover, we show that divergent WTGs are determined with respect to the memoryless value (as we obtained previously for the stochastic value).

**Theorem 6.1.** In all divergent WTGs, for all $(\ell, \nu)$, $dVal_{\ell,\nu} = \overline{mVal}_{\ell,\nu} = \underline{mVal}_{\ell,\nu}$.

The proof is decomposed into two inequalities:

* we show in Lemma 6.2 that $dVal_{\ell,\nu} \le \underline{mVal}_{\ell,\nu}$, relying on the existence of a $\varepsilon$-optimal deterministic and memoryless strategy of Max against the deterministic value (Theorem 5.7);

* we show in Lemma 6.3 that memoryless stochastic strategies can emulate deterministic ones: $\overline{mVal}_{\ell,\nu} \le dVal_{\ell,\nu}$.

Combined with the fact that $\underline{mVal}_{\ell,\nu} \le \overline{mVal}_{\ell,\nu}$, we indeed obtain the desired equalities.

As shown in Example 4.7, the theorem does not hold for all WTGs, and the divergence property is therefore useful (though it might be possible to weaken it).

We start by showing that the deterministic value is at most equal to the memoryless lower-value:

**Lemma 6.2.** In all divergent WTGs $\mathcal{G}$, for all locations $\ell$ and valuations $\nu$, $dVal_{\ell,\nu} \le \underline{mVal}_{\ell,\nu}$.

*Proof.* Let $\varepsilon > 0$. By Theorem 5.7, Max has a memoryless deterministic $\varepsilon$-optimal strategy $\tau$ for the deterministic value. Against any deterministic strategy of Min, from $(\ell, \nu)$, it guarantees a weight at least $dVal_{\ell,\nu} - \varepsilon$.

Let $\eta$ be any memoryless proper strategy of Min. Every play conforming to $\eta$ and $\tau$ has a weight at least $dVal_{\ell,\nu} - \varepsilon$ (since it is conforming to $\tau$), so that, by definition of the expectation,

$$ \mathbb{E}_{\ell,\nu}^{\eta,\tau} = \int_{\rho} \mathrm{wt}(\rho) d\mathbb{P}_{\ell,\nu}^{\eta,\tau}(\rho) \ge \mathrm{dVal}_{\ell,\nu} - \varepsilon $$

Since this inequality holds for all proper strategies of Min, we deduce that

$$ \inf_{\eta \in \mathrm{mStrat}_{\mathrm{Min}}^{\mathrm{p}}} \mathbb{E}_{\ell,\nu}^{\eta,\tau} \ge \mathrm{dVal}_{\ell,\nu} - \varepsilon. $$

By taking the supremum over all memoryless strategies of Max (that contain the memoryless and deterministic strategy $\tau$), we have

$$ \sup_{\theta \in \mathrm{mStrat}_{\mathrm{Max}}} \inf_{\eta \in \mathrm{mStrat}_{\mathrm{Min}}^{\mathrm{p}}} \mathbb{E}_{\ell,\nu}^{\eta,\theta} \ge \mathrm{dVal}_{\ell,\nu} - \varepsilon. $$

In particular, $\underline{mVal}_{\ell,\nu} \ge \underline{dVal}_{\ell,\nu} - \varepsilon$. To conclude, we remark that this inequality holds for all $\varepsilon > 0$, and thus also when $\varepsilon$ is set to 0. $\square$

The most technical inequality is the remaining one, showing that we can simulate deterministic strategies with memoryless strategies:

**Lemma 6.3.** In all divergent WTGs $\mathcal{G}$, for all locations $\ell$ and valuations $\nu$, $\overline{mVal}_{\ell,\nu} \le \underline{dVal}_{\ell,\nu}$.

We prove this result in the rest of this section. To do so, we build a memoryless strategy of Min at least as good as a deterministic strategy. By Theorem 5.5, we can start from a switching strategy for Min. For $N \in \mathbb{N}$ and $\varepsilon > 0$, we thus consider a switching strategy $\sigma = (\sigma^1, \sigma^2, K)$ of value $dVal_{\ell,\nu}^{\sigma} \le \max(-N, dVal_{\ell,\nu}) + \varepsilon$, and simulate it with a memoryless
strategy for Min, denoted $η^p$, with a probability parameter $p \in (0, 1)$. This new strategy is a probabilistic superposition of the two memoryless deterministic strategies $\sigma^1$ and $\sigma^2$.

**Definition of $η^p$**. The definition of $η^p(\ell, \nu)$, with $\ell \in L_{\text{Min}}$, depends on the sign of the SCC containing the location $(\ell, r)$, with $r$ the region of $\nu$, of the region game $\mathcal{R}(\mathcal{G})$. In a positive SCC, Min always chooses to play $\sigma^1$, thus looking for a negative cycle in the next SCCs (in topological order) if any, i.e. we let $η^p(\ell, \nu) = \text{Dirac}_{\sigma^1(\ell, \nu)}$. In a negative SCC, Min chooses to play $\sigma^1$ with probability $p$, and $\sigma^2$ with probability $1-p$, i.e. we let $η^p(\ell, \nu) = p \times \text{Dirac}_{\sigma^1(\ell, \nu)} + (1-p) \times \text{Dirac}_{\sigma^2(\ell, \nu)}$.

These choices can be decomposed as first choosing a transition and then a delay as follows: letting $(\delta_1, t_1) = \sigma^1(\ell, \nu)$, and $(\delta_2, t_2) = \sigma^2(\ell, \nu)$, we define

$$ \eta_{\Delta}^{p}(\ell, \nu) = \begin{cases} \text{Dirac}_{\delta_1} & \text{if } \ell \text{ is in a positive SCC} \\ p \times \text{Dirac}_{\delta_1} + (1-p) \times \text{Dirac}_{\delta_2} & \text{otherwise} \end{cases} $$

and

$$ \eta_{\mathbb{R}^+}^{p}(\ell, \nu)(\delta) = \begin{cases} \text{Dirac}_{t_1} & \text{if } \ell \text{ is in a positive SCC} \\ p \times \text{Dirac}_{t_1} + (1-p) \times \text{Dirac}_{t_2} & \text{if } \ell \text{ is in a negative SCC, and } \delta_1 = \delta_2 \\ \text{Dirac}_{t_1} & \text{if } \ell \text{ is in a negative SCC, and } \delta = \delta_1 \\ \text{Dirac}_{t_2} & \text{if } \ell \text{ is in a negative SCC, and } \delta = \delta_2 \end{cases} $$

Theorem 5.5 ensuring that strategies $\sigma^1$ and $\sigma^2$ are smooth, the superposition $η^p$ is also smooth. Moreover, it is also proper:

**Lemma 6.4.** For all $p \in (0, 1)$, the strategy $η^p$ is proper.

*Proof.* We prove that $η^p$ satisfies the second item of Hypothesis 3.9, with $m = |\mathcal{R}(\mathcal{G})|$ and $\alpha = (1-p)^{m+1}$. Let $\theta \in \text{Strat}_{\text{Max}}$, and $\rho_0$ a finite play. We prove that $\mathbb{P}_{\rho_0}^{\eta^p, \theta}(\bigcup_{n \le m} \text{TPlays}_{\rho_0}^n) \ge \alpha$. Not reaching the target in at most $m$ steps is equivalent to having a prefix of length $m+1$, so that $\mathbb{P}_{\rho_0}^{\eta^p, \theta}(\bigcup_{n \le m} \text{TPlays}_{\rho_0}^n) = 1 - \mathbb{P}_{\rho_0}^{\eta^p, \theta}(\bigcup_{\pi \parallel \pi = m+1} \text{Cyl}_{\rho_0}(\pi))$. We thus prove that $\mathbb{P}_{\rho_0}^{\eta^p, \theta}(\bigcup_{\pi \parallel \pi = m+1} \text{Cyl}_{\rho_0}(\pi)) \le 1 - \alpha$.

Since $m = |\mathcal{R}(\mathcal{G})|$, a play is in $\bigcup_{\pi \parallel \pi = m+1} \text{Cyl}_{\rho_0}(\pi)$ if and only if it is of the form $\rho_0 \rho \rho'$ with $|\rho| = m+1$: in particular, $\rho$ contains a cycle in the region game, so cannot be conforming to the attractor strategy $\sigma_2$. As a consequence, $\rho$ goes through a transition played by $\sigma_1$, chosen with probability $p$ in $η^p$. Given $k \ge 1$, calling $S_{\rho_0}^k$ the set of plays $\rho_0 \rho \rho'$ with $\rho$ of length $k$ containing a transition of probability $p$ chosen by $η^p$, we have

$$ \mathbb{P}_{\rho_0}^{\eta^p, \theta}(\bigcup_{\pi \parallel \pi = m+1} \text{Cyl}_{\rho_0}(\pi)) = \mathbb{P}_{\rho_0}^{\eta^p, \theta}(S_{\rho_0}^{m+1}). $$

We conclude by showing that $\mathbb{P}_{\rho_0}^{\eta^p, \theta}(S_{\rho_0}^k) \le 1 - (1-p)^k$ holds for all $k \ge 1$ by induction. We let $\pi_0$ be the path followed by $\rho_0$.

When $k=1$, the transition of every play in $S_{\rho_0}^1$ after the common prefix $\rho_0$ is chosen by Min with a probability $p$. Thus, $\rho_0 \in \text{FPlays}_{\text{Min}}$, $η^p(\rho_0) = p \text{Dirac}_{(\delta_0, t_0)} + (1-p) \text{Dirac}_{(\delta'_0, t'_0)}$ with $(\delta_0, t_0) \ne (\delta'_0, t'_0)$ and the transition of every play in $S_{\rho_0}^1$ after the common prefix $\rho_0$ is
<figure><img src="image_13.png" /><figcaption>Figure 7: The partition of $S_{\rho_0}^k$ when $\rho_0 \in \text{FPlays}_{\text{Min}}$.</figcaption></figure>

($\delta_0, t_0$). Indeed, $S_{\rho_0}^1 = \text{Cyl}_{\rho_0}(\pi_0\delta_0, \mathbb{R}_{\ge 0}^{\vert\pi_0\vert} \times \{t_0\})$. As a consequence,

$$ 
\begin{align*}
\mathbb{P}_{\rho_0}^{\eta^p, \theta}(S_{\rho_0}^1) &= \mathbb{P}_{\rho_0}^{\eta^p, \theta}(\text{Cyl}_{\rho_0}(\pi_0\delta_0, \mathbb{R}_{\ge 0}^{\vert\pi_0\vert} \times \{t_0\})) \\
&= \eta^p(\rho_0)(\delta_0, t_0) \times \mathbb{P}_{\rho_0[\delta_0, t_0]}^{\eta^p, \theta}(\text{Cyl}_{\rho_0[\delta_0, t_0]}(\pi_0\delta_0, \mathbb{R}_{\ge 0}^{\vert\pi_0\vert} \times \{t_0\})) \\
&= p \times 1 = 1 - (1-p)^1
\end{align*}
$$

When $k \ge 2$, we distinguish three cases.

* If $\rho_0 \in \text{FPlays}_{\text{Min}}$ and $\eta^p(\rho_0) = p\text{Dirac}_{(\delta_0, t_0)} + (1-p)\text{Dirac}_{(\delta'_0, t'_0)}$ with $(\delta_0, t_0) \ne (\delta'_0, t'_0)$, we have (as illustrated in Figure 7)

$$ S_{\rho_0}^k = \text{Cyl}_{\rho_0}(\pi_0\delta_0, \mathbb{R}_{\ge 0}^{\vert\pi_0\vert} \times \{t_0\}) \cup S_{\rho_0[\delta'_0, t'_0]}^{k-1}. $$

As before, we have $\mathbb{P}_{\rho_0}^{\eta^p, \theta}(\text{Cyl}_{\rho_0}(\pi_0\delta_0, \mathbb{R}_{\ge 0}^{\vert\pi_0\vert} \times \{t_0\})) = p$. We show that

$$ \mathbb{P}_{\rho_0}^{\eta^p, \theta}(S_{\rho_0[\delta'_0, t'_0]}^{k-1}) = (1-p)\mathbb{P}_{\rho_0[\delta'_0, t'_0]}^{\eta^p, \theta}(S_{\rho_0[\delta'_0, t'_0]}^{k-1}) \quad (6.1) $$

and, by induction hypothesis, we deduce that $\mathbb{P}_{\rho_0[\delta'_0, t'_0]}^{\eta^p, \theta}(S_{\rho_0[\delta'_0, t'_0]}^{k-1}) \le 1 - (1-p)^{k-1}$. In conclusion, we obtain

$$ 
\begin{align*}
\mathbb{P}_{\rho_0}^{\eta^p, \theta}(S_{\rho_0}^k) &= p + (1-p)\mathbb{P}_{\rho_0[\delta'_0, t'_0]}^{\eta^p, \theta}(S_{\rho_0[\delta'_0, t'_0]}^{k-1}) \\
&\le p + (1-p)(1 - (1-p)^{k-1}) = 1 - (1-p)^k.
\end{align*}
$$

Now, we show (6.1): to do it, we must come back to the definition of the probabilities with respect to cylinders. First, $S_{\rho_0[\delta'_0, t'_0]}^{k-1}$ can be decomposed a union of cylinders over some paths $\pi_0\delta'_0\pi$ with $|\pi| = k-1$. For such a path $\pi$, let $C_\pi$ be the set of sequences of delays of plays appearing in $S_{\rho_0[\delta'_0, t'_0]}^{k-1}$ so that

$$ S_{\rho_0[\delta'_0, t'_0]}^{k-1} = \bigcup_{|\pi|=k-1} \text{Cyl}_{\rho_0}(\pi_0\delta'_0\pi, C_\pi) = \bigcup_{|\pi|=k-1} \text{Cyl}_{\rho_0[\delta'_0, t'_0]}(\pi_0\delta'_0\pi, C_\pi). $$

The set $C_\pi$ is Lebesgue-measurable since it can be obtained as a finite unions and intersections of the constraints appearing in $\eta^p_{\mathbb{R}_+}$ (and thus in $\sigma_1$ or $\sigma_2$) or $\theta_{\mathbb{R}_+}$, that are all Lebesgue-measurable by Hypothesis 3.3 (the explanation of this decomposition is given in
Appendix D). Thus,

$$
\begin{align*}
\mathbb{P}_{\rho_0}^{\eta^p, \theta}(S_{\rho_0[\delta'_0, t'_0]}^{k-1}) &= \sum_{|\pi|=k-1} \mathbb{P}_{\rho_0}^{\eta^p, \theta}(\mathrm{Cyl}_{\rho_0}(\pi_0 \delta'_0 \pi, C_\pi)) \\
&= \sum_{|\pi|=k-1} \eta^p(\rho_0)(\delta'_0, t'_0) \times \mathbb{P}_{\rho_0[\delta'_0, t'_0]}^{\eta^p, \theta}(\mathrm{Cyl}_{\rho_0[\delta'_0, t'_0]}(\pi_0 \delta'_0 \pi, C_\pi)) \\
&= (1-p) \sum_{|\pi|=k-1} \mathbb{P}_{\rho_0[\delta'_0, t'_0]}^{\eta^p, \theta}(\mathrm{Cyl}_{\rho_0[\delta'_0, t'_0]}(\pi_0 \delta'_0 \pi, C_\pi)) \\
&= (1-p) \mathbb{P}_{\rho_0[\delta'_0, t'_0]}^{\eta^p, \theta}(S_{\rho_0[\delta'_0, t'_0]}^{k-1})
\end{align*}
$$

• If $\rho_0 \in \text{FPlays}_{\text{Min}}$ and $\eta^p(\rho_0) = \text{Dirac}_{\delta_0, t_0}$, then $S_{\rho_0}^k = S_{\rho_0[\delta_0, t_0]}^{k-1}$. As in (6.1), we can obtain that

$$
\mathbb{P}_{\rho_0}^{\eta^p, \theta}(S_{\rho_0[\delta_0, t_0]}^{k-1}) = \eta^p(\rho_0)(\delta_0, t_0) \times \mathbb{P}_{\rho_0[\delta_0, t_0]}^{\eta^p, \theta}(S_{\rho_0[\delta_0, t_0]}^{k-1}).
$$

Then, we have directly

$$
\mathbb{P}_{\rho_0}^{\eta^p, \theta}(S_{\rho_0}^k) = \mathbb{P}_{\rho_0[\delta_0, t_0]}^{\eta^p, \theta}(S_{\rho_0[\delta_0, t_0]}^{k-1}) \le 1 - (1-p)^{k-1} \le 1 - (1-p)^k.
$$

• If $\rho_0 \in \text{FPlays}_{\text{Max}}$, then

$$
S_{\rho_0}^k = \bigcup_{(\delta_0, t_0) \in \text{supp}(\theta(\rho_0))} S_{\rho_0[\delta_0, t_0]}^{k-1}.
$$

Again by decomposing on cylinders, we have that

$$
\mathbb{P}_{\rho_0}^{\eta^p, \theta}(S_{\rho_0}^k) = \sum_{\delta_0} \int_{t_0} \theta_{\Delta}(\rho_0)(\delta_0) \mathbb{P}_{\rho_0[\delta_0, t_0]}^{\eta^p, \theta}(S_{\rho_0[\delta_0, t_0]}^{k-1}) d\theta_{\mathbb{R}^+}(\rho_0, \delta_0)(t_0).
$$

By induction hypothesis, we obtain

$$
\begin{align*}
\mathbb{P}_{\rho_0}^{\eta^p, \theta}(S_{\rho_0}^k) &\le (1 - (1-p)^{k-1}) \sum_{\delta_0} \int_{t_0} \theta_{\Delta}(\rho_0)(\delta_0) d\theta_{\mathbb{R}^+}(\rho_0, \delta_0)(t_0) \\
&\le 1 - (1-p)^{k-1} \le 1 - (1-p)^k. \quad \square
\end{align*}
$$

To show that $\overline{\mathbf{mVal}}_{\ell,\nu} \le \mathbf{dVal}_{\ell,\nu}$ for all $(\ell, \nu)$, we prove that $\mathbf{mVal}_{\ell,\nu}^{\eta^p} \le \max(-N, \mathbf{dVal}_{\ell,\nu}) + 3\epsilon$
for all $(\ell, \nu)$, for $p$ close enough to 1: we conclude by taking the limit when $N$ tends to $+\infty$
and $\epsilon$ tends to 0. We get that inequality by showing the following result, paired with the
fact that $\mathbf{dVal}_{\ell,\nu}^{\sigma} \le \max(-N, \mathbf{dVal}_{\ell,\nu}) + \epsilon$.

**Proposition 6.5.** For all configurations $(\ell, \nu)$ and $\varepsilon > 0$ small enough, there exists $\tilde{p} \in (0, 1)$
so that for all $p \in [\tilde{p}, 1)$,

$$
\mathbf{mVal}_{\ell, \nu}^{\eta^p} \leq \mathbf{dVal}_{\ell, \nu}^{\sigma} + 2\varepsilon.
$$

*Proof.* Since $\eta^p$ is memoryless and proper (by Lemma 6.4), we can use Lemma 4.2 (with $\varepsilon/2$), to obtain the existence of a (smooth) deterministic strategy $\tau \in \mathbf{sdStrat}_{\text{Max}}$ such that for all configurations $(\ell, \nu)$, $\mathbb{E}_{\ell, \nu}^{\eta^p, \tau} \ge \mathbf{mVal}_{\ell, \nu}^{\eta^p} - \varepsilon/2$. The proof then consists in computing the bound $\tilde{p}$ on the probabilities such that for all $p \in [\tilde{p}, 1)$, $\mathbb{E}_{\ell, \nu}^{\eta^p, \tau} \le \mathbf{dVal}_{\ell, \nu}^{\sigma} + 3\varepsilon/2$. We conclude by combining both inequalities.
<figure><img src="image_14.png" /><figcaption>Figure 8: Partition of the plays TPlays<sub>ℓ,ν</sub><sup>η<sup>p</sup>,τ</sub></figcaption></figure>

Notice that η^p and τ are both discrete strategies so that we can apply Lemma 3.16: for all (ℓ, ν),

$$ \mathbb{E}_{\ell, \nu}^{\eta^p, \tau} = \sum_{\rho \in \text{TPlays}_{\ell, \nu}^{\eta^p, \tau}} \text{wt}(\rho) \times \mathbb{P}_{\ell, \nu}^{\eta^p, \tau}(\rho) $$

where TPlays<sub>ℓ,ν</sub><sup>η<sup>p</sup>,τ</sub> is the $\mathbb{P}_{\ell,\nu}^{\eta^p,\tau}$-measurable set of plays starting in (ℓ, ν), conforming to η^p and θ and ending in the target.

The case where the whole region game only contains positive SCCs is easy, since then η^p chooses the transition and delay given by σ^1 with probability 1. By divergence, G then contains no negative cycles. A play conforming to η^p is also conforming to the deterministic strategy σ^1, so it must be acyclic. In particular, there exists only one play ρ conforming to η^p and τ. This one is also conforming to σ and thus reaches the target with a cumulated weight wt<sub>Σ</sub>(ρ) = E<sub>ℓ,ν</sub><sup>η^p,τ</sup> ≤ dVal<sub>ℓ,ν</sub><sup>σ</sup> as expected.

Now, suppose that the region graph contains at least a negative SCC. Thus, we let c > 0 be the maximal size of an elementary cycle of the region game (that visits each pair (ℓ, r) at most once) and w<sup>-</sup> > 0 be the opposite of the maximal cumulated weight of an elementary negative cycle in $\mathcal{R}(G)$ (necessarily bounded by w<sub>max</sub><sup>e</sup> |$\mathcal{R}(G)$|).

We partition the set TPlays<sub>ℓ,ν</sub><sup>η<sup>p</sup>,τ</sub> into subsets Π<sub>i,j</sub> of plays according to the number i of edges (ℓ, ν) δ,t → (ℓ', ν') chosen by Min with a probability η^p(ℓ, ν)(δ, t) = 1 - p, and their length j (we always have i ≤ j). The partition is depicted in Figure 8:

* Π<sub>N,≥K</sub>, depicted in blue, contains all plays with a length greater than K (the switching threshold)

* Π<sub>0,≤K</sub>, depicted in yellow, contains all plays without edges of probability 1 - p, with a length at most K;

* $\tilde{\Pi}$, depicted in red, contains the rest of the plays.

We have

$$ \mathbb{E}_{\ell, \nu}^{\eta^p, \tau} = \underbrace{\sum_{\rho \in \Pi_{0, \le K}} \text{wt}(\rho) \mathbb{P}_{\ell, \nu}^{\eta^p, \tau}(\rho)}_{\gamma_{0, \le K}} + \underbrace{\sum_{\rho \in \Pi_{N, \ge K}} \text{wt}(\rho) \mathbb{P}_{\ell, \nu}^{\eta^p, \tau}(\rho)}_{\gamma_{N, \ge K}} + \underbrace{\sum_{\rho \in \tilde{\Pi}} \text{wt}(\rho) \mathbb{P}_{\ell, \nu}^{\eta^p, \tau}(\rho)}_{\tilde{\gamma}} \quad (6.2) $$

We now compute and bound the three expectations γ<sub>0,≤K</sub>, γ<sub>N,≥K</sub> and $\tilde{\gamma}$.
The red zone is such that $\tilde{\gamma} \le \varepsilon/4$. All plays in $\tilde{\Pi}$ have a length at most $K$: so the cumulated weight of all such plays is at most $K w_{\max}^e$. So, we have

$$ \tilde{\gamma} = \sum_{\rho \in \tilde{\Pi}} \mathrm{wt}(\rho) \mathbb{P}_{\ell, \nu}^{\eta^p, \tau}(\rho) \le \sum_{\rho \in \tilde{\Pi}} K w_{\max}^e \mathbb{P}_{\ell, \nu}^{\eta^p, \tau}(\rho) = K w_{\max}^e \mathbb{P}_{\ell, \nu}^{\eta^p, \tau}(\tilde{\Pi}). $$

But all plays $\rho \in \bigcup_{j \le K} \Pi_{i,j}$ with $i \le K$ take $i$ edges of probability $1-p$. In particular, by bounding all other probabilities by 1, and since there are at most $2^K$ plays in $\bigcup_{j \le K} \Pi_{i,j}$ (since $\tau$ is deterministic and the support of all $\eta^p(\ell, \nu)$ contains at most two edges), we obtain (using that $1 - (1-p)^K \le 1$)

$$ \mathbb{P}_{\ell, \nu}^{\eta^p, \tau}(\tilde{\Pi}) \le 2^K \sum_{i=1}^{K-1} (1-p)^i = 2^K \frac{(1-p)(1-(1-p)^K)}{p} \le 2^K \frac{1-p}{p} \xrightarrow{p \to 1} 0 \quad (6.3) $$

If we suppose that

$$ p \ge \frac{1}{1 + \varepsilon/(4 \times 2^K K w_{\max}^e)} $$

we obtain as desired

$$ \tilde{\gamma} \le 2^K K w_{\max}^e \frac{1-p}{p} \le \frac{\varepsilon}{4}. $$

The yellow and blue zones are such that $\gamma_{0, \le K} + \gamma_{\mathbb{N}, \ge K} \le \mathrm{dVal}_{\ell, \nu}^{\sigma} + 5\varepsilon/4$. All plays in $\Pi_{0, \le K}$ reach the target without taking any edge of probability $1-p$, so they are conforming to $\sigma^1$. In the case where $\mathrm{dVal}_{\ell, \nu} = -\infty$, $\Pi_{0, \le K} = \emptyset$ and $\gamma_{0, \le K} = 0$, since no play conforming to $\sigma^1$ from $(\ell, \nu)$ reaches the target. In this case, Min can stay in a cycle with a negative cumulated weight as long as wanted. Now, if $\mathrm{dVal}_{\ell, \nu}$ is finite, by Lemma 5.6, the cumulated weight of a play in $\Pi_{0, \le K}$ is at most $\mathrm{dVal}_{\ell, \nu} + K\varepsilon/K = \mathrm{dVal}_{\ell, \nu} + \varepsilon$. As $\mathrm{dVal}_{\ell, \nu} = \inf_{\sigma \in \mathrm{dStrat}_{\min}} \mathrm{dVal}_{\ell, \nu}^{\sigma} \le \mathrm{dVal}_{\ell, \nu}^{\sigma}$, in both cases, we can write

$$ \gamma_{0, \le K} \le (\mathrm{dVal}_{\ell, \nu}^{\sigma} + \varepsilon) \mathbb{P}_{\ell, \nu}^{\eta^p, \tau}(\Pi_{0, \le K}). $$

Let $\rho$ be a play in $\Pi_{i,j}$ with $0 \le i$ and $j \ge K$. Since $\eta^p$ only allows cycles in negative SCCs, all region cycles in $\rho$ have a cumulated weight at most $-1$. By definition of $K$ and the proof of Theorem 5.5, $\mathrm{wt}(\rho) \le \mathrm{dVal}_{\ell, \nu}^{\sigma} \le \mathrm{dVal}_{\ell, \nu}^{\sigma} + \varepsilon$.

By summing up the contribution of yellow and blue zones, we get

$$ \gamma_{0, \le K} + \gamma_{\mathbb{N}, \ge K} \le (\mathrm{dVal}_{\ell, \nu}^{\sigma} + \varepsilon) \mathbb{P}_{\ell, \nu}^{\eta^p, \tau}(\Pi_{0, \le K} \cup \Pi_{\mathbb{N}, \ge K}). \quad (6.4) $$

To conclude, we distinguish two cases. First, we suppose that $\mathrm{dVal}_{\ell, \nu}^{\sigma} \ge -5\varepsilon/4$. By having $\mathbb{P}_{\ell, \nu}^{\eta^p, \tau}(\Pi_{0, \le K} \cup \Pi_{\mathbb{N}, \ge K}) \le 1$, we get

$$ \gamma_{0, \le K} + \gamma_{\mathbb{N}, \ge K} \le \left( \mathrm{dVal}_{\ell, \nu}^{\sigma} + \frac{5\varepsilon}{4} \right) \mathbb{P}_{\ell, \nu}^{\eta^p, \tau} (\Pi_{0, \le K} \cup \Pi_{\mathbb{N}, \ge K}) \le \mathrm{dVal}_{\ell, \nu}^{\sigma} + \frac{5\varepsilon}{4}. $$

Otherwise $\mathrm{dVal}_{\ell, \nu}^{\sigma} < -5\varepsilon/4$, and then, by (6.3),

$$ \mathbb{P}_{\ell, \nu}^{\eta^p, \tau}(\Pi_{0, \le K} \cup \Pi_{\mathbb{N}, \ge K}) = 1 - \mathbb{P}_{\ell, \nu}^{\eta^p, \tau}(\tilde{\Pi}) \ge 1 - 2^K \frac{1-p}{p} \xrightarrow{p \to 1} 1. $$

If we suppose that

$$ p \ge \frac{2^K}{2^K + 1 - \frac{\mathrm{dVal}_{\ell, \nu}^{\sigma} + 5\varepsilon/4}{\mathrm{dVal}_{\ell, \nu}^{\sigma} + \varepsilon}} \in (0, 1) $$
then

$$ \mathbb{P}_{\ell, \nu}^{\eta^p, \tau} (\Pi_{0, \le K} \cup \Pi_{\mathbb{N}, \ge K}) \ge \frac{\mathrm{dVal}_{\ell, \nu}^{\sigma} + 5\varepsilon/4}{\mathrm{dVal}_{\ell, \nu}^{\sigma} + \varepsilon} $$

and, by negativity of $\mathrm{dVal}_{\ell, \nu}^{\sigma} + \varepsilon$, we can rewrite (6.4) as

$$ \gamma_{0, \le K} + \gamma_{\mathbb{N}, \ge K} \le (\mathrm{dVal}_{\ell, \nu}^{\sigma} + \varepsilon) \frac{\mathrm{dVal}_{\ell, \nu}^{\sigma} + 5\varepsilon/4}{\mathrm{dVal}_{\ell, \nu}^{\sigma} + \varepsilon} = \mathrm{dVal}_{\ell, \nu}^{\sigma} + \frac{5\varepsilon}{4}. $$

In all cases, we have $\gamma_{0, \le K} + \gamma_{\mathbb{N}, \ge K} \le \mathrm{dVal}_{\ell, \nu}^{\sigma} + 5\varepsilon/4$.

**Gathering all constraints on p.** We gather all the lower bounds over p that we need in the proof, letting

$$ \tilde{p} = \begin{cases} \max \left( \frac{1}{1+\varepsilon/(4 \times 2^K K w_{\max}^e)}, \frac{1}{2} \right) & \text{if } \mathrm{dVal}_{\ell, \nu}^{\sigma} \ge -5\varepsilon/4 \\ \max \left( \frac{1}{1+\varepsilon/(4 \times 2^K K w_{\max}^e)}, \frac{1}{2}, \frac{2^K}{2^K + 1 - \frac{\mathrm{dVal}_{\ell, \nu}^{\sigma} + 5\varepsilon/4}{\mathrm{dVal}_{\ell, \nu}^{\sigma} + \varepsilon}} \right) & \text{otherwise} \end{cases} $$

Then, for $p \in (\tilde{p}, 1)$, we have $\mathbb{E}_{\ell, \nu}^{\eta^p, \tau} \le \mathrm{dVal}_{\ell, \nu}^{\sigma} + 3\varepsilon/2$. Since $\tilde{p}$ does not depend on $\tau$, we conclude that for $p \in (\tilde{p}, 1)$, we have $\mathrm{mVal}_{\ell, \nu}^{\eta^p} \le \mathrm{dVal}_{\ell, \nu}^{\sigma} + 2\varepsilon$. $\square$

## 7. THE UNTIMED SETTING: SHORTEST-PATH GAMES

In this section, we restrict ourselves to WTGs that use no clocks. These are generally called shortest-path games, and their deterministic value have previously been studied [BGHM17, BMR17]: both players have optimal strategies, Max does not require memory, while Min requires pseudo-polynomial size memory. Since there are no clocks, we simply remove from transitions the component regarding the guards and clock resets. We also only provide the weight of locations (usually called vertices or states, in this setting), and not of transitions. To summarise, here is a self-contained definition of the games we study in this section.

**Definition 7.1.** A shortest-path game (SPG) is a tuple $\langle L_{\text{Max}}, L_{\text{Min}}, \Delta, \text{wt}, L_T \rangle$ where $L := L_{\text{Max}} \uplus L_{\text{Min}} \uplus L_T$ is a finite set of vertices partitioned into the sets $L_{\text{Max}}$ and $L_{\text{Min}}$ of Max and Min respectively, and a set $L_T$ of target vertices, $\Delta \subseteq L \setminus L_T \times L$ is a set of directed edges, and wt: $\Delta \to \mathbb{Z}$ is the weight function, associating an integer weight with each edge.

Since SPGs are special cases of WTGs, the definition of stochastic strategies and values from WTGs can be adapted. In this context, all distributions over transitions are finite, and thus all strategies are smooth. Moreover, all strategies are discrete, and if the strategies of Min are supposed to be proper, the various values exist and Lemma 3.16 applies. In particular, smooth deterministic values are defined only by a restriction over strategies of Min, i.e. $\text{sdStrat}_{\text{Max}} = \text{dStrat}_{\text{Max}}$).
**7.1. Memoryless value.** In SPGs, we are able to extend the result of Theorem 6.1 without imposing the divergence condition:

**Theorem 7.2.** For all SPGs $\mathcal{G}$, for all vertices $\ell$, we have

$$dVal_{\ell} = \overline{mVal}_{\ell} = \underline{mVal}_{\ell}.$$

The proof strategy follows the same path as in the divergent case:

* we show in Lemma 7.3 that $dVal_{\ell} \le \underline{mVal}_{\ell}$, by adapting the proof of Lemma 6.2 relying on the existence of an optimal deterministic and memoryless strategy of Max against the deterministic value [BGHM17];

* we show in Lemma 7.4 that memoryless stochastic strategies can emulate deterministic ones: $\underline{mVal}_{\ell} \le dVal_{\ell}$ (with similar but more involved techniques as in Lemma 6.3).

Combined with the fact that $\underline{mVal}_{\ell} \le \overline{mVal}_{\ell}$, we indeed obtain the desired equalities. We start by adapting the proof of Lemma 6.2:

**Lemma 7.3.** In all SPGs $\mathcal{G}$, for all vertices $\ell$, $dVal_{\ell} \le \underline{mVal}_{\ell}$.

*Proof.* By [BGHM17], Max has a memoryless and deterministic optimal strategy $\tau$ for the deterministic value. Against any deterministic strategy of Min, from vertex $\ell$, it guarantees a weight at least $dVal_{\ell}$.

The rest of the proof is entirely similar, but reproduced here for ease. Let $\eta$ be any memoryless proper strategy of Min. Every play conforming to $\eta$ and $\tau$ has a weight at least $dVal_{\ell,\nu}$ (since it is conforming to $\tau$), so that, by definition of the expectation,

$$\mathbb{E}_{\ell, \nu}^{\eta, \tau} = \int_{\rho} \mathrm{wt}(\rho) \mathrm{d}\mathbb{P}_{\ell, \nu}^{\eta, \tau}(\rho) \geq \mathrm{dVal}_{\ell, \nu}$$

Notice that this integral is indeed a finite sum here, since the strategies are necessarily discrete. Since the inequality holds for all proper strategies of Min, we deduce that

$$\inf_{\eta \in \mathrm{mStrat}_{\mathrm{Min}}^{p}} \mathbb{E}_{\ell}^{\eta, \tau} \geq \mathrm{dVal}_{\ell}.$$

By taking the supremum over all memoryless strategies of Max (that contain the memoryless and deterministic strategy $\tau$), we have

$$\sup_{\theta \in \mathrm{mStrat}_{\mathrm{Max}}} \inf_{\eta \in \mathrm{mStrat}_{\mathrm{Min}}^{p}} \mathbb{E}_{\ell}^{\eta, \theta} \geq \mathrm{dVal}_{\ell}.$$

In particular, $\underline{mVal}_{\ell} \ge \mathrm{dVal}_{\ell}$, as expected.

<figure><img src="image_15.png" /></figure>

The rest of this section is devoted to the proof of the final piece of the proof:

**Lemma 7.4.** In all SPGs $\mathcal{G}$, for all vertices $\ell$, $\overline{mVal}_{\ell} \le \mathrm{dVal}_{\ell}$.

In an SPG, once we fix a memoryless strategy $\eta \in \mathrm{mStrat}_{\mathrm{Min}}$, we obtain a Markov decision process (MDP) where the other player must still choose how to react. An MDP is a tuple $\langle L, A, P \rangle$ where $L$ is a set of vertices, $A$ is a set of actions, and $P: L \times A \to \mathrm{Dist}(L)$ is a partial function mapping to some pair of vertices and actions a distribution of probabilities over the successor vertices. In our context, we let $\mathcal{G}^{\eta}$ be the MDP with the same set $L$ of vertices as $\mathcal{G}$, actions $A = L \cup \{\perp\}$ being either successor vertices of the game or an additional action $\perp$ denoting the random choice of $\eta$, and a probability distribution $P$ defined by:

* if $\ell \in L_{\mathrm{Max}}$, $P(\ell, \ell')$ is only defined if $(\ell, \ell') \in \Delta$ in which case $P(\ell, \ell') = \mathrm{Dirac}_{\ell'}$, and $P(\ell, \perp)$ is also undefined;
• if $\ell \in L_{\text{Min}}$, $P(\ell, \perp) = \eta(\ell)$, and $P(\ell, \ell')$ is undefined for all $\ell' \in L$.

In drawings of MDPs (and also of Markov chains, later), we show weights as trivially transferred from the game graph.

**Example 7.5.** In Figure 1, an SPG is presented on the left, with the MDP in the middle obtained by picking as a memoryless strategy for Min the one choosing to go to $\ell_{\text{Max}}$ with probability $p \in (0, 1)$ and to the target vertex with probability $1-p$. Another more complex example is given in Figure 9 where the memoryless strategy for Min consists, in vertex $\ell_1$, to choose successor $\ell_0$ with probability $p \in (0, 1)$ and successor $\ell_2$ with probability $1-p$, and in vertex $\ell_3$, to choose successor $\ell_1$ with the same probability $p$ and the target vertex with probability $1-p$.

In such an MDP, when player Max has chosen a strategy, there will remain no “choices” to make, and we will thus end up in a Markov chain. A Markov chain (MC) is a tuple $M = \langle L, P \rangle$ where $L$ is a set of vertices, and $P: L \to \text{Dist}(L)$ associates to each vertex a distribution of probabilities over the successor vertices. In our context, for all memoryless strategies $\theta \in \text{mStrat}_{\text{Max}}$, we let $G^{\eta, \theta}$ the MC obtained from the MDP $G^{\eta}$ by following strategy $\theta$ and action $\perp$. Formally, it consists of the same set $L$ of vertices as $G$, and mapping $P$ associating to a vertex $\ell \in L_{\text{Min}}$, $P(\ell) = \eta(\ell)$ and to a vertex $\ell \in L_{\text{Max}}$, $P(\ell) = \theta(\ell)$.

**Example 7.6.** On the right of Figure 1 is depicted the MC obtained when Max decides to go to $\ell_{\text{Min}}$ with probability $q \in [0, 1]$ and to the target vertex with probability $1-q$.

By [BK08, Section 10.5.1], the value $\text{mVal}_{\ell}^{\eta}$ is finite if and only if strategy $\eta$ ensures the reachability of a target vertex with probability 1, no matter how the opponent plays. Thus, for memoryless strategies, Hypothesis 3.9 can be restricted to only checking that for all vertices $\ell_0$ and strategies $\theta \in \text{Strat}_{\text{Max}}$, $\mathbb{P}_{\ell_0}^{\eta, \theta}(\text{TPlays}) = 1$. From Lemma 4.3, we obtain a Bellman-like equation as follows, once simplified since we restrict ourselves to memoryless strategies:

$$ \mathbb{E}_{\ell}^{\eta, \theta} = \begin{cases} 0 & \text{if } \ell \in L_T \\ \sum_{(\ell, \ell') \in \Delta} \eta(\ell, \ell') \times (\text{wt}(\ell, \ell') + \mathbb{E}_{\ell'}^{\eta, \theta}) & \text{if } v \in L_{\text{Min}} \setminus L_T \\ \sum_{(\ell, \ell') \in \Delta} \theta(\ell, \ell') \times (\text{wt}(\ell, \ell') + \mathbb{E}_{\ell'}^{\eta, \theta}) & \text{if } \ell \in L_{\text{Max}} \setminus L_T \end{cases} \quad (7.1) $$

**Example 7.7.** For the game of Figure 1, we let $\eta$ and $\theta$ the memoryless strategies that result in the MC on the right. Letting $x = \mathbb{E}_{\ell_{\text{Min}}}^{\eta, \theta}$ and $y = \mathbb{E}_{\ell_{\text{Max}}}^{\eta, \theta}$, the system (7.1) rewrites as $x = (1-p) \times 1 + p \times y$ and $y = q \times (-1+x) + (1-q) \times (-10)$. We thus have $x = p(9q-10)/(1-pq)$. Two cases happen, depending on the value of $p$: if $p < 9/10$, then Max maximises $x$ by choosing $q = 1$, while choosing $q = 0$ when $p \ge 9/10$. In all cases, player Max will therefore play deterministically: if $p < 9/10$, the expected payoff from $\ell_{\text{Min}}$ will then be $\text{mVal}^{\eta}(\ell_{\text{Min}}) = -p/(1-p)$; if $p \ge 9/10$, it will be $\text{mVal}^{\eta}(\ell_{\text{Min}}) = -10p$. This value is always greater than the optimum $-10$ that Min were able to achieve with memory, since we must keep $1-p > 0$ to ensure reaching the target with probability 1. We thus obtain $\overline{\text{mVal}}(\ell_{\text{Min}}) = \overline{\text{mVal}}(\ell_{\text{Max}}) = -10$ as before. There are no optimal strategies for Min, but an $\varepsilon$-optimal one consisting in choosing probability $p \ge 1 - \varepsilon/10$.

The fact that Max can play optimally with a deterministic strategy in the MDP $G^{\eta}$ is not specific to this example. Indeed, in an MDP $G^{\eta}$ such that $\mathbb{P}_{\ell}^{\eta, \theta}(\text{TPlays}) = 1$ for all $\theta$, Max cannot avoid reaching the target, and must then ensure the most expensive play possible. Considering the MDP $\tilde{G}^{\eta}$ obtained by multiplying all the weights in the graph by $-1$, the
<figure><img src="image_16.png" /><figcaption>Figure 9: On the left, a more complex example of shortest-path game. On the right, the MDP associated with a randomised strategy of Min with a parametric probability $p \in (0, 1)$.</figcaption></figure>

objective of Max becomes a shortest-path objective. We can then deduce from [BT91] that Max has an optimal deterministic memoryless strategy: the same applies in the original MDP $G^\eta$.

**Proposition 7.8.** In the MDP $G^\eta$ such that $P_\ell^{\eta,\theta}(TPlays) = 1$ for all $\theta$, Max has an optimal deterministic memoryless strategy.

The divergence of WTGs was used to obtain an $\varepsilon$-optimal switching strategy for Min wrt the deterministic value. For SPGs, divergence is not required to obtain it:

**Proposition 7.9** [BGHM17]. There exists a switching strategy $\sigma = (\sigma^1, \sigma^2, K)$ with $\sigma^1$ a fake-optimal strategy$^4$, $\sigma^2$ an attractor and $K = (2w_{\max}^\Delta(|V|-1)+n)|V|+1$ such that $\mathrm{dVal}_\ell^\sigma \le \max(-n, \mathrm{dVal}_\ell)$, for all initial vertices $\ell \in L$ and $n \in \mathbb{N}$.

In particular, if $\mathrm{dVal}_\ell$ is finite, for $n$ large enough, the switching strategy is optimal. If $\mathrm{dVal}_\ell = -\infty$ however, the sequence $(\sigma^n)_{n \in \mathbb{N}}$ of strategies, each with a different parameter $n$, has a value that tends to $-\infty$.

Now, we consider a switching strategy $\sigma$ defined in Proposition 7.9, and define the memoryless strategy $\eta^p$, with $p \in (0,1)$ as follows: for $\ell \in L$, letting $\sigma^1(\ell) = \delta_1$ and $\sigma^2(\ell) = \delta_2$, we let

$$ \eta^p(\ell) = \begin{cases} \mathrm{Dirac}_{\delta_1} & \text{if } \ell \text{ is in a positive SCC} \\ p \times \mathrm{Dirac}_{\delta_1} + (1-p) \times \mathrm{Dirac}_{\delta_2} & \text{otherwise} \end{cases} $$

We conclude as before by showing the following result paired with the fact that $\mathrm{dVal}_\ell^\sigma \le \max(-n, \mathrm{dVal}_\ell)$:

**Proposition 7.10.** For all vertices $\ell$ and $\varepsilon > 0$ small enough, there exists $\tilde{p} \in (0,1)$ so that for all $p \in [\tilde{p}, 1)$,

$$ \mathrm{mVal}_\ell^{\eta^p} \le \mathrm{dVal}_\ell^\sigma + 2\varepsilon. $$

*Proof.* Unlike in the proof of Proposition 6.5, some SCCs of SPGs may contain positive and negative cycles (e.g. the SPG depicted on the left of Figure 9): we will thus refine our partition to compute the expected values.

<footnote n="4">⁴Remember from [BGHM17] that all plays conforming to a fake-optimal strategy and reaching the target have a weight at most the deterministic value, and every cyclic play conforming to it has a negative cumulative weight.</footnote>
<figure><img src="image_17.png" /><figcaption>Figure 10: A new partition of plays Π in a SPG.</figcaption></figure>

First, by Lemma 6.4, we still know that $η^p$ is proper, i.e. $\mathbb{P}_ℓ^{η^p, τ}(\text{TPlays}) = 1$. We can thus use again Lemma 4.2 to obtain the existence of a deterministic strategy $τ$ such that $\mathbb{E}_ℓ^{η^p, τ} \ge \text{mVal}_ℓ^{η^p} - \varepsilon/2$.

We let $c > 0$ be the maximal size of an elementary cycle (that visits a vertex at most once) in $G$, $w^- > 0$ be the opposite of the maximal weight of an elementary negative cycle in $G$, and $w^+ \ge 0$ be the maximal weight of an elementary non-negative cycle in $G$ (or 0 if such cycle does not exist).

We now find the bound $\tilde{p}$ such that $\mathbb{E}_ℓ^{η^p, τ} \le \text{dVal}_ℓ^σ + 3\varepsilon/2$ to conclude. To do so, we consider a new partition of the set Π of plays starting in $ℓ$, conforming to $η^p$ and $τ$, and reaching the target, as depicted in Figure 10: as before the partition relies on the number $i$ of transitions of probability $1-p$ a play goes through, and its length $j$:

* $Π_{0,N}$, depicted in yellow, contains all plays with no edges of probability $1-p$;

* $Π_{>0,≥J}$, depicted in blue, contains all plays with $i \ge 1$ edges of probability $1-p$, and a length at least

$$J(i) = \lfloor ia + b \rfloor \quad \text{with} \quad a = c \left( 1 + \frac{w^+}{w^-} \right) \quad \text{and} \quad b = \frac{|\text{dVal}_\ell^\sigma| + |L|w_{\max}^\Delta + w^-}{w^-} c + |L|$$

* $Π_{>0,<J}$, depicted in red, is the rest of the plays.

We let $γ_{0,N}$ (respectively, $γ_{>0,≥J}$ and $γ_{>0,<J}$) be the expectation $\mathbb{E}_ℓ^{η^p, τ}$ restricted to plays in $Π_{0,N}$ (respectively, $Π_{>0,≥J}$ and $Π_{>0,<J}$). By Lemma 3.16,

$$\text{mVal}_ℓ^{η^p, τ} = \mathbb{E}_ℓ^{η^p, τ} = \sum_{\rho} \text{wt}(\rho) \times \mathbb{P}_ℓ^{η, τ}(\rho) = \gamma_{0,N} + \gamma_{>0,≥J} + \gamma_{>0,<J} \quad (7.2)$$

We thus analyse separately the three terms of (7.2).

First, we analyse the weight of a play depending on the number of edges $1-p$ it goes through. Let $ρ$ be a play in $Π_{i,j}$, with $1 \le i$ and $j \ge i$: it goes through $i$ edges of probability $1-p$.

Each cycle conforming to $η^p$ and $τ$ with a non-negative cumulative weight contains at least one transition taken by $η^p$ with probability $1-p$ (otherwise, all its edges would be of probability $p$ or $1$, and the cycle would be conforming to the fake-optimal strategy $σ^1$, implying that the cumulative weight would be negative).

In particular, $ρ$ contains at most $i$ elementary cycles of non-negative cumulated weight (at most $w^+$). The total length of these cycles is at most $ic$. Once we have removed these cycles from the play, it remains a play of length at least $j-ic$. By a repeated pumping
argument, it still contains at least $\lfloor \frac{j-ic-|L|}{c} \rfloor$ elementary cycles, that all have a negative cumulated weight (at most $-w^{-}$). The remaining part, once removed the last negative cycles it contains, has length at most $|L|$, and thus a cumulative weight at most $|L|w_{\max}^{\Delta}$. In summary the cumulative weight of every play in $\Pi_{i,j}$ is at most

$$iw^{+} + \left\lfloor \frac{j - ic - |L|}{c} \right\rfloor (-w^{-}) + |L|w_{\max}^{\Delta} \quad (7.3)$$

Red zone is such that $\gamma_{>0,<J} \le \varepsilon/2$. Let $\rho$ be a play in $\Pi_{i,j}$, with $i \ge 1$ and $j < J(i)$. By (7.3), its cumulative weight is at most

$$iw^{+} + \left\lfloor \frac{j - ic - |V|}{c} \right\rfloor (-w^{-}) + |L|w_{\max}^{\Delta} \le iw^{+} + |L|w_{\max}^{\Delta}.$$

So, we can decompose the expectation $\gamma_{>0,<J}$ as follows:

$$\gamma_{>0,<J} = \sum_{\rho \in \Pi_{>0,<J}} \mathrm{wt}(\rho) \mathbb{P}_{\ell}^{\eta^{p}, \tau}(\rho) \le \sum_{i=1}^{+\infty} (iw^{+} + |L|w_{\max}^{\Delta}) \mathbb{P}_{\ell}^{\eta^{p}, \tau}(\Pi_{i,<J(i)}) \quad (7.4)$$

Moreover, the probability of a play in $\Pi_{i,<J(i)}$, given by the $i$ edges of probability $(1-p)$ and the $j-i$ edges with a probability bounded by 1, is at most $(1-p)^i$. Since the number of plays in $\Pi_{i,<J(i)}$ is bounded by $2^{J(i)}$ (for each of the at most $J(i)$ steps, Min has at most 2 choices in its distribution, while Max plays a deterministic strategy), we have

$$\mathbb{P}_{\ell}^{\eta^{p}, \tau}(\Pi_{i,<J(i)}) \le (1-p)^{i} 2^{J(i)} \quad (7.5)$$

We rewrite (7.4) as

$$\begin{aligned} \gamma_{>0,<J} &\le \sum_{i=1}^{+\infty} (iw^{+} + |L|w_{\max}^{\Delta})(1-p)^{i} 2^{J(i)} \le \sum_{i=1}^{+\infty} (iw^{+} + |L|w_{\max}^{\Delta})(1-p)^{i} 2^{ai+b} \\ &\le w^{+} 2^{b} \sum_{i=1}^{+\infty} i((1-p)2^{a})^{i} + |L|w_{\max}^{\Delta} 2^{b} \sum_{i=1}^{+\infty} ((1-p)2^{a})^{i} \end{aligned}$$

these sums converging as soon as we consider $p \ge 1 - \frac{1}{2^a}$. We finally obtain

$$\gamma_{>0,<J} \le w^{+} 2^{b} \frac{2^{a}(1-p)}{(1-2^{a}(1-p))^{2}} + |L|w_{\max}^{\Delta} 2^{b} \frac{2^{a}(1-p)}{1-2^{a}(1-p)}.$$

We consider a stronger assumption on $p$, namely that $p \ge 1 - \frac{1}{2^{a+1}}$. Then, we know that $1 \le \frac{1}{1-2^a(1-p)} \le 2$, so that we rewrite the previous inequality as

$$\gamma_{>0,<J} \le w^{+} 2^{b+a+2}(1-p) + |L|w_{\max}^{\Delta} 2^{b+a+1}(1-p).$$

By choosing $p$ such that

$$p \ge 1 - \frac{\varepsilon}{2^{b+a+2}(|L|w_{\max}^{\Delta} + 2w^{+})}$$

we obtain as desired $\gamma_{>0,<J} \le \varepsilon/2$.
Yellow and blue zones are such that $\gamma_{0,N} + \gamma_{>0,\ge J} \le dVal_{\ell}^{\sigma} + \varepsilon$. We first upper-bound the cumulative weight of all plays of these two zones. On the one hand, all plays of $\Pi_{0,N}$ reach the target without edges of probability $1-p$, i.e. by conforming to $\sigma^1$. By fake-optimality of $\sigma^1$, their cumulative weight is upper-bounded by $dVal_{\ell}^{\sigma}$. On the other hand, by (7.3), all plays $\rho$ of $\Pi_{i,j}$, with $0 \le i < I$ and $j \ge J(i)$, have a cumulative weight at most

$$ 
\begin{aligned}
\mathrm{wt}(\rho) &\le i w^+ + \left\lfloor \frac{j - ic - |L|}{c} \right\rfloor (-w^-) + |L| w_{\max}^{\Delta} \\
&\le i w^+ + \frac{J(i) - ic - |L|}{c} (-w^-) + |L| w_{\max}^{\Delta} \\
&= i w^+ + \frac{a i + \frac{|d\mathrm{Val}_{\ell}^{\sigma}| + |L| w_{\max}^{\Delta} + w^-}{w^-} c + |L| - ic - |L|}{c} (-w^-) + |L| w_{\max}^{\Delta} \\
&= i w^+ + \left( i \left( 1 + \frac{w^+}{w^-} \right) + \frac{|d\mathrm{Val}_{\ell}^{\sigma}| + |L| w_{\max}^{\Delta} - i}{w^-} \right) (-w^-) + |L| w_{\max}^{\Delta} \\
&= i w^+ - i w^+ - |d\mathrm{Val}_{\ell}^{\sigma}| - |L| w_{\max}^{\Delta} + |L| w_{\max}^{\Delta} = -|d\mathrm{Val}_{\ell}^{\sigma}| \le d\mathrm{Val}_{\ell}^{\sigma}
\end{aligned}
$$

Therefore, all plays in the yellow and blue zones have a cumulative weight bounded by $dVal_{\ell}^{\sigma}$. This implies

$$ \gamma_{0,N} + \gamma_{>0,\ge J} \le \sum_{\rho \in \Pi_{0,N}} dVal_{\ell}^{\sigma} \mathbb{P}_{\ell}^{\eta^p, \tau}(\rho) + \sum_{\rho \in \Pi_{>0,\ge J}} dVal_{\ell}^{\sigma} \mathbb{P}_{\ell}^{\eta^p, \tau}(\rho) \le dVal_{\ell}^{\sigma} \mathbb{P}_{\ell}^{\eta^p, \tau}(\Pi_{0,N} \cup \Pi_{>0,\ge J}). $$

Depending on the sign of $dVal_{\ell}^{\sigma}$, we can conclude:

* If $dVal_{\ell}^{\sigma} \ge 0$, then upper-bounding the probability $\mathbb{P}_{\ell}^{\eta^p, \tau}(\Pi_{0,N} \cup \Pi_{>0,\ge J})$ by 1, suffices to get $\gamma_{0,N} + \gamma_{>0,\ge J(i)} \le dVal_{\ell}^{\sigma}$.

* If $dVal_{\ell}^{\sigma} < 0$, then, by the bound (7.5) found for the red zone, we have

$$ 
\begin{aligned}
\mathbb{P}_{\ell}^{\eta^p, \tau} (\Pi_{0,N} \cup \Pi_{>0,\ge J}) &= 1 - \mathbb{P}_{\ell}^{\eta^p, \tau} (\Pi_{>0,<J}) \\
&\ge 1 - \sum_{i=1}^{\infty} (1-p)^i 2^{ai+b} \\
&= 1 - \frac{2^{a+b}(1-p)}{1 - (1-p)2^a} \\
&\ge 1 - 2^{a+b+1}(1-p) \quad (\text{since } 1/(1 - (1-p)2^a) \le 2).
\end{aligned}
$$

This allows us to obtain

$$ \gamma_{0,N} + \gamma_{>0,\ge J} \le dVal_{\ell}^{\sigma} (1 - 2^{a+b+1}(1-p)). $$

In case we have moreover

$$ p \ge 1 - \frac{\varepsilon}{2^{a+b+1} |dVal_{\ell}^{\sigma}|} $$

we finally obtain $\gamma_{0,N} + \gamma_{>0,\ge J} \le dVal_{\ell}^{\sigma} + \varepsilon$ as expected.
**Lower bound over p.** If we gather all the lower bounds over p that we need in the proof, we get that:

* if $dVal_\ell^\sigma \ge 0$, we must have

$$p \ge \max \left( 1 - \frac{1}{2^{a+1}}, 1 - \frac{\varepsilon}{2^{b+a+2}(|L|w_{\max}^\Delta + 2w^+)} \right)$$

* if $dVal_\ell^\sigma < 0$, we must have

$$p \ge \max \left( 1 - \frac{1}{2^{a+1}}, 1 - \frac{\varepsilon}{2^{b+a+2}(|L|w_{\max}^\Delta + 2w^+)} \right), 1 - \frac{\varepsilon}{2^{a+b+1}|dVal_\ell^\sigma|}$$

with $\varepsilon$ small enough so that this bound is less than 1. $\square$

This ends the proof that for all vertices $\ell$, $\overline{mVal}_\ell \le dVal_\ell$.

**Discussion about smooth deterministic values in SPG.** With the existence of a switching optimal strategy with respect to the deterministic value for Min (by Proposition 7.9), we obtain the existence of proper smooth deterministic optimal strategies with respect to the deterministic value for Min in all SPGs. Finally, we can deduce that SPGs are determined with respect to the stochastic value, and the stochastic and (smooth) deterministic values are equal:

**Corollary 7.11.** In all SPGs, for all locations $\ell$,

$$dVal_\ell = \underline{dVal}_\ell = \overline{dVal}_\ell = \underline{Val}_\ell = \overline{Val}_\ell.$$

*Proof.* Since Max has an optimal deterministic strategy [BGHM17], there exists $\sigma \in \text{sdStrat}_{\text{Min}}^p$ and $\tau \in \text{dStrat}_{\text{Max}}$ such that

$$dVal_{\ell, \nu}^{\eta} \le dVal \le dVal_{\ell, \nu}^{\tau}$$

by Proposition 7.9. First, since $\text{sdStrat}_{\text{Max}} = \text{dStrat}_{\text{Max}}$, we deduce that

$$\overline{\text{sdVal}}_{\ell, \nu} \le \sup_{\tau \in \text{sdStrat}_{\text{Max}}} \text{wt}(\text{Play}((\ell, \nu), \sigma, \tau)) = \text{dVal}_{\ell, \nu}^{\sigma}.$$

Next, since $\text{sdStrat}_{\text{Min}}^p \subseteq \text{dStrat}_{\text{Min}}$, we deduce that

$$dVal_{\ell, \nu}^{\tau} = \inf_{\sigma \in \text{dStrat}_{\text{Min}}} \text{wt}(\text{Play}((\ell, \nu), \sigma, \tau)) \le \inf_{\sigma \in \text{sdStrat}_{\text{Min}}^p} \text{wt}(\text{Play}((\ell, \nu), \sigma, \tau)) \le \underline{dVal}_{\ell, \nu}.$$

Finally, we obtain $\underline{dVal}_{\ell, \nu} = \overline{dVal}_{\ell, \nu}$ and we conclude the proof by applying Theorem 4.1. $\square$

**7.2. Characterisation of optimality in weighted timed games without clocks.** All SPGs admit an optimal deterministic strategy for both players: however, as we have seen in Figure 1, Min may require memory to play optimally. In this case, Min does not have an optimal memoryless (randomised) strategy, but only has $\varepsilon$-optimal ones, for all $\varepsilon > 0$. But some SPGs indeed admit optimal memoryless strategies for Min: the strategy $\eta^p$ described in the proof of Lemma 7.4 is indeed optimal in SPGs not containing negative cycles, for instance. We characterise here the SPGs in which Min admits an optimal memoryless strategy. For sure, Min does not have an optimal strategy if there is some vertex $\ell$ of value $dVal_\ell = -\infty$. Thus, **we only consider in this section SPGs without vertices $\ell$ with a deterministic value $-\infty$**.

We first recall the computations performed in [BGHM17] to compute values $dVal_\ell$. As for divergent WTGs, it consists of an iterated computation, called *value iteration* based on
the operator $\mathcal{F}: (\mathbb{Z} \cup \{+\infty\})^L \to (\mathbb{Z} \cup \{+\infty\})^L$ defined for all $X = (X_\ell)_{\ell \in L} \in (\mathbb{Z} \cup \{+\infty\})^L$ and all vertices $\ell \in L$ by

$$ \mathcal{F}(X)_\ell = \begin{cases} 0 & \text{if } \ell \in L_T \\ \min_{(\ell, \ell') \in \Delta}(\text{wt}(\ell, \ell') + X_{\ell'}) & \text{if } \ell \in L_{\text{Min}} \\ \max_{(\ell, \ell') \in \Delta}(\text{wt}(\ell, \ell') + X_{\ell'}) & \text{if } \ell \in L_{\text{Max}} \end{cases} $$

We let $f_\ell^{(0)} = 0$ if $\ell \in L_T$ and $+\infty$ otherwise. By monotony of $\mathcal{F}$, the sequence $(f^{(i)}) = \mathcal{F}^i(f^{(0)})_{i \in \mathbb{N}}$ is non-increasing. It is proved to be ultimately constant, and converging towards $(\text{dVal}_\ell)_{\ell \in L}$, the smallest fixpoint of $\mathcal{F}$. The pseudo-polynomial complexity of computing the values of SPGs comes from the fact that this sequence may become stationary after a pseudo-polynomial (and not polynomial) number of steps: the game of Figure 1 is one of the typical examples.

We introduce a new notion, being the most permissive strategy of Min at each step $i \ge 0$ of the computation. It maps each vertex $\ell \in L_{\text{Min}}$ to the set

$$ \tilde{\Delta}^{(i)}(\ell) = \{(\ell, \ell') \in \Delta \mid \text{wt}(\ell, \ell') + f_{\ell'}^{(i-1)} = f_{\ell}^{(i)}\} $$

of vertices that Min can choose. For each such most permissive strategy $\tilde{\Delta}^{(i)}$, we let $\tilde{\mathcal{G}}^{(i)}$ be the SPG where we remove all edges $(\ell, \ell')$ with $\ell \in L_{\text{Min}}$ and $(\ell, \ell') \notin \tilde{\Delta}^{(i)}(\ell)$. This allows us to state the following result:

**Theorem 7.12.** *The following assertions are equivalent:*

(1) Min has an optimal memoryless deterministic strategy in $\mathcal{G}$ (for dVal);

(2) Min has an optimal memoryless (randomised) strategy in $\mathcal{G}$ (for mVal = mVal);

(3) $f_\ell^{(|L|-1)} = f_\ell^{(|L|)} = \text{dVal}_\ell$ for all vertices $\ell$ (this means that the sequence $(f^{(i)})$ is stationary as soon as step $|L| - 1$), and Min can guarantee that a vertex of $L_T$ is reached from all vertices in the game $\tilde{\mathcal{G}}^{(|L|-1)}$.

**Remark 7.13.** This characterisation of the existence of optimal memoryless strategy is testable in polynomial time since it is enough to compute vectors $f^{(|L|-1)}$ and $f^{(|L|)}$, check their equality, compute the sets $\tilde{\Delta}^{(|L|-1)}(\ell)$ (this can be done while computing $f^{(|L|)}$) and check whether Min can guarantee that a target is reached in $\tilde{\mathcal{G}}^{(|L|-1)}$ by an attractor computation.

We prove Theorem 7.12 in the rest of this section. Implication $1 \Rightarrow 2$ is trivial by the result of Theorem 7.2.

For implication $3 \Rightarrow 1$, consider any memoryless deterministic strategy $\sigma$ that guarantees Min to reach $L_T$ from all vertices in the game graph $\tilde{\mathcal{G}}^{(|L|-1)}$. Then, for all vertices $\ell$, we show by induction on $n$, that each play $\rho$ from $\ell$ that reaches the target in at most $n$ steps, and conforming to $\sigma$, has a cumulative weight $\text{wt}(\rho) \le \text{dVal}_\ell$. This is trivial for $n = 0$. If $\rho = \ell \xrightarrow{\delta} \rho'$ with $\rho'$ starting in $\ell'$, then

$$ \text{wt}(\rho) = \text{wt}(\delta) + \text{wt}(\rho') \le \text{wt}(\delta) + \text{dVal}_{\ell'} = \text{wt}(\delta) + f_{\ell}^{(|L|-1)}. $$

If $\ell \in L_{\text{Max}}$, we have

$$ \text{wt}(\rho) \le \text{wt}(\delta) + f_{\ell}^{(|L|-1)} \le f_{\ell}^{(|L|)} = \text{dVal}_{\ell}. $$

If $\ell \in L_{\text{Min}}$, since $\ell' \in \tilde{\Delta}^{(|L|-1)}(\ell)$,

$$ \text{wt}(\rho) = f_{\ell}^{(|L|)} = \text{dVal}_{\ell}. $$
This ends the proof by induction. To conclude that 1 holds, since $\sigma$ guarantees that the target is reached, all plays conforming to it reach the target in less than $|L|$ steps, which proves that $\mathrm{dVal}_{\ell}^{\sigma} \le \mathrm{dVal}_{\ell}$, showing that $\sigma$ is optimal.

For implication $1 \Rightarrow 3$, consider an optimal deterministic memoryless strategy $\sigma^*$, such that for all $\ell$, $\mathrm{dVal}_{\ell}^{\sigma^*} = \mathrm{dVal}_{\ell}$.

First, we show that $f_{\ell}^{(|L|-1)} = \mathrm{dVal}_{\ell}$ for all vertices $\ell$. For that, consider the deterministic strategy $\tau$ of Max defined for all finite plays $\rho$ having $n \le |L|$ vertices, ending in a vertex $\ell \in L_{\mathrm{Max}}$, by $\tau(\rho) = (\ell, \ell')$ such that $\mathrm{wt}(\ell, \ell') + f_{\ell'}^{(|L|-1-n)} = f_{\ell}^{(|L|-n)}$. For longer finite plays, we define $\tau$ arbitrarily. Then, let $\rho$ be the play from $\ell$ conforming to $\sigma^*$ and $\tau$. Since $\sigma^*$ ensures reaching the target and is memoryless and deterministic, $\rho$ reaches the target in at most $|L|-1$ steps. Let $\rho = \ell_0 \xrightarrow{\delta_0} \ell_1 \cdots \xrightarrow{\delta_{k-1}} \ell_k$ with $k \le |L|$. Let us show that $\mathrm{wt}(\rho) \ge f_{\ell_0}^{(|L|-1)}$. We prove by induction on $0 \le j \le k$ that

$$ \sum_{i=j}^{k-1} \mathrm{wt}(\delta_i) \ge f_{\ell_j}^{(|L|-1-j)}. $$

When $j=k$, the result is trivial since the sum is

$$ 0 = f_{\ell_k}^{(0)} \ge f_{\ell_k}^{(|L|-1-k)} $$

by using that $(f_{\ell_k}^{(i)})_i$ is non-increasing. Otherwise, by induction hypothesis

$$ \sum_{i=j}^{k-1} \mathrm{wt}(\delta_i) \ge \mathrm{wt}(\delta_j) + f_{\ell_{j+1}}^{(|L|-1-(j+1))}. $$

If $\ell_j \in L_{\mathrm{Max}}$, $\ell_{j+1}$ is chosen by $\tau$ so that

$$ \mathrm{wt}(\delta_j) + f_{\ell_{j+1}}^{(|L|-1-(j+1))} = f_{\ell_j}^{(|L|-1-j)}. $$

If $\ell \in L_{\mathrm{Min}}$, by definition of $\mathcal{F}$,

$$ \mathrm{wt}(\delta_j) + f_{\ell_{j+1}}^{(|L|-1-(j+1))} \ge f_{\ell_j}^{(|L|-1-j)}. $$

We can conclude in all cases, so that $f_{\ell}^{(|L|-1)} = \mathrm{dVal}_{\ell}$ for all vertices $\ell$.

Then, we show that Min can guarantee to reach $L_T$ from all vertices in the SPG $\tilde{\mathcal{G}}^{(|L|-1)}$. Let us suppose that this is not the case. Then, there exists a set $L'$ of vertices of $\tilde{\mathcal{G}}^{(|L|-1)}$ in which Max can trap Min forever: for all $\ell' \in L' \cap L_{\mathrm{Min}}$, $\tilde{\Delta}^{(|L|-1)}(\ell') \subseteq L'$, and for all $\ell' \in L' \cap L_{\mathrm{Max}}$, $\Delta(\ell) \cap \Delta' \ne \emptyset$. Since $\sigma^*$ guarantees that a target is reached, there exists $\ell \in L' \cap L_{\mathrm{Min}}$ such that $\sigma^*(\ell) = \ell' \notin L'$: then $\mathrm{wt}(\ell, \ell') + \mathrm{dVal}_{\ell'} > \mathrm{dVal}_{\ell}$ (here we use that $\mathrm{dVal}_{\ell} = f_{\ell}^{(|L|-1)} = f_{\ell}^{(|L|)}$). Consider an optimal deterministic memoryless strategy $\tau^*$ of Max in $\mathcal{G}$ (which we know exists by [BGHM17]). Then, the play $\rho$ from $\ell$ conforming to $\sigma^*$ and $\tau^*$ starts by taking the edge $(\ell, \ell')$ and continues with a play $\rho'$. By optimality, we know that $\mathrm{wt}(\rho) = \mathrm{dVal}_{\ell}$ and $\mathrm{wt}(\rho') = \mathrm{dVal}_{\ell'}$. However,

$$ \mathrm{wt}(\rho) = \mathrm{wt}(\ell, \ell') + \mathrm{wt}(\rho') = \mathrm{wt}(\ell, \ell') + \mathrm{dVal}_{\ell'} > \mathrm{dVal}_{\ell} $$

which raises a contradiction.

We finish the proof by showing $2 \Rightarrow 1$: the proof will be constructive and actually allows one to build an optimal memoryless deterministic strategy when it exists. Consider
<figure><img src="image_18.png" /><figcaption>Figure 11: An SPG (on the left) and the Markov chain obtained by fixing an optimal memoryless strategy, with $p \in (0, 1)$.</figcaption></figure>

thus an optimal memoryless strategy $\eta^*$ for the memoryless value. We build a memoryless deterministic strategy $\sigma^*$, and show that it is also optimal. The construction of $\sigma^*$ is performed in two steps.

We first select transitions that minimise the value of $\eta^*$ at horizon 1. Formally, for all locations $\ell$, we define

$$ \tilde{\Delta}(\ell) = \underset{(\ell, \ell') \in \text{supp}(\eta(\ell))}{\operatorname{argmin}} \left[ \text{wt}(\ell, \ell') + \text{mVal}_{\ell'}^{\eta} \right] \quad (7.6) $$

In a first approximation, we thus fix $\sigma^*(\ell)$ to be any edge of $\tilde{\Delta}(\ell)$, for all vertices $\ell$. The next example shows that $\sigma^*$ may not be optimal.

**Example 7.14.** Consider the game of Figure 11, with the memoryless strategy $\eta^*$ defined by $\eta^*(\ell_0) = \text{Dirac}_{(\ell_0, \ell_1)}$ and $\eta^*(\ell_1) = (1-p)\text{Dirac}_{(\ell_1, \ell_0)} + p\text{Dirac}_{(\ell_1, \mathbb{S})}$, where $p \in (0, 1)$. Then, we can check that $\text{mVal}^{\eta^*}(\ell_0) = -2$ and $\text{mVal}^{\eta^*}(\ell_1) = -1$, which implies that $\eta^*$ is optimal. We have $\tilde{\Delta}(\ell_0) = \{(\ell_0, \ell_1)\}$ and $\tilde{\Delta}(\ell_1) = \{(\ell_1, \ell_0), (\ell_1, \mathbb{S})\}$. However, considering the strategy $\sigma^*$ defined by $\sigma^*(\ell_0) = (\ell_0, \ell_1)$ and $\sigma^*(\ell_1) = (\ell_1, \ell_0)$, results in a value $\text{dVal}^{\sigma^*}(\ell_0) = \text{dVal}^{\sigma^*}(\ell_1) = +\infty$: thus $\sigma^*$ is not optimal.

We employ techniques already used in [CdAH04] to refine the definition of $\eta^*$. For each vertex $\ell$ in the game, we let $d(\ell)$ be the attractor distance of $\ell$ to the target in the finite MDP $\mathcal{G}^\eta$, i.e. the smallest number of steps such that Min has a path of this length reaching the target, no matter how is playing Max (notice that this may be different from the attractor distance given in the whole game, since some edges are taken with probability 0 in $\eta$). For all vertices $\ell$, $d(\ell) < +\infty$ since otherwise ($\eta$ being a memoryless strategy) the finite MDP $\mathcal{G}^\eta$ would contain a bottom strongly connected component without target states, which would contradict the fact that $\eta$ ensures to reach $L_T$ with probability 1. We then let, for all vertices $\ell \in L_{\text{Min}}$, $\sigma^*(\ell)$ be any edge in $\text{argmin}_{(\ell, \ell') \in \tilde{\Delta}(\rho)} d(\ell')$.

**Example 7.15.** On the same example as above, using the fact that $d(\mathbb{S}) = 0$, $d(\ell_1) = 1$ and $d(\ell_0) = 2$ (since the edge $(\ell_0, \mathbb{S})$ is not present in $\mathcal{G}^\eta$), we have no choice but to let $\sigma^*$ be defined by $\sigma^1(\ell_0) = (\ell_0, \ell_1)$ and $\sigma^1(\ell_1) = (\ell_1, \mathbb{S})$, which is indeed an optimal deterministic (and memoryless) strategy.

**Lemma 7.16.** The memoryless deterministic strategy $\sigma^*$ defined above is optimal.

*Proof.* We show this by proving independently that:

(1) Each finite play $\rho$ conforming to $\sigma^*$ from $\ell$ and reaching the target has a cumulated weight at most $\text{mVal}_{\ell}^{\eta}$.

(2) No play conforming to $\sigma^*$ can contain a cycle.
From the second item, we are thus certain that all plays conforming to $\sigma^*$ reach the target. The first item then allows us to conclude that $\sigma^*$ is optimal.

(1) We prove the property by induction on the length of finite plays $\rho$ conforming to $\sigma^*$ that reaches the target, for all initial vertices $\ell$. If $\rho$ has length 0, this means that $\ell \in L_T$, in which case $\mathrm{wt}(\rho) = 0 = \mathrm{mVal}_{\ell}^{\eta^*}$. Consider then a play $\rho = \ell \xrightarrow{\delta} \rho'$ such that $|\rho| \ge 1$ and $\rho'$ starting by the vertex $\ell'$, so that $\mathrm{wt}(\rho) = \mathrm{wt}(\delta) + \mathrm{wt}(\rho')$. By induction hypothesis, $\mathrm{wt}(\rho') \le \mathrm{mVal}_{\ell'}^{\eta^*}$, so that $\mathrm{wt}(\rho) \le \mathrm{wt}(\delta) + \mathrm{mVal}_{\ell'}^{\eta^*}$.

Suppose first that $\ell \in L_{\mathrm{Max}}$. By Proposition 7.8, consider a deterministic best-response strategy $\tau$ of Max against $\eta^*$. Then $\mathbb{E}_{u}^{\eta^*, \tau} = \mathrm{mVal}_{u}^{\eta^*}$ for all $u \in L_{\mathrm{Max}}$, and by (7.1), letting $(u, u') = \tau(u)$, $\mathbb{E}_{u}^{\eta^*, \tau} = \mathrm{wt}(u, u') + \mathbb{E}_{u'}^{\eta^*, \tau}$. We thus know that $\mathrm{wt}(u, u') + \mathbb{E}_{u'}^{\eta^*, \tau} = \mathrm{mVal}_{u}^{\eta^*}$. In particular, for all vertices $u \in L_{\mathrm{Max}}$ and edge $(u, u') \in \Delta$,

$$ \mathrm{wt}(u, u') + \mathrm{mVal}_{u'}^{\eta^*} \le \mathrm{mVal}_{u}^{\eta^*} \quad (7.7) $$

In particular, $\mathrm{wt}(\rho) \le \mathrm{wt}(\ell, \ell') + \mathrm{mVal}_{\ell'}^{\eta^*} \le \mathrm{mVal}_{\ell}^{\eta^*}$.

If $\ell \in L_{\mathrm{Min}}$, then $\delta = (\ell, \ell') \in \tilde{\Delta}(\ell)$ so that $\mathrm{wt}(\delta) + \mathrm{mVal}_{\ell'}^{\eta^*}$ is minimum over all possible $(\ell, \ell') \in \mathrm{supp}(\eta^*(\ell))$. The system (7.1) implies that

$$ \mathbb{E}_{\ell}^{\eta^*, \theta} = \sum_{(\ell, \ell'') \in \Delta} \eta^*(\ell)(\ell, \ell'') \times (\mathrm{wt}(\ell, \ell'') + \mathbb{E}_{\ell''}^{\eta^*, \theta}). $$

for all memoryless strategies $\theta$ of Max. In particular, for the best-response deterministic and memoryless strategy $\theta$ given by Proposition 7.8,

$$ \mathrm{mVal}_{\ell}^{\eta^*} = \mathbb{E}_{\ell}^{\eta^*, \theta} = \sum_{(\ell, \ell'') \in \mathrm{supp}(\eta^*(\ell))} \eta^*(\ell)(\ell, \ell'') \times (\mathrm{wt}(\ell, \ell'') + \mathrm{mVal}_{\ell''}^{\eta^*}) \ge \mathrm{wt}(\ell, \ell') + \mathrm{mVal}_{\ell'}^{\eta^*} \quad (7.8) $$

so that we also get $\mathrm{wt}(\rho) \le \mathrm{mVal}_{\ell}^{\eta^*}$.

(2) Suppose that a cycle $\ell_1\ell_2\cdots\ell_k\ell_1$ conforms to $\sigma^*$, with $\ell_1$ a vertex of minimal distance $d(\ell_1)$. We can choose $\ell_1$ such that it belongs to Min, since the distance is computed by an attractor for Min (and thus all successors of a vertex of Max must have a smaller distance). By minimality of $d(\ell_1)$ among the vertices of the cycle, $d(\ell_2) \ge d(\ell_1)$. Moreover, by the attractor computation, there exists $(\ell_1, \ell') \in \Delta(\ell_1)$ such that $d(\ell') = d(\ell_1) - 1 < d(\ell_1)$. By definition of $\sigma^*$, we know that $(\ell_1, \ell') \notin \tilde{\Delta}(\ell_1)$, so that

$$ \mathrm{wt}(\ell_1, \ell') + \mathrm{mVal}_{\ell'}^{\eta^*} > \mathrm{wt}(\ell_1, \ell_2) + \mathrm{mVal}_{\ell_2}^{\eta^*}. $$

By (7.8), we know that in this case

$$ \mathrm{mVal}_{\ell_1}^{\eta^*} > \mathrm{wt}(\ell_1, \ell_2) + \mathrm{mVal}_{\ell_2}^{\eta^*}. $$

By optimality of $\eta^*$, this rewrites in

$$ \overline{\mathrm{mVal}}_{\ell_1} > \mathrm{wt}(\ell_1, \ell_2) + \overline{\mathrm{mVal}}_{\ell_2}. $$

By Theorem 7.2, this also rewrites in

$$ \mathrm{dVal}_{\ell_1} > \mathrm{wt}(\ell_1, \ell_2) + \mathrm{dVal}_{\ell_2} \ge \mathcal{F}((\mathrm{dVal}_{\ell})_{\ell \in L})(\ell_1). $$

(since $\ell_1 \in L_{\mathrm{Min}}$): this contradicts the fact that the vector $(\mathrm{dVal}_{\ell})_{\ell \in L}$ is a fixpoint of $\mathcal{F}$.

□
## 8. DISCUSSION

This article studies the trade-off between memoryless and deterministic strategies, showing that Min guarantees the same value when restricted to these two kinds of strategies, or when allowed to play with both memory and randomisation. This result holds both in divergent WTGs, or SPGs.

We have studied the notions of deterministic values, (stochastic) values, and memoryless values. From a controller synthesis perspective, it could be more meaningful to study the value obtained by Min when being forced to play with a memoryless strategy, while not enforcing any properties on the strategy of Max. The result of Lemma 4.2, on the best response of Max, ensures that this value is identical to the memoryless value.

We aim at extending our study to more general WTGs, though we have studied counter-examples (Examples 4.6 and 4.7) to the determinacy result with respect to the memoryless value, and thus of the equality between memoryless and deterministic values. We could still hope to weaken slightly the necessary condition to obtain our results, for instance considering the class of almost-divergent WTGs (adding the possibility for an execution following a region cycle to have weight *exactly* 0), used in [BJM15, BMR18] to obtain an approximation schema of the optimal value. We wonder if similar $\varepsilon$-optimal switching strategies may exist also in this context, one of the crucial arguments in order to extend our emulation result.

Another question concerns the implementability of the randomised strategies: even if they use no memory, they still need to know the precise current clock valuation. In (non-weighted) timed games, previous work [CHP08] aimed at removing this need for precision, by using stochastic strategies where the delays are chosen with probability distributions that do not require exact knowledge of the clocks' measurements. In our setting, we aim at further studying the implementability of the randomised strategies of Min in WTGs, e.g. by requiring them to be robust against small imprecisions.

## REFERENCES

[ABM04] Rajeev Alur, Mikhail Bernadsky, and P. Madhusudan. Optimal reachability for weighted timed games. In Josep Díaz, Juhani Karhumäki, Arto Lepistö, and Donald Sannella, editors, *Automata, Languages and Programming: 31st International Colloquium, ICALP 2004, Turku, Finland, July 12-16, 2004. Proceedings*, volume 3142 of LNCS, pages 122–133. Springer, 2004. doi: 10.1007/978-3-540-27836-8\_13.

[AD94] Rajeev Alur and David L. Dill. A theory of timed automata. *Theoretical Computer Science*, 126(2):183–235, 1994. doi:10.1016/0304-3975(94)90010-8.

[AM99] Eugene Asarin and Oded Maler. As soon as possible: Time optimal control for timed automata. In Frits W. Vaandrager and Jan H. van Schuppen, editors, *Hybrid Systems: Computation and Control, Second International Workshop, HSCC'99, Berg en Dal, The Netherlands, March 29-31, 1999, Proceedings*, volume 1569 of Lecture Notes in Computer Science, pages 19–30. Springer, 1999. doi:10.1007/3-540-48983-5\_6.

[BBB$^{+}$14] Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, Quentin Menet, Christel Baier, Marcus Größer, and Marcin Jurdzinski. Stochastic timed automata. *Log. Methods Comput. Sci.*, 10(4), 2014. doi:10.2168/LMCS-10(4:6)2014.

[BBBC18] Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, and Pierre Carlier. When are stochastic transition systems tameable? *Journal of Logical and Algebraic Methods in Programming*, 99:41–96, 2018. doi:10.1016/J.JLAMP.2018.03.004.

[BBBR07] Patricia Bouyer, Thomas Brihaye, Véronique Bruyère, and Jean-François Raskin. On the optimal reachability problem of weighted timed automata. *Formal Methods in System Design*, 31(2):135–175, 2007. doi:10.1007/S10703-007-0035-4.
[BBCM16] Patricia Bouyer, Thomas Brihaye, Pierre Carlier, and Quentin Menet. Compositional design of stochastic timed automata. In Alexander S. Kulikov and Gerhard J. Woeginger, editors, *Computer Science - Theory and Applications - 11th International Computer Science Symposium in Russia, CSR 2016, St. Petersburg, Russia, June 9-13, 2016, Proceedings*, volume 9691 of Lecture Notes in Computer Science, pages 117-130. Springer, 2016. doi:10.1007/978-3-319-34171-2\_9.

[BBR05] Thomas Brihaye, Véronique Bruyère, and Jean-François Raskin. On optimal timed strategies. In Paul Pettersson and Wang Yi, editors, *Formal Modeling and Analysis of Timed Systems, Third International Conference, FORMATS 2005, Uppsala, Sweden, September 26-28, 2005, Proceedings*, volume 3829 of Lecture Notes in Computer Science, pages 49-64. Springer, 2005. doi:10.1007/11603009\_5.

[BBR+20] Patricia Bouyer, Thomas Brihaye, Mickael Randour, Cédric Rivière, and Pierre Vandenhove. Decisiveness of stochastic systems and its application to hybrid models. In Davide Bresolin and Jean-François Raskin, editors, *11th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2020, Brussels, Belgium, September 21-22, 2020*, volume 326 of *Electronic Proceedings in Theoretical Computer Science*, 2020. doi:10.4204/EPTCS.326.10.

[BCFL04] Patricia Bouyer, Franck Cassez, Emmanuel Fleury, and Kim G. Larsen. Optimal strategies in priced timed game automata. In Kamal Lodaya and Meena Mahajan, editors, *FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 24th International Conference, Chennai, India, December 16-18, 2004, Proceedings*, pages 148-160, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. Long version at https://doi.org/10.7146/brics.v11i4.21829. doi:10.1007/978-3-540-30538-5\_13.

[BFH+01] Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim Guldstrand Larsen, Paul Pettersson, Judi Romijn, and Frits W. Vaandrager. Minimum-cost reachability for priced timed automata. In Maria Domenica Di Benedetto and Alberto L. Sangiovanni-Vincentelli, editors, *Hybrid Systems: Computation and Control, 4th International Workshop, HSCC 2001, Rome, Italy, March 28-30, 2001, Proceedings*, volume 2034 of Lecture Notes in Computer Science, pages 147-161. Springer, 2001. doi:10.1007/3-540-45351-2\_15.

[BGH+15] Thomas Brihaye, Gilles Geeraerts, Axel Haddad, Engel Lefaucheux, and Benjamin Monmege. Simple priced timed games are not that simple. In Prahladh Harsha and G. Ramalingam, editors, *35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2015, December 16-18, 2015, Bangalore, India*, volume 45 of LIPICS, pages 278-292. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. doi:10.4230/LIPICS.FSTTCS.2015.278.

[BGHM17] Thomas Brihaye, Gilles Geeraerts, Axel Haddad, and Benjamin Monmege. Pseudopolynomial iterative algorithm to solve total-payoff games and min-cost reachability games. *Acta Informatica*, 54(1):85-125, 2017. doi:10.1007/S00236-016-0276-z.

[BJM15] Patricia Bouyer, Samy Jaziri, and Nicolas Markey. On the value problem in weighted timed games. In Luca Aceto and David de Frutos-Escrig, editors, *26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015*, volume 42 of Leibniz International Proceedings in Informatics, pages 311-324. Leibniz-Zentrum für Informatik, 2015. doi:10.4230/LIPICS.CONCUR.2015.311.

[BK08] Christel Baier and Joost-Pieter Katoen. *Principles of model checking*. MIT Press, 2008.

[BMR17] Damien Busatto-Gaston, Benjamin Monmege, and Pierre-Alain Reynier. Optimal reachability in divergent weighted timed games. In Javier Esparza and Andrzej S. Murawski, editors, *Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings*, volume 10203 of Lecture Notes in Computer Science, pages 162-178, 2017. doi:10.1007/978-3-662-54458-7\_10.

[BMR18] Damien Busatto-Gaston, Benjamin Monmege, and Pierre-Alain Reynier. Symbolic approximation of weighted timed games. In Sumit Ganguly and Paritosh Pandya, editors, *38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018, December 11-13, 2018, Ahmedabad, India*, volume 122 of Leibniz International Proceedings in Informatics (LIPICS), pages 28:1-28:16. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2018. doi:10.4230/LIPICS.FSTTCS.2018.28.