论文标题
不纯净的简单复合物：完整的公理化
Impure Simplicial Complexes: Complete Axiomatization
论文作者
论文摘要
组合拓扑用于分布式计算，以建模并发和异步。组合拓扑结构的基本结构是Simplecial Complex，这是一组称为一组顶点的简单的子集集合，在封装下封闭。纯净的简单复合物描述了在所有过程（代理）都活着的异步系统中传递的消息，而不纯净的简单复合物描述了传递的消息传递在同步系统中，这些系统可能已经死亡（已崩溃）。不纯净的简单复合物的性质可以在三值多机构认知逻辑中描述，其中第三个值代表未定义的公式，例如，死者的知识和局部命题。在这项工作中，我们为不纯净的复合物类别的逻辑介绍了一个公理化，并显示出健全和完整性。完整性证明涉及规范简单模型的新建，并且需要仔细操纵未定义的公式。
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.
