Safety Verification of Wait-Only Non-Blocking Broadcast Protocols
This provides a significant complexity reduction for safety verification in distributed systems, specifically for protocols with restricted communication patterns, though it is incremental as it builds on known hardness results.
The paper tackles the complexity of coverability problems in networks of processes with synchronous communication, showing that for Wait-Only protocols (where no state allows both sending and receiving), the state coverability problem reduces to P and the configuration coverability problem to PSPACE, compared to Ackermann-hard complexity in the general case.
We study networks of processes that all execute the same finite protocol and communicate synchronously in two different ways: a process can broadcast one message to all other processes or send it to at most one other process. In both cases, if no process can receive the message, it will still be sent. We establish a precise complexity class for two coverability problems with a parameterised number of processes: the state coverability problem and the configuration coverability problem. It is already known that these problems are Ackermann-hard (but decidable) in the general case. We show that when the protocol is Wait-Only, i.e., it has no state from which a process can send and receive messages, the complexity drops to P and PSPACE, respectively.