Determining Existence of Logical Obstructions to the Distributed Task Solvability

TL;DR

This paper develops a systematic method to determine the existence of logical obstructions in distributed task solvability, providing tools to construct or prove their non-existence, with applications to specific tasks like k-set agreement.

Contribution

It introduces a simulation-based approach to decide whether logical obstructions exist for finite distributed tasks and protocols, and constructs explicit obstructions when they do.

Findings

Logical obstructions do not exist for certain tasks in standard epistemic logic.

No logical obstruction exists for multi-round immediate snapshot in the same logic.

Concrete obstructions are constructed for the know-all model and k-set agreement tasks.

Abstract

To study the distributed task solvability, Goubault, Ledent, and Rajsbaum devised a model of dynamic epistemic logic that is equivalent to the topological model for distributed computing. In the logical model, the unsolvability of a particular distributed task can be proven by finding a formula, called logical obstruction. This logical method is very appealing because the concrete formulas that prevent to solve task would have implications of intuitive factors for the unsolvability. However, it has not been well studied when a logical obstruction exists and how to systematically construct a concrete logical obstruction formula, if any. In addition, it is proved that there are some tasks that are solvable but do not admit logical obstructions. In this paper, we propose a method to prove the non-existence of logical obstructions to the solvability of distributed tasks, based on the technique of simulation. Moreover, we give a method to determine whether a logical obstruction exists or not for a finite protocol and a finite task, and if it exists, construct a concrete obstruction. Using this method, we demonstrate that the language of the standard epistemic logic, without distributed knowledge, does not admit logical obstruction to the solvability of $k$-set agreement tasks. We also show that there is no logical obstruction for multi-round immediate snapshot even in the language of epistemic logic with distributed knowledge. In addition, for the know-all model, we provide a concrete obstruction formula that shows the unsolvability of the $k$-set agreement task.