In recent years, several authors have been investigating simplicial models, a model of epistemic logic based on higher-dimensional structures called simplicial complexes. In the original formulation, simplicial models were always assumed to be pure, meaning that all worlds have the same dimension. This is equivalent to the standard S5n semantics of epistemic logic, based on Kripke models. By removing the assumption that models must be pure, we can go beyond the usual Kripke semantics and study epistemic logics where the number of agents participating in a world can vary. This approach has been developed in a number of papers, with applications in fault-tolerant distributed computing where processes may crash during the execution of a system. A difficulty that arises is that subtle design choices in the definition of impure simplicial models can result in different axioms of the resulting logic. In this paper, we classify those design choices systematically, and axiomatize the corresponding logics. We illustrate them via distributed computing examples of synchronous systems where processes may crash.
翻译:近年来,多位学者致力于研究一种基于高维结构——单纯复形的认知逻辑模型,即单纯模型。在原始表述中,单纯模型通常被假定为纯粹的,即所有世界具有相同维度。这等价于基于克里普克模型的标准认知逻辑S5n语义。通过移除模型必须纯粹的假设,我们可以超越传统克里普克语义,研究参与同一世界的主体数量可变的认知逻辑体系。该思路在多篇论文中得以发展,并应用于容错分布式计算领域——系统执行过程中进程可能崩溃的场景。由此产生的挑战在于,非纯粹单纯模型定义中的细微设计差异会导致不同逻辑公理体系的产生。本文系统化地分类了这些设计选择,并对相应的逻辑体系进行了公理化。我们通过同步系统中进程可能崩溃的分布式计算实例进行了具体阐释。