Abstract

We propose a logic of knowledge for impure simplicial complexes. Impure simplicial complexes represent distributed systems under uncertainty over which processes are still active and which processes have failed or crashed. Our work generalizes the logic of knowledge for pure simplicial complexes, where all processes are alive, by Goubault et al. Our logical semantics has a satisfaction relation defined simultaneously with a definability relation. The latter restricts which formulas are allowed to have a truth value: dead processes cannot know or be uncertain about any proposition, and live processes cannot know or be uncertain about propositions involving processes they know to be dead. The logic satisfies some but not all axioms and rules of the modal logic S5. Impure simplicial complexes correspond to Kripke models where each agent’s accessibility relation is an equivalence relation on a subset of the domain only. We also propose a notion of bisimulation for impure simplicial complexes and show bisimulation correspondence.