Document Open Access Logo

Phase-Bounded Broadcast Networks over Topologies of Communication

Authors Lucie Guillou , Arnaud Sangnier , Nathalie Sznajder

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2024.26.pdf
  • Filesize: 0.9 MB
  • 16 pages

Document Identifiers

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

  • Guillou, Lucie: ANR project PaVeDyS (ANR-23-CE48-0005)

Cite AsGet BibTex

Lucie Guillou, Arnaud Sangnier, and Nathalie Sznajder. Phase-Bounded Broadcast Networks over Topologies of Communication. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 26:1-26:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CONCUR.2024.26

Abstract

We study networks of processes that all execute the same finite state protocol and that communicate through broadcasts. The processes are organized in a graph (a topology) and only the neighbors of a process in this graph can receive its broadcasts. The coverability problem asks, given a protocol and a state of the protocol, whether there is a topology for the processes such that one of them (at least) reaches the given state. This problem is undecidable [G. Delzanno et al., 2010]. We study here an under-approximation of the problem where processes alternate a bounded number of times k between phases of broadcasting and phases of receiving messages. We show that, if the problem remains undecidable when k is greater than 6, it becomes decidable for k = 2, and ExpSpace-complete for k = 1. Furthermore, we show that if we restrict ourselves to line topologies, the problem is in P for k = 1 and k = 2.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
Keywords
  • Parameterized verification
  • Coverability
  • Broadcast Networks

Metrics

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

Related Versions

References

  1. B. Aminof, S. Jacobs, A. Khalimov, and S. Rubin. Parametrized model checking of token-passing systems. In VMCAI'14, volume 8318 of LNCS, pages 262-281. Springer-Verlag, 2014. Google Scholar
  2. D. Angluin, J. Aspnes, Z. Diamadi, M. J. Fischer, and R. Peralta. Computation in networks of passively mobile finite-state sensors. In PODC'04, pages 290-299. ACM, 2004. Google Scholar
  3. M. F. Atig, A. Bouajjani, and S. Qadeer. Context-bounded analysis for concurrent programs with dynamic creation of threads. Log. Methods Comput. Sci., 7(4), 2011. Google Scholar
  4. B. Bollig, M. Lehaut, and N. Sznajder. Round-bounded control of parameterized systems. In ATVA'18, volume 11138 of Lecture Notes in Computer Science, pages 370-386. Springer, 2018. Google Scholar
  5. E. M. Clarke, M. Talupur, T. Touili, and H. Veith. Verification by network decomposition. In CONCUR'04, volume 3170 of LNCS, pages 276-291. Springer-Verlag, 2004. Google Scholar
  6. G. Delzanno, A.Sangnier, and G. Zavattaro. Parameterized verification of ad hoc networks. In CONCUR'10, volume 6269 of LNCS, pages 313-327. Springer, 2010. Google Scholar
  7. G. Delzanno, A. Sangnier, and G. Zavattaro. On the power of cliques in the parameterized verification of ad hoc networks. In FOSSACS'11, volume 6604 of LNCS, pages 441-455. Springer, 2011. Google Scholar
  8. A. Durand-Gasselin, J. Esparza, P. Ganty, and R. Majumdar. Model checking parameterized asynchronous shared-memory systems. Formal Methods Syst. Des., 50(2-3):140-167, 2017. Google Scholar
  9. J. Esparza, A. Finkel, and R. Mayr. On the verification of broadcast protocols. In LICS'99, pages 352-359. IEEE Computer Society, 1999. Google Scholar
  10. J. Esparza, P. Ganty, J. Leroux, and R. Majumdar. Verification of population protocols. Acta Informatica, 54(2):191-215, 2017. Google Scholar
  11. J. Esparza, P. Ganty, and R. Majumdar. Parameterized verification of asynchronous shared-memory systems. J. ACM, 63(1):10:1-10:48, 2016. Google Scholar
  12. J. Esparza, S. Jaax, M. A. Raskin, and C. Weil-Kennedy. The complexity of verifying population protocols. Distributed Comput., 34(2):133-177, 2021. Google Scholar
  13. S. M. German and A. P. Sistla. Reasoning about systems with many processes. Journal of the ACM, 39(3):675-735, 1992. Google Scholar
  14. L. Guillou, A. Sangnier, and N. Sznajder. Safety analysis of parameterised networks with non-blocking rendez-vous. In CONCUR'23, volume 279 of LIPIcs, pages 7:1-7:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. Google Scholar
  15. L. Guillou, A. Sangnier, and N. Sznajder. Phase-bounded broadcast networks over topologies of communication, 2024. URL: https://arxiv.org/abs/2406.15202.
  16. O. H. Ibarra. Reversal-bounded multicounter machines and their decision problems. J. ACM, 25(1):116-133, 1978. Google Scholar
  17. S. La Torre, P. Madhusudan, and G. Parlato. Model-checking parameterized concurrent programs using linear interfaces. In CAV'10, volume 6174 of LNCS, pages 629-644. Springer, 2010. Google Scholar
  18. R.J. Lipton. The reachability problem requires exponential space. Research report (Yale University. Department of Computer Science). Department of Computer Science, Yale University, 1976. Google Scholar
  19. M. L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, Inc., 1967. Google Scholar
  20. S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software. In TACAS'05, volume 3440 of LNCS, pages 93-107. Springer, 2005. Google Scholar
  21. C. Rackoff. The covering and boundedness problems for vector addition systems. Theoretical Computer Science, 6:223-231, 1978. Google Scholar
  22. G. Ramalingam. Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst., 22(2):416-430, 2000. Google Scholar
  23. W. J. Savitch. Relationships between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci., 4(2):177-192, 1970. URL: https://doi.org/10.1016/S0022-0000(70)80006-X.
  24. S. Schmitz and P. Schnoebelen. The power of well-structured systems. In CONCUR'13, volume 8052 of LNCS, pages 5-24. Springer, 2013. 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