2026-07-23T19:56:47Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:24160 2025-11-12T13:33:50Z ddc:004 open_access

Wait-Only Broadcast Protocols Are Easier to Verify Guillou, Lucie Sangnier, Arnaud Sznajder, Nathalie Parameterised verification Reachability Broadcast 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Lucie Guillou and Arnaud Sangnier and Nathalie Sznajder 2025 Is Part Of LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.MFCS.2025.53 urn:nbn:de:0030-drops-241609 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.53 eng https://creativecommons.org/licenses/by/4.0/legalcode