Abstract
We study the reactive synthesis problem for distributed systems with an unbounded number of participants interacting with an uncontrollable environment. Executions of those systems are modeled by data words, and specifications are given as first-order logic formulas from a fragment we call prefix first-order logic that implements a limited kind of order. We show that this logic has nice properties that enable us to prove decidability of the synthesis problem.
Supported by the ERC Consolidator grant D-SynMA (No. 772459).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Bérard, B., Bollig, B., Lehaut, M., Sznajder, N.: Parameterized synthesis for fragments of first-order logic over data words. In: FoSSaCS 2020. LNCS, vol. 12077, pp. 97–118. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-45231-5_6
Bojanczyk, M., Muscholl, A., Schwentick, T., Segoufin, L., David, C.: Two-variable logic on words with data. In: 21th IEEE Symposium on Logic in Computer Science LICS (2006)
Büchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society (1969)
Church, A.: Applications of recursive arithmetic to the problem of circuit synthesis. In: Summaries of the Summer Institute of Symbolic Logic, vol. 1 (1957)
Demri, S., d’Souza, D., Gascon, R.: Temporal logics of repeating values. J. Log. Comput. 22(5), 1059–1096 (2012)
Demri, S., Lazić, R.: Ltl with the freeze quantifier and register automata. ACM Trans. Comput. Logic (TOCL) 10(3), 1–30 (2009)
Exibard, L., Filiot, E., Khalimov, A.: A generic solution to register-bounded synthesis with an application to discrete orders. ar**v preprint ar**v:2205.01952 (2022)
Figueira, D., Praveen, M.: Playing with repetitions in data words using energy games. In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS (2018)
Grange, J., Lehaut, M.: First order synthesis for data words revisited. ar**v preprint ar**v:2307.04499 (2023)
Grange, J., Lehaut, M.: Synthesis for prefix first-order logic on data words. ar**v preprint ar**v:2404.14517 (2024)
Kaminski, M., Francez, N.: Finite-memory automata. Theoret. Comput. Sci. 134(2), 329–363 (1994)
Kara, A.: Logics on data words (2016)
Neven, F., Schwentick, T., Vianu, V.: Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Logic (TOCL) 5(3), 403–435 (2004)
Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: Proceedings [1990] 31st Annual Symposium on Foundations of Computer Science, pp. 746–757. IEEE (1990)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 IFIP International Federation for Information Processing
About this paper
Cite this paper
Grange, J., Lehaut, M. (2024). Synthesis for Prefix First-Order Logic on Data Words. In: Castiglioni, V., Francalanza, A. (eds) Formal Techniques for Distributed Objects, Components, and Systems. FORTE 2024. Lecture Notes in Computer Science, vol 14678. Springer, Cham. https://doi.org/10.1007/978-3-031-62645-6_5
Download citation
DOI: https://doi.org/10.1007/978-3-031-62645-6_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-62644-9
Online ISBN: 978-3-031-62645-6
eBook Packages: Computer ScienceComputer Science (R0)
