Undecidability of the Emptiness Problem for Weak Models of Distributed Computing
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916682833854464 |
|---|---|
| author | Principato, Flavio T. Esparza, Javier Czerner, Philipp |
| author_facet | Principato, Flavio T. Esparza, Javier Czerner, Philipp |
| contents | Esparza and Reiter have recently conducted a systematic comparative study of weak asynchronous models of distributed computing, in which a network of identical finite-state machines acts cooperatively to decide properties of the network's graph. They introduced a distributed automata framework encompassing many different models, and proved that w.r.t. their expressive power (the graph properties they can decide) distributed automata collapse into seven equivalence classes. In this contribution, we turn our attention to the formal verification problem: Given a distributed automaton, does it decide a given graph property? We consider a fundamental instance of this question - the emptiness problem: Given a distributed automaton, does it accept any graph at all? Our main result is negative: the emptiness problem is undecidable for six of the seven equivalence classes, and trivially decidable for the remaining class. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_07339 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Undecidability of the Emptiness Problem for Weak Models of Distributed Computing Principato, Flavio T. Esparza, Javier Czerner, Philipp Formal Languages and Automata Theory Esparza and Reiter have recently conducted a systematic comparative study of weak asynchronous models of distributed computing, in which a network of identical finite-state machines acts cooperatively to decide properties of the network's graph. They introduced a distributed automata framework encompassing many different models, and proved that w.r.t. their expressive power (the graph properties they can decide) distributed automata collapse into seven equivalence classes. In this contribution, we turn our attention to the formal verification problem: Given a distributed automaton, does it decide a given graph property? We consider a fundamental instance of this question - the emptiness problem: Given a distributed automaton, does it accept any graph at all? Our main result is negative: the emptiness problem is undecidable for six of the seven equivalence classes, and trivially decidable for the remaining class. |
| title | Undecidability of the Emptiness Problem for Weak Models of Distributed Computing |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2504.07339 |