Document Open Access Logo

Wait-Only Broadcast Protocols Are Easier to Verify

Authors Lucie Guillou , Arnaud Sangnier , Nathalie Sznajder

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2025.53.pdf
  • Filesize: 1.42 MB
  • 17 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
Keywords
  • Parameterised verification
  • Reachability
  • Broadcast

Metrics

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

Abstract

We study networks of processes that all execute the same finite-state protocol and communicate via broadcasts. We are interested in two problems with a parameterized number of processes: the synchronization problem which asks whether there is an execution which puts all processes on a given state; and the repeated coverability problem which asks if there is an infinite execution where a given transition is taken infinitely often. Since both problems are undecidable in the general case, we investigate those problems when the protocol is Wait-Only, i.e., it has no state from which a process can both broadcast and receive messages. We establish that the synchronization problem becomes Ackermann-complete, and the repeated coverability problem is in ExpSpace and PSpace-hard.

Cite As Get BibTex

Lucie Guillou, Arnaud Sangnier, and Nathalie Sznajder. Wait-Only Broadcast Protocols Are Easier to Verify. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 53:1-53:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.MFCS.2025.53

Author Details

Lucie Guillou
  • IRIF, CNRS, Université Paris Cité, France
Arnaud Sangnier
  • DIBRIS, Università di Genova, Italy
Nathalie Sznajder
  • LIP6, CNRS, Sorbonne Université, Paris, France

Funding

ANR project PaVeDyS (ANR-23-CE48-0005).

References

  1. K. R. Apt and D. C. Kozen. Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett., 22(6):307-309, 1986. URL: https://doi.org/10.1016/0020-0190(86)90071-2.
  2. Peter Chini, Roland Meyer, and Prakash Saivasan. Liveness in broadcast networks. Computing, 104(10):2203-2223, 2022. URL: https://doi.org/10.1007/S00607-021-00986-Y.
  3. Wojciech Czerwinski and Lukasz Orlikowski. Reachability in vector addition systems is ackermann-complete. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 1229-1240. IEEE, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00120.
  4. Giorgio Delzanno, Jean-François Raskin, and Laurent Van Begin. Towards the automated verification of multithreaded java programs. In TACAS 2002, volume 2280 of LNCS, pages 173-187. Springer, 2002. URL: https://doi.org/10.1007/3-540-46002-0_13.
  5. Giorgio Delzanno, Arnaud Sangnier, and Gianluigi Zavattaro. Parameterized verification of ad hoc networks. In Paul Gastin and François Laroussinie, editors, CONCUR 2010 - Concurrency Theory, pages 313-327, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-15375-4_22.
  6. E.A. Emerson and K.S. Namjoshi. On model checking for non-deterministic infinite-state systems. In Proceedings. Thirteenth Annual IEEE Symposium on Logic in Computer Science (LICS), pages 70-80, 1998. URL: https://doi.org/10.1109/LICS.1998.705644.
  7. J. Esparza, P. Ganty, and R. Majumdar. Parameterized verification of asynchronous shared-memory systems. In CAV'13, volume 8044 of LNCS, pages 124-140. Springer-Verlag, 2013. URL: https://doi.org/10.1007/978-3-642-39799-8_8.
  8. Javier Esparza, Alain Finkel, and Richard Mayr. On the verification of broadcast protocols. In 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999, pages 352-359. IEEE Computer Society, 1999. URL: https://doi.org/10.1109/LICS.1999.782630.
  9. S. M. German and A. P. Sistla. Reasoning about systems with many processes. Journal of the ACM, 39(3):675-735, 1992. URL: https://doi.org/10.1145/146637.146681.
  10. Lucie Guillou, Arnaud Sangnier, and Nathalie Sznajder. Safety analysis of parameterised networks with non-blocking rendez-vous. In CONCUR'23, volume 279 of LIPIcs, pages 7:1-7:17. loss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.CONCUR.2023.7.
  11. Lucie Guillou, Arnaud Sangnier, and Nathalie Sznajder. Safety verification of wait-only non-blocking broadcast protocols. In Application and Theory of Petri Nets and Concurrency - 45th International Conference, PETRI NETS 2024, volume 14628 of Lecture Notes in Computer Science, pages 291-311. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-61433-0_14.
  12. Lucie Guillou, Arnaud Sangnier, and Nathalie Sznajder. Wait-only broadcast protocols are easier to verify, 2025. URL: https://arxiv.org/abs/2506.22144.
  13. Peter Habermehl. On the complexity of the linear-time mu -calculus for petri-nets. In Pierre Azéma and Gianfranco Balbo, editors, Application and Theory of Petri Nets 1997, 18th International Conference, ICATPN '97, Toulouse, France, June 23-27, 1997, Proceedings, volume 1248 of Lecture Notes in Computer Science, pages 102-116. Springer, 1997. URL: https://doi.org/10.1007/3-540-63139-9_32.
  14. John E. Hopcroft and Jean-Jacques Pansiot. On the reachability problem for 5-dimensional vector addition systems. Theor. Comput. Sci., 8:135-159, 1979. URL: https://doi.org/10.1016/0304-3975(79)90041-0.
  15. Dexter Kozen. Lower bounds for natural proof systems. In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pages 254-266. IEEE Computer Society, 1977. URL: https://doi.org/10.1109/SFCS.1977.16.
  16. Jérôme Leroux. Vector addition system reversible reachability problem. In Joost-Pieter Katoen and Barbara König, editors, CONCUR 2011 - Concurrency Theory - 22nd International Conference, CONCUR 2011, Aachen, Germany, September 6-9, 2011. Proceedings, volume 6901 of Lecture Notes in Computer Science, pages 327-341. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-23217-6_22.
  17. Jérôme Leroux. The reachability problem for petri nets is not primitive recursive. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 1241-1252. IEEE, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00121.
  18. Jérôme Leroux and Sylvain Schmitz. Reachability in vector addition systems is primitive-recursive in fixed dimension. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785796.
  19. R.J. Lipton. The reachability problem requires exponential space. Research report (Yale University. Department of Computer Science). Department of Computer Science, Yale University, 1976. URL: https://books.google.fr/books?id=7iSbGwAACAAJ.
  20. S. Schmitz and P. Schnoebelen. The power of well-structured systems. In CONCUR'13, volume 8052 of Lecture Notes in Computer Science, pages 5-24. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40184-8_2.
  21. Rüdiger Valk. Self-modifying nets, a natural extension of petri nets. In ICALP'78, volume 62 of LNCS, pages 464-476. Springer, 1978. URL: https://doi.org/10.1007/3-540-08860-1_35.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact