Wait-Only Broadcast Protocols are Easier to Verify
Wait-Only Broadcast Protocols are Easier to Verify
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.
Lucie Guillou、Arnaud Sangnier、Nathalie Sznajder
计算技术、计算机技术
Lucie Guillou,Arnaud Sangnier,Nathalie Sznajder.Wait-Only Broadcast Protocols are Easier to Verify[EB/OL].(2025-06-27)[2025-07-09].https://arxiv.org/abs/2506.22144.点此复制
评论