Wait-Only Broadcast Protocols are Easier to Verify
Abstract
We study networks of processes that all execute the same finite-state protocol and communicate via broadcasts. We are interested in two problems with a parameterized number of processes: the synchronization problem which asks whether there is an execution which puts all processes on a given state; and the repeated coverability problem which asks if there is an infinite execution where a given transition is taken infinitely often. Since both problems are undecidable in the general case, we investigate those problems when the protocol is Wait-Only, i.e., it has no state from which a process can both broadcast and receive messages. We establish that the synchronization problem becomes Ackermann-complete, and the repeated coverability problem is in EXPSPACE, and PSPACE-hard.
Keywords
Cite
@article{arxiv.2506.22144,
title = {Wait-Only Broadcast Protocols are Easier to Verify},
author = {Lucie Guillou and Arnaud Sangnier and Nathalie Sznajder},
journal= {arXiv preprint arXiv:2506.22144},
year = {2025}
}
Comments
Long version of a paper accepted to appear at MFCS 2025