Wait-Only Broadcast Protocols are Easier to Verify
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866918072941543424 |
|---|---|
| author | Guillou, Lucie Sangnier, Arnaud Sznajder, Nathalie |
| author_facet | Guillou, Lucie Sangnier, Arnaud Sznajder, Nathalie |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_22144 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Wait-Only Broadcast Protocols are Easier to Verify Guillou, Lucie Sangnier, Arnaud Sznajder, Nathalie Logic in Computer Science 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. |
| title | Wait-Only Broadcast Protocols are Easier to Verify |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2506.22144 |