LIPIcs.CONCUR.2024.26.pdf
- Filesize: 0.9 MB
- 16 pages
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.
Feedback for Dagstuhl Publishing