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提出的逻辑方法通过逻辑障碍（一种描述不可解性原因的认知逻辑公式）提供了一种展示分布式任务不可解性的新颖途径。本文引入部分乘积更新的概念——该概念是对原始逻辑方法中乘积更新的精炼——以涵盖由非纯单纯复形建模的分布式任务与协议。凭借这一扩展的部分乘积更新概念，原始逻辑方法得以泛化，从而允许应用逻辑障碍在智能体故障可检测的分布式环境中展示不可解性结果。我们通过给出具体的逻辑障碍，并证明单轮同步消息传递协议下共识任务的不可解性，演示了该逻辑方法的应用。