Document Open Access Logo

Church Synthesis on Register Automata over Linearly Ordered Data Domains

Authors Léo Exibard, Emmanuel Filiot, Ayrat Khalimov

PDF
Thumbnail PDF

File

LIPIcs.STACS.2021.28.pdf
  • Filesize: 0.73 MB
  • 16 pages

Document Identifiers

Author Details

Léo Exibard
  • Aix Marseille Univ, Université de Toulon, CNRS, LIS, Marseille, France
  • Université libre de Bruxelles, Brussels, Belgium
Emmanuel Filiot
  • Université libre de Bruxelles, Brussels, Belgium
Ayrat Khalimov
  • Université libre de Bruxelles, Brussels, Belgium

Funding

This work was supported by the Fonds de la Recherche Scientifique - FNRS under Grant n°F.4510.9. Emmanuel Filiot is research associate of the Fonds de la Recherche Scientifique - FNRS.

Cite AsGet BibTex

Léo Exibard, Emmanuel Filiot, and Ayrat Khalimov. Church Synthesis on Register Automata over Linearly Ordered Data Domains. In 38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 187, pp. 28:1-28:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.STACS.2021.28

Abstract

Register automata are finite automata equipped with a finite set of registers in which they can store data, i.e. elements from an unbounded or infinite alphabet. They provide a simple formalism to specify the behaviour of reactive systems operating over data ω-words. We study the synthesis problem for specifications given as register automata over a linearly ordered data domain (e.g. (ℕ, ≤) or (ℚ, ≤)), which allow for comparison of data with regards to the linear order. To that end, we extend the classical Church synthesis game to infinite alphabets: two players, Adam and Eve, alternately play some data, and Eve wins whenever their interaction complies with the specification, which is a language of ω-words over ordered data. Such games are however undecidable, even when the specification is recognised by a deterministic register automaton. This is in contrast with the equality case, where the problem is only undecidable for nondeterministic and universal specifications. Thus, we study one-sided Church games, where Eve instead operates over a finite alphabet, while Adam still manipulates data. We show they are determined, and deciding the existence of a winning strategy is in ExpTime, both for ℚ and ℕ. This follows from a study of constraint sequences, which abstract the behaviour of register automata, and allow us to reduce Church games to ω-regular games. Lastly, we apply these results to the transducer synthesis problem for input-driven register automata, where each output data is restricted to be the content of some register, and show that if there exists an implementation, then there exists one which is a register transducer.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Transducers
Keywords
  • Synthesis
  • Church Game
  • Register Automata
  • Transducers
  • Ordered Data Words

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Piotr Hofman, Richard Mayr, K. Narayan Kumar, and Patrick Totzke. Infinite-state energy games. In Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 7:1-7:10, 2014. Google Scholar
  2. Parosh Aziz Abdulla, Ahmed Bouajjani, and Julien d’Orso. Deciding monotonic games. In International Workshop on Computer Science Logic, pages 1-14. Springer, 2003. Google Scholar
  3. Béatrice Bérard, Benedikt Bollig, Mathieu Lehaut, and Nathalie Sznajder. Parameterized synthesis for fragments of first-order logic over data words. In FOSSACS, volume 12077 of Lecture Notes in Computer Science, pages 97-118. Springer, 2020. Google Scholar
  4. M. Bojańczyk and T. Colcombet. Bounds in ω-regularity. In Proc. 21st IEEE Symp. on Logic in Computer Science, pages 285-296, 2006. Google Scholar
  5. M. Bojanczyk, A. Muscholl, T. Schwentick, L. Segoufin, and C. David. Two-variable logic on words with data. In Proc. 21st IEEE Symp. on Logic in Computer Science, pages 7-16, 2006. Google Scholar
  6. Mikołaj Bojańczyk. A bounding quantifier. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, Computer Science Logic, pages 41-55, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. Google Scholar
  7. Mikołaj Bojańczyk. Weak MSO with the unbounding quantifier. Theory of Computing Systems, 48(3):554-576, 2011. Google Scholar
  8. Mikołaj Bojańczyk. Weak MSO+U with path quantifiers over infinite trees. In Automata, Languages, and Programming - 41st International Colloquium, ICALP 2014, Copenhagen, Denmark, July 8-11, 2014, Proceedings, Part II, pages 38-49, 2014. Google Scholar
  9. A. Bouajjani, P. Habermehl, Y. Jurski, and M. Sighireanu. Rewriting systems with data. In FCT, pages 1-22, 2007. Google Scholar
  10. A. Bouajjani, P. Habermehl, and R R. Mayr. Automatic verification of recursive procedures with one integer parameter. Theoretical Computer Science, 295:85-106, 2003. Google Scholar
  11. A.-J. Bouquet, O. Serre, and I. Walukiewicz. Pushdown games with unboundedness and regular conditions. In Proc. 23rd Conf. on Foundations of Software Technology and Theoretical Computer Science, volume 2914 of Lecture Notes in Computer Science, pages 88-99. Springer, 2003. Google Scholar
  12. J.R. Büchi and L.H. Landweber. Solving sequential conditions by finite-state strategies. Trans. AMS, 138:295-311, 1969. Google Scholar
  13. C.S. Calude, S. Jain, B. Khoussainov, W. Li, and F. Stephan. Deciding parity games in quasipolynomial time. In Proc. 49th ACM Symp. on Theory of Computing, pages 252-263, 2017. Google Scholar
  14. S. Ceri, P. Fraternali, A. Bongio, M. Brambilla, S. Comai, and M. Matera. Designing Data-Intensive Web Applications. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 2002. Google Scholar
  15. G. Delzanno, A. Sangnier, and R. Traverso. Parameterized verification of broadcast networks of register automata. In P. A. Abdulla and I. Potapov, editors, Reachability Problems, pages 109-121, Berlin, Heidelberg, 2013. Springer. Google Scholar
  16. R. Ehlers, S. Seshia, and H. Kress-Gazit. Synthesis with identifiers. In Proc. 15th Int. Conf. on Verification, Model Checking, and Abstract Interpretation, volume 8318 of Lecture Notes in Computer Science, pages 415-433. Springer, 2014. Google Scholar
  17. L. Exibard, E. Filiot, and P-A. Reynier. Synthesis of data word transducers. In Proc. 30th Int. Conf. on Concurrency Theory, 2019. Google Scholar
  18. Léo Exibard, Emmanuel Filiot, and Ayrat Khalimov. Church synthesis on register automata over infinite ordered alphabets, 2020. URL: http://arxiv.org/abs/2004.12141.
  19. Rachel Faran and Orna Kupferman. On synthesis of specifications with arithmetic. In Alexander Chatzigeorgiou, Riccardo Dondi, Herodotos Herodotou, Christos Kapoutsis, Yannis Manolopoulos, George A. Papadopoulos, and Florian Sikora, editors, SOFSEM 2020: Theory and Practice of Computer Science, pages 161-173, Cham, 2020. Springer International Publishing. Google Scholar
  20. Azadeh Farzan and Zachary Kincaid. Strategy synthesis for linear arithmetic games. Proceedings of the ACM on Programming Languages, 2(POPL):1-30, 2017. Google Scholar
  21. Diego Figueira, Anirban Majumdar, and M. Praveen. Playing with repetitions in data words using energy games. Log. Methods Comput. Sci., 16(3), 2020. URL: https://lmcs.episciences.org/6614.
  22. B. Finkbeiner, F. Klein, R. Piskac, and M. Santolucito. Temporal stream logic: Synthesis beyond the bools. In Proc. 31st Int. Conf. on Computer Aided Verification, 2019. Google Scholar
  23. Stefan Göller, Richard Mayr, and Anthony Widjaja To. On the computational complexity of verifying one-counter processes. In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, 11-14 August 2009, Los Angeles, CA, USA, pages 235-244, 2009. Google Scholar
  24. E. Grädel, W. Thomas, and T. Wilke. Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of Lecture Notes in Computer Science. Springer, 2002. Google Scholar
  25. R. Hojati, D.L. Dill, and R.K. Brayton. Verifying linear temporal properties of data insensitive controllers using finite instantiations. In Hardware Description Languages and their Applications, pages 60-73. Springer, 1997. Google Scholar
  26. M. Kaminski and N. Francez. Finite-memory automata. Theoretical Computer Science, 134(2):329-363, 1994. Google Scholar
  27. A. Khalimov, B. Maderbacher, and R. Bloem. Bounded synthesis of register transducers. In 16th Int. Symp. on Automated Technology for Verification and Analysis, volume 11138 of Lecture Notes in Computer Science, pages 494-510. Springer, 2018. Google Scholar
  28. Ayrat Khalimov and Orna Kupferman. Register-bounded synthesis. In 30th International Conference on Concurrency Theory (CONCUR 2019). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2019. Google Scholar
  29. Ayrat Khalimov and Orna Kupferman. Register-bounded synthesis. In Wan 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.
  30. Bartek Klin and Mateusz Łełyk. Scalar and Vectorial mu-calculus with Atoms. Logical Methods in Computer Science, Volume 15, Issue 4, October 2019. URL: https://doi.org/10.23638/LMCS-15(4:5)2019.
  31. Paul Krogmeier, Umang Mathur, Adithya Murali, P. Madhusudan, and Mahesh Viswanathan. Decidable synthesis of programs with uninterpreted functions. In Shuvendu K. Lahiri and Chao Wang, editors, Computer Aided Verification, pages 634-657, Cham, 2020. Springer International Publishing. Google Scholar
  32. R. Lazić and D. Nowak. A unifying approach to data-independence. In Proc. 11th Int. Conf. on Concurrency Theory, pages 581-596. Springer Berlin Heidelberg, 2000. Google Scholar
  33. M.O. Rabin. Automata on infinite objects and Church’s problem. Amer. Mathematical Society, 1972. Google Scholar
  34. Thomas Schwentick and Thomas Zeume. Two-variable logic with two order relations. Log. Methods Comput. Sci., 8(1), 2012. Google Scholar
  35. Luc Segoufin and Szymon Torunczyk. Automata-based verification over linearly ordered data domains. In 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2011. Google Scholar
  36. Olivier Serre. Parity games played on transition graphs of one-counter processes. In Foundations of Software Science and Computation Structures, 9th International Conference, FOSSACS 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25-31, 2006, Proceedings, pages 337-351, 2006. Google Scholar
  37. V. Vianu. Automatic verification of database-driven systems: a new frontier. In ICDT '09, pages 1-13, 2009. Google Scholar
  38. I. Walukiewicz. Model checking CTL properties of pushdown systems. In Proc. 20th Conf. on Foundations of Software Technology and Theoretical Computer Science, volume 1974 of Lecture Notes in Computer Science, pages 127-138. Springer, 2000. Google Scholar
  39. P. Wolper. Expressing interesting properties of programs in propositional temporal logic. In Proc. 13th ACM Symp. on Principles of Programming Languages, pages 184-192, 1986. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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