One-clock synthesis problems
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2026
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866908753895358464 |
|---|---|
| author | Lasota, Sławomir Lehaut, Mathieu Parreaux, Julie Piórkowski, Radosław |
| author_facet | Lasota, Sławomir Lehaut, Mathieu Parreaux, Julie Piórkowski, Radosław |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2601_04902 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | One-clock synthesis problems Lasota, Sławomir Lehaut, Mathieu Parreaux, Julie Piórkowski, Radosław Formal Languages and Automata Theory 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. |
| title | One-clock synthesis problems |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2601.04902 |