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语义。通过取消模型必须为纯的假设,我们可以超越传统的克里普克语义,研究参与某个世界的智能体数量可变的认知逻辑。这种研究思路已在多篇论文中得到发展,并应用于容错分布式计算领域——在该领域中,进程可能在系统执行过程中崩溃。由此产生的一个难点在于,非纯单纯模型定义中的细微设计选择会导致所导出逻辑的公理不同。本文系统地分类了这些设计选择,并公理化了相应的逻辑体系。我们通过同步系统的分布式计算实例(其中进程可能崩溃)对上述研究进行了阐释。