2026-07-24T09:35:38Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20798 2024-08-29T05:40:58Z ddc:004 open_access

Phase-Bounded Broadcast Networks over Topologies of Communication Guillou, Lucie Sangnier, Arnaud Sznajder, Nathalie Parameterized verification Coverability Broadcast Networks 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Lucie Guillou and Arnaud Sangnier and Nathalie Sznajder 2024 Is Part Of LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2024.26 urn:nbn:de:0030-drops-207987 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.26 eng https://creativecommons.org/licenses/by/4.0/legalcode