One-clock synthesis problems
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.
Keywords
Cite
@article{arxiv.2601.04902,
title = {One-clock synthesis problems},
author = {Sławomir Lasota and Mathieu Lehaut and Julie Parreaux and Radosław Piórkowski},
journal= {arXiv preprint arXiv:2601.04902},
year = {2026}
}