Wait-Only Broadcast Protocols are Easier to Verify

TL;DR

This paper investigates the verification complexity of wait-only broadcast protocols, showing that certain problems become computationally hard but more manageable in this restricted setting.

Contribution

It proves that the synchronization problem is Ackermann-complete and the repeated coverability problem is in EXPSPACE and PSPACE-hard for wait-only broadcast protocols.

Findings

Synchronization problem is Ackermann-complete.

Repeated coverability problem is in EXPSPACE.

Verification complexity is reduced in wait-only protocols.

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.