Impure Simplicial Complexes: Complete Axiomatization

Combinatorial topology is used in distributed computing to model concurrencyand asynchrony. The basic structure in combinatorial topology is the simplicialcomplex, a collection of subsets called simplices of a set of vertices, closedunder containment. Pure simplicial complexes describe message passing inasynchronous systems where all processes (agents) are alive, whereas impuresimplicial complexes describe message passing in synchronous systems whereprocesses may be dead (have crashed). Properties of impure simplicial complexescan be described in a three-valued multi-agent epistemic logic where the thirdvalue represents formulae that are undefined, e.g., the knowledge and localpropositions of dead agents. In this work we present an axiomatization for thelogic of the class of impure complexes and show soundness and completeness. Thecompleteness proof involves the novel construction of the canonical simplicialmodel and requires a careful manipulation of undefined formulae