2026-10-01T07:51:46Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:25553 2026-09-23T23:43:46Z ddc:004 open_access

One-Clock Synthesis Problems Lasota, Sławomir Lehaut, Mathieu Parreaux, Julie Piórkowski, Radosław timed automata register automata Büchi-Landweber games Church synthesis problem reactive synthesis problem We study a generalisation of Büchi-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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Sławomir Lasota and Mathieu Lehaut and Julie Parreaux and Radosław Piórkowski 2026 Is Part Of LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.STACS.2026.64 urn:nbn:de:0030-drops-255533 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.64 eng https://creativecommons.org/licenses/by/4.0/legalcode