Decidability of One-Clock Weighted Timed Games with Arbitrary Weights

TL;DR

This work resolves the long-standing open question of whether one-clock weighted timed games with arbitrary weights are decidable. It introduces an unfolding-based strategy that, together with a region-closure construction, reduces the problem to a finite acyclic WTG, enabling value computation. The value function is shown to be the greatest fixpoint of a natural operator $\mathcal{F}$, and the authors prove convergence of iterative approximations to this fixpoint. A key technical breakthrough is that Max admits a memoryless optimal strategy in the closure to avoid negative cycles, while Min can be steered via switching strategies to bound unfolding depth. Consequently, the value function is computable in exponential time when weights are unary-encoded, advancing the frontier for synthesis problems with real-time and quantitative constraints.

Abstract

Weighted Timed Games (WTG for short) are the most widely used model to describe controller synthesis problems involving real-time issues. Unfortunately, they are notoriously difficult, and undecidable in general. As a consequence, one-clock WTGs have attracted a lot of attention, especially because they are known to be decidable when only non-negative weights are allowed. However, when arbitrary weights are considered, despite several recent works, their decidability status was still unknown. In this paper, we solve this problem positively and show that the value function can be computed in exponential time (if weights are encoded in unary).

Figures (8)

• Figure 1: On the left, a WTG with a cyclic path of weight $[-1, 1]$ containing a reset. Its weights are depicted in bold font, and the missing ones are $0$. Locations belonging to $\mathsf{Min}$ (resp. $\mathsf{Max}$) are depicted by circles (resp. squares). Transitions that contain the reset of $x$ are labelled with $x := 0$. The intervals of guards are described, as classically done in timed automata, via equality or inequality constraints on the unique clock $x$. The target location is ${\Large\smiley}$, whose final weight function is zero. Location $q_3$ is urgent. On the right, the restriction of its closure to locations $q_0, q_1, q_2$ and ${\Large\smiley}$.
• Figure 2: On the left, a WTG where $\mathsf{Max}\xspace$ needs memory to play $\varepsilon$-optimally. On the right, its closure where we merged several transitions by removing unnecessary guards.
• Figure 3: On the left, a WTG such that its closure on the right contains a cyclic path of value $0$, but some cyclic paths of negative weight. Moreover, $\mathsf{Max}\xspace$ uses the cyclic path to play optimally.
• Figure 4: A WTG (left) and a portion of its closure (right) where $\delta\xspace'_2$ belongs to a cyclic path of non-negative value and another cyclic path of negative value.
• Figure 5: Scheme of the unfolding of a closure of a WTG.

Theorems & Definitions (54)

• Definition 2.1
• Example 2.2
• Example 2.3
• Theorem 2.4
• Definition 2.5
• Lemma 2.6: brihaye2021oneclock
• Lemma 2.6
• Theorem 2.7: brihaye2021oneclock
• Example 2.8
• Theorem 2.9