Deciding the Value of Two-Clock Almost Non-Zeno Weighted Timed Games

Vialard, Isa

doi:10.4230/LIPIcs.CSL.2026.33

Deciding the Value of Two-Clock Almost Non-Zeno Weighted Timed Games

Isa Vialard

Max Planck Institute for Informatics, Saarland Informatics Campus, Saarbrücken, Germany

Abstract

The Value Problem for weighted timed games (wtgs) consists in determining, given a two-player weighted timed game with a reachability objective and a rational threshold, whether or not the value of the game exceeds the threshold. When restrained to wtgs with non-negative weight, this problem is known to be undecidable for weighted timed games with three or more clocks, and decidable for one-clock wtgs. The Value Problem for two-clock non-negative wtgs, which remained stubbornly open for a decade, was recently shown to be undecidable. In this paper, we show that the Value Problem is decidable when considering two-clock almost non-Zeno wtgs.

Keywords and phrases:

Weighted timed games, decidability, real-time systems

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Timed and hybrid models

Related Version:

arXiv Version: https://arxiv.org/abs/2508.00014

Acknowledgements:

I want to thank Quentin Guilmant for his help in formalizing the proofs in Section A.1.

DOI:

10.4230/LIPIcs.CSL.2026.33

Event:

34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Editors:

Stefano Guerrini and Barbara König

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Introduced by Alur and Dill ([2]) in the early 1990s, a timed automaton is an automaton where transitions are limited by time constraints on a set of finite clocks. Weighted timed automata, also known as priced timed automata, are timed automata with integer costs added to locations and transitions. These costs can be punctual, or linear in terms of time spent in a location. Timed automata and weighted timed automata are powerful models for real-time systems – for instance task scheduling, controller synthesis, energy-aware systems, etc.

Real-time systems often have to deal with perturbations from an uncontrollable environment (for instance, a user). This can be modelled by timed games: timed automata where transitions are divided among two players, the control, who has a reachability objective, versus the environment.

When adding costs to timed games, we obtain weighted timed games (wtgs): $\mathsf{Min}$ (the control) now attempts to reach a goal location while minimizing the cost of doing so, against her opponent $\mathsf{Max}$ (the environment).

A natural problem on wtgs is the following: Given a wtg, can we compute its Value, i.e., the infimum of the optimal cost¹¹1where the optimal cost is the supremum on all possible strategies of $\mathsf{Max}$ of the weight of the path produced by the strategy profile. on all strategies of $\mathsf{Min}$ ? Or, formulated as a decision problem: is its Value less than or equal to $c$ ?

This is the Value Problem, not to be confused with the Existence Problem: Given a wtg and a threshold $c$ , does $\mathsf{Min}$ have a strategy to reach her goal location with cost at most $c$ ? These two problems can yield different answers (see Figure 1).

Figure 1: Example of a wtg where the Value is

0

, but every strategy of

\mathsf{Min}

yields cost

>0

.

In this paper, we focus on the Value Problem. While decidable for weighted timed automata, the Value Problem is undecidable for weighted timed games ([6]).

However, one can recover decidability by restricting the number of clocks. Bouyer et al. ([7]) establish that the Value problem is decidable for one-clock wtg with non-negative weights. This decidability result is extended to one-clock wtg with arbitrary weights in [16]. On the other hand, Bouyer et al. ([6]) prove undecidability for wtgs with non-negative weight and $3$ -clocks or more. Brihaye et al. ([10]) show undecidability of two-clock wtg with arbitrary weights. Only recently, Guilmant et al. ([15]) proved undecidability of two-clock, time-bounded wtg with non-negative weights.

Another way to recover decidability is with non-Zeno (or divergence) properties. A wtg with non-negative weights has a strictly non-Zeno cost property when every cycle is of cost at least $1$ . Intuitively, this property forbids any “Zeno paradox” behaviour. Strictly non-Zeno wtgs can be enfolded into acyclic wtgs; hence, the Value Problem is decidable ([5]). This result was generalized to wtgs with arbitrary weight in [11], for which non-Zenoness becomes divergence.²²2A wtg is divergent if every strongly connected component has either cycles of weight in $\mathchoice{\left(-\infty,-1\right]}{\left(-\infty,-1\right]}{\left(-\infty,-1% \right]}{\left(-\infty,-1\right]}$ or cycles of weight in $\mathchoice{\left[1,\infty\right)}{\left[1,\infty\right)}{\left[1,\infty\right% )}{\left[1,\infty\right)}$ .

Divergence properties can be weakened into almost-divergence properties. A wtg with non-negative weight is said to be almost non-Zeno (or almost strictly non-Zeno, or almost strongly non-Zeno) if its cycles are of weight $0$ , or at least $1$ . Bouyer et al. ([6]) establish that the Value of such wtgs is approximable³³3i.e., can be computed to arbitrary precision. (but still undecidable). Busatto-Gaston et al. ([12]) extend this result to almost divergent⁴⁴4A wtg is almost divergent if every strongly connected component has either cycles of weight in $\mathchoice{\left(-\infty,-1\right]}{\left(-\infty,-1\right]}{\left(-\infty,-1% \right]}{\left(-\infty,-1\right]}\cup\{0\}$ , or cycles of weight in $\{0\}\cup\mathchoice{\left[1,\infty\right)}{\left[1,\infty\right)}{\left[1,% \infty\right)}{\left[1,\infty\right)}$ . wtgs with arbitrary weights.

Figure 2: Landscape of WTG decidability and approximability.

Contributions

The main theorem of this paper is the following:

Theorem 1.

Given a two-player, turn-based, two-clocks, almost non-Zeno weighted timed game with non-negative integer weights, the Value Problem is decidable.

The proof of Theorem 1 relies on the partial unfolding used in the approximability proof of [6], and on several techniques to turn a wtg into an equivalent, simpler game with desirable properties, such as the relaxing of guards, or adding clock resets to every transition.

2 Definitions

Let $\mathcal{X}$ be a finite set of clocks. Clock constraints (or guards) over $\mathcal{X}$ are expressions of the form $x\mathrel{\bowtie}n$ , where $x,y\in\mathcal{X}$ are clocks, ${\bowtie}\in\{<,\leq,=,\geq,>\}$ is a comparison symbol, and $n\in\mathbb{N}$ is a natural number. We write $\mathcal{C}$ to denote the set of all clock constraints over $\mathcal{X}$ . A valuation on $\mathcal{X}$ is a function $\nu:\mathcal{X}\to\mathbb{R}_{\geq 0}$ . For $d\in\mathbb{R}_{\geq 0}$ we denote by $\nu+d$ the valuation such that, for every clock $x\in\mathcal{X}$ , $(\nu+d)(x)=\nu(x)+d$ . Let $X\subseteq\mathcal{X}$ be a subset of all clocks. We write $\nu[X:=0]$ for the valuation such that, for every clock $x\in X$ , $\nu[X:=0](x)=0$ , and $\nu[X:=0](y)=\nu(y)$ for all other clocks $y\notin X$ . For $C\subseteq\mathcal{C}$ a set of clock constraints over $\mathcal{X}$ , we say that the valuation $\nu$ satisfies $C$ , denoted $\nu\models C$ , if and only if all the comparisons in $C$ hold when replacing each clock $x$ by its corresponding value $\nu(x)$ .

Definition 2.

A (turn-based) weighted timed game is given by a tuple $\mathcal{G}=$ $(L_{\mathsf{Min}},L_{\mathsf{Max}},G,\mathcal{X},T,w)$ , where:

$\blacksquare$

$L_{\mathsf{Min}}$ and $L_{\mathsf{Max}}$ are the (disjoint) sets of locations belonging to Players $\mathsf{Min}$ and $\mathsf{Max}$ respectively; we let $L=L_{\mathsf{Min}}\cup L_{\mathsf{Max}}$ denote the set of all locations. (In drawings, locations belonging to $\mathsf{Min}$ are depicted by blue circles, and those belonging to $\mathsf{Max}$ are depicted by red squares.)
$\blacksquare$

$G\subseteq L_{\mathsf{Min}}$ are the goal locations.
$\blacksquare$

$\mathcal{X}$ is a set of clocks.
$\blacksquare$

$T\subseteq(L\setminus G)\times 2^{\mathcal{C}}\times 2^{\mathcal{X}}\times L$ is a set of (discrete) transitions. A transition $\ell\xrightarrow{C,X}\ell^{\prime}$ enables moving from location $\ell$ to location $\ell^{\prime}$ , provided all clock constraints in $C$ are satisfied, and afterwards resetting all clocks in $X$ to zero.
$\blacksquare$

$w:(L\setminus G)\cup T\to\mathbb{Z}$ is a weight function.

In the above, we assume that all data (set of locations, set of clocks, set of transitions, set of clock constraints) are finite.

Let $\mathcal{G}=(L_{\mathsf{Min}},L_{\mathsf{Max}},G,\mathcal{X},T,w)$ be a wtg. A configuration over $\mathcal{G}$ is a pair $(\ell,\nu)$ , where $\ell\in L$ and $\nu$ is a valuation on $\mathcal{X}$ . Let $d\in\mathbb{R}_{\geq 0}$ be a delay and $t=\ell\xrightarrow{C,X}\ell^{\prime}\in T$ be a discrete transition. One then has a delayed transition (or simply a transition if the context is clear) $(\ell,\nu)\xrightarrow{d,t}(\ell^{\prime},\nu^{\prime})$ provided that $\nu+d\models C$ and $\nu^{\prime}=(\nu+d)[X:=0]$ . Intuitively, control remains in location $\ell$ for $d$ time units, after which it transitions to location $\ell^{\prime}$ , resetting all the clocks in $X$ to zero in the process. The weight of such a delayed transition is $d\cdot w(\ell)+w(t)$ , taking account both of the time spent in $\ell$ as well as the weight of the discrete transition $t$ .

As noted in [13], without loss of generality one can assume that no configuration (other than those associated with goal locations) is deadlocked; in other words, for any location $\ell\in L\setminus G$ and valuation $\nu\in\mathbb{R}_{\geq 0}^{\mathcal{X}}$ , there exists $d\in\mathbb{R}_{\geq 0}$ and $t\in T$ such that $(\ell,\nu)\xrightarrow{d,t}(\ell^{\prime},\nu^{\prime})$ .⁵⁵5This can be achieved by adding unguarded transitions to a sink location for all locations controlled by $\mathsf{Min}$ and unguarded transitions to a goal location for the ones controlled by $\mathsf{Max}$ .

Let $k\in\mathbb{N}$ . A run $\rho$ of length $k$ over $\mathcal{G}$ from a given configuration $(\ell_{0},\nu_{0})$ is a sequence of matching delayed transitions, as follows:

\rho=(\ell_{0},\nu_{0})\xrightarrow{d_{0},t_{0}}(\ell_{1},\nu_{1})\xrightarrow% {d_{1},t_{1}}\cdots\xrightarrow{d_{k-1},t_{k-1}}(\ell_{k},\nu_{k})\,.

The weight of $\rho$ is the cumulative weight of the underlying delayed transitions:

\mathsf{weight}(\rho)=\sum_{i=0}^{k-1}(d_{i}\cdot w(\ell_{i})+w(t_{i}))\,.

An infinite run $\rho$ is defined in the obvious way; however, since no goal location is ever reached, its weight is defined to be infinite: $\mathsf{weight}(\rho)=+\infty$ .

A run is maximal if it is either infinite or cannot be extended further. Thanks to our deadlock-freedom assumption, finite maximal runs must end in a goal location. We refer to maximal runs as plays.

We now define the notion of strategy. Recall that locations of $\mathcal{G}$ are partitioned into sets $L_{\mathsf{Min}}$ and $L_{\mathsf{Max}}$ , belonging respectively to Players $\mathsf{Min}$ and $\mathsf{Max}$ . Let Player $\mathsf{P}\in\{\mathsf{Min},\mathsf{Max}\}$ , and write $\mathcal{FR}_{\mathcal{G}}^{\mathsf{P}}$ to denote the collection of all non-maximal finite runs of $\mathcal{G}$ ending in a location belonging to Player $\mathsf{P}$ . A strategy for Player $\mathsf{P}$ is a mapping $\sigma_{\mathsf{P}}:\mathcal{FR}_{\mathcal{G}}^{\mathsf{P}}\to\mathbb{R}_{\geq 0% }\times T$ such that for all finite runs $\rho\in\mathcal{FR}_{\mathcal{G}}^{\mathsf{P}}$ ending in configuration $(\ell,\nu)$ with $\ell\in L_{\mathsf{P}}$ , the delayed transition $(\ell,\nu)\xrightarrow{d,t}(\ell^{\prime},\nu^{\prime})$ is valid, where $\sigma_{\mathsf{P}}(\rho)=(d,t)$ and $(\ell^{\prime},\nu^{\prime})$ is some configuration (uniquely determined by $\sigma_{\mathsf{P}}(\rho)$ and $\nu$ ).

Let us fix a starting configuration $(\ell_{0},\nu_{0})$ , and let $\sigma_{\mathsf{Min}}$ and $\sigma_{\mathsf{Max}}$ be strategies for Players $\mathsf{Min}$ and $\mathsf{Max}$ respectively (one speaks of a strategy profile). Let us denote by $\mathsf{play}_{\mathcal{G}}((\ell_{0},\nu_{0}),\sigma_{\mathsf{Min}},\sigma_{% \mathsf{Max}})$ the unique maximal run starting from configuration $(\ell_{0},\nu_{0})$ and unfolding according to the strategy profile $(\sigma_{\mathsf{Min}},\sigma_{\mathsf{Max}})$ : in other words, for every strict finite prefix $\rho$ of $\mathsf{play}_{\mathcal{G}}((\ell_{0},\nu_{0}),\sigma_{\mathsf{Min}},\sigma_{% \mathsf{Max}})$ in $\mathcal{FR}_{\mathcal{G}}^{\mathsf{P}}$ , the delayed transition immediately following $\rho$ in $\mathsf{play}_{\mathcal{G}}((\ell_{0},\nu_{0}),\sigma_{\mathsf{Min}},\sigma_{% \mathsf{Max}})$ is labelled with $\sigma_{\mathsf{P}}(\rho)$ .

Recall that the objective of Player $\mathsf{Min}$ is to reach a goal location through a play whose weight is as small possible. Player $\mathsf{Max}$ has an opposite objective, trying to avoid goal locations, and, if not possible, to maximise the cumulative weight of any attendant play. This gives rise to the following two symmetrical definitions:

	$\displaystyle\overline{\mathsf{Val}}_{\mathcal{G}}(\ell_{0},\nu_{0})$	$\displaystyle=\inf_{\sigma_{\mathsf{Min}}}\left\{\sup_{\sigma_{\mathsf{Max}}}% \left\{\mathsf{weight}(\mathsf{play}_{\mathcal{G}}((\ell_{0},\nu_{0}),\sigma_{% \mathsf{Min}},\sigma_{\mathsf{Max}}))\right\}\right\}\mbox{\ and}$
	$\displaystyle\underline{\mathsf{Val}}_{\mathcal{G}}(\ell_{0},\nu_{0})$	$\displaystyle=\sup_{\sigma_{\mathsf{Max}}}\left\{\inf_{\sigma_{\mathsf{Min}}}% \left\{\mathsf{weight}(\mathsf{play}_{\mathcal{G}}((\ell_{0},\nu_{0}),\sigma_{% \mathsf{Min}},\sigma_{\mathsf{Max}}))\right\}\right\}\,.$

$\overline{\mathsf{Val}}_{\mathcal{G}}(\ell_{0},\nu_{0})$ represents the smallest possible weight that Player $\mathsf{Min}$ can possibly achieve, starting from configuration $(\ell_{0},\nu_{0})$ , against best play from Player $\mathsf{Max}$ , and conversely for $\overline{\mathsf{Val}}_{\mathcal{G}}(\ell_{0},\nu_{0})$ : the latter represents the largest possible weight that Player $\mathsf{Max}$ can enforce, against best play from Player $\mathsf{Min}$ .⁶⁶6Technically speaking, these values may not be literally achievable; however given any $\varepsilon>0$ , both players are guaranteed to have strategies that can take them to within $\varepsilon$ of the optimal value. As noted in [13], turned-based wtgs are determined, and therefore $\overline{\mathsf{Val}}_{\mathcal{G}}(\ell_{0},\nu_{0})=\underline{\mathsf{Val% }}_{\mathcal{G}}(\ell_{0},\nu_{0})$ for any starting configuration $(\ell_{0},\nu_{0})$ ; we denote this common value by $\mathsf{Val}_{\mathcal{G}}(\ell_{0},\nu_{0})$ .

$\blacktriangleright$ Remark 3.

Note that $\mathsf{Val}_{\mathcal{G}}(\ell_{0},\nu_{0})$ can take on real numbers, or either of the values $-\infty$ and $+\infty$ . However, since reachability is decidable in timed games, it is decidable whether $\mathsf{Val}_{\mathcal{G}}(\ell_{0},\nu_{0})=+\infty$ or not.

In the remainder of this paper, every weighted timed game is turn-based, with non-negative weights, of value in $\mathbb{R}$ .

3 Unfolding Almost Non-Zeno Weighted Timed Games

Let us first give an informal definition of the region construction $\mathcal{R}(\mathcal{G})$ of a wtg $\mathcal{G}$ . In Section 4.2, we will give a more formal definition, in the special case of $\mathchoice{\left[0,1\right)}{\left[0,1\right)}{\left[0,1\right)}{\left[0,1% \right)}$ -wtgs. The region partition of $\mathcal{G}$ is the finest partition of the clock valuations into regions, where each region is defined by guards of the form $x\bowtie k$ or $x-y\bowtie n$ with $x,y\in\mathcal{X}$ , $\bowtie\in\{<,\leq,=,\geq,>\}$ and $n\leq N$ the largest constant in guards of $\mathcal{G}$ . For instance, $\left\{{(x,y)}\;:\;{x=3,N<y}\right\}$ and $\left\{{(x,y)}\;:\;{1<x<2,3<y<4,x-2<y-3}\right\}$ are regions.

We denote by $\mathcal{R}(\mathcal{G})$ the region automaton associated with a wtg $\mathcal{G}$ (see [2]). In $\mathcal{R}(\mathcal{G})$ , every location $\ell$ is assigned a unique region $\mathsf{reg}(\ell)$ of accessible valuations.

Bouyer et al. ([6]) showed that, even though the Value Problem is undecidable for wtg with non-negative weight and $3$ clocks or more, it is approximable in the subclass of almost non-Zeno wtg. In this section, we use the structure of their proof of approximability to prove decidability for almost non-Zeno wtgs with $2$ clocks.

Definition 4 (Almost non-Zeno wtg).

A wtg $\mathcal{G}$ is almost non-Zeno if there exists $\kappa>0$ such that for any finite run $\rho$ in $\mathcal{G}$ that follows a region cycle of $\mathcal{R}(\mathcal{G})$ , $\mathsf{weight}(\rho)=0$ or $\geq\kappa$ .

$\blacktriangleright$ Remark 5.

It is decidable whether a weighted timed game is almost non-Zeno or not (by enumerating all simple cycles in the corner-point abstraction of $\mathcal{G}$ , see [4]).

In an acyclic wtg, the value is decidable and can be computed from the target locations up to the initial location, by computing for each node $\ell$ a function $W_{\ell}:\mathsf{reg}(\ell)\to\mathbb{R}$ which assigns to a valuation $\nu\in\mathsf{reg}(\ell)$ the optimal weight $\mathsf{Val}_{\mathcal{G}}(\ell,\nu)$ . By construction, every $W_{\ell}$ is a piecewise linear function.

Intuitively, we will unfold cycles of weight $\geq\kappa$ to obtain a “tree-like” wtg where only cycles of weight $0$ are left; we will deal with them separately.

Semi-unfolding

For any wtg $\mathcal{G}$ , let $\tilde{\mathcal{G}}$ be the semi-unfolded wtg built from $\mathcal{R}(\mathcal{G})$ in [6]:

First color in green every location and edge that are part of a cycle of weight $0$ . Observe that you can modify any wtg such that any green location has weight $0$ ⁷⁷7[6] make a similar observation, but their construction implies adding a clock.: in a trimmed⁸⁸8A trimmed region wtg is a region wtg where we have erased inaccessible locations and redundant guards. It will be detailed later in Definition 13. region wtg, if a location $\ell\in L_{\mathsf{P}}$ of weight $p>0$ is part of a cycle of weight $0$ , then there exists an outgoing transition from $\ell$ with a guard $x=0$ for some clock $x$ . Therefore, as in Figure 3, one can add a location $\ell_{0}$ of weight $0$ in $L_{\mathsf{P}}$ such that:

$\blacksquare$

every transition arriving in $\ell$ arrives in $\ell_{0}$ instead.
$\blacksquare$

every green transition leaving $\ell$ leaves $\ell_{0}$ instead.
$\blacksquare$

there is a transition $\ell_{0}\overset{x=0}{\rightarrow}\ell$ .

Thus let us assume that every green location has weight $0$ .

Figure 3: How to ensure that every green location has weight

0

. Thick green transitions and locations are part of cycles of weight

0

, locations labeled with weight

0

or

p

belong to the same player.

We define $\mathcal{K}$ the kernel of $\mathcal{G}$ as the restriction of $\mathcal{R}(\mathcal{G})$ to fully-green strongly connected components. Edges that leave $\mathcal{K}$ are called the output edges of $\mathcal{K}$ .

Then we partially unfold $\mathcal{R}(\mathcal{G})$ into a finite tree structure $\mathcal{T}(\mathcal{G})$ : starting from the initial location $i$ as a root, we follow every possible path in $\mathcal{G}$ , with a node for each time we visit a (non kernel) location, as to avoid creating cycles. However when along a branch we enter the kernel in some location $\ell$ , we create a node $\mathcal{K}_{\ell}$ instead of $\ell$ , and for each output edge $t$ of $\mathcal{K}$ accessible from $\ell$ , with $t$ leading to a location $\ell^{\prime}$ , let $\ell^{\prime}$ (or $\mathcal{K}_{\ell}^{\prime}$ if $\ell^{\prime}\in\mathcal{K}$ ) be a child of $\mathcal{K}_{\ell}$ , and continue to unfold from there.

We stop unfolding when, along any branch, a location or edge with positive weight of $\mathcal{R}(\mathcal{G})$ is visited at least $W/\kappa+2$ times, where $W$ is an upper bound on the value of $\mathcal{G}$ .⁹⁹9obtained by using the corner-point abstraction, or considering a memoryless region-uniform strategy for $\mathsf{Min}$ .

To obtain $\tilde{\mathcal{G}}$ from $\mathcal{T}(\mathcal{G})$ , replace each node $\mathcal{K}_{\ell}$ by a copy of the strongly connected component of $\mathcal{K}$ that contains $\ell$ (see [6] for the formal construction). Then $\mathsf{Val}_{\tilde{\mathcal{G}}}(i,\nu)=\mathsf{Val}_{\mathcal{G}}(i,\nu)$ for any $\nu\in\mathsf{reg}(i)$ .

In the partially unfolded games $\tilde{\mathcal{G}}$ with three clocks or more, the cause of undecidability is inside the kernel nodes. Hence, in [6], the approximation happens in the kernels. However, with only two clocks, the value is decidable in kernel weighted timed games:

Definition 6 (Kernel weighted timed games).

A kernel weighted timed game $\mathcal{G}$ is a $[0,1]$ -wtg $(L_{\mathsf{Min}},L_{\mathsf{Max}},G,\mathcal{X},T,w,w_{\mathsf{out}})$ where every location or transition is of weight $0$ , and each target location $\ell\in G$ has an output weight function $w_{\mathsf{out}}(\ell,\cdot):\mathsf{reg}(\ell)\to\mathbb{R}$ which is continuous and piecewise linear. In later notations, we omit $w$ .

Theorem 7.

For any two-clock kernel wtg $\mathcal{G}$ , for any location $i\in\mathcal{G}$ , $W_{i}$ is a continuous piecewise linear function which can be computed through the value iteration algorithm.

This is the main technical result of this paper, which we will prove in Section 5. Let us show first how Theorem 7 entails value decidability of the partial enfolding $\tilde{\mathcal{G}}$ :

Lemma 8.

For every node $n$ in the tree $\mathcal{T}(\mathcal{G})$ , one can compute $W_{n}$ a continuous piecewise linear function such that $W_{n}:\nu\mapsto\mathsf{Val}_{\tilde{\mathcal{G}}}(\ell,\nu)$ , where $\ell$ is either $n$ if $n\not\in\mathcal{K}$ , or the entrance location of $n=\mathcal{K}_{\ell}$ .

Proof.

In the tree structure of $\tilde{\mathcal{G}}$ , consider a node $n$ : if $n$ is a leaf, then $n\in G$ . Thus let $W_{n}$ be the constant null function. Now consider that $n$ is not a leaf, and by induction hypothesis assume that for every child $n^{\prime}$ of $n$ , $W_{n}^{\prime}$ is continuous and piecewise linear. If $n=\ell\not\in\mathcal{K}$ then

W_{n}:\nu\mapsto\underset{\nu+\delta\models C}{\underset{n\overset{C,X}{% \rightarrow}n^{\prime}\in\mathcal{T}(\mathcal{G})}{\inf/\sup}}W_{n^{\prime}}(% \nu+\delta[{X}:=0])\,.

Thus by induction $W_{n}$ is also continuous and piecewise linear.

Otherwise, $n=\mathcal{K}_{\ell}$ for some $\ell\in\mathcal{K}$ . Let $K$ be the SCC containing $\ell$ , and $T_{\mathsf{out}}$ the output edges leaving from $K$ . Consider the kernel wtg $K_{\ell}=(L^{\prime}_{\mathsf{Min}},L^{\prime}_{\mathsf{Max}},G^{\prime},% \mathcal{X},T^{\prime},w_{\mathsf{out}})$ where

$\blacksquare$

$G^{\prime}=\left\{{\ell_{t}}\;:\;{t\in T_{out}}\right\}$ .
$\blacksquare$

For every $\mathsf{P}$ , $L^{\prime}_{\mathsf{P}}=K\cap L_{\mathsf{P}}$ .
$\blacksquare$

$T^{\prime}=T_{|K\times K}\cup\left\{\;{\ell^{\prime}\overset{C,X}{\to}\ell_{t}% \,|\,t:\ell^{\prime}\overset{C,X}{\to}\ell^{\prime\prime}\in T_{out}}\;\right\}$
$\blacksquare$

for every $t:\ell^{\prime}\overset{C,X}{\to}\ell^{\prime\prime}\in T_{\mathsf{out}}$ , $w_{\mathsf{out}}(\ell_{t},\cdot):\nu\mapsto W_{\ell^{\prime\prime}}(\nu)+w(t)$ , which is piecewise linear by induction hypothesis.
$\blacksquare$

$w^{\prime}$ maps to $0$ always.

Then $W_{n}=\mathsf{Val}_{K_{\ell}}(\ell,\cdot)$ , which is piecewise linear according to Theorem 7. $\hfill\blacktriangleleft$

This is sufficient to conclude the proof of Theorem 1.

Theorem 1. [Restated, see original statement.]

Given a two-player, turn-based, two-clocks, almost non-Zeno weighted timed game with non-negative integer weights, the Value Problem is decidable.

4 Simplifying Transformations of Kernel Games

Before proving Theorem 7, let us apply some useful simplifying transformations that preserve the value. These transformations happen in four steps:

Step $1$ :: Transform a WTG into a WTG with clock values in $\mathchoice{\left[0,1\right)}{\left[0,1\right)}{\left[0,1\right)}{\left[0,1% \right)}$ .
Step $2$ :: Transform a wtg into a region trimmed wtg, i.e., a wtg where to every location is assigned a region, and without any “useless” transition, or guard on transition.
Step $3$ :: Transform a trimmed region kernel wtg by relaxing every strict guard into a strict-or-equal guard.
Step $4$ :: Transform a relaxed trimmed region kernel wtg such that every transition resets at least one clock.

Commentaries

Step $1$ only serves to lighten notations in the rest of this paper. In terms of state complexity, the transformations $1+2$ increase the number of locations as much as the classical region construction.

Trimming a wtg in step $2$ is necessary: without it, Step $3$ would create pathological cases where relaxing some guards would allow a player to take transitions that would have been unreachable in the original wtg.

Relaxing guards in step $3$ is a technique that has merits of its own outside of the scope of the proof. For instance, the value of a wtg might not be reached by an optimal strategy for $\mathsf{Min}$ , but could be the infimum produced by a set of strategies $\epsilon$ -close to an optimal strategy in the relaxed wtg.

Relaxing guard is also a prerequisite for step $4$ , which is the most important of all four steps. In a two-clock wtg, resetting at least one clock in each transition allows us to consider only regions in one dimension. Reducing a two-dimension problem to a one-dimension one is key to the termination argument in Section 5.

4.1 Restraining Clock Values to [0,1)

Before presenting the well-known notions of regions and region wtgs, let us first restrict the setting to $\mathchoice{\left[0,1\right)}{\left[0,1\right)}{\left[0,1\right)}{\left[0,1% \right)}$ -wtgs, which will simplify the region notations.

Definition 9.

A [0,1)-wtg is a weighted timed game where for every reachable configuration $(\ell,\nu)$ , $0\leq\nu(x)<1$ for any clock $x$ .

Lemma 10.

For any wtg $\mathcal{G}$ , there is an equivalent $\mathchoice{\left[0,1\right)}{\left[0,1\right)}{\left[0,1\right)}{\left[0,1% \right)}$ -wtg $\mathcal{G}^{\prime}$ .

Proof.

See [7], Proposition 2 for a detailed proof. Their proof is for $1$ -clock wtg, however, the construction can easily be generalized to any number of clocks.

The intuition of the construction is that the information of the integer parts of the clock can be contained in the locations, while the clocks keep track only of the fractional part: Let $\mathcal{G}=(L_{\mathsf{Min}},L_{\mathsf{Max}},G,\mathcal{X},T,w)$ and let us build $\mathcal{G^{\prime}}=(L^{\prime}_{\mathsf{Min}},L^{\prime}_{\mathsf{Max}},G,% \mathcal{X},T^{\prime},w^{\prime})$ . First, w.l.o.g., let us assume that all clocks are bounded by an integer $M$ ([3]). Then, for $\mathsf{P}\in\left\{\;{\mathsf{Min},\mathsf{Max}}\;\right\}$ , let $L_{\mathsf{P}}^{\prime}=L_{\mathsf{P}}\times M^{|\mathcal{X}|}$ , and define $T^{\prime}$ and $w^{\prime}$ such that a valuation $\nu=(x_{1},\dots,x_{|\mathcal{X}|})\in\mathchoice{\left[0,1\right)}{\left[0,1% \right)}{\left[0,1\right)}{\left[0,1\right)}^{\mathcal{X}}$ in a location $(\ell,n_{1},\dots,n_{|\mathcal{X}|})$ in $\mathcal{G}^{\prime}$ is equivalent to a valuation $(n_{1}+x_{1},\dots,n_{|\mathcal{X}|}+x_{|\mathcal{X}|})$ in location $\ell$ in $\mathcal{G}$ . Note that every transition of $\mathcal{G}^{\prime}$ , with a guard $x=1$ for some clock $x$ , resets $x$ . $\hfill\blacktriangleleft$

4.2 Regions and Region Trimmed Games

Definition 11.

Let $\mathcal{X}$ be a set of clocks in a $\mathchoice{\left[0,1\right)}{\left[0,1\right)}{\left[0,1\right)}{\left[0,1% \right)}$ -wtg. A region over $\mathcal{X}$ is a tuple $r=(X_{0},\dots,X_{p},X_{=1})$ such that $X_{i}\neq\emptyset$ for all $1\leq i\leq p$ , and $\{X_{0},\dots,X_{p},X_{=1}\}$ is a partition of $\mathcal{X}$ : $\mathcal{X}=\biguplus_{i=0}^{p}X_{i}$

We denote by $\operatorname{Reg}_{\mathcal{X}}$ the set of regions over $\mathcal{X}$ . A valuation $\nu$ is said to belong to the region $r$ , denoted by $\nu\sqsubset r$ , whenever

$\blacksquare$

$\forall x\in\mathcal{X}$ , $\nu(x)=0\Leftrightarrow x\in X_{0}$ ,
$\blacksquare$

$\forall x\in\mathcal{X}$ , $\nu(x)=1\Leftrightarrow x\in X_{=1}$ ,
$\blacksquare$

$\forall x,y\in\mathcal{X}$ , $\ \nu(x)<\nu(y)<1\Leftrightarrow\exists i,j\in\{0,\dots,p\}\text{ s.t. }i<j% \wedge x\in X_{i}\wedge y\in X_{j}$ .

For $r=(X_{0},\dots,X_{p},X_{=1})$ a region and $X$ a non-empty subset of $\mathcal{X}$ , we denote by $r[X:=0]$ the region $(X_{0}\cup X,X_{1}\setminus X,\dots,X_{p}\setminus X,X_{=1}\setminus X)$ . In other words, $r[X:=0]$ is the region such that if $\nu$ belongs to $r$ then $\nu[X:=0]$ belongs to $r[X:=0]$ . A $\mathchoice{\left[0,1\right)}{\left[0,1\right)}{\left[0,1\right)}{\left[0,1% \right)}$ -region is a region $(X_{0},\dots,X_{p},X_{=1})$ where $X_{=1}=\emptyset$ . Let us abuse notation and denote $r$ by $(X_{0},\dots,X_{p})$ . We denote by $\operatorname{Reg}^{<}_{\mathcal{X}}$ the set $\mathchoice{\left[0,1\right)}{\left[0,1\right)}{\left[0,1\right)}{\left[0,1% \right)}$ -regions over $\mathcal{X}$ .

A time-successor of a region $r$ , with $r=(X_{0},\dots,X_{p})\in\operatorname{Reg}^{<}_{\mathcal{X}}$ is a region $r^{\prime}=(X^{\prime}_{0},\dots,X^{\prime}_{p^{\prime}},X^{\prime}_{=1})$ such that either $r^{\prime}=r$ ; or $X_{0}^{\prime}=\emptyset$ and $X^{\prime}_{i}=X_{i-1}$ for $1\leq i\leq p$ , and either $X_{p}=X^{\prime}_{=1}$ or $X_{p}=X^{\prime}_{p+1}$ (and then $X^{\prime}_{=1}=\emptyset$ ).

We often abuse notation and write $r$ for the set of valuations $\nu\sqsubset r$ it represents.

Definition 12 (Region wtg [4, 12]).

Let $\mathcal{G}=(L_{\mathsf{Min}},L_{\mathsf{Max}},G,\mathcal{X},T,w)$ be a $\mathchoice{\left[0,1\right)}{\left[0,1\right)}{\left[0,1\right)}{\left[0,1% \right)}$ -wtg. The region wtg $\mathcal{R}(\mathcal{G})$ of $\mathcal{G}$ is the $\mathchoice{\left[0,1\right)}{\left[0,1\right)}{\left[0,1\right)}{\left[0,1% \right)}$ -wtg $\mathcal{R}(\mathcal{G})=(L^{\prime}_{\mathsf{Min}},L^{\prime}_{\mathsf{Max}},% G^{\prime},\mathcal{X},T^{\prime},w^{\prime})$ with

$\blacksquare$

$L^{\prime}_{\mathsf{P}}=L_{\mathsf{P}}\times\operatorname{Reg}^{<}_{\mathcal{X}}$ for $\mathsf{P}\in\{\mathsf{Min},\mathsf{Max}\}$ .
$\blacksquare$

$G^{\prime}=G\times\operatorname{Reg}^{<}_{\mathcal{X}}$ .
$\blacksquare$

For every $r=(X_{0},\dots X_{p})\in\operatorname{Reg}^{<}_{\mathcal{X}}$ , for every $r^{\prime}=(X^{\prime}_{0},\dots,X^{\prime}_{p^{\prime}},X^{\prime}_{=1})\in% \operatorname{Reg}_{\mathcal{X}}$ a time-successor of $r$ , if $\ell\xrightarrow{C,X}\ell^{\prime}\in T$ then $(\ell,r)\xrightarrow{C\cup C(r^{\prime}),X}(\ell^{\prime},r^{\prime}[X:=0])$ , with

$C(r^{\prime})=\left\{{(x=0)}\;:\;{x\in X^{\prime}_{0}}\right\}\cup\left\{{(x=1% )}\;:\;{x\in X^{\prime}_{=1}}\right\}\cup\left\{{(0<x<1)}\;:\;{x\in X^{\prime}% _{i},1\leq i\leq p}\right\}.$
$\blacksquare$

For $\ell\in L_{\mathsf{Min}}\cup L_{\mathsf{Max}}$ and $r\in\operatorname{Reg}^{<}_{\mathcal{X}}$ , $w^{\prime}(\ell,r)=w(\ell)$ .
$\blacksquare$

For $t=(\ell,r)\xrightarrow{C\cup C(r^{\prime}),X}(\ell^{\prime},r^{\prime}[X:=0])% \in T^{\prime}$ , $w^{\prime}(t)=w\left(\ell\xrightarrow{C,X}\ell^{\prime}\right)$ .

While applying simplifying transformations to $\mathcal{R}(\mathcal{G})$ , we wish to preserve the “one-region-per-location” property. Thus let us formally define what is a region wtg (as opposed to the region wtg). A wtg $\mathcal{G}$ is a region weighted timed game if there is a region assignment $\mathsf{reg}:L\to\operatorname{Reg}^{<}_{\mathcal{X}}$ , such that for any transition $t:\ell\xrightarrow{C,X}\ell^{\prime}$ , the valuations $\nu+\delta$ with $\nu\sqsubset\mathsf{reg}(\ell)$ and $\delta\geq 0$ that satisfy $C$ are contained in a unique region $r$ , such that $r[X:=0]=\mathsf{reg}(\ell^{\prime})$ . Furthermore, for any initial configuration $(i,\nu)$ , we require $\nu\sqsubset\mathsf{reg}(i)$ .

Obviously $\mathcal{R}(\mathcal{G})$ is a region wtg for any $\mathchoice{\left[0,1\right)}{\left[0,1\right)}{\left[0,1\right)}{\left[0,1% \right)}$ -wtg $\mathcal{G}$ . For any location $\ell$ in a region wtg, let $X_{\ell}^{\uparrow}\stackrel{{\scriptstyle\mathsf{def}}}{{=}}X_{p}$ with $\mathsf{reg}(\ell)=(X_{0},\dots X_{p})$ .

Let us now “trim” $\mathcal{R}(\mathcal{G})$ , i.e., delete every useless transition, and every useless guard on transitions :

Definition 13 (Trimmed region wtg).

A region $\mathchoice{\left[0,1\right)}{\left[0,1\right)}{\left[0,1\right)}{\left[0,1% \right)}$ -wtg $\mathcal{G}$ is trimmed if for any transition $t:\ell\xrightarrow{C,X}\ell^{\prime}$ and any region $r=\mathsf{reg}(\ell)$ in $\mathcal{G}$ ,

$\blacksquare$

for any valuation $\nu\sqsubset r$ there exist some $\delta\geq 0$ such that $\nu+\delta\models C$ .
$\blacksquare$

for any $c\in C$ , there exists a valuation $\nu\sqsubset r$ and some $\delta\geq 0$ such that $\nu+\delta$ is in $\mathchoice{\left[0,1\right]}{\left[0,1\right]}{\left[0,1\right]}{\left[0,1% \right]}^{\mathcal{X}}$ and $\nu+\delta\not\models c$ .

In other words, there are no inaccessible transitions from any tuple location-region. Furthermore, there are no unnecessary clauses in $C$ (the ones that are always verified from the region). Removing inaccessible transitions and unnecessary clauses can always be done from any region wtg without change in value.

Since every $\mathchoice{\left[0,1\right)}{\left[0,1\right)}{\left[0,1\right)}{\left[0,1% \right)}$ -wtg $\mathcal{G}$ is equivalent to the region $\mathchoice{\left[0,1\right)}{\left[0,1\right)}{\left[0,1\right)}{\left[0,1% \right)}$ -wtg $\mathcal{R}(\mathcal{G})$ , and every region wtg is equivalent to a trimmed region wtg, we can always assume $\mathcal{G}$ to be a trimmed region wtg.

Observation 14.

For $\mathcal{G}$ a trimmed region $\mathchoice{\left[0,1\right)}{\left[0,1\right)}{\left[0,1\right)}{\left[0,1% \right)}$ -wtg, for any transition $t:\ell\xrightarrow{C,X}\ell^{\prime}$ , with $\mathsf{reg}(\ell)=(X_{0},\dots,X_{p})$ :

$\blacksquare$

if $(y=0)\in C$ or $(y>0)\in C$ for some clock $y$ then $y\in X_{0}$ , in other words $y$ is $0$ on the whole region $r$ .
$\blacksquare$

if $(y=1)\in C$ for some clock $y$ , then $y\in X_{p}$ in other words $y$ is one of the clocks with largest value in $r$ .
$\blacksquare$

there cannot be both $x=0$ and $y=1$ in $C$ for any two clocks $x, y$ .

Proof.

For the first point, notice that if $y$ was not $0$ , then either the transition or the clause would have been trimmed. For the second one, if $y\notin X_{p}$ then upon taking the transition with condition $y=1$ there is a clock $x\in X_{p}$ such that $x>y=1$ . For the third point, for any valuation in $r$ , there is no $\delta$ such that $\nu+\delta$ satisfies both clause. $\hfill\blacktriangleleft$

4.3 Relaxing Strict Guards

A kernel wtg can easily be transformed into a kernel wtg without strict guards, without change in value.

Definition 15.

Let $r=(X_{0},\dots,X_{p})$ . Then the adherence or $r$ , denoted by $\overline{r}$ , is the set of regions of the form $(Y_{0},\dots,Y_{p^{\prime}},Y_{=1})$ with $p^{\prime}\leq p$ and $\iota:\mathchoice{\left[0,p^{\prime}+1\right]}{\left[0,p^{\prime}+1\right]}{% \left[0,p^{\prime}+1\right]}{\left[0,p^{\prime}+1\right]}\to\mathchoice{\left[% 0,p\right]}{\left[0,p\right]}{\left[0,p\right]}{\left[0,p\right]}$ strictly increasing such that $\iota(p^{\prime}+1)=p$ and $Y_{0}=X_{0}\cup\dots\cup X_{\iota{0}}$ and $Y_{i}=X_{\iota(i-1)+1}\cup\dots\cup X_{\iota(i)}$ for all $1\leq i\leq p^{\prime}$ and $Y_{=1}=X_{\iota(p^{\prime})+1}\cup\dots\cup X_{\iota(p^{\prime}+1)}$ .

Let us abuse notation and write $\nu\sqsubset\overline{r}$ when $\nu\sqsubset{r^{\prime}}$ for $r^{\prime}\in\overline{r}$ .

Lemma 16.

Let $\mathcal{G}_{\prec}=(L_{\mathsf{Min}}^{\prec},L_{\mathsf{Max}}^{\prec},G,% \mathcal{X},T^{\prec},w_{\mathsf{out}}^{\prec})$ be a trimmed region kernel wtg. Let $\mathcal{G}_{\preceq}=(L_{\mathsf{Min}}^{\preceq},L_{\mathsf{Max}}^{\preceq},G% ,\mathcal{X},T^{\preceq},w_{\mathsf{out}}^{\preceq})$ be a copy of $\mathcal{G}_{\prec}$ where

$\blacksquare$

every guard has been relaxed, i.e., every guard of the form $x>0$ and $x<1$ have been replaced by $x\geq 0$ or $x\leq 1$ , respectively, for all $x\in\mathcal{X}$ .
$\blacksquare$

For any $\ell\in G$ , the output function ${w_{\mathsf{out}}}^{\preceq}(\ell,\cdot)$ is $w_{\mathsf{out}}^{\prec}(\ell,\cdot)$ extended continuously to $\overline{\mathsf{reg}(\ell)}$ in $\mathcal{G}_{\preceq}$ .

Then $\mathsf{Val}_{\mathcal{G}_{\prec}}=\mathsf{Val}_{\mathcal{G}_{\preceq}}$ .

The proof of this theorem relies on a bisimulation argument that is detailed in the appendix.

Note that $\mathcal{G}_{\preceq}$ is not a $\mathchoice{\left[0,1\right)}{\left[0,1\right)}{\left[0,1\right)}{\left[0,1% \right)}$ -wtg, but a $\mathchoice{\left[0,1\right]}{\left[0,1\right]}{\left[0,1\right]}{\left[0,1% \right]}$ -wtg, i.e., every accessible valuation is in $\mathchoice{\left[0,1\right]}{\left[0,1\right]}{\left[0,1\right]}{\left[0,1% \right]}^{\mathcal{X}}$ . Furthermore, $\mathcal{G}_{\preceq}$ is not a region wtg:

Definition 17.

A relaxed region wtg is a $\mathchoice{\left[0,1\right]}{\left[0,1\right]}{\left[0,1\right]}{\left[0,1% \right]}$ -wtg without strict guard where to each location $\ell$ is assigned a region $\mathsf{reg}(\ell)$ : for any transition $t:\ell\xrightarrow{C,X}\ell^{\prime}$ , the valuations $\nu+\delta$ , with $\nu\sqsubset\overline{\mathsf{reg}(\ell))}$ and $\delta\geq 0$ , that satisfy $C$ are contained in $\overline{r}$ for a unique region $r$ , such that $r[X:=0]=\mathsf{reg}(\ell^{\prime})$ . Furthermore, initial configuration $(i,\nu)$ must verify $\nu\in\overline{\mathsf{reg}(i)}$ . A relaxed trimmed region wtg is a relaxed region wtg if for any transition $t:\ell\xrightarrow{C,X}\ell^{\prime}$ and any region $r=\mathsf{reg}(\ell)$ in $\mathcal{G}$ ,

$\blacksquare$

for any valuation $\nu\sqsubset\overline{r}$ there exist some $\delta\geq 0$ such that $\nu+\delta\models C$ .
$\blacksquare$

for any $c\in C$ , there exists a valuation $\nu\sqsubset\overline{r}$ and some $\delta\geq 0$ such that $\nu+\delta$ is in $\mathchoice{\left[0,1\right]}{\left[0,1\right]}{\left[0,1\right]}{\left[0,1% \right]}^{\mathcal{X}}$ and $\nu+\delta\not\models c$ .

Lemma 18.

Let $\mathcal{G}_{\prec}$ be a region trimmed $\mathchoice{\left[0,1\right)}{\left[0,1\right)}{\left[0,1\right)}{\left[0,1% \right)}$ -wtg of region assignment $\mathsf{reg}$ . Let $\mathcal{G}_{\preceq}$ be a copy of $\mathcal{G}_{\prec}$ where

$\blacksquare$

every guard has been relaxed, i.e., every guard of the form $x>0$ and $x<1$ have been replaced by $x\geq 0$ or $x\leq 1$ respectively, for all $x\in\mathcal{X}$ .
$\blacksquare$

useless guards (see the second point of Definition 17) have been removed.

Then $\mathcal{G}_{\preceq}$ is a relaxed trimmed region wtg, of region assignment $\mathsf{reg}$ .

4.4 Adding Resets to every Transition

Lemma 19.

For any relaxed region trimmed kernel $\mathchoice{\left[0,1\right]}{\left[0,1\right]}{\left[0,1\right]}{\left[0,1% \right]}$ -wtg $\mathcal{G}$ , such that $\mathcal{G}$ has no requirement $x<1$ for any $x\in\mathcal{X}$ then there exists a relaxed region trimmed kernel $\mathchoice{\left[0,1\right]}{\left[0,1\right]}{\left[0,1\right]}{\left[0,1% \right]}$ -wtg $\mathcal{G}^{\prime}$ of same value and verifying the same conditions such that every transition of $\mathcal{G}^{\prime}$ is a reset transition or a transition to the target location. Furthermore, any transition of $\mathcal{G}^{\prime}$ with, for some clock $x$ , a guard of the form $x=0$ or $x=1$ , resets $x$ .

See Section A.2 for the proof.

5 Value Iteration in Two-clock Kernel Games

In this section, we prove Theorem 7 using the value iteration paradigm (see [1, 9, 8]):

Let $\mathcal{G}=(L_{\mathsf{Min}},L_{\mathsf{Max}},G,\mathcal{X},T,w\text{ or }w_{% \mathsf{out}})$ be a trimmed region (kernel) wtg. In a wtg, the value iteration algorithm builds, for each location $\ell$ and for all $k\geq 0$ , a function $\mathsf{opt}^{\ell}_{k}:\mathbb{R}_{\geq 0}^{\mathcal{X}}\to\mathbb{R}$ such that $\mathsf{opt}^{\ell}_{k}(\nu)$ is the value of the game started in $\ell$ with clock valuation $\nu$ , where $\mathsf{Min}$ has to win in at most $k$ steps. The $\mathsf{opt}$ functions are built inductively:

$\blacksquare$

$\mathsf{opt}^{\ell}_{0}$ is the constant $0$ function if $\ell\in G$ (or $w_{\mathsf{out}}(\ell,\cdot)$ in the case of a kernel wtg), or the constant $+\infty$ function otherwise.
$\blacksquare$

for any $k\in\mathbb{N}$ , $\mathsf{opt}^{\ell}_{k+1}$ is obtained from the $\mathsf{opt}$ functions at step $k$ : if $\ell$ belongs to $\mathsf{Min}$ (resp. $\mathsf{Max}$ ), then

$\mathsf{opt}^{\ell}_{k+1}(\nu)=\inf\text{(resp.\nobreak\ $\sup$) }\left\{{% \mathsf{opt}^{\ell^{\prime}}_{k}((\nu+\delta)[X:=0])}\;:\;{\ell\overset{C,X}{% \rightarrow}\ell^{\prime}\in T,\nu+\delta\models C}\right\}\,.$

Note that $\mathsf{opt}^{\ell}_{k}(\nu)=\mathsf{Val}^{\leq k}(\ell,\nu)$ the value of the game started from configuration $\ell,\nu$ when ${Min}\;$ must reach $G$ in at most $k$ steps. Naturally, $\mathsf{opt}^{\ell}_{k+1}(\nu)\leq\mathsf{opt}^{\ell}_{k}(\nu)$ for all valuation $\nu$ . If there exists $k$ such that, for all locations $\ell$ , $\mathsf{opt}^{\ell}_{k+1}=\mathsf{opt}^{\ell}_{k}$ , then the value iteration algorithm terminates.

In general, there is no termination guarantee. However, if there exists $k$ such that $\mathsf{opt}^{\ell}_{k+1}=\mathsf{opt}^{\ell}_{k}$ for all $\ell$ , then $\mathsf{opt}^{\ell}_{k}(\nu)=\mathsf{Val}_{\mathcal{G}}(\ell,\nu)$ . This means that the value of the wtg is obtained even when considering plays of length at most $k$ .

Here is an example where the value iteration algorithm does not terminate.

Figure 4: A wtg where the value iteration algorithm does not terminate. Blue circle locations belong to

\mathsf{Min}

, red square locations belong to

\mathsf{Max}

, the green circle location

G

is the target. The flags serve to easily refer to locations. The

+1

label is a transition cost.

Example 20.

The wtg $\mathcal{G}$ in Figure 4 is a $3$ -clock, almost non-Zeno wtg with a value of $1$ . The kernel of $\mathcal{G}$ contains only the cycle between and . The cost of the output edge in is $a+2\delta$ for a valuation $(x,y,t)=(\delta,a+\delta,0)$ , whereas the cost of the output edge in is exactly $1$ , for a valuation $(x,y,t)=(0,1,0)$ .

An optimal strategy for $\mathsf{Min}$ is to loop in the kernel an arbitrary number of times: In this strategy, each time she enters with valuation $(x,y,t)=(0,a,t)$ , she should waits $\delta$ such that $2\delta=1-a$ and enters , then $\mathsf{Max}$ can either reach $G$ with a cost of exactly $a+2\delta=1$ , or return to . When $\mathsf{Min}$ decides to end the game, she then picks $\delta=1-a$ instead. Then $\mathsf{Max}$ chooses between going to $G$ at cost $1+(1-a)$ , or letting $\mathsf{Min}$ leave from at cost $1$ . Each time $\mathsf{Min}$ takes the cycle with delay $\delta$ such that $2\delta=1-a$ , $y$ gets closer to $1$ , thus minimizing the cost of picking $\delta=1-a$ at some point. Thus $\mathsf{Min}$ has a strategy to reach $G$ with cost $>1$ , but arbitrarily close to $1$ depending on how long she plays. This entails that the value of this wtg is obtained by considering arbitrarily long plays. Thus, the value iteration algorithm does not terminate on this example.

However, the value iteration algorithm terminates for two-clock kernel wtgs.

Theorem 7. [Restated, see original statement.]

For any two-clock kernel wtg $\mathcal{G}$ , for any location $i\in\mathcal{G}$ , $W_{i}$ is a continuous piecewise linear function which can be computed through the value iteration algorithm.

Proof.

Without loss of generality, let us assume that $\mathcal{G}$ is a relaxed trimmed region kernel $\mathchoice{\left[0,1\right]}{\left[0,1\right]}{\left[0,1\right]}{\left[0,1% \right]}$ -wtg where every transition is either a transition to a target location, or resets at least one clock (see Lemmas 10, 16, and 19). Furthermore, we assume that there is no transition to the initial location $i$ .¹⁰¹⁰10This can be done by making a copy of the initial location, such that all transition that should enter the initial location only enter the copy instead.

For every location $\ell\not\in G\cup\{i\}$ , the set of valuations $\overline{\mathsf{reg}(\ell)}$ is either $\left\{{(0,y)}\;:\;{y\in\mathchoice{\left[0,1\right]}{\left[0,1\right]}{\left[% 0,1\right]}{\left[0,1\right]}}\right\}$ or $\left\{{(x,0)}\;:\;{x\in\mathchoice{\left[0,1\right]}{\left[0,1\right]}{\left[% 0,1\right]}{\left[0,1\right]}}\right\}$ , or the singleton $\{(0,0)\}$ . Note that the $\mathsf{opt}^{\ell}$ functions will be defined on $\overline{\mathsf{reg}(\ell)}$ for any location $\ell$ . This entails that the value iteration algorithm will mainly build $1$ -dimensional functions.

Let us highlight this observation with a subtle change of variable: Let $\Delta$ the circular clock difference of a valuation $\nu\in\overline{\mathsf{reg}(\ell)}$ be defined as:

\Delta(\nu)=\begin{cases}y\text{ when }\nu=(0,y)\text{ with $y\geq 0$,}\\ 1-x\text{ when }\nu=(x,0)\text{ with $x>0$.}\end{cases}

Now, for any $\ell\not\in G\cup\{i\}$ , for any $k\in\mathbb{N}$ , let $\mathsf{Opt}^{\ell}_{k}(\Delta(\nu))\stackrel{{\scriptstyle\mathsf{def}}}{{=}}% \mathsf{opt}^{\ell}_{k}(\nu)$ for all $\nu\in\overline{\mathsf{reg}(\ell)}$ . The function $\mathsf{Opt}^{\ell}_{k}$ is either defined on $\{0\}$ if $\overline{\mathsf{reg}(\ell)}=\{(0,0)\}$ , or on $\mathchoice{\left[0,1\right]}{\left[0,1\right]}{\left[0,1\right]}{\left[0,1% \right]}$ .

Figure 5: Evolution of

\Delta

in a one-clock-reset transition, without guards

=0

or

=1

, from region

\left\{{(0,y)}\;:\;{y\in\mathchoice{\left[0,1\right]}{\left[0,1\right]}{\left[% 0,1\right]}{\left[0,1\right]}}\right\}

.

Figure 6: Evolution of

\Delta

in a one-clock-reset transition, without guards

=0

or

=1

, from region

\left\{{(x,0)}\;:\;{x\in\mathchoice{\left[0,1\right]}{\left[0,1\right]}{\left[% 0,1\right]}{\left[0,1\right]}}\right\}

.

The following observation motivates this change of variable: In Figures 5 and 6, we consider a transition $t$ , from locations $\ell$ to $\ell^{\prime}$ such that the $\mathsf{Opt}^{\ell}$ and $\mathsf{Opt}^{\ell^{\prime}}$ functions are defined on $\mathchoice{\left[0,1\right]}{\left[0,1\right]}{\left[0,1\right]}{\left[0,1% \right]}$ , with no $=0$ or $=1$ guards. For a transition $(\ell,\nu)\overset{t,\delta}{\rightarrow}(\ell^{\prime},\nu^{\prime})$ , we then observe that $\Delta(\nu^{\prime})\in[\Delta(\nu),1]$ if $\nu(x)=0$ (Figure 5), and $\Delta(\nu^{\prime})\in[0,\Delta(\nu)]$ if $\nu(y)=0$ (Figure 6). Thus the variation of $\Delta$ only depends on the region of $\ell$ , not $\ell^{\prime}$ . In other words, it does not matter which clocks are reset by a transition, just the number of clocks that are reset.

Let us now define the induction relation between the $\mathsf{Opt}$ functions. Let $\ell$ be a location such that $\ell\not\in G\cup\{i\}$ . Moreover, assume that $\ell$ belongs to $\mathsf{Min}$ (resp. $\mathsf{Max}$ ). For $k=0$ , $\mathsf{Opt}^{\ell}_{k}=\Delta\mapsto+\infty$ . Consider $\mathsf{Leaving}(\ell)$ the set of outgoing transition from a location $\ell$ belonging to $\mathsf{Min}$ (resp. $\mathsf{Max}$ ), with $\ell\neq i$ . For each $t:\ell\overset{C,X}{\rightarrow}\ell^{\prime}$ , for any $k\in\mathbb{N}$ , let us define a function $\mathsf{Opt}^{t}_{k}$ such that $\mathsf{Opt}^{\ell}_{k+1}=\min_{t\in\mathsf{Leaving}(\ell)}\mathsf{Opt}^{t}_{k}$ (resp. $\max$ ):

$\blacksquare$
if $\ell^{\prime}$ is a goal location, then for all $k\in\mathbb{N}$ ,
- –
  
  If $\overline{\mathsf{reg}(\ell)}=\left\{{(0,y)}\;:\;{y\in\mathchoice{\left[0,1% \right]}{\left[0,1\right]}{\left[0,1\right]}{\left[0,1\right]}}\right\}$ , then
  
  $\mathsf{Opt}^{t}_{k}=\mathsf{Opt}^{t}_{0}:\Delta\mapsto\underset{(\delta,% \Delta+\delta)\models C}{\underset{0\leq\delta\leq 1-\Delta}{\inf}}\,w_{% \mathsf{out}}(\ell^{\prime},(\delta,\Delta+\delta)[X:=0])\text{ (resp.\nobreak% \ $\sup$).}$
- –
  
  If $\overline{\mathsf{reg}(\ell)}=\left\{{(x,0)}\;:\;{x\in\mathchoice{\left[0,1% \right]}{\left[0,1\right]}{\left[0,1\right]}{\left[0,1\right]}}\right\}$ , then
  
  $\mathsf{Opt}^{t}_{k}=\mathsf{Opt}^{t}_{0}:\Delta\mapsto\underset{(1-\Delta+% \delta,\delta)\models C}{\underset{0\leq\delta\leq\Delta}{\inf}}\,w_{\mathsf{% out}}(\ell^{\prime},(1-\Delta+\delta,\delta)[X:=0])\text{ (resp.\nobreak\ $% \sup$).}$
- –
  
  If $\overline{\mathsf{reg}(\ell)}=\{0,0\}$ , then $\mathsf{Opt}^{t}_{k}(0)=\mathsf{Opt}^{t}_{0}(0)=\underset{(\delta,\delta)% \models C}{\underset{0\leq\delta\leq 1}{\inf}}\,w_{\mathsf{out}}(\ell^{\prime}% ,(\delta,\delta)[X:=0])$ (resp. $\sup$ ).
$\blacksquare$
if $\ell^{\prime}$ is not a goal location, then $X\neq\emptyset$ ( $t$ resets one or two clocks).
- –
  
  If $X=\{x,y\}$ then, since $\mathcal{G}$ is almost trimmed, every valuation in $\overline{\mathsf{reg}(\ell)}$ can reach $(\ell^{\prime},(0,0))$ . Therefore $\mathsf{Opt}^{t}_{k}=\Delta\mapsto\mathsf{Opt}^{\ell^{\prime}}_{k}(0)$ .
- –
  Otherwise, $\mathsf{Opt}^{\ell^{\prime}}_{k}$ is defined on $\mathchoice{\left[0,1\right]}{\left[0,1\right]}{\left[0,1\right]}{\left[0,1% \right]}$ . Then:
  - *
    
    If $\overline{\mathsf{reg}(\ell)}=\left\{{(0,y)}\;:\;{y\in\mathchoice{\left[0,1% \right]}{\left[0,1\right]}{\left[0,1\right]}{\left[0,1\right]}}\right\}$ ,
    
    ·
    
    If $(x=0)\in C$ (thus $X=\{x\}$ ) or $(y=1)\in C$ (thus $X=\{y\}$ ),¹¹¹¹11Note that since $\mathcal{G}$ is almost trimmed, both guards cannot be in $C$ at the same time. then this forces a delay such that $t$ preserves $\Delta$ .
    
    ·
    
    Otherwise, as observed in Figure 5,
    
    $\mathsf{Opt}^{t}_{k}:\Delta\mapsto\underset{\Delta\leq\Delta^{\prime}\leq 1}{% \inf}\,\mathsf{Opt}^{\ell^{\prime}}_{k}(\Delta^{\prime})\text{ (resp.\nobreak% \ $\sup$).}$
  - *
    
    Symetrically, if $\overline{\mathsf{reg}(\ell)}=\left\{{(x,0)}\;:\;{x\in\mathchoice{\left[0,1% \right]}{\left[0,1\right]}{\left[0,1\right]}{\left[0,1\right]}}\right\}$ ,
    
    ·
    
    If $(y=0)\in C$ or $(x=1)\in C$ , then $\mathsf{Opt}^{t}_{k}=\Delta\mapsto\mathsf{Opt}^{\ell^{\prime}}_{k}(\Delta)$ .
    
    ·
    
    Otherwise, as observed in Figure 6,
    
    $\mathsf{Opt}^{t}_{k}:\Delta\mapsto\underset{0\leq\Delta^{\prime}\leq\Delta}{% \inf}\,\mathsf{Opt}^{\ell^{\prime}}_{k}(\Delta^{\prime})\text{ (resp.\nobreak% \ $\sup$).}$
  - *
    
    If $\overline{\mathsf{reg}(\ell)}=\{(0,0)\}$ , $\mathsf{Opt}^{t}_{k}(0)=\underset{0\leq\Delta\leq 1}{\inf}\mathsf{Opt}^{\ell^{% \prime}}_{k}(\Delta)$ (resp. $\sup$ ).

We call the functions $\mathsf{Opt}^{t}_{0}$ , for all transitions $t$ to a goal location, the projected output functions of $\mathcal{G}$ . The projected output functions serve to initialize the value iteration algorithm on the $\mathsf{Opt}$ functions, as do $w_{\mathsf{out}}(\ell,\cdot)$ functions for the value iteration algorithm on the $\mathsf{opt}$ functions. Observe that, since $w_{\mathsf{out}}(\ell,\cdot)$ is piecewise linear and continuous for any $\ell\in G$ , the projected output functions are continuous piecewise linear functions.

Figure 7:

\mathsf{Opt}_{k}

induction relation, with

t

a transition from a

\mathsf{Min}

location

\ell

where

x\leq y

.

t

has no

=0

or

=1

guards, and applies

y:=0

.

Thus the functions $\mathsf{Opt}^{\ell}_{k}$ are by construction continuous piecewise linear functions. Furthermore, as can be seen in Figure 7, $\mathsf{Opt}^{t}_{k}$ is obtained from $\mathsf{Opt}^{\ell^{\prime}}_{k}$ by replacing $\mathsf{Opt}^{\ell^{\prime}}_{k}$ on a finite number of intervals by constant functions $\Delta\mapsto c$ (while preserving continuity) where the constants $c$ are taken among local extremums of $\mathsf{Opt}^{\ell^{\prime}}_{k}$ .

Hence every linear piece of a function $\mathsf{Opt}^{\ell}_{k}$ is:

$\blacksquare$

either equal to some projected output function,
$\blacksquare$

or of slope $0$ , equal to some $z\in\mathbb{R}^{+}$ , where $z$ is a local extremum of some function $\mathsf{Opt}^{\ell}_{k^{\prime}}$ for $k^{\prime}<k$ . Hence, by induction, $z$ is either a local extremum of some projected output function, or a local extremum of the minimum or maximum of two projected output functions.

There is a finite number of such pieces, hence only a finite number of way they can be assembled to make a continuous piecewise linear function on $\mathchoice{\left[0,1\right]}{\left[0,1\right]}{\left[0,1\right]}{\left[0,1% \right]}$ . Thus there is a finite number of functions of this form.

Since the $\mathsf{opt}$ and $\mathsf{Opt}$ functions decrease at each iteration ( $\mathsf{Opt}^{\ell}_{k+1}(\Delta)\leq\mathsf{Opt}^{\ell}_{k}(\Delta)$ ), then the value iteration algorithm on the $\mathsf{Opt}$ functions terminates.

Furthermore, since no transition enters $i$ , $\mathsf{opt}^{i}_{k}$ does not affect $\mathsf{opt}^{\ell}_{k+1}$ for any location $\ell$ . Therefore, the value iteration algorithm on the $\mathsf{opt}$ functions aside from $\mathsf{opt}^{i}$ stabilizes. Thus, if it terminates in $k$ steps for every location except $i$ , then, adding $\mathsf{opt}^{i}$ , the value iteration algorithm terminates in at most $k+1$ steps. $\hfill\blacktriangleleft$

Note that all transformations in Section 4.4 only serve to make the termination argument of Theorem 7 more visible. However, the value iteration algorithm on two-clock kernel wtgs terminates even without these simplifications. Indeed, termination in $k$ steps entails that $\mathsf{Min}$ needs only to consider strategies that access a goal location in at most $k$ steps. Since the transformations described in Section 4 do not make arbitrarily long paths equivalent to one shorter path, then termination of the value algorithm on the transformed kernel wtgs immediately implies termination on the original kernel wtgs. This in turn entails that the value iteration algorithm terminates on the semi-unfolding $\tilde{\mathcal{G}}$ , thus on any two-clock wtg with non-negative weight.

Complexity analysis

Assume that the output weight functions of a kernel game $\mathcal{G}$ consist of a total of $k$ pieces. Then the number of possible $\mathsf{Opt}$ functions, which bounds the number of steps of the value iteration algorithm according to Theorem 7, is exponential in $k$ .

In the semi-unfolding of a weighted timed game $\mathcal{G}$ , the number of pieces of the piecewise linear value functions $W_{n}$ of nodes $n$ increases at most exponentially along a branch. Each branch has length bounded by $|\mathcal{R}(\mathcal{G})|\cdot(W/\kappa+2)$ (see [6]). Since $W\leq|\mathcal{R}(\mathcal{G})|\cdot P$ , where $P$ is the maximal rate appearing in the automaton, applying the Value Iteration algorithm requires double exponential time in $|\mathcal{R}(\mathcal{G})|$ .

Finally, the size of $\mathcal{T}(\mathcal{G})$ is bounded by $|\mathcal{R}(\mathcal{G})|^{|\mathcal{R}(\mathcal{G})|\cdot(W/\kappa+2)+1}$ , hence computing the Value is doubly exponential in $|\mathcal{R}(\mathcal{G})|$ (or triple-exponential in the size of the original game).

Note that the approximation algorithm for almost non-Zeno wtgs given in [6] is in double-exponential time. Hence computing the exact value of a two-clock almost non-Zeno wtg is exponentially more complex than computing an approximation.

Conclusion: Extension to arbitrary weights

Decidability actually holds even for almost divergent wtgs with arbitrary (negative and positive) weights. There exists a similar semi-unfolding construction in [12], for approximation of almost-divergent wtgs with arbitrary weights. The main technical difficulty is that a kernel in this semi-unfolding is defined as an SCC where every cycle is of weight $0$ . However, this does not mean that every location or transition of the kernel has weight $0$ . Thus accumulated cost can increase (or decrease) while crossing a kernel, even though cycling in a SCC does not change the accumulated cost. The construction to transform such a kernel game into a zero-weight kernel game is quite technical; it will be developed in a journal version of this article.

References

[1] 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, pages 122–133, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. doi:10.1007/978-3-540-27836-8_13.
[2] Rajeev Alur and David L. Dill. A theory of timed automata. Theor. Comput. Sci., 126(2):183–235, 1994. doi:10.1016/0304-3975(94)90010-8.
[3] 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, Berlin, Heidelberg, 2001. Springer. doi:10.1007/3-540-45351-2_15.
[4] Patricia Bouyer, Ed Brinkshma, and Kim G. Larsen. Optimal infinite scheduling for multi-priced timed automata. Formal Methods Syst. Des., 32:3–23, 2008. doi:10.1007/s10703-007-0043-4.
[5] Patricia Bouyer, Franck Cassez, Emmanuel Fleury, and Kim Guldstrand 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, volume 3328 of Lecture Notes in Computer Science, pages 148–160, Berlin, Heidelberg, 2004. Springer. doi:10.1007/978-3-540-30538-5_13.
[6] 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), volume 42 of Leibniz International Proceedings in Informatics (LIPIcs), pages 311–324, Dagstuhl, Germany, 2015. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.CONCUR.2015.311.
[7] Patricia Bouyer, Kim Guldstrand Larsen, Nicolas Markey, and Jacob Illum Rasmussen. Almost optimal strategies in one clock priced timed games. In S. Arun-Kumar and Naveen Garg, editors, FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings, volume 4337 of Lecture Notes in Computer Science, pages 345–356, Berlin, Heidelberg, 2006. Springer. doi:10.1007/11944836_32.
[8] Thomas Brihaye, Gilles Geeraerts, Axel Haddad, Engel Lefaucheux, and Benjamin Monmege. One-clock priced timed games with negative weights. Logical Methods in Computer Science, Volume 18, Issue 3, August 2022. doi:10.46298/lmcs-18(3:17)2022.
[9] 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, February 2017. doi:10.1007/s00236-016-0276-z.
[10] Thomas Brihaye, Gilles Geeraerts, Shankara Narayanan Krishna, Lakshmi Manasa, Benjamin Monmege, and Ashutosh Trivedi. Adding negative prices to priced timed games. CoRR, abs/1404.5894, 2014. doi:10.48550/arXiv.1404.5894.
[11] 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, pages 162–178, Berlin, Heidelberg, 2017. Springer Berlin Heidelberg. doi:10.1007/978-3-662-54458-7_10.
[12] 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), volume 122 of Leibniz International Proceedings in Informatics (LIPIcs), pages 28:1–28:16, Dagstuhl, Germany, 2018. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.FSTTCS.2018.28.
[13] Damien Busatto-Gaston, Benjamin Monmege, and Pierre-Alain Reynier. Optimal controller synthesis for timed systems. Log. Methods Comput. Sci., 19(1), 2023. doi:10.46298/lmcs-19(1:20)2023.
[14] Quentin Guilmant and Joël Ouaknine. Inaproximability in Weighted Timed Games. In Rupak Majumdar and Alexandra Silva, editors, 35th International Conference on Concurrency Theory (CONCUR 2024), volume 311 of Leibniz International Proceedings in Informatics (LIPIcs), pages 27:1–27:15, Dagstuhl, Germany, 2024. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.CONCUR.2024.27.
[15] Quentin Guilmant, Joël Ouaknine, and Isa Vialard. The value problem for weighted timed games with two clocks is undecidable, 2025. doi:10.48550/arXiv.2507.10550.
[16] Benjamin Monmege, Julie Parreaux, and Pierre-Alain Reynier. Decidability of one-clock weighted timed games with arbitrary weights. CoRR, abs/2207.01608, 2022. doi:10.48550/arXiv.2207.01608.

Appendix A Proofs of Section 4.4

A.1 Proof of Lemma 16

Definition 21 (Simulation and bisimulation).

Let $\mathcal{G}=(L_{\mathsf{Min}},L_{\mathsf{Max}},G,\mathcal{X},T,w)$ and $\mathcal{G}^{\prime}=(L^{\prime}_{\mathsf{Min}},L^{\prime}_{\mathsf{Max}},G^{% \prime},\mathcal{X},T^{\prime},w^{\prime})$ be wtgs. Then a relation $R\subseteq(L_{\mathsf{Min}}\times\mathbb{R}^{\mathcal{X}}\times L^{\prime}_{% \mathsf{Min}}\times\mathbb{R}^{\mathcal{X}})\cup(L_{\mathsf{Max}}\times\mathbb% {R}^{\mathcal{X}}\times L^{\prime}_{\mathsf{Max}}\times\mathbb{R}^{\mathcal{X}})$ is a simulation relation when

(\ell,\nu)\,R\,(\ell^{\prime},\nu^{\prime})\implies\begin{cases}\vskip 6.0pt % plus 2.0pt minus 2.0pt\text{$\ell\in G$ and $\ell^{\prime}\in G^{\prime}$,}\\ \text{or, for all $t\in T$, $\delta\in\mathbb{R}$, there exist $t^{\prime}$ % and $\delta^{\prime}\in\mathbb{R}$ such that if }\\ \text{$(\ell,\nu)\xrightarrow{\delta,t}(l_{2},\nu_{2})$ then $(\ell^{\prime},% \nu^{\prime})\xrightarrow{\delta^{\prime},t^{\prime}}(\ell^{\prime}_{2},\nu^{% \prime}_{2})$ where $(\ell_{2},\nu_{2})\,R\,(\ell^{\prime}_{2},\nu^{\prime}_{2% })$.}\end{cases}

$R$ is a bisimulation if $R$ and its converse are both simulations.

Example 22.

The region relation $R$ between configurations of a same wtg, where $(l_{1},\nu_{1})R(l_{2},\nu_{2})$ iff $l_{1}=l_{2}$ and $\nu_{1},\nu_{2}$ are in the same region, is a bisimulation.

A (bi)simulation relation $R$ can be extended to runs: $\rho_{1}\,R\,\rho_{2}$ when $|\rho_{1}|=|\rho_{2}|$ , and $\rho_{1}^{\mathcal{C}}(n)\,R\,\rho_{2}^{\mathcal{C}}(n)$ for all $n<|\rho_{i}|$ .

Lemma 23.

Let $\mathcal{G}_{1}$ and $\mathcal{G}_{2}$ be two wtgs. Let $R$ be a bisimulation relation between $\mathcal{G}_{1}$ and $\mathcal{G}_{2}$ , such that $\mathcal{G}_{1}$ and $\mathcal{G}_{2}$ start from configurations $c_{1}\,R\,c_{2}$ . Assume that $\mathsf{Val}_{\mathcal{G}_{i}}\neq+\infty$ for $i\in\{1,2\}$ . Then

|\mathsf{Val}_{\mathcal{G}_{1}}-\mathsf{Val}_{\mathcal{G}_{2}}|\leq\sup\left\{% \left.|\mathsf{weight}(\rho_{1})-\mathsf{weight}(\rho_{2})|\ \vphantom{\begin{% array}[]{c}\rho_{1},\rho_{2}\text{ plays of }\mathcal{G}_{1},\mathcal{G}_{2}\\ \rho_{1}\,R\,\rho_{2}\\ \end{array}}\right|\ \begin{array}[]{c}\rho_{1},\rho_{2}\text{ plays of }% \mathcal{G}_{1},\mathcal{G}_{2}\\ \rho_{1}\,R\,\rho_{2}\\ \end{array}\right\}\;.

Proof.

For all $\sigma_{1}^{\mathsf{Min}}$ a strategy for Min on $\mathcal{G}_{1}$ and $\sigma_{2}^{\mathsf{Max}}$ a strategy for Max on $\mathcal{G}_{2}$ , there exists $\sigma_{2}^{\mathsf{Min}}$ and $\sigma_{1}^{\mathsf{Max}}$ strategies for Min and Max on $\mathcal{G}_{2}$ and $\mathcal{G}_{1}$ respectively, such that $\rho_{1}\,R\,\rho_{2}$ for $\rho_{i}=\textit{play}(c_{i},\sigma_{i}^{\mathsf{Min}},\sigma_{i}^{\mathsf{Max% }})$ . (In any Min location, $\sigma_{2}^{\mathsf{Min}}$ simulates $\sigma_{1}^{\mathsf{Min}}$ following $R$ . Similarly in any Max location, $\sigma_{1}^{\mathsf{Max}}$ simulates $\sigma_{2}^{\mathsf{Max}}$ following $R$ .)

Note that $\sigma_{1}^{\mathsf{Max}},\sigma_{2}^{\mathsf{Min}}$ and $\rho_{1},\rho_{2}$ are functions of $\sigma_{1}^{\mathsf{Min}},\sigma_{2}^{\mathsf{Max}}$ . However, we omit these arguments to lighten notations.

Since the set of strategies obtained by such a simulation is included in the set of all strategies,

	$\displaystyle\sup_{\sigma_{2}^{\mathsf{Max}}}\mathsf{weight}(\rho_{1})\leq\sup% _{\sigma^{\mathsf{Max}}}V_{\mathcal{G}_{1}}(\sigma_{1}^{\mathsf{Min}},\sigma^{% \mathsf{Max}})\text{ for a fixed $\sigma_{1}^{\mathsf{Min}}$,}$
and
	$\displaystyle\inf_{\sigma_{1}^{\mathsf{Min}}}\mathsf{weight}(\rho_{2})\geq\inf% _{\sigma^{\mathsf{Min}}}V_{\mathcal{G}_{2}}(\sigma^{\mathsf{Min}},\sigma_{2}^{% \mathsf{Max}})\text{ for a fixed $\sigma_{2}^{\mathsf{Max}}$.}$

Therefore

\inf_{\sigma_{1}^{\mathsf{Min}}}\sup_{\sigma_{2}^{\mathsf{Max}}}\mathsf{weight% }(\rho_{1})\leq\inf_{\sigma^{\mathsf{Min}}}\sup_{\sigma^{\mathsf{Max}}}\mathsf% {weight}(\textit{play}_{\mathcal{G}_{1}}(c_{1},\sigma^{\mathsf{Min}},\sigma^{% \mathsf{Max}}))=\mathsf{Val}_{\mathcal{G}_{1}}

and

	$\displaystyle\inf_{\sigma_{1}^{\mathsf{Min}}}\sup_{\sigma_{2}^{\mathsf{Max}}}% \mathsf{weight}(\rho_{2})$	$\displaystyle\geq\sup_{\sigma_{2}^{\mathsf{Max}}}\inf_{\sigma_{1}^{\mathsf{Min% }}}\mathsf{weight}(\rho_{2})$
		$\displaystyle\geq\sup_{\sigma^{\mathsf{Max}}}\inf_{\sigma^{\mathsf{Min}}}% \mathsf{weight}(\textit{play}_{\mathcal{G}_{2}}(c_{2},\sigma^{\mathsf{Min}},% \sigma^{\mathsf{Max}}))=\mathsf{Val}_{\mathcal{G}_{2}}$

Therefore $\mathsf{Val}_{\mathcal{G}_{2}}-\mathsf{Val}_{\mathcal{G}_{1}}\leq\sup\left\{{% \mathsf{weight}(\rho_{2})-\mathsf{weight}(\rho_{1})}\;:\;{\rho_{1}\,R\,\rho_{2% }}\right\}\;.$

Reasoning in mirror, one can obtain

\mathsf{Val}_{\mathcal{G}_{1}}-\mathsf{Val}_{\mathcal{G}_{2}}\leq\sup\left\{{% \mathsf{weight}(\rho_{1})-\mathsf{weight}(\rho_{2})}\;:\;{\rho_{1}\,R\,\rho_{2% }}\right\}\;.

and combine to conclude. $\hfill\blacktriangleleft$

Now let us define the following relation between valuations: For $\epsilon>0$ , two valuations $\nu,\nu^{\prime}$ are $\epsilon$ -neighbours if there exists $\epsilon_{1},\epsilon_{2}\geq 0$ such that $\epsilon_{1}+\epsilon_{2}<\epsilon$ , and for any clock $x\in\mathcal{X}$ , $\nu(x)-\nu^{\prime}(x)\in[-\epsilon_{1},\epsilon_{2}]$ .

Let $\mathcal{G}_{\prec}=(L_{\mathsf{Min}}^{\prec},L_{\mathsf{Max}}^{\prec},G,% \mathcal{X},T^{\prec},w_{\mathsf{out}}^{\prec})$ be a trimmed region weighted timed game. We consider $\mathcal{G}_{\preceq}=(L_{\mathsf{Min}}^{\preceq},L_{\mathsf{Max}}^{\preceq},G% ,\mathcal{X},T^{\preceq},w_{\mathsf{out}}^{\preceq})$ a copy of $\mathcal{G}_{\prec}$ where every strict guard has been relaxed into a strict-or-equal guard.

Lemma 24.

For any configurations $(\ell_{\prec},\nu_{\prec})$ in $\mathcal{G}_{\prec}$ , and $(\ell_{\preceq},\nu_{\preceq})$ in $\mathcal{G}_{\preceq}$ ,

Let $(\ell_{\prec},\nu_{\prec})\,R_{\epsilon}\,(\ell_{\preceq},\nu_{\preceq})$ iff

$\blacksquare$

$\ell_{\prec}=\ell_{\preceq}$
$\blacksquare$

$\nu_{\prec}\sqsubset\mathsf{reg}(\ell_{\prec})$ and $\nu_{\preceq}\sqsubset\overline{\mathsf{reg}(\ell_{\prec})}$
$\blacksquare$

$\nu_{\prec}$ and $\nu_{\preceq}$ are $\epsilon$ -neighbours

Then $R_{\epsilon}$ is a bisimulation relation.

Proof.

First observe that one side of the bisimulation is easier than the other one, since transitions in $\mathcal{G}_{\preceq}$ are more permissive. Therefore we will detail only the other side:

Let $t:\ell_{1}\xrightarrow{C,X}\ell_{2}$ . Let $\overline{C}$ be the relaxation of $C$ . Let $\nu_{1}$ be a valuation belonging to $\mathsf{reg}(\ell_{1})$ in $\mathcal{G}_{\prec}$ and let $\nu_{1}^{\prime}$ be an $\epsilon$ -neighbour of $\nu_{1}$ . By definition, there are $\epsilon_{1},\epsilon_{2}\geq 0$ such that $\epsilon_{1}+\epsilon_{2}<\epsilon$ and for any clock $x\in\mathcal{X}$ , $\nu_{1}(x)-\nu_{1}^{\prime}(x)\in[-\epsilon_{1},\epsilon_{2}]$ .

Let $\delta^{\prime}\geq 0$ such that $\nu_{1}^{\prime}+\delta^{\prime}\models\overline{C}$ and let $\nu_{2}^{\prime}=(\nu_{1}^{\prime}+\delta^{\prime})[X:=0]$ . Then let us show that there exists $\delta\geq 0$ such that $\nu_{1}+\delta\models C$ , and $(\ell_{2},\nu_{2})R_{\epsilon}(\ell^{\prime}_{2},\nu^{\prime}_{2})$ with $\nu_{2}=(\nu_{1}+\delta)[X:=0]$ . To prove that, one only needs to show that $\nu^{\prime}_{1}+\delta^{\prime}$ is in the adherence of the region of $\nu_{1}+\delta$ , and that $\nu_{1}+\delta$ and $\nu^{\prime}_{1}+\delta^{\prime}$ are $\epsilon$ -neighbours.

Consider the interval

\Delta=\left\{\left.\delta\geq 0\ \vphantom{\begin{array}[]{c}\nu_{1}+\delta% \models C\\ \nu_{1}+\delta\sqsubset r\text{ s.t. }\nu_{1}^{\prime}+\delta^{\prime}% \sqsubset\overline{r}\\ \end{array}}\right|\ \begin{array}[]{c}\nu_{1}+\delta\models C\\ \nu_{1}+\delta\sqsubset r\text{ s.t. }\nu_{1}^{\prime}+\delta^{\prime}% \sqsubset\overline{r}\\ \end{array}\right\}

Since $\mathcal{G}_{\prec}$ is region trimmed, there exists $\delta$ such that $\nu_{1}+\delta\models C$ , and every valuation of the form $\nu+\delta$ that satisfy $C$ with $\nu\sqsubset\mathsf{reg}(\ell_{1})$ belong to a unique region $r_{t}$ . Since $\nu^{\prime}_{1}\sqsubset\overline{\mathsf{reg}(\ell_{1})}$ and $\nu^{\prime}_{1}+\delta^{\prime}\models\overline{C}$ , $\nu^{\prime}_{1}+\delta^{\prime}\sqsubset\overline{r_{t}}$ . Therefore, $\Delta$ is not empty.

If $\delta^{\prime}\in\Delta$ , then $(\nu_{1}+\delta^{\prime})[X:=0]$ and $\nu_{1}^{\prime}+\delta^{\prime}$ are $\epsilon$ -neighbours. Otherwise, when $\delta^{\prime}\not\in\Delta$ , it entails that $\Delta$ is constrained by some guards in $C$ . These guards can be of the form $x=1$ , $x>0$ , $x<1$ or $x\leq 1$ for any $x\in\mathcal{X}$ ¹²¹²12There cannot be any guard of the form $x=0$ in $C$ , otherwise $\Delta=\{\delta^{\prime}\}=\{0\}$ . .

$\blacksquare$

If there is a guard $x=1$ in $C$ for some $x\in\mathcal{X}$ , then $\Delta$ is the singleton $\{1-\nu_{1}(x)\}$ . Indeed $\Delta$ is not empty and $\delta\stackrel{{\scriptstyle\mathsf{def}}}{{=}}1-\nu_{1}(x)$ is the only delay that can satisfy the guard $x=1$ . Note that, for the same reason, $\delta^{\prime}=1-\nu^{\prime}_{1}(x)$ . By definition of $\Delta$ , $\nu_{2}=(\nu_{1}+\delta)$ and $\nu_{2}^{\prime}$ are in the same region. Moreover, for all $y\in\mathcal{X}$ , if $y\in X$ , then $\nu_{2}(y)=\nu_{2}^{\prime}(y)=0$ and if $y\in\mathcal{X}\setminus X$ , then $(\nu_{1}(y)+\delta)-(\nu_{1}^{\prime}(y)+\delta^{\prime}\in\mathchoice{\left[-% (\epsilon_{1}+\delta^{\prime}-\delta),\epsilon_{2}-(\delta^{\prime}-\delta)% \right]}{\left[-(\epsilon_{1}+\delta^{\prime}-\delta),\epsilon_{2}-(\delta^{% \prime}-\delta)\right]}{\left[-(\epsilon_{1}+\delta^{\prime}-\delta),\epsilon_% {2}-(\delta^{\prime}-\delta)\right]}{\left[-(\epsilon_{1}+\delta^{\prime}-% \delta),\epsilon_{2}-(\delta^{\prime}-\delta)\right]}$ . Now, $\delta^{\prime}-\delta=\nu_{1}(x)-\nu_{1}^{\prime}(x)\in\mathchoice{\left[-% \epsilon_{1},\epsilon_{2}\right]}{\left[-\epsilon_{1},\epsilon_{2}\right]}{% \left[-\epsilon_{1},\epsilon_{2}\right]}{\left[-\epsilon_{1},\epsilon_{2}% \right]}$ entails that $\epsilon_{2}^{\prime}\stackrel{{\scriptstyle\mathsf{def}}}{{=}}\epsilon_{2}-(% \delta^{\prime}-\delta)\geq 0$ , and $\epsilon_{1}^{\prime}\stackrel{{\scriptstyle\mathsf{def}}}{{=}}\epsilon_{1}+(% \delta^{\prime}-\delta)\geq 0$ . Finally, $\epsilon_{1}^{\prime}+\epsilon_{2}^{\prime}=\epsilon_{1}+\epsilon_{2}<\epsilon$ .

Now assume that there are no such guards in $C$ :

$\blacksquare$

If there is a guard $x>0$ in $C$ for some $x\in\mathcal{X}$ such that $\nu_{1}+\delta^{\prime}\not\models(x>0)$ but $\nu_{1}^{\prime}+\delta^{\prime}\models(x>0)$ then $\nu_{1}^{\prime}(x)+\delta^{\prime}=0$ . Furthermore, since $\mathcal{G}_{\prec}$ is trimmed, $\nu_{1}(x)=0$ . Therefore, $\Delta$ is an interval of the form $]0,\dots]$ . Pick $\delta\in\Delta$ such that $0<\delta<\epsilon-(\epsilon_{1}+\epsilon_{2})$ . Let $\epsilon_{2}^{\prime}\stackrel{{\scriptstyle\mathsf{def}}}{{=}}\epsilon_{2}-(% \delta^{\prime}-\delta)=\epsilon_{2}+\delta$ , and $\epsilon_{1}^{\prime}\stackrel{{\scriptstyle\mathsf{def}}}{{=}}\min\{0,% \epsilon_{1}+(\delta^{\prime}-\delta)\}\geq 0$ . Then $\epsilon_{1}^{\prime}+\epsilon_{2}^{\prime}\leq\epsilon_{1}+\epsilon_{2}+% \delta<\epsilon$ , hence $\nu_{1}+\delta$ and $\nu_{1}^{\prime}+\delta^{\prime}$ are $\epsilon$ -neighbourss.
$\blacksquare$

If there is a guard $x<1$ in $C$ (resp. $x\leq 1$ ) for some $x\in\mathcal{X}$ , such that $\nu_{1}^{\prime}+\delta^{\prime}\models(x\leq 1)$ but $\nu_{1}+\delta^{\prime}\not\models(x<1)$ (resp. $x\leq 1$ ), then $\Delta<\delta^{\prime}$ . If $\delta^{\prime}+\nu_{1}^{\prime}(x)-\nu_{1}(x)\in\Delta$ then pick $\delta=\delta^{\prime}+\nu_{1}^{\prime}(x)-\nu_{1}(x)$ . Since $\delta^{\prime}-\delta=\nu_{1}(x)-\nu_{1}^{\prime}(x)\in\mathchoice{\left[-% \epsilon_{1},\epsilon_{2}\right]}{\left[-\epsilon_{1},\epsilon_{2}\right]}{% \left[-\epsilon_{1},\epsilon_{2}\right]}{\left[-\epsilon_{1},\epsilon_{2}% \right]}$ , $\nu_{1}+\delta$ and $\nu_{1}^{\prime}+\delta^{\prime}$ are $\epsilon$ -neighbours.

Otherwise pick $\delta\in\Delta$ such that $1-\epsilon+(\epsilon_{1}+\epsilon_{2})<\nu_{1}(x)+\delta<1$ . Then $\nu_{1}(x)-\nu_{1}^{\prime}(x)<\delta^{\prime}-\delta<\nu_{1}(x)-\nu_{1}^{% \prime}(x)+\epsilon-(\epsilon_{1}+\epsilon_{2})$ , with $\nu_{1}(x)-\nu_{1}^{\prime}(x)\in\mathchoice{\left[-\epsilon_{1},\epsilon_{2}% \right]}{\left[-\epsilon_{1},\epsilon_{2}\right]}{\left[-\epsilon_{1},\epsilon% _{2}\right]}{\left[-\epsilon_{1},\epsilon_{2}\right]}$ . Let $\epsilon_{2}^{\prime}\stackrel{{\scriptstyle\mathsf{def}}}{{=}}\min(0,\epsilon% _{2}-(\delta^{\prime}-\delta))\geq 0$ and $\epsilon_{1}^{\prime}\stackrel{{\scriptstyle\mathsf{def}}}{{=}}\epsilon_{1}+(% \delta^{\prime}-\delta)\geq 0$ . Then $\epsilon_{1}^{\prime}+\epsilon_{2}^{\prime}<\epsilon$ , hence $\nu_{1}^{\prime}+\delta^{\prime}$ is an $\epsilon$ -neighbour of $\nu_{1}+\delta$ .

$\hfill\blacktriangleleft$

We are now ready to prove Lemma 16.

Lemma 16. [Restated, see original statement.]

Let $\mathcal{G}_{\prec}=(L_{\mathsf{Min}}^{\prec},L_{\mathsf{Max}}^{\prec},G,% \mathcal{X},T^{\prec},w_{\mathsf{out}}^{\prec})$ be a trimmed region kernel wtg. Let $\mathcal{G}_{\preceq}=(L_{\mathsf{Min}}^{\preceq},L_{\mathsf{Max}}^{\preceq},G% ,\mathcal{X},T^{\preceq},w_{\mathsf{out}}^{\preceq})$ be a copy of $\mathcal{G}_{\prec}$ where

$\blacksquare$

every guard has been relaxed, i.e., every guard of the form $x>0$ and $x<1$ have been replaced by $x\geq 0$ or $x\leq 1$ , respectively, for all $x\in\mathcal{X}$ .
$\blacksquare$

For any $\ell\in G$ , the output function ${w_{\mathsf{out}}}^{\preceq}(\ell,\cdot)$ is $w_{\mathsf{out}}^{\prec}(\ell,\cdot)$ extended continuously to $\overline{\mathsf{reg}(\ell)}$ in $\mathcal{G}_{\preceq}$ .

Then $\mathsf{Val}_{\mathcal{G}_{\prec}}=\mathsf{Val}_{\mathcal{G}_{\preceq}}$ .

Proof.

$\mathcal{G}_{\prec}$ and $\mathcal{G}_{\preceq}$ start from the same configuration, thus their first configurations are in bisimulation $R_{\epsilon}$ for any $\epsilon>0$ .

Therefore, according to Lemma 23,

|\mathsf{Val}_{\mathcal{G}_{\prec}}-\mathsf{Val}_{\mathcal{G}_{\preceq}}|\leq% \sup\left\{\left.|\mathsf{weight}(\rho_{\prec})-\mathsf{weight}(\rho_{\preceq}% )|\ \vphantom{\begin{array}[]{c}\rho_{\prec},\rho_{\preceq}\text{ plays of }% \mathcal{G}_{\prec},\mathcal{G}_{\preceq}\\ \rho_{\prec}\,R_{\epsilon}\,\rho_{\preceq}\\ \end{array}}\right|\ \begin{array}[]{c}\rho_{\prec},\rho_{\preceq}\text{ plays% of }\mathcal{G}_{\prec},\mathcal{G}_{\preceq}\\ \rho_{\prec}\,R_{\epsilon}\,\rho_{\preceq}\\ \end{array}\right\}\;.

In a kernel, for any finite run $\rho$ of length $n$ , $\mathsf{weight}(\rho)=w_{\mathsf{out}}(\rho^{C}(n))$ . Let $s$ be the maximal slope (in absolute value, in one variable) in functions $w_{\mathsf{out}}(\ell,\cdot)$ . Then

	$\displaystyle\sup$	$\displaystyle\left\{{\|\mathsf{weight}(\rho_{1})-\mathsf{weight}(\rho_{2})\|}\;:% \;{\rho_{1}\,R_{\epsilon}\,\rho_{2}}\right\}$
		$\displaystyle\leq\sup\left\{{\|w_{\mathsf{out}}(\ell,\nu_{1})-w_{\mathsf{out}}(% \ell,\nu_{2})\|}\;:\;{\ell\in G,(\ell,\nu_{1})\,R_{\epsilon}\,(\ell,\nu_{2})}\right\}$
		$\displaystyle\leq\epsilon\cdot s\cdot\|\mathcal{X}\|\$

Conclude with Lemma 23.

$\hfill\blacktriangleleft$

A.2 Proof of Lemma 19

Lemma 25.

For $A,B=\mathsf{Min},\mathsf{Max}$ or $\mathsf{Max},\mathsf{Min}$ . In a relaxed region kernel $\mathchoice{\left[0,1\right]}{\left[0,1\right]}{\left[0,1\right]}{\left[0,1% \right]}$ -wtg, consider a transition $t:\ell_{A}\overset{C,X}{\rightarrow}\ell_{B}$ between $\ell_{A}$ a location belonging to Player $A$ , and $\ell_{B}$ a location belonging to Player $B$ , such that $C$ has no guard of the form $x=0,x=1,x<1$ , and $X=\emptyset$ . Then adding the guard $x=1$ to $C$ for some $x\in X^{\uparrow}_{\ell_{A}}$ does not change the value.

Proof.

Pick some $x\in X^{\uparrow}_{\ell_{A}}$ . By picking a delay $\delta<1-\nu(x)$ , Player $A$ offers Player $B$ more options than if they picked $\delta=1-\nu(x)$ . From the perspective of $B$ , if a larger delay is advantageous, then they can take it from $\ell_{B}$ at cost $0$ . Hence it is optimal for either $A$ or $B$ to pick the largest delay possible, i.e. $\delta=1-\nu(x)$ . However, since $w(\ell_{A})=w(\ell_{B})=0$ , forcing $A$ to take a delay in $\ell_{A}$ which would have been taken in $\ell_{B}$ by Player $B$ given the chance does not change the value. Thus, restricting $A$ to strategies which, when choosing $t$ from a valuation $\nu$ , choose a delay $\delta$ such that $(\nu+\delta)(x)=1$ for all $x\in X^{\uparrow}_{\ell_{A}}$ does not change the value of the wtg. $\hfill\blacktriangleleft$ See 19

Proof.

Let $\mathcal{G}=(L_{\mathsf{Min}},L_{\mathsf{Max}},G,\mathcal{X},T,w,w_{\mathsf{% out}})$ . We assume that $\mathsf{Max}$ does not have full control over any cycle (i.e., in any cycle there is a $\mathsf{Min}$ location from which she can decide to leave the cycle). Indeed, if $\mathsf{Max}$ could reach such a cycle, the Value of $\mathcal{G}$ would be $+\infty$ . Furthermore, let us assume that there is no $\mathsf{Min}$ self-loop (a transition $\ell\in L_{\mathsf{Min}}\overset{C,X}{\rightarrow}\ell$ ) with $X=\emptyset$ in $\mathcal{G}$ : it does not make strategic sense for $\mathsf{Min}$ to take such a loop, hence they can be deleted without change in value.

Let us transform $\mathcal{G}$ through the following operations. For any $t:\ell_{1}\overset{C,X}{\rightarrow}\ell_{2}$ of $\mathcal{G}$ such that $\ell_{2}$ is not a target location, and $X=\emptyset$ and $C$ has no guards of the form $x=1$ for any clock $x$ :

$\blacksquare$

If $C$ has a $x=0$ requirement for some clock $x$ , then add $x$ to $X$ .
$\blacksquare$

If $C$ has no $x=0$ requirement for every clock $x$ , and $\ell_{1}$ and $\ell_{2}$ belong to the same player, then remove $t$ and, for any $t^{\prime}:\ell_{2}\to\ell_{3}$ with $\ell_{3}\neq\ell_{1}$ , ¹³¹³13Adding a transition in the case $\ell_{3}=\ell_{1}$ would create a self-loop: $\mathsf{Min}$ has no use for self-loops without reset, and we assume that $\mathsf{Max}$ has full control over no cycle, so this situation never happens when $\ell_{1}$ belongs to $\mathsf{Max}$ . create a transition $t^{\prime}:\ell_{1}\to\ell_{3}$ such that $C(t^{\prime\prime})=C(t)\cup C(t^{\prime})$
$\blacksquare$

If $C$ has no $x=0$ requirement for every clock $x$ , and $\ell_{1}$ and $\ell_{2}$ do not belong to the same player, then let us add a $x=1$ requirement to $C$ where $x\in X^{\uparrow}_{\ell_{1}}$ . According to Lemma 25, it does not change the value.

After these transformations, every transition without reset in $\mathcal{G}$ is either a transition to a target location, or has a $x=1$ guard for some $x\in\mathcal{X}$ .

Then let us build $\mathcal{G}^{\prime}=(L^{\prime}_{\mathsf{Min}},L^{\prime}_{\mathsf{Max}},G^{% \prime},\mathcal{X},T^{\prime},w^{\prime},w_{\mathsf{out}}^{\prime})$ a kernel wtg where:

$\blacksquare$

For any player $\mathsf{P}$ , let $L^{\prime}_{\mathsf{P}}=L_{\mathsf{P}}\cup\left\{{\ell_{\downarrow}}\;:\;{\ell% \in L_{\mathsf{P}}}\right\}$ .
$\blacksquare$

Let $G^{\prime}=G\cup\left\{{\ell_{\downarrow}}\;:\;{\ell\in G}\right\}$ .
$\blacksquare$
Start from $T^{\prime}=\emptyset$ . For any $t:\ell\overset{C,X}{\to}\ell^{\prime}$ in $T$ ,
- –
  
  if $\ell^{\prime}\in G$ then for all $X\subseteq X_{\ell}^{\uparrow}$ add $t^{\prime}:\ell\overset{C,X}{\to}\ell^{\prime}$ and $t^{\prime}:\ell_{\downarrow}\overset{C_{\downarrow},X}{\to}\ell^{\prime}_{\downarrow}$ to $T^{\prime}$ , where $C_{\downarrow}$ is $C\cup\left\{{x=0}\;:\;{x\in X_{\ell}^{\uparrow}}\right\}$ deprived of guards $(x=1)$ for all $x\in X_{\ell}^{\uparrow}$ . Note that here $X_{\ell}^{\uparrow}$ is defined according to $\mathsf{reg}(\ell)$ the region assignment in the relaxed trimmed region wtg $\mathcal{G}$ .
- –
  
  if $\ell^{\prime}\not\in G$ and $X=\emptyset$ then $(x=1)\in C$ for some $x\in X_{\ell}^{\uparrow}$ . Then add $t^{\prime}:\ell\overset{C,X_{\ell}^{\uparrow}}{\to}\ell^{\prime}_{\downarrow}$ and $t^{\prime\prime}:\ell_{\downarrow}\overset{C_{\downarrow},X_{\ell}^{\uparrow}}% {\to}\ell^{\prime}_{\downarrow}$ to $T^{\prime}$ .
- –
  
  if $\ell^{\prime}\not\in G$ and $X=X_{\ell}^{\uparrow}$ , then add $t^{\prime}:\ell\overset{C,X}{\to}\ell^{\prime}$ and $t^{\prime\prime}:\ell_{\downarrow}\overset{C_{\downarrow},X}{\to}\ell^{\prime}$ to $T^{\prime}$ , such that $X^{\prime}=X_{\ell}^{\uparrow}$ and $C^{\prime}=C\cup\left\{{x=0}\;:\;{x\in X_{1}}\right\}\setminus\left\{{x=1}\;:% \;{x\in X_{1}}\right\}$ .
- –
  
  if $\ell^{\prime}\not\in G$ and $X\neq\emptyset$ , then add $t^{\prime}:\ell\overset{C,X}{\to}\ell^{\prime}$ and $t^{\prime\prime}:\ell_{\downarrow}\overset{C^{\prime},X^{\prime}}{\to}\ell^{% \prime}_{\downarrow}$ to $T^{\prime}$ such that $X^{\prime}=X_{\ell}^{\uparrow}$ and $C^{\prime}=C\cup\left\{{x=0}\;:\;{x\in X_{1}}\right\}\setminus\left\{{x=1}\;:% \;{x\in X_{1}}\right\}$ .
$\blacksquare$

For all $\ell\in G$ , let $w_{\mathsf{out}}^{\prime}(\ell,\nu)=w_{\mathsf{out}}(\ell,\nu)$ , $w_{\mathsf{out}}^{\prime}(\ell_{\downarrow},\nu)=w_{\mathsf{out}}(\ell,\nu^{% \prime})$ where $\nu^{\prime}(x)=\nu(x)$ for all $x\not\in X$ , and $\nu^{\prime}(x)=1$ otherwise.

Intuitively, in $\mathcal{G}$ , when one or several clocks are made to reach $1$ by a guard, there will usually be some urgent transitions taken until all these clocks have been reset. In $\mathcal{G}^{\prime}$ , those clocks are immediately reset, and control moves to a location $\ell_{\downarrow}$ . All paths leaving $\ell_{\downarrow}$ have $(x=0)$ conditions (for all $x$ that have been reset in $\mathcal{G}^{\prime}$ but not in $\mathcal{G}$ ) to guarantee urgency. A valuation $\nu^{\prime}$ in a location $\ell_{\downarrow}$ in $\mathcal{G}^{\prime}$ is thus equivalent to a valuation $\nu$ in $\ell$ in $\mathcal{G}$ iff $\nu(x)=\nu^{\prime}(x)$ if $x\not\in X_{\ell}^{\uparrow}$ , and $\nu(x)=1$ and $\nu^{\prime}(x)=0$ for $x\in X_{\ell}^{\uparrow}$ .

$\mathcal{G}^{\prime}$ is a relaxed region wtg with region assignment $\mathsf{reg}^{\prime}(\ell)=\mathsf{reg}(\ell)$ and $\mathsf{reg}^{\prime}(\ell_{\downarrow})=(X_{0}\cup X_{p},X_{1},\dots,X_{p-1})$ when $\mathsf{reg}(\ell)=(X_{0},X_{1},\dots,X_{p})$ . From there, trim $\mathcal{G}^{\prime}$ to obtain a relaxed trimmed region wtg. $\hfill\blacktriangleleft$

[bib.bib1] [1] 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, pages 122–133, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. doi:10.1007/978-3-540-27836-8_13.

[bib.bib2] [2] Rajeev Alur and David L. Dill. A theory of timed automata. Theor. Comput. Sci., 126(2):183–235, 1994. doi:10.1016/0304-3975(94)90010-8.

[bib.bib3] [3] 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, Berlin, Heidelberg, 2001. Springer. doi:10.1007/3-540-45351-2_15.

[bib.bib4] [4] Patricia Bouyer, Ed Brinkshma, and Kim G. Larsen. Optimal infinite scheduling for multi-priced timed automata. Formal Methods Syst. Des., 32:3–23, 2008. doi:10.1007/s10703-007-0043-4.

[bib.bib5] [5] Patricia Bouyer, Franck Cassez, Emmanuel Fleury, and Kim Guldstrand 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, volume 3328 of Lecture Notes in Computer Science, pages 148–160, Berlin, Heidelberg, 2004. Springer. doi:10.1007/978-3-540-30538-5_13.

[bib.bib6] [6] 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), volume 42 of Leibniz International Proceedings in Informatics (LIPIcs), pages 311–324, Dagstuhl, Germany, 2015. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.CONCUR.2015.311.

[bib.bib7] [7] Patricia Bouyer, Kim Guldstrand Larsen, Nicolas Markey, and Jacob Illum Rasmussen. Almost optimal strategies in one clock priced timed games. In S. Arun-Kumar and Naveen Garg, editors, FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings, volume 4337 of Lecture Notes in Computer Science, pages 345–356, Berlin, Heidelberg, 2006. Springer. doi:10.1007/11944836_32.

[bib.bib8] [8] Thomas Brihaye, Gilles Geeraerts, Axel Haddad, Engel Lefaucheux, and Benjamin Monmege. One-clock priced timed games with negative weights. Logical Methods in Computer Science, Volume 18, Issue 3, August 2022. doi:10.46298/lmcs-18(3:17)2022.

[bib.bib9] [9] 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, February 2017. doi:10.1007/s00236-016-0276-z.

[bib.bib10] [10] Thomas Brihaye, Gilles Geeraerts, Shankara Narayanan Krishna, Lakshmi Manasa, Benjamin Monmege, and Ashutosh Trivedi. Adding negative prices to priced timed games. CoRR, abs/1404.5894, 2014. doi:10.48550/arXiv.1404.5894.

[bib.bib11] [11] 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, pages 162–178, Berlin, Heidelberg, 2017. Springer Berlin Heidelberg. doi:10.1007/978-3-662-54458-7_10.

[bib.bib12] [12] 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), volume 122 of Leibniz International Proceedings in Informatics (LIPIcs), pages 28:1–28:16, Dagstuhl, Germany, 2018. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.FSTTCS.2018.28.

[bib.bib13] [13] Damien Busatto-Gaston, Benjamin Monmege, and Pierre-Alain Reynier. Optimal controller synthesis for timed systems. Log. Methods Comput. Sci., 19(1), 2023. doi:10.46298/lmcs-19(1:20)2023.

[bib.bib14] [14] Quentin Guilmant and Joël Ouaknine. Inaproximability in Weighted Timed Games. In Rupak Majumdar and Alexandra Silva, editors, 35th International Conference on Concurrency Theory (CONCUR 2024), volume 311 of Leibniz International Proceedings in Informatics (LIPIcs), pages 27:1–27:15, Dagstuhl, Germany, 2024. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.CONCUR.2024.27.

[bib.bib15] [15] Quentin Guilmant, Joël Ouaknine, and Isa Vialard. The value problem for weighted timed games with two clocks is undecidable, 2025. doi:10.48550/arXiv.2507.10550.

[bib.bib16] [16] Benjamin Monmege, Julie Parreaux, and Pierre-Alain Reynier. Decidability of one-clock weighted timed games with arbitrary weights. CoRR, abs/2207.01608, 2022. doi:10.48550/arXiv.2207.01608.

	$\displaystyle\sup$	$\displaystyle\left\{{\|\mathsf{weight}(\rho_{1})-\mathsf{weight}(\rho_{2})\|}\;:% \;{\rho_{1}\,R_{\epsilon}\,\rho_{2}}\right\}$
		$\displaystyle\leq\sup\left\{{\|w_{\mathsf{out}}(\ell,\nu_{1})-w_{\mathsf{out}}(% \ell,\nu_{2})\|}\;:\;{\ell\in G,(\ell,\nu_{1})\,R_{\epsilon}\,(\ell,\nu_{2})}\right\}$
		$\displaystyle\leq\epsilon\cdot s\cdot\|\mathcal{X}\|\$

Deciding the Value of Two-Clock Almost Non-Zeno Weighted Timed Games

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

Related Version:

Acknowledgements:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

Contributions

Theorem 1.

2 Definitions

Definition 2.

▶ Remark 3.

3 Unfolding Almost Non-Zeno Weighted Timed Games

Definition 4 (Almost non-Zeno wtg).

▶ Remark 5.

Semi-unfolding

Definition 6 (Kernel weighted timed games).

Theorem 7.

Lemma 8.

Proof.

Theorem 1. [Restated, see original statement.]

4 Simplifying Transformations of Kernel Games

Commentaries

4.1 Restraining Clock Values to [0,1)

Definition 9.

Lemma 10.

Proof.

4.2 Regions and Region Trimmed Games

Definition 11.

Definition 12 (Region wtg [4, 12]).

Definition 13 (Trimmed region wtg).

Observation 14.

Proof.

4.3 Relaxing Strict Guards

Definition 15.

Lemma 16.

Definition 17.

Lemma 18.

4.4 Adding Resets to every Transition

Lemma 19.

5 Value Iteration in Two-clock Kernel Games

Example 20.

Theorem 7. [Restated, see original statement.]

Proof.

Complexity analysis

Conclusion: Extension to arbitrary weights

References

Appendix A Proofs of Section 4.4

A.1 Proof of Lemma 16

Definition 21 (Simulation and bisimulation).

Example 22.

Lemma 23.

Proof.

Lemma 24.

Proof.

Lemma 16. [Restated, see original statement.]

Proof.

A.2 Proof of Lemma 19

Lemma 25.

Proof.

Proof.

$\blacktriangleright$ Remark 3.

$\blacktriangleright$ Remark 5.