The logical method proposed by Goubault, Ledent, and Rajsbaum provides a novel way to show the unsolvability of distributed tasks by means of a logical obstruction, which is an epistemic logic formula describing the reason of unsolvability. In this paper, we introduce the notion of partial product update, which refines that of product update in the original logical method, to encompass distributed tasks and protocols modeled by impure simplicial complexes. With this extended notion of partial product update, the original logical method is generalized so that it allows the application of logical obstruction to show unsolvability results in a distributed environment where the failure of agents is detectable. We demonstrate the use of the logical method by giving a concrete logical obstruction and showing that the consensus task is unsolvable by the single-round synchronous message-passing protocol.

翻译：Goubault、Ledent和Rajsbaum提出的逻辑方法通过逻辑阻碍——一种描述不可解性原因的知识逻辑公式——为展示分布式任务的不可解性提供了新途径。本文引入部分乘积更新的概念，对原始逻辑方法中的乘积更新进行精细刻画，以涵盖由非单纯复形建模的分布式任务及协议。借助这一扩展的部分乘积更新概念，原始逻辑方法得以推广，使其能够运用逻辑阻碍来展示在智能体故障可检测的分布式环境中的不可解性结果。我们通过给出具体的逻辑阻碍，并证明共识任务在单轮同步消息传递协议下不可解，展示了该逻辑方法的应用。