Verifying epistemic protocols under common knowledge
Verifying epistemic protocols under common knowledge
复制标题
DOI：
10.1145/1562814.1562848
复制
发表时间：
2009-07
期刊：
影响因子：
--
通讯作者：
Yanjing Wang;Lakshmanan Kuppusamy;J. Eijck
中科院分区：
文献类型：
--
作者：
Yanjing Wang;Lakshmanan Kuppusamy;J. Eijck
认知协议是一种旨在以受控方式传递知识的通信协议。通常，协议动作的前提条件或目标取决于代理的知识，通常以嵌套的形式。非正式的认知协议描述泥泞的孩子，协调攻击，用餐密码，俄罗斯卡，秘密密钥交换是众所周知的。本文的贡献是对认知协议的一个自然要求进行了形式化研究，即协议的内容可以假设为公共知识。通过形式化这一要求，我们可以证明，不可能有无偏确定性协议的俄罗斯卡问题。为了我们的形式化分析，我们引入了一个认知协议语言，我们证明了它的模型检测问题是可判定的。
Epistemic protocols are communication protocols aiming at transfer of knowledge in a controlled way. Typically, the preconditions or goals for protocol actions depend on the knowledge of agents, often in nested form. Informal epistemic protocol descriptions for muddy children, coordinated attack, dining cryptographers, Russian cards, secret key exchange are well known. The contribution of this paper is a formal study of a natural requirement on epistemic protocols, that the contents of the protocol can be assumed to be common knowledge. By formalizing this requirement we can prove that there can be no unbiased deterministic protocol for the Russian cards problem. For purposes of our formal analysis we introduce an epistemic protocol language, and we show that its model checking problem is decidable.