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.
翻译:我們提出了一種針對不純單純複合體的知識邏輯。不純單純複合體表示在存在不確定性的同步分布式系統,其中不確定哪些進程仍然活躍(活著),哪些進程已失敗或崩潰(死亡)。我們的工作推廣了 Goubault 等人提出的純粹單純複合體知識邏輯(其中所有進程都是活著的)。在我們的語義中,給定複合體中的一個指定面,公式只能在定義時才為真或假。以下情況是未定義的:死亡的進程無法知道或無知於任何命題,而活著的進程無法知道或無知於涉及它們已知已死亡的進程的事實命題。因此,語義是三分值的,未定義為第三個值。我們提出了一個公理化系統,它是模態邏輯 S5 的一個版本。我們還表明,不純單純複合體對應於某些克里普克模型,其中主體的可及關係僅在域的子集上是等價關係。這項工作擴展了標題相同的 WoLLIC 21 會議論文。