2024/06/21 by Guillou, Lucie, Sangnier, Arnaud, Sznajder, Nathalie
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Multiagent Systems (cs.MA)
paper · doi:10.48550/arxiv.2406.15202
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. 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.