A dynamic epistemic logic analysis of the equality negation task

TL;DR

This paper uses an extended dynamic epistemic logic framework to analyze the unsolvability of the equality negation task in wait-free distributed systems, providing a formal logical explanation for its impossibility.

Contribution

It introduces an extension to the DEL framework enabling the construction of a formula that explains the task's unsolvability, advancing formal methods in distributed computing.

Findings

The equality negation task is proven unsolvable in the given model.

An extension to the DEL framework allows for formal explanation of task impossibility.

The extended logic can construct formulas that explain why certain distributed tasks are unsolvable.

Abstract

In this paper we study the solvability of the equality negation task in a simple wait-free model where processes communicate by reading and writing shared variables or exchanging messages. In this task, two processes start with a private input value in the set {0,1,2}, and after communicating, each one must decide a binary output value, so that the outputs of the processes are the same if and only if the input values of the processes are different. This task is already known to be unsolvable; our goal here is to prove this result using the dynamic epistemic logic (DEL) approach introduced by Goubault, Ledent and Rajsbaum in GandALF 2018. We show that in fact, there is no epistemic logic formula that explains why the task is unsolvable. We fix this issue by extending the language of our DEL framework, which allows us to construct such a formula, and discuss its utility.