One-clock synthesis problems

TL;DR

This paper investigates the synthesis problems in timed games with automaton-based winning conditions, revealing widespread undecidability even with simple one-clock automata, and characterizing cases where finite memory suffices.

Contribution

It provides a comprehensive analysis of undecidability in timed game synthesis and characterizes when finite-memory strategies are sufficient, extending previous results.

Findings

Undecidability in all variants with one-clock automata

Finite memory strategies are sufficient iff a strategy exists

Results extend to one-register automata in data settings

Abstract

We study a generalisation of B\"uchi-Landweber games to the timed setting. The winning condition is specified by a non-deterministic timed automaton, and one of the players can elapse time. We perform a systematic study of synthesis problems in all variants of timed games, depending on which player's winning condition is specified, and which player's strategy (or controller, a finite-memory strategy) is sought. As our main result we prove ubiquitous undecidability in all the variants, both for strategy and controller synthesis, already for winning conditions specified by one-clock automata. This strengthens and generalises previously known undecidability results. We also fully characterise those cases where finite memory is sufficient to win, namely existence of a strategy implies existence of a controller. All our results are stated in the timed setting, while analogous results hold in the data setting where one-clock automata are replaced by one-register ones.