Document Open Access Logo

Synthesising Full-Information Protocols

Authors Dietmar Berwanger , Laurent Doyen , Thomas Soullard

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2025.13.pdf
  • Filesize: 0.66 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Representations of games and their complexity
  • Computing methodologies → Planning under uncertainty
Keywords
  • Infinite Games on Finite Graphs
  • Imperfect Information
  • Reactive Processes
  • Distributed Synthesis
  • Dynamic Networks

Metrics

Abstract

We study a communication model where processes reveal their entire local information whenever they interact. However, the system involves an indeterminate environment that may control when a communication event occurs and which participants are involved. As a result, the amount of information a process may receive at once is unbounded. 
Such full-information protocols are common in the distributed-computing literature. Here, we consider synchronous systems, modelled as infinite games with imperfect information played on finite graphs. We present a decision procedure for the synthesis of a process with an ω-regular specification in a system where the other participating processes are fixed. The challenge lies in constructing a finite representation of information trees with unbounded branching. Our construction is non-elementary in the size of the problem instance, and we establish a matching non-elementary lower bound for the complexity of the synthesis problem.

Cite As Get BibTex

Dietmar Berwanger, Laurent Doyen, and Thomas Soullard. Synthesising Full-Information Protocols. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.FSTTCS.2025.13

Author Details

Dietmar Berwanger
  • Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, Paris, France
Laurent Doyen
  • Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, Paris, France
Thomas Soullard
  • Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, Paris, France

References

  1. André Arnold, Aymeric Vincent, and Igor Walukiewicz. Games for synthesis of controllers with partial observation. Theoretical computer science, 303(1):7-34, 2003. URL: https://doi.org/10.1016/S0304-3975(02)00442-5.
  2. Salman Azhar, Gary Peterson, and John Reif. Lower bounds for multiplayer non-cooperative games of incomplete information. Journal of Computers and Mathematics with Applications, 41:957-992, 2001. URL: https://doi.org/10.1016/S0898-1221(00)00333-3.
  3. Pablo Barceló, Chih-Duo Hong, Xuan-Bach Le, Anthony W. Lin, and Reino Niskanen. Monadic Decomposability of Regular Relations. In Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi, editors, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019), volume 132 of Leibniz International Proceedings in Informatics (LIPIcs), pages 103:1-103:14, Dagstuhl, Germany, 2019. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ICALP.2019.103.
  4. D. Berwanger and L. Doyen. Observation and distinction. representing information in infinite games. Theory of Computing Systems, 67(1):4-27, 2023. URL: https://doi.org/10.1007/s00224-021-10044-x.
  5. D. Berwanger, A. B. Mathew, and M. van den Bogaard. Hierarchical information and the synthesis of distributed strategies. Acta Informatica, 55(8):669-701, 2018. URL: https://doi.org/10.1007/s00236-017-0306-5.
  6. Dietmar Berwanger, Lukasz Kaiser, and Bernd Puchala. A perfect-information construction for coordination in games. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2011, December 12-14, 2011, Mumbai, India, volume 13 of LIPIcs, pages 387-398. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2011.387.
  7. J. R. Büchi and L. H. Landweber. Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society, 138:295-311, 1969. URL: https://doi.org/10.1090/S0002-9947-1969-0280205-0.
  8. Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasi-polynomial time. SIAM J. Comput., 51(2):17-152, 2022. URL: https://doi.org/10.1137/17M1145288.
  9. K. Chatterjee, L. Doyen, T. A. Henzinger, and J.-F. Raskin. Algorithms for omega-regular games of incomplete information. Logical Methods in Computer Science, 3(3:4), 2007. URL: https://doi.org/10.2168/LMCS-3(3:4)2007.
  10. A. Church. Logic, arithmetics, and automata. Proc. Int. Congr. Math., pages 23-35, 1962. Google Scholar
  11. Cynthia Dwork and Yoram Moses. Knowledge and common knowledge in a byzantine environment: Crash failures. Inf. Comput., 88(2):156-186, 1990. URL: https://doi.org/10.1016/0890-5401(90)90014-9.
  12. Kousha Etessami, Thomas Wilke, and Rebecca A. Schuller. Fair simulation relations, parity games, and state space reduction for Büchi automata. SIAM J. Comput., 34(5):1159-1175, 2005. URL: https://doi.org/10.1137/S0097539703420675.
  13. Bernd Finkbeiner and Sven Schewe. Uniform distributed synthesis. In 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA, Proceedings, pages 321-330. IEEE Computer Society, 2005. URL: https://doi.org/10.1109/LICS.2005.53.
  14. B. Genest, H. Gimbert, A. Muscholl, and I. Walukiewicz. Asynchronous games over tree architectures. In Proc. of ICALP: Automata, Languages, and Programming, LNCS 7966, pages 275-286. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39212-2_26.
  15. Valentin Goranko and Martin Otto. Model theory of modal logic. In Patrick Blackburn, J. F. A. K. van Benthem, and Frank Wolter, editors, Handbook of Modal Logic, volume 3 of Studies in logic and practical reasoning, pages 249-329. North-Holland, 2007. URL: https://doi.org/10.1016/S1570-2464(07)80008-5.
  16. Yuri Gurevich and Leo Harrington. Trees, automata, and games. In Proceedings of the fourteenth annual ACM symposium on theory of computing, pages 60-65, 1982. URL: https://doi.org/10.1145/800070.802177.
  17. D. Harel and A. Pnueli. On the development of reactive systems. In Krzysztof R. Apt, editor, Logics and Models of Concurrent Systems, pages 477-498, Berlin, Heidelberg, 1985. Springer Berlin Heidelberg. Google Scholar
  18. M. Jurdzinski, R. Morvan, and K. S. Thejaswini. Universal algorithms for parity games and nested fixpoints. In Principles of Systems Design - Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday, LNCS 13660, pages 252-271. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-22337-2_12.
  19. Orna Kupferman and Moshe Y. Vardi. Synthesizing distributed systems. In Proc. of LICS '01, pages 389-398. IEEE Computer Society Press, June 2001. URL: https://doi.org/10.1109/LICS.2001.932514.
  20. Karoliina Lehtinen, Pawel Parys, Sven Schewe, and Dominik Wojtczak. A recursive approach to solving parity games in quasipolynomial time. Log. Methods Comput. Sci., 18(1), 2022. URL: https://doi.org/10.46298/LMCS-18(1:8)2022.
  21. Tal Mizrahi and Yoram Moses. Continuous consensus with ambiguous failures. Theor. Comput. Sci., 411(34-36):3031-3041, 2010. URL: https://doi.org/10.1016/J.TCS.2010.04.025.
  22. M. Pease, R. Shostak, and L. Lamport. Reaching agreements in the presence of faults. Journal of the ACM, 27(2):228-234, April 1980. URL: https://doi.org/10.1145/322186.322188.
  23. A. Pnueli and R. Rosner. Distributed reactive systems are hard to synthesize. In Proc. of FOCS: Foundations of Computer Science, pages 746-757. IEEE, 1990. Google Scholar
  24. M. O. Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the AMS, 141:1-35, 1969. Google Scholar
  25. M. O. Rabin. Automata on Infinite Objects and Church’s Problem. American Mathematical Society, Boston, MA, USA, 1972. Google Scholar
  26. John H. Reif. The complexity of two-player games of incomplete information. Journal of Computer and System Sciences, 29(2):274-301, 1984. URL: https://doi.org/10.1016/0022-0000(84)90034-5.
  27. D. Sangiorgi. Introduction to Bisimulation and Coinduction. Cambridge University Press, 2011. Google Scholar
  28. Sven Schewe. Distributed synthesis is simply undecidable. Inf. Process. Lett., 114(4):203-207, April 2014. URL: https://doi.org/10.1016/j.ipl.2013.11.012.
  29. W. Thomas. On the synthesis of strategies in infinite games. In Proc. of STACS: Symposium on Theoretical Aspects of Computer Science, LNCS 900. Springer, 1995. URL: https://doi.org/10.1007/3-540-59042-0_57.
  30. W. Thomas. Languages, automata, and logic. In Handbook of Formal Languages, volume 3, Beyond Words, chapter 7, pages 389-455. Springer, 1997. URL: https://doi.org/10.1007/978-3-642-59126-6_7.
  31. Thomas YC Woo and Simon S Lam. A lesson on authentication protocol design. ACM SIGOPS Operating Systems Review, 28(3):24-37, 1994. URL: https://doi.org/10.1145/182110.182113.
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