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

TL;DR

This paper proves that the problem of determining game values in two-clock weighted timed games with non-negative weights is undecidable, filling a key gap in understanding the computational limits of such models.

Contribution

It establishes the undecidability of the value problem for two-clock WTGs with non-negative weights, even under time constraints, which was previously unknown.

Findings

Undecidability of the value problem for two-clock WTGs proven

Results hold even with non-negative weights and time bounds

Completes the classification of decidability for WTGs based on clock count

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.