流言逻辑中的未决问题
Open Problems in a Logic of Gossips
摘要:
流言协议是在每个代理持有秘密的设置中使用的程序,目的是达到所有代理都知道所有秘密的情况。这种协议依赖于点对点或组通信。分布式认知八卦协议使用认知公式的组件程序的代理。使用认知逻辑的优点是,由此产生的协议是非常简洁的,易于进行简单的验证。最近,我们引入了一个自然模态逻辑,它允许人们表达分布式的认知八卦协议,并对它们的正确性进行推理。我们证明了由此产生的协议是可实现的,其正确性的各个方面,包括终止,是可判定的。为了建立这些结果,我们证明了语义的定义和底层逻辑的真值都是可判定的。我们还表明,类似的结果保持了这个逻辑与“常识”的运营商的扩展。然而,关于这种逻辑和相应的八卦协议的几个问题(通常看似简单)仍然是开放的。本文的目的是列出和阐明这些问题,并以部分相关结果的形式为它们提供适当的背景信息。
英文摘要:
Gossip protocols are programs used in a setting in which each agent holds a secret and the aim is to reach a situation in which all agents know all secrets. Such protocols rely on a point-to-point or group communication. Distributed epistemic gossip protocols use epistemic formulas in the component programs for the agents. The advantage of the use of epistemic logic is that the resulting protocols are very concise and amenable for a simple verification. Recently, we introduced a natural modal logic that allows one to express distributed epistemic gossip protocols and to reason about their correctness. We proved that the resulting protocols are implementable and that all aspects of their correctness, including termination, are decidable. To establish these results we showed that both the definition of semantics and of truth of the underlying logic are decidable. We also showed that the analogous results hold for an extension of this logic with the 'common knowledge' operator. However, several, often deceptively simple, questions about this logic and the corresponding gossip protocols remain open. The purpose of this paper is to list and elucidate these questions and provide for them an appropriate background information in the form of partial of related results.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。