We prove that the Value Problem for weighted timed games (WTGs) with two clocks and non-negative integer weights is undecidable -- even under a time bound. 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. Our reduction encodes a deterministic two-counter machine using two clocks and uses "punishment" gadgets that let the opponent detect and penalize any incorrect simulation. This closes one of the last remaining major gaps in our algorithmic understanding of WTGs.
Proceedings of FOSSACS 26, LNCS XXXX, 2026. 29
pages.
ETAPS distinguished paper.
PDF
© 2026 Quentin Guilmant, Joël
Ouaknine, and Isa Vialard.