Defining logical obstruction with fixpoints in epistemic logic

Abstract

The logical method proposed by Goubault, Ledent, and Rajsbaum provides a means of demonstrating the unsolvability of distributed tasks within the epistemic logic framework. To show that a task is unsolvable, we need to find a logical obstruction, which is an epistemic logic formula describing the reason for the unsolvability, or more precisely, the incompatibility between the task, which is a model of what is to be solved, and the protocol, which is a model of what the distributed system can compute. To date, only a few concrete instances of logical obstructions have been devised. In particular, existing proposals of logical obstruction to the k-set agreement task are unsatisfactory because they work only for the case 𝓀 ＝ 1 or the protocol is restricted to single-round execution. This is because the unsolvability of the k-set agreement task is tied with the higher-dimensional property of the corresponding combinatorial topological model, while the language of epistemic logic has a limited ability to express it. This study proposes the use of an epistemic μ-calculus variant, which extends epistemic logic with distributed knowledge modalities and propositional greatest fixpoints. With these extensions, we can define an epistemic formula whose epistemic content contradicts a property regarding the higher-dimensional connectivity, which is indicated in the proof of Sperner’s lemma. This formula thus works as a logical obstruction, showing that the k-set agreement task is unsolvable by the multiple-round immediate snapshot protocol. Further, we show that the same formula works as a logical obstruction for the k-concurrency, which is a protocol of a limited degree of concurrency.