Abstract
We study the synthesis problem for systems with a parameterized number of processes. As in the classical case due to Church, the system selects actions depending on the program run so far, with the aim of fulfilling a given specification. The difficulty is that, at the same time, the environment executes actions that the system cannot control. In contrast to the case of fixed, finite alphabets, here we consider the case of parameterized alphabets. An alphabet reflects the number of processes, which is static but unknown. The synthesis problem then asks whether there is a finite number of processes for which the system can satisfy the specification. This variant is already undecidable for very limited logics. Therefore, we consider a first-order logic without the order on word positions. We show that even in this restricted case synthesis is undecidable if both the system and the environment have access to all processes. On the other hand, we prove that the problem is decidable if the environment only has access to a bounded number of processes. In that case, there is even a cutoff meaning that it is enough to examine a bounded number of process architectures to solve the synthesis problem.
Partly supported by ANR FREDDA (ANR-17-CE40-0013).
Chapter PDF
Similar content being viewed by others
References
P. A. Abdulla, R. Mayr, A. Sangnier, and J. Sproston. Solving parity games on integer vectors. In P. R. D’Argenio and H. C. Melgratti, editors, CONCUR 2013 -Concurrency Theory - 24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings, volume 8052 of Lecture Notes in Computer Science, pages 106–120. Springer, 2013.
B. Bérard, B. Bollig, M. Lehaut, and N. Sznajder. Parameterized synthesis for fragments of first-order logic over data words. CoRR, abs/1910.14294, 2019.
R. Beutner, B. Finkbeiner, and J. Hecking-Harbusch. Translating Asynchronous Games for Distributed Synthesis. In W. Fokkink and R. van Glabbeek, editors, 30th International Conference on Concurrency Theory (CONCUR 2019), volume 140 of Leibniz International Proceedings in Informatics (LIPIcs), pages 26:1–26:16, Dagstuhl, Germany, 2019. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik
R. Bloem, S. Jacobs, A. Khalimov, I. Konnov, S. Rubin, H. Veith, and J. Widder. Decidability of Parameterized Verification. Morgan & Claypool Publishers, 2015.
M. Bojanczyk, C. David, A. Muscholl, T. Schwentick, and L. Segoufin. Two-variable logic on data words. ACM Trans. Comput. Log., 12(4):27, 2011.
T. Brázdil, P. Jancar, and A. Kucera. Reachability games on extended vector addition systems with states. In ICALP’10, Part II, volume 6199 of LNCS, pages 478–489. Springer, 2010.
B. Brütsch and W. Thomas. Playing games in the Baire space. In Proc. Cassting Workshop on Games for the Synthesis of Complex Systems and 3rd Int. Workshop on Synthesis of Complex Parameters, volume 220 of EPTCS, pages 13–25, 2016.
J. R. Büchi, and L. H. Landweber. Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society, 138:295–311, Apr. 1969.
A. Church. Applications of recursive arithmetic to the problem of circuit synthesis. In Summaries of the Summer Institute of Symbolic Logic - Volume 1, pages 3–50. Institute for Defense Analyses, 1957.
J. Courtois and S. Schmitz. Alternating vector addition systems with states. In E. Csuhaj-Varjú, M. Dietzfelbinger, and Z. Ésik, editors, Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 2014, Budapest, Hungary, August 25-29, 2014. Proceedings, Part I, volume 8634 of Lecture Notes in Computer Science, pages 220–231. Springer, 2014.
S. Demri, D. D’Souza, and R. Gascon. Temporal logics of repeating values. J. Log. Comput., 22(5):1059–1096, 2012.
S. Demri and R. Lazić.LTL with the freeze quantifier and register automata. ACM Transactions on Computational Logic, 10(3), 2009.
J. Esparza. Keeping a crowd safe: On the complexity of parameterized verification. In STACS’14, volume 25 of Leibniz International Proceedings in Informatics, pages 1–10. Leibniz-Zentrum für Informatik, 2014.
K. Etessami, M. Y. Vardi, and T. Wilke. First-order logic with two variables and unary temporal logic. Inf. Comput., 179(2):279–295, 2002.
L. Exibard, E. Filiot, and P.-A. Reynier. Synthesis of Data Word Transducers. In W. Fokkink and R. van Glabbeek, editors, 30th International Conference on Concurrency Theory (CONCUR 2019), volume 140 of Leibniz International Proceedings in Informatics (LIPIcs), pages 24:1–24:15, Dagstuhl, Germany, 2019. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.
D. Figueira and M. Praveen. Playing with repetitions in data words using energy games. In A. Dawar and E. Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09–12, 2018, pages 404–413. ACM, 2018.
D. Figueira and M. Praveen. Playing with repetitions in data words using energy games. arXiv preprint arXiv:1802.07435, 2018.
B. Finkbeiner and E. Olderog. Petri games: Synthesis of distributed systems with causal memory. Inf. Comput., 253:181–203, 2017.
H. Frenkel, O. Grumberg, and S. Sheinvald. An automata-theoretic approach to model-checking systems and specifications over infinite data domains. J. Autom. Reasoning, 63(4):1077–1101, 2019.
M. Fürer. The computational complexity of the unconstrained limited domino problem (with implications for logical decision problems). In E. Börger, G. Hasenjaeger, and D. Rödding, editors, Logic and Machines: Decision Problems and Complexity, Proceedings of the Symposium "Rekursive Kombinatorik" held from May 23–28, 1983 at the Institut für Mathematische Logik und Grundlagenforschung der Universität Münster/Westfalen, volume 171 of Lecture Notes in Computer Science, pages 312–319. Springer, 1983.
P. Gastin and N. Sznajder. Fair synthesis for asynchronous distributed systems. ACM Transactions on Computational Logic, 14(2:9), 2013.
E. Grädel, P. G. Kolaitis, and M. Y. Vardi. On the decision problem for two-variable first-order logic. Bulletin of Symbolic Logic, 3(1):53–69, 1997.
W. Hanf. Model-theoretic methods in the study of elementary logic. In J. W. Addison, L. Henkin, and A. Tarski, editors, The Theory of Models. North-Holland, Amsterdam, 1965.
F. Horn, W. Thomas, N. Wallmeier, and M. Zimmermann. Optimal strategy synthesis for request-response games. RAIRO - Theor. Inf. and Applic., 49(3):179–203, 2015.
S. Jacobs and R. Bloem. Parameterized synthesis. Logical Methods in Computer Science, 10(1), 2014.
S. Jacobs, L. Tentrup, and M. Zimmermann. Distributed synthesis for parameterized temporal logics. Inf. Comput., 262(Part):311–328, 2018.
P. Jancar. On reachability-related games on vector addition systems with states. In RP’15, volume 9328 of LNCS, pages 50–62. Springer, 2015.
M. Jenkins, J. Ouaknine, A. Rabinovich, and J. Worrell. The church synthesis problem with metric. In M. Bezem, editor, Computer Science Logic, 25th International Workshop / 20th Annual Conference of the EACSL, CSL 2011, September 12–15, 2011, Bergen, Norway, Proceedings, volume 12 of LIPIcs, pages 307–321. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2011.
M. Kaminski and N. Francez. Finite-memory automata. Theoretical Computer Science, 134(2):329–363, 1994.
A. Khalimov and O. Kupferman. Register-Bounded Synthesis. In W. Fokkink and R. van Glabbeek, editors, 30th International Conference on Concurrency Theory (CONCUR 2019), volume 140 of Leibniz International Proceedings in Informatics (LIPIcs), pages 25:1–25:16, Dagstuhl, Germany, 2019. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.
A. Khalimov, B. Maderbacher, and R. Bloem. Bounded synthesis of register transducers. In S. K. Lahiri and C. 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.
E. Kieronski and M. Otto. Small substructures and decidability issues for first-order logic with two variables. J. Symb. Log., 77(3):729–765, 2012.
L. Libkin, T. Tan, and D. Vrgoc. Regular expressions for data words. J. Comput. Syst. Sci., 81(7):1278–1297, 2015.
M. L. Minsky. Computation: Finite and Infinite Machines. Prentice Hall, Upper Saddle River, NJ, USA, 1967.
A. Muscholl. Automated synthesis of distributed controllers. In M. M. Halldórsson, K. Iwama, N. Kobayashi, and B. Speckmann, editors, Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, volume 9135 of Lecture Notes in Computer Science, pages 11–27. Springer, 2015.
A. Pnueli and R. Rosner. Distributed reactive systems are hard to synthesize. In 31st Annual Symposium on Foundations of Computer Science, St. Louis, Missouri, USA, October 22-24, 1990, Volume II, pages 746–757. IEEE Computer Society, 1990.
M. O. Rabin. Automata on infinite objects and Church’s problem. Number 13 in Regional Conference Series in Mathematics. American Mathematical Soc., 1972.
J. Raskin, M. Samuelides, and L. V. Begin. Games for counting abstractions. Electr. Notes Theor. Comput. Sci., 128(6):69–85, 2005.
A. Sangnier and O. Stietel. Private communication, 2020.
L. Schröder, D. Kozen, S. Milius, and T. Wißmann. Nominal automata with name binding. In J. Esparza and A. S. Murawski, editors, Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10203 of Lecture Notes in Computer Science, pages 124–142, 2017.
T. Schwentick and K. Barthelmann. Local normal forms for first-order logic with applications to games and automata. In Annual Symposium on Theoretical Aspects of Computer Science, pages 444–454. Springer, 1998.
W. Thomas. Church’s problem and a tour through automata theory. In Pillars of Computer Science, Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, volume 4800 of Lecture Notes in Computer Science, pages 635–655. Springer, 2008.
Y. Velner and A. Rabinovich. Church synthesis problem for noisy input. In M. Hofmann, editor, Foundations of Software Science and Computational Structures - 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings, volume 6604 of Lecture Notes in Computer Science, pages 275–289. Springer, 2011.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Bérard, B., Bollig, B., Lehaut, M., Sznajder, N. (2020). Parameterized Synthesis for Fragments of First-Order Logic Over Data Words. In: Goubault-Larrecq, J., König, B. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2020. Lecture Notes in Computer Science(), vol 12077. Springer, Cham. https://doi.org/10.1007/978-3-030-45231-5_6
Download citation
DOI: https://doi.org/10.1007/978-3-030-45231-5_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45230-8
Online ISBN: 978-3-030-45231-5
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)