Deciding the Value of Two-Clock Almost Non-Zeno Weighted Timed Games

TL;DR

This paper investigates the decidability of the value problem in two-clock almost non-Zeno weighted timed games, providing new insights into the boundary between decidability and undecidability in timed game models.

Contribution

It establishes the decidability of the value problem for two-clock almost non-Zeno weighted timed games, resolving a long-standing open question.

Findings

Decidability of the value problem for two-clock almost non-Zeno wtgs.

Contrasts with undecidability results for other classes of wtgs.

Advances understanding of the boundary between decidability and undecidability.

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. When restrained to wtgs with non-negative weight, this problem is known to be undecidable for weighted timed games with three or more clocks, and decidable for one-clock wtgs. The Value Problem for two-clock non-negative wtgs, which remained stubbornly open for a decade, was recently shown to be undecidable. In this article, we show that the Value Problem is decidable when considering two-clock almost non-Zeno wtgs.