The Value Problem for weighted timed games 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 is known to be undecidable for weighted timed games with three or more clocks, and decidable for one-clock weighted timed games. In this paper, we settle the remaining two-clock case, which has remained stubbornly open for a decade. We show that two-clock weighted timed games lie precisely at the decidability frontier: On the one hand the Value problem is undecidable for two-clock weighted timed games, even when restricted to non-negative weights and under a time bound; On the other hand, we establish decidability under an almost divergence restriction, by providing a $3$\textsc{ExpTime} algorithm for computing the value of almost divergent turn-based two-clock weighted timed games.

翻译：暂无翻译