Impure Simplicial Complexes: Complete Axiomatization
Rojo Randrianomentsoa, Hans van Ditmarsch, Roman Kuznets
TL;DR
This work delivers a complete axiomatization, $\mathsf{S5}^{ \bowtie }$, for a three-valued epistemic logic interpreted on impure simplicial complexes that model crash-prone distributed systems. It advances the field by introducing a canonical simplicial model built from definability-maximal consistent sets and proving soundness and completeness, addressing undefined knowledge for dead agents. The approach clarifies how dead or alive statuses alter standard modal reasoning, including non-normal aspects and revised axioms such as $\mathbf{K}^{\bowtie}$ and $\mathbf{K\widehat{K}}$, thereby enabling rigorous epistemic analysis in synchronous/crash scenarios. The results provide a robust theoretical basis for extending epistemic semantics in distributed computing, with potential generalizations to distributed knowledge and simplicial sets.
Abstract
Combinatorial topology is used in distributed computing to model concurrency and asynchrony. The basic structure in combinatorial topology is the simplicial complex, a collection of subsets called simplices of a set of vertices, closed under containment. Pure simplicial complexes describe message passing in asynchronous systems where all processes (agents) are alive, whereas impure simplicial complexes describe message passing in synchronous systems where processes may be dead (have crashed). Properties of impure simplicial complexes can be described in a three-valued multi-agent epistemic logic where the third value represents formulae that are undefined, e.g., the knowledge and local propositions of dead agents. In this work we present an axiomatization for the logic of the class of impure complexes and show soundness and completeness. The completeness proof involves the novel construction of the canonical simplicial model and requires a careful manipulation of undefined formulae.