Revisiting Robustness in Priced Timed Games

TL;DR

This paper investigates the decidability of robust priced timed games, showing undecidability for certain subclasses with five or more clocks, but also establishing decidability results for one-clock cases.

Contribution

It improves understanding of the decidability boundaries in robust priced timed games, especially reducing the clock threshold for undecidability and confirming decidability in one-clock scenarios.

Findings

Undecidability for subclasses with 5 or more clocks.

Decidability of almost optimal strategies in one-clock robust priced timed games.

Extension of classical constructions to new subclasses.

Abstract

Priced timed games are optimal-cost reachability games played between two players---the controller and the environment---by moving a token along the edges of infinite graphs of configurations of priced timed automata. The goal of the controller is to reach a given set of target locations as cheaply as possible, while the goal of the environment is the opposite. Priced timed games are known to be undecidable for timed automata with $3$ or more clocks, while they are known to be decidable for automata with $1$ clock. In an attempt to recover decidability for priced timed games Bouyer, Markey, and Sankur studied robust priced timed games where the environment has the power to slightly perturb delays proposed by the controller. Unfortunately, however, they showed that the natural problem of deciding the existence of optimal limit-strategy---optimal strategy of the controller where the perturbations tend to vanish in the limit---is undecidable with $10$ or more clocks. In this paper we revisit this problem and improve our understanding of the decidability of these games. We show that the limit-strategy problem is already undecidable for a subclass of robust priced timed games with $5$ or more clocks. On a positive side, we show the decidability of the existence of almost optimal strategies for the same subclass of one-clock robust priced timed games by adapting a classical construction by Bouyer at al. for one-clock priced timed games.