Document Open Access Logo

Register-Bounded Synthesis from Constraint LTL

Authors Nino Dauvier, Emmanuel Filiot , Pierre-Alain Reynier

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.8.pdf
  • Filesize: 1 MB
  • 18 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Modal and temporal logics
Keywords
  • Synthesis
  • Data words
  • Constraint linear time logic
  • Register transducer

Metrics

Abstract

We consider synthesis problems from logical specifications over infinite data domains, expressed in the logic constraint LTL (CLTL), which extends LTL with predicates over an infinite set of data values. We consider register-bounded synthesis, where the goal is to automatically generate, if it exists, a transducer with r registers that realizes a given CLTL formula, where r is also given as input. We prove that CLTL register-bounded synthesis is 2ExpTime-c for various data domains such as any infinite set with equality, (ℚ, <), and (ℕ, <). For the latter domain, this contrasts with known undecidability results of (unbounded) register CLTL synthesis, by Bhaskar and Praveen. Lastly, we consider synthesis in a partial observation setting by extending CLTL with invisible variables.

Cite As Get BibTex

Nino Dauvier, Emmanuel Filiot, and Pierre-Alain Reynier. Register-Bounded Synthesis from Constraint LTL. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.8

Author Details

Nino Dauvier
  • Aix Marseille Univ, CNRS, LIS, Marseille, France
Emmanuel Filiot
  • Université libre de Bruxelles, Belgium
Pierre-Alain Reynier
  • Aix Marseille Univ, CNRS, LIS, Marseille, France

Funding

  • Filiot, Emmanuel: E. Filiot is research director at F.R.S.-FNRS. This work was partially funded by the FNRS/FWO Weave project T011724F.
  • Reynier, Pierre-Alain: This work was partially funded by ANR project QuaSy (ANR-23-CE48-0008).

References

  1. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  2. Ashwin Bhaskar and M. Praveen. Realizability problem for constraint LTL. Information and Computation, 2024. URL: https://arxiv.org/abs/2207.06708.
  3. Roderick Bloem, Krishnendu Chatterjee, and Barbara Jobstmann. Graph games and reactive synthesis. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 921-962. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_27.
  4. J. Richard Buchi 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.
  5. Stéphane Demri. LTL over integer periodicity constraints. Theor. Comput. Sci., 360(1-3):96-123, 2006. URL: https://doi.org/10.1016/J.TCS.2006.02.019.
  6. 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.
  7. Stéphane Demri and Karin Quaas. Concrete domains in logics: a survey. ACM SIGLOG News, 8(3):6-29, July 2021. URL: https://doi.org/10.1145/3477986.3477988.
  8. Stéphane Demri and Karin Quaas. Constraint automata on infinite data trees: from CTL(Z)/ CTL*(Z) to decision procedures. In Guillermo A. Pérez and Jean-François Raskin, editors, 34th International Conference on Concurrency Theory, CONCUR 2023, September 18-23, 2023, Antwerp, Belgium, volume 279 of LIPIcs, pages 29:1-29:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2023.29.
  9. Stéphane Demri and Deepak D’Souza. An automata-theoretic approach to constraint LTL. Information and Computation, 205(3):380-415, 2007. URL: https://doi.org/10.1016/j.ic.2006.09.006.
  10. 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.
  11. 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.
  12. Léo Exibard, Emmanuel Filiot, and Pierre-Alain Reynier. Synthesis of data word transducers. Log. Methods Comput. Sci., 17(1), 2021. URL: https://lmcs.episciences.org/7279.
  13. Emmanuel Filiot, Naiyong Jin, and Jean-François Raskin. Antichains and compositional algorithms for LTL synthesis. Formal Methods Syst. Des., 39(3):261-296, 2011. URL: https://doi.org/10.1007/S10703-011-0115-3.
  14. Sabína Gulcíková and Ondrej Lengál. Register set automata (technical report). CoRR, abs/2205.12114, 2022. URL: https://doi.org/10.48550/arXiv.2205.12114.
  15. Swen Jacobs, Guillermo A. Pérez, Remco Abraham, Véronique Bruyère, Michaël Cadilhac, Maximilien Colange, Charly Delfosse, Tom van Dijk, Alexandre Duret-Lutz, Peter Faymonville, Bernd Finkbeiner, Ayrat Khalimov, Felix Klein, Michael Luttenberger, Klara J. Meyer, Thibaud Michaud, Adrien Pommellet, Florian Renkin, Philipp Schlehuber-Caissier, Mouhammad Sakr, Salomon Sickert, Gaëtan Staquet, Clément Tamines, Leander Tentrup, and Adam Walker. The reactive synthesis competition (SYNTCOMP): 2018-2021. Int. J. Softw. Tools Technol. Transf., 26(5):551-567, 2024. URL: https://doi.org/10.1007/S10009-024-00754-1.
  16. Ayrat Khalimov, Emmanuel Filiot, and Léo Exibard. A generic solution to register-bounded synthesis with an application to discrete orders. CoRR, abs/2105.09978, 2021. URL: https://arxiv.org/abs/2105.09978.
  17. Ayrat Khalimov and Orna Kupferman. Register-bounded synthesis. 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 25:1-25:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2019.25.
  18. Ayrat Khalimov, Benedikt Maderbacher, and Roderick Bloem. Bounded synthesis of register transducers. In Shuvendu K. Lahiri and Chao Wang, editors, Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings, volume 11138 of Lecture Notes in Computer Science, pages 494-510. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-01090-4_29.
  19. Orna Kupferman and Moshe Y. Vardi. Synthesis with Incomplete Information, pages 109-127. Springer Netherlands, Dordrecht, 2000. URL: https://doi.org/10.1007/978-94-015-9586-5_6.
  20. Orna Kupferman and Moshe Y. Vardi. Safraless decision procedures. In 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2005), 23-25 October 2005, Pittsburgh, PA, USA, Proceedings, pages 531-542. IEEE Computer Society, 2005. URL: https://doi.org/10.1109/SFCS.2005.66.
  21. A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '89, pages 179-190, New York, NY, USA, 1989. Association for Computing Machinery. URL: https://doi.org/10.1145/75277.75293.
  22. Luc Segoufin and Szymon Torunczyk. Automata based verification over linearly ordered data domains. In Thomas Schwentick and Christoph Dürr, editors, 28th International Symposium on Theoretical Aspects of Computer Science, STACS 2011, Dortmund, Germany, March 10-12, 2011, volume 9 of LIPIcs, pages 81-92. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. URL: https://doi.org/10.4230/LIPIcs.STACS.2011.81.
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