Logical Obstruction to Set Agreement Tasks for Superset-Closed Adversaries

TL;DR

This paper advances the logical framework for proving the impossibility of distributed set agreement tasks by developing formulas for superset-closed adversaries, extending previous work and offering a simpler proof method than topological approaches.

Contribution

It refines Nishida's logical obstruction formulas to $k$-set agreement for a broader class of adversaries, demonstrating the framework's applicability beyond wait-free models.

Findings

Logical obstruction formulas are constructed for $k$-set agreement with superset-closed adversaries.

The logical method provides a simpler, inductive proof compared to topological techniques.

The approach is currently limited to one-round distributed protocols.

Abstract

In their recent paper (GandALF 2018), Goubault, Ledent, and Rajsbaum provided a formal epistemic model for distributed computing. Their logical model, as an alternative to the well-studied topological model, provides an attractive framework for refuting the solvability of a given distributed task by means of logical obstruction: One just needs to devise a formula, in the formal language of epistemic logic, that describes a discrepancy between the model of computation and that of the task. However, few instances of logical obstruction were presented in their paper and specifically logical obstruction to the wait-free 2-set agreement task was left as an open problem. Soon later, Nishida affirmatively answered to the problem by providing inductively defined logical obstruction formulas to the wait-free $k$-set agreement tasks. The present paper refines Nishida's work and devises logical obstruction formulas to $k$-set agreement tasks for superset-closed adversaries, which supersede the wait-free model. These instances of logical obstruction formulas exemplify that the logical framework can provide yet another feasible method for showing impossibility of distributed tasks, though it is currently being confined to one-round distributed protocols. The logical method has an advantage over the topological method that it enjoys a self-contained, elementary induction proof. This is in contrast to topological methods, in which sophisticated topological tools, such as Nerve lemma, are often assumed as granted.