In this paper we provide a first-ever epistemic formulation of stabilizing agreement, defined as the non-terminating variant of the well established consensus problem. In stabilizing agreements, agents are given (possibly different) initial values, with the goal to eventually always decide on the same value. While agents are allowed to change their decisions finitely often, they are required to agree on the same value eventually. We capture these properties in temporal epistemic logic and we use the Runs and Systems framework to formally reason about stabilizing agreement problems. We then epistemically formalize the conditions for solving stabilizing agreement, and identify the knowledge that the agents acquire during any execution to choose a particular value under our system assumptions. This first formalization of a sufficient condition for solving stabilizing agreement sets the stage for a planned necessary and sufficient epistemic characterization of stabilizing agreement.
翻译:本文首次提出了稳定一致性的认知形式化表述,该问题定义为经典共识问题的非终止变体。在稳定一致性问题中,智能体被赋予(可能不同的)初始值,其目标是最终始终达成对同一值的判定。尽管智能体允许有限多次地更改其决策,但必须最终一致地达成相同值。我们在时序认知逻辑中捕捉这些性质,并利用运行与系统框架对稳定一致性问题进行形式化推理。随后,我们以认知方式形式化求解稳定一致性的条件,并识别出在系统假设下,智能体在任何执行过程中为选择特定值所需获取的知识。这种对求解稳定一致性充分条件的首次形式化,为后续计划中稳定一致性的充要认知刻画奠定了基础。