# Safety Verification of Wait-Only Non-Blocking Broadcast Protocols

arXiv: https://arxiv.org/abs/2403.18591 · HTML: https://mlsanity.com/paper/2403.18591/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 4 of its 24 references that are in the map.
- First posted on arXiv 27 Mar 2024.

## Builds on (most cited first, 4 of 4)

- [The Power of Well-Structured Systems](https://mlsanity.com/paper/1402.2908/) (2014)
- [Deciding the existence of cut-off in parameterized rendez-vous networks](https://mlsanity.com/paper/2007.05789/) (2020)
- [Finding Cut-Offs in Leaderless Rendez-Vous Protocols is Easy](https://mlsanity.com/paper/2010.09471/) (2020)
- [Safety Analysis of Parameterised Networks with Non-Blocking Rendez-Vous](https://mlsanity.com/paper/2307.04546/) (2023)

## Abstract (arXiv)

Broadcast protocols are programs designed to be executed by networks of processes. Each process runs the same protocol, and communication between them occurs in synchronously in two ways: broadcast, where one process sends a message to all others, and rendez-vous, where one process sends a message to at most one other process. In both cases, communication is non-blocking, meaning the message is sent even if no process is able to receive it. We consider two coverability problems: the state coverability problem asks whether there exists a number of processes that allows reaching a given state of the protocol, and the configuration coverability problem asks whether there exists a number of processes that allows covering a given configuration. These two problems are known to be decidable and Ackermann-hard. We show that when the protocol is Wait-Only (i.e., it has no state from which a process can both send and receive messages), these problems become P-complete and PSPACE-complete, respectively.