A dynamic epistemic logic analysis of equality negation and other epistemic covering tasks (Q2043796)

The authors study the solvability of the equality negation task in a simple wait-free model where two processes communicate by reading and writing shared variables or exchanging messages. In this task, the 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; the goal here is to prove this result using the dynamic epistemic logic (DEL) approach introduced by \textit{É. Goubault} et al. [Electron. Proc. Theor. Comput. Sci. (EPTCS) 277, 73--87 (2018; Zbl 1498.03045)]. The authors show that, in fact, there is no epistemic logic formula that explains why the task is unsolvable. Furthermore, they observe that this task is a particular case of an epistemic covering task. They thus establish a connection between the existing DEL framework and the theory of covering spaces in topology, and prove that the same result holds for any epistemic covering task: no epistemic formula explains the unsolvability.