无论死活:面向非纯单纯复形的认知逻辑
Wanted Dead or Alive : Epistemic logic for impure simplicial complexes
AI总结:
本文针对进程生死不确定的同步分布式系统,提出非纯单纯复形的三值认知逻辑、S5 风格公理化及其与受限 Kripke 模型的对应关系。
摘要:
我们提出了一种面向非纯单纯复形的知识逻辑。非纯单纯复形表示在哪些进程仍处于活动状态(存活)以及哪些进程已经失败或崩溃(死亡)存在不确定性的同步分布式系统。我们的工作推广了 Goubault 等人提出的面向纯单纯复形(其中所有进程均存活)的知识逻辑。在我们的语义中,给定复形中的一个指定面,一个公式只有在该处有定义时才可能为真或为假。以下情况是未定义的:死亡进程不能知道或不知道任何命题,而存活进程不能知道或不知道涉及它们已知已死亡进程的事实命题。因此,该语义是三值的,并以未定义作为第三个值。我们提出了一个公理化,它是模态逻辑 S5 的一个版本。我们还表明,非纯单纯复形对应于某些 Kripke 模型,在这些模型中,智能体的可达性关系仅在论域的一个子集上是等价关系。本工作扩展了一篇同名的 WoLLIC 21 会议论文。
英文摘要:
We propose a logic of knowledge for impure simplicial complexes. Impure simplicial complexes represent synchronous distributed systems under uncertainty over which processes are still active (are alive) and which processes have failed or crashed (are dead). Our work generalizes the logic of knowledge for pure simplicial complexes, where all processes are alive, by Goubault et al. In our semantics, given a designated face in a complex, a formula can only be true or false there if it is defined. The following are undefined: dead processes cannot know or be ignorant of any proposition, and live processes cannot know or be ignorant of factual propositions involving processes they know to be dead. The semantics are therefore three-valued, with undefined as the third value. We propose an axiomatization that is a version of the modal logic S5. We also show that impure simplicial complexes correspond to certain Kripke models where agents' accessibility relations are equivalence relations on a subset of the domain only. This work extends a WoLLIC 21 conference publication with the same title.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。