| Summary: | 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.
|
|---|