Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Undecidability of the Emptiness Problem for Weak Models of Distributed Computing

Flavio T. Principato, Javier Esparza, Philipp Czerner

TL;DR

The paper investigates the emptiness problem for seven equivalence classes of distributed automata in weak distributed computing, proving undecidability for all but the daf class. It achieves this via a halting-on-blank-tape reduction: for any TM T, it constructs automata in the relevant classes whose languages intersect to reflect T's halting behavior, exploiting the fact that L(A^T) = L(A^L) ∩ L(A^H). The authors establish closure of distributed automata under intersection, enabling A^T = A^L ∩ A^H and allowing the non-da classes to encode arbitrary finite tape segments through carefully designed graph families. They introduce two tape-representation graph families—Numbered Linear Graphs (NLGs) and Numbered Quasi-Linear Graphs (NQLGs)—to accommodate the expressive power of stronger and weaker classes, respectively, and show how these constructions yield the main undecidability results, with the daf class remaining trivially decidable. Overall, the work delineates the boundary between decidable and undecidable emptiness in weak distributed automata and provides structural graph-encoding techniques to realize TM-simulation within this framework.

Abstract

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.

Undecidability of the Emptiness Problem for Weak Models of Distributed Computing

TL;DR

The paper investigates the emptiness problem for seven equivalence classes of distributed automata in weak distributed computing, proving undecidability for all but the daf class. It achieves this via a halting-on-blank-tape reduction: for any TM T, it constructs automata in the relevant classes whose languages intersect to reflect T's halting behavior, exploiting the fact that L(A^T) = L(A^L) ∩ L(A^H). The authors establish closure of distributed automata under intersection, enabling A^T = A^L ∩ A^H and allowing the non-da classes to encode arbitrary finite tape segments through carefully designed graph families. They introduce two tape-representation graph families—Numbered Linear Graphs (NLGs) and Numbered Quasi-Linear Graphs (NQLGs)—to accommodate the expressive power of stronger and weaker classes, respectively, and show how these constructions yield the main undecidability results, with the daf class remaining trivially decidable. Overall, the work delineates the boundary between decidable and undecidable emptiness in weak distributed automata and provides structural graph-encoding techniques to realize TM-simulation within this framework.

Abstract

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.

Paper Structure

This paper contains 9 sections, 5 theorems, 3 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Distributed Machines
  4. Distributed Automata
  5. Classes of Distributed Automata
  6. Simulating Turing Machines with Distributed Automata
  7. Representing the Tape
  8. Simulating the Head
  9. Weakly Representing the Tape

Key Result

Proposition 1

For all $xy \in \{\mathtt{d},\mathtt{D}\}\{\mathtt{a},\mathtt{A}\}$, the classes $xy\mathtt{f}$ and $xy\texttt{\$}\mathtt{f}$ have the same expressive power. Moreover, given a distributed automaton in one of the classes, one can effectively construct an equivalent automaton in the other class.

Figures (3)

  • Figure 1: The hierarchy of expressive power of classes of distributed automata as proven in classification --- The arrows indicate strictly increasing expressive power.
  • Figure 2: A numbered linear graph of length $7$.
  • Figure 3: A numbered quasi-linear graph of length $5$.

Theorems & Definitions (6)

  • Proposition 1: classification
  • Theorem 2: Undecidability of the Emptiness Problem for Distributed Automata
  • Lemma 2: Closure under Intersection
  • Lemma 2: Decidability of Numbered Linear Graphs
  • Lemma 2: Simulating the Head
  • Definition 3: Numbered Quasi-Linear Graphs