The Value Problem for Weighted Timed Games with Two Clocks is Undecidable

TL;DR

This paper resolves the last major gap in the decidability landscape of weighted timed games by proving that the Value Problem for two-clock WTGs with non-negative weights is undecidable, even under time bounds. The authors achieve this via a reduction from the Halting Problem of deterministic two-counter machines, encoding counter values with two clocks and enforcing faithful simulation through punishment gadgets. Central to the construction are the Counter Evolution Control (CEC) and Multiplication-Control (MC) gadgets, which manage proportional delays and arithmetic checks within a two-clock framework. They also show the Existence Problem is undecidable under the same hypotheses, and discuss how the two-clock reduction compares to prior three-clock reductions, highlighting the bounded-duration nature of their encoding. This result closes a central gap in the algorithmic understanding of WTGs and has implications for real-time controller synthesis under quantitative objectives.

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. This problem was shown to be undecidable some ten years ago for WTGs making use of at least three clocks, and is known to be decidable for single-clock WTGs. In this paper, we establish undecidability for two-clock WTGs making use of non-negative weights, even in a time-bounded setting, closing the last remaining major gap in our algorithmic understanding of WTGs.

Figures (9)

• Figure 1: State of the art on the Value Problem for weighted timed games. Approximability for 2-clock WTGs, and 3-clock WTGs with weights in $\mathbb{N}$, remain open. This paper's main contribution (undecidability for WTGs with two clocks and weights in $\mathbb{N}$) is highlighted in boldface blue.
• Figure 2: Transition module for increments. Here $x-y$ is the previous value of $x$, and $y$ contains the delay $\mathbf{Min}$ waited in $q$.
• Figure 3: Transition module for branching decrement of counter $e\in\{c,d\}$.
• Figure 4: $\mathbf{Min}$'s exit module. Yields a final cost of at most $64+ 1 - x$.
• Figure 5: The CEC (Counter Evolution Control) module. Enforces $b=\gamma(1-a)$ with $\gamma = 1 - \frac{\beta}{\alpha}$.

Theorems & Definitions (26)

• theorem thmcountertheorem
• definition thmcounterdefinition
• definition thmcounterdefinition: Value Problem
• definition thmcounterdefinition: Existence Problem
• remark thmcounterremark
• proposition thmcounterproposition
• proposition thmcounterproposition
• proof
• proposition thmcounterproposition
• proof