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 formulas that are undefined, e.g., the knowledge and local propositions of dead agents. In this work we present the axiomatization called $\mathsf{S5}^{\bowtie}$ and show that it is sound and complete for the class of impure complexes. The completeness proof involves the novel construction of the canonical simplicial model and requires a careful manipulation of undefined formulas.

翻译：组合拓扑学被用于分布式计算中对并发性和异步性进行建模。组合拓扑学中的基本结构是单纯复形，它是由顶点集的子集（称为单形）构成的集合，且对包含关系封闭。纯单纯复形描述了异步系统中所有进程（主体）均存活时的消息传递，而不纯单纯复形则描述了同步系统中进程可能死亡（崩溃）时的消息传递。不纯单纯复形的性质可用三值多主体认知逻辑描述，其中第三值表示未定义的公式，例如死亡主体的知识和局部命题。本文提出了名为$\mathsf{S5}^{\bowtie}$的公理化体系，并证明了其对不纯复形类是可靠且完备的。完备性证明涉及规范单纯模型的新颖构造，并要求对未定义公式进行细致处理。