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

van Ditmarsch, Hans and Goubault, Éric and Lazić, Marijana and Ledent, Jérémy and Rajsbaum, Sergio (2021) A dynamic epistemic logic analysis of equality negation and other epistemic covering tasks. Journal of Logical and Algebraic Methods in Programming, 121. 100662. ISSN 2352-2216 (https://doi.org/10.1016/j.jlamp.2021.100662)

[thumbnail of vanDitmarsch-etal-JLAMP-2021-A-dynamic-epistemic-logic-analysis-of-equality-negation]
Preview
 Text. Filename: vanDitmarsch_etal_JLAMP_2021_A_dynamic_epistemic_logic_analysis_of_equality_negation.pdf
Accepted Author Manuscript
License: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 logo
Download (411kB)| Preview

Abstract

In this paper we 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; our goal here is to prove this result using the dynamic epistemic logic (DEL) approach introduced by Goubault et al. (2018) [18]. We show that in fact, there is no epistemic logic formula that explains why the task is unsolvable. Furthermore, we observe that this task is a particular case of an epistemic covering task. We 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.

ORCID iDs

van Ditmarsch, Hans, Goubault, Éric, Lazić, Marijana, Ledent, Jérémy ORCID logoORCID: https://orcid.org/0000-0001-7375-4725 and Rajsbaum, Sergio;
CORE (COnnecting REpositories)