Document Open Access Logo

One-Clock Synthesis Problems

Authors Sławomir Lasota , Mathieu Lehaut , Julie Parreaux , Radosław Piórkowski

PDF

File

Thumbnail PDF
PDF
LIPIcs.STACS.2026.64.pdf
  • Filesize: 1.21 MB
  • 21 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Timed and hybrid models
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Quantitative automata
  • Theory of computation → Logic and verification
Keywords
  • timed automata
  • register automata
  • Büchi-Landweber games
  • Church synthesis problem
  • reactive synthesis problem

Metrics

Abstract

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.

Cite As Get BibTex

Sławomir Lasota, Mathieu Lehaut, Julie Parreaux, and Radosław Piórkowski. One-Clock Synthesis Problems. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 64:1-64:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.STACS.2026.64

Author Details

Sławomir Lasota
  • University of Warsaw, Poland
Mathieu Lehaut
  • University of Warsaw, Poland
Julie Parreaux
  • Univ Rennes IRISA, Inria, CNRS, France
Radosław Piórkowski
  • University of Oxford, UK

Funding

  • Lasota, Sławomir: Partially supported by ERC grant INFSYS, agreement no. 950398 and by the NCN grant 2024/55/B/ST6/01674.
  • Lehaut, Mathieu: Partially supported by the NCN grant 2021/41/B/ST6/00535.
  • Parreaux, Julie: Partially supported by the ANR project BisoUS (ANR-22-CE48-0012).

References

  1. Parosh Aziz Abdulla, Pavel Krcal, and Wang Yi. Sampled universality of timed automata. In Foundations of Software Science and Computational Structures, pages 2-16, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. Google Scholar
  2. Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994. URL: https://doi.org/10.1016/0304-3975(94)90010-8.
  3. Eugene Asarin and Oded Maler. As soon as possible: Time optimal control for timed automata. In Proc. of HSCC'99, HSCC '99, pages 19-30, London, UK, UK, 1999. Springer-Verlag. URL: https://doi.org/10.1007/3-540-48983-5_6.
  4. Eugene Asarin, Oded Maler, Amir Pnueli, and Joseph Sifakis. Controller synthesis for timed automata. In Proc. of SSSC'98, volume 31 of 5th IFAC Conference on System Structure and Control, pages 447-452, 1998. URL: https://doi.org/10.1016/S1474-6670(17)42032-5.
  5. Gerd Behrmann, Alexandre David, Kim G. Larsen, John Hakansson, Paul Petterson, Wang Yi, and Martijn Hendriks. Uppaal 4.0. In Proceedings of the 3rd International Conference on the Quantitative Evaluation of Systems, QEST '06, pages 125-126, Washington, DC, USA, 2006. IEEE Computer Society. URL: https://doi.org/10.1109/QEST.2006.59.
  6. Béatrice Bérard, Antoine Petit, Volker Diekert, and Paul Gastin. Characterization of the expressive power of silent transitions in timed automata. Fundam. Inf., 36(2–3):145-182, November 1998. URL: https://doi.org/10.3233/FI-1998-36233.
  7. Sougata Bose, Thomas A. Henzinger, Karoliina Lehtinen, Sven Schewe, and Patrick Totzke. History-deterministic timed automata. Log. Methods Comput. Sci., 20(4), 2024. URL: https://doi.org/10.46298/LMCS-20(4:1)2024.
  8. Patricia Bouyer, Fabrice Chevalier, and Deepak D'Souza. Fault diagnosis using timed automata. In Proc. of FOSSACS'05, FOSSACS'05, pages 219-233, Berlin, Heidelberg, 2005. Springer-Verlag. URL: https://doi.org/10.1007/978-3-540-31982-5_14.
  9. Thomas Brihaye, Thomas A. Henzinger, Vinayak S. Prabhu, and Jean-François Raskin. Minimum-time reachability in timed games. In Lars Arge, Christian Cachin, Tomasz Jurdziński, and Andrzej Tarlecki, editors, Proc. of ICALP'07, pages 825-837, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-73420-8_71.
  10. J. Richard Büchi and Lawrence H. Landweber. Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society, 138:295-311, 1969. URL: http://www.jstor.org/stable/1994916.
  11. Franck Cassez, Alexandre David, Emmanuel Fleury, Kim G. Larsen, and Didier Lime. Efficient on-the-fly algorithms for the analysis of timed games. In Martín Abadi and Luca de Alfaro, editors, Proc. of CONCUR'05, pages 66-80, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. Google Scholar
  12. Lorenzo Clemente, Sławomir Lasota, and Radosław Piórkowski. Determinisability of One-Clock Timed Automata. In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory (CONCUR 2020), volume 171 of Leibniz International Proceedings in Informatics (LIPIcs), pages 42:1-42:17, Dagstuhl, Germany, 2020. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.42.
  13. Lorenzo Clemente, Sławomir Lasota, and Radosław Piórkowski. Timed games and deterministic separability. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, July 8-11, 2020, Saarbrücken, Germany (Virtual Conference), volume 168 of LIPIcs, pages 121:1-121:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.ICALP.2020.121.
  14. Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, and Mariëlle Stoelinga. The element of surprise in timed games. In Roberto Amadio and Denis Lugiez, editors, Proc. of CONCUR'03, pages 144-158, Berlin, Heidelberg, 2003. Springer Berlin Heidelberg. Google Scholar
  15. Stéphane Demri and Ranko Lazic. LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log., 10(3):16:1-16:30, 2009. URL: https://doi.org/10.1145/1507244.1507246.
  16. Deepak D’souza and P. Madhusudan. Timed control synthesis for external specifications. In Helmut Alt and Afonso Ferreira, editors, Proc. of STACS'02, pages 571-582, Berlin, Heidelberg, 2002. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-45841-7_47.
  17. Léo Exibard. Automatic Synthesis of Systems with Data. (Synthèse Automatique de Systèmes avec Données). PhD thesis, Aix-Marseille University, France, 2021. URL: https://tel.archives-ouvertes.fr/tel-03409602.
  18. Léo Exibard, Emmanuel Filiot, and Ayrat Khalimov. Church synthesis on register automata over linearly ordered data domains. Formal Methods Syst. Des., 61(2):290-337, 2022. URL: https://doi.org/10.1007/S10703-023-00435-W.
  19. Léo Exibard, Emmanuel Filiot, and Pierre-Alain Reynier. Synthesis of data word transducers. In Wan J. Fokkink and Rob van Glabbeek, editors, 30th International Conference on Concurrency Theory, CONCUR 2019, August 27-30, 2019, Amsterdam, the Netherlands, volume 140 of LIPIcs, pages 24:1-24:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2019.24.
  20. Diego Figueira, Piotr Hofman, and Sławomir Lasota. Relating timed and register automata. Math. Struct. Comput. Sci., 26(6):993-1021, 2016. URL: https://doi.org/10.1017/S0960129514000322.
  21. Mark Jenkins, Joël Ouaknine, Alexander Rabinovich, and James Worrell. The church synthesis problem with metric. In Computer Science Logic (CSL'11)-25th International Workshop/20th Annual Conference of the EACSL (2011), pages 307-321. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. URL: https://doi.org/10.4230/LIPIcs.CSL.2011.307.
  22. Marcin Jurdziński and Ashutosh Trivedi. Reachability-time games on timed automata. In Proc. of ICALP'07, pages 838-849, Berlin, Heidelberg, 2007. Springer-Verlag. URL: http://dl.acm.org/citation.cfm?id=2394539.2394637.
  23. Michael Kaminski and Nissim Francez. Finite-memory automata. Theor. Comput. Sci., 134(2):329-363, 1994. URL: https://doi.org/10.1016/0304-3975(94)90242-9.
  24. M. Kwiatkowska, G. Norman, and D. Parker. PRISM 4.0: Verification of probabilistic real-time systems. In G. Gopalakrishnan and S. Qadeer, editors, Proc. of CAV'11, volume 6806 of LNCS, pages 585-591. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22110-1_47.
  25. Sławomir Lasota and Igor Walukiewicz. Alternating timed automata. ACM Transactions on Computational Logic, 9(2, Article 10), 2008. Google Scholar
  26. Sławomir Lasota, Mathieu Lehaut, Julie Parreaux, and Radosław Piórkowski. One-clock synthesis problems, 2026. URL: https://arxiv.org/abs/2601.04902.
  27. Oded Maler and Amir Pnueli. On recognizable timed languages. In Igor Walukiewicz, editor, Proc. of FOSSACS'04, volume 2987 of LNCS, pages 348-362. Springer Berlin Heidelberg, 2004. URL: https://doi.org/10.1007/978-3-540-24727-2_25.
  28. Oded Maler, Amir Pnueli, and Joseph Sifakis. On the synthesis of discrete controllers for timed systems. In Ernst W. Mayr and Claude Puech, editors, Proc. of STACS'95, pages 229-242, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg. Google Scholar
  29. Richard Mayr. Undecidable problems in unreliable computations. Theor. Comput. Sci., 297(1-3):337-354, 2003. URL: https://doi.org/10.1016/S0304-3975(02)00646-1.
  30. Brian Nielsen and Arne Skou. Automated test generation from timed automata. International Journal on Software Tools for Technology Transfer, 5(1):59-77, November 2003. URL: https://doi.org/10.1007/s10009-002-0094-1.
  31. Joël Ouaknine and James Worrell. On the language inclusion problem for timed automata: Closing a decidability gap. In 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings, pages 54-63. IEEE Computer Society, 2004. URL: https://doi.org/10.1109/LICS.2004.1319600.
  32. Radosław Piórkowski. Simplification problems for infinite-state systems. PhD thesis, University of Warsaw, 2022. Google Scholar
  33. Alexander Rabinovich and Daniel Fattal. The Church synthesis problem over continuous time. Log. Methods Comput. Sci., 21(3), 2025. URL: https://doi.org/10.46298/LMCS-21(3:8)2025.
  34. Philippe Schnoebelen. Lossy counter machines decidability cheat sheet. In Antonín Kučera and Igor Potapov, editors, Reachability Problems, pages 51-75, 2010. URL: https://doi.org/10.1007/978-3-642-15349-5_4.
  35. Luc Segoufin. Automata and logics for words and trees over an infinite alphabet. In Zoltán Ésik, editor, Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25-29, 2006, Proceedings, volume 4207 of Lecture Notes in Computer Science, pages 41-57. Springer, 2006. URL: https://doi.org/10.1007/11874683_3.
  36. Martin Tappler, Bernhard K. Aichernig, Kim Guldstrand Larsen, and Florian Lorber. Time to learn - learning timed automata from tests. In Étienne André and Mariëlle Stoelinga, editors, Proc. of FORMATS'19, pages 216-235, Cham, 2019. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-29662-9_13.
  37. Sicco Verwer, Mathijs de Weerdt, and Cees Witteveen. An algorithm for learning real-time automata. In Proc of. the Annual Belgian-Dutch Machine Learning Conference (Benelearn'078), 2007. Google Scholar
  38. H. Wong-Toi and G. Hoffmann. The control of dense real-time discrete event systems. In Proc. of CDC'91, volume 2 of Proceedings of the 30th IEEE Conference on Decision and Control, pages 1527-1528, December 1991. URL: https://doi.org/10.1109/CDC.1991.261658.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact