  We propose a logic of knowledge for impure simplicial complexes. Impure
simplicial complexes represent 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. 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 ignorant of any proposition,
and live processes cannot know or be ignorant of 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, and otherwise empty, and where each propositional
variable is known by an agent. We also propose a notion of bisimulation for
impure simplexes and show bisimulation correspondence on certain finitary
simplexes. % Dynamic aspects of our semantics, such as how to formalize
possibly incomplete tasks and algorithms in distributed computing, is left for
future research.
