Wanted Dead or Alive : Epistemic logic for impure simplicial complexes

TL;DR

This paper develops a modal logic of knowledge tailored for impure simplicial complexes, modeling distributed systems with uncertain process activity, extending pure complexes logic by incorporating undefined states and dead processes.

Contribution

It introduces a three-valued semantics and an S5-based axiomatization for knowledge in impure complexes, generalizing prior pure complexes logic to more realistic distributed systems.

Findings

Semantics incorporate undefined states for dead processes.

Logic models knowledge limitations due to process failures.

Extension of pure complexes logic to impure cases.

Abstract

We propose a logic of knowledge for impure simplicial complexes. Impure simplicial complexes represent synchronous distributed systems under uncertainty over which processes are still active (are alive) and which processes have failed or crashed (are dead). Our work generalizes the logic of knowledge for pure simplicial complexes, where all processes are alive, by Goubault et al. In our semantics, given a designated face in a complex, a formula can only be true or false there if it is defined. The following are undefined: dead processes cannot know or be ignorant of any proposition, and live processes cannot know or be ignorant of factual propositions involving processes they know to be dead. The semantics are therefore three-valued, with undefined as the third value. We propose an axiomatization that is a version of the modal logic S5. We also show that impure simplicial complexes correspond to certain Kripke models where agents' accessibility relations are equivalence relations on a subset of the domain only. This work extends a WoLLIC 21 conference publication with the same title.