Playing Stochastically in Weighted Timed Games to Emulate Memory

TL;DR

This work investigates how stochastic (randomized) strategies can substitute for finite-memory strategies in weighted timed games (WTGs) and, conversely, how memory can emulate randomness. It defines a rigorous stochastic framework for WTGs, establishing measurability and finiteness conditions for expected payoffs, and demonstrates that in divergent WTGs and in untimed shortest-path games (SPGs) the stochastic value equals the deterministic value. The authors prove that Min can emulate memory with randomization and that Max can play memoryless optimally against Min’s strategies, leading to a determinacy result where stochastic, memoryless, and deterministic values all coincide for these classes. They also introduce switching strategies for Min in divergent WTGs and construct a memoryless stochastic interpolation η^p to approximate switching behavior, providing algorithmic insights via region-based analyses. Overall, the paper clarifies the memory-randomness trade-off, yielding practical implications for strategy design in real-time quantitative games and suggesting avenues for efficient synthesis and implementation.

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.

Figures (12)

• Figure 1: On the left, an SPG, where $\mathsf{Min}\xspace$ requires memory to play optimally. In the middle, the Markov Decision Process obtained when letting $\mathsf{Min}\xspace$ play at random, with a parametric probability $p\in(0,1)$. On the right, the Markov Chain obtained when $\mathsf{Max}\xspace$ plays along a memoryless randomised strategy, with a parametric probability $q\in[0,1]$.
• Figure 2: On the left, a (one-clock) weighted timed game. On the right, the value function of location $\ell\xspace_2$, with respect to the value of clock $x$, is obtained as the minimum of two curves.
• Figure 3: A (one-player) WTG with a single clock $x$ and all weights equal to 0.
• Figure 4: A WTG where $\mathsf{Min}\xspace$ has a strategy reaching the target with probability 1 but with an expected weight equal to $+\infty$.
• Figure 5: A one-clock WTG where $\overline{\mathsf{mVal}\xspace}\xspace_{\ell\xspace_0, 0} > \underline{\mathsf{mVal}\xspace}\xspace_{\ell\xspace_0, 0}$.

Theorems & Definitions (81)

• Definition 2.1
• Definition 3.1
• Example 3.2
• Remark 3.4
• Lemma 3.5
• proof
• Proposition 3.5
• Lemma 3.6
• proof
• Example 3.7