Phase-Bounded Broadcast Networks over Topologies of Communication

TL;DR

This work analyzes the parameterized verification problem for broadcast networks whose processes run a common finite-state protocol and communicate via broadcasts over fixed topologies. It introduces phase-bounded under-approximations, formalized through $k$-phase unfoldings, to regain decidability where the general problem is undecidable. A pivotal result is the equivalence of Cover on Graphs and Trees, together with precise decidability/undecidability boundaries: for $k\ge 6$ the problem is undecidable, for $k=2$ it becomes decidable, and for $k=1$ it is EXPSPACE-complete; on line topologies, the problem is in P for $k\in\{1,2\}$. The paper further shows that 1-phase-bounded Cover[Graphs] is ExpSpace-complete via a VASS reduction, while 2-phase-bounded protocols yield decidability for Cover on Trees and a polynomial-time algorithm for Lines, leveraging bounded-height tree unfoldings and bounded-path results. These findings delineate the precise trade-offs between expressive power of broadcast protocols and tractable verification under phase-bounded constraints, with implications for scalable analysis of parameterized distributed systems.

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. 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$.

Figures (28)

• Figure 1: Example of a broadcast protocol denoted $P$
• Figure 2: Example of an execution of protocol $P$ (\ref{['fig:bp:examples']}).
• Figure 3: $P_2$: the 2-unfolding of protocol $P$ (\ref{['fig:bp:examples']}).
• Figure 4: Protocol $P_h$ executed by $v_0$.
• Figure 5: Protocol $P_t$ executed by $v_n$.

Theorems & Definitions (56)

• Definition 1
• Definition 2
• Example 3
• Theorem 4
• Example 5
• Definition 6
• Example 7
• Lemma 8
• Theorem 9
• Theorem 10