• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of applied non-classical logics >Verifying one hundred prisoners and a lightbulb
【24h】

Verifying one hundred prisoners and a lightbulb

机译：验证一百名囚犯和一个灯泡

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

This is a case-study in knowledge representation and dynamic epistemic protocol verification. We analyze the 'one hundred prisoners and a lightbulb' puzzle. In this puzzle it is relevant what the agents (prisoners) know, how their knowledge changes due to observations, and how they affect the state of the world by changing facts, i.e., by their actions. These actions depend on the history of previous actions and observations. Part of its interest is that all actions are local, i.e. not publicly observable, and part of the problem is therefore how to disseminate local results to other agents, and make them global. The various solutions to the puzzle are presented as protocols (iterated functions from agent's local states, and histories of actions, to actions). The paper consists of three parts. First, we present different versions of the puzzle, and their solutions. This includes a probabilistic version, and a version assuming synchronicity (the interval between prisoners' interrogations is known). The latter is very informative for the prisoners, and allows different protocols (with faster expected termination). Then, we model the puzzle in an epistemic logic incorporating dynamic operators for the effects of information changing events. Such events include both informative actions, where agents become more informed about the non-changing state of the world, and factual changes, wherein the world and the facts describing it change themselves as well. Finally, we verify the basic protocol to solve the problem. Novel contributions in this paper are: Firstly, Protocol 2 and Protocol 4. Secondly, the modelling in dynamic epistemic logic in its entirety — we do not know of a case study that combines factual and informational dynamics in a setting of non-public events, or of a similar proposal to handle asynchronous behaviour in a dynamic epistemic logic. Thirdly, our method to verify dynamic epistemic protocols by reasoning over possibly infinite execution sequences of these protocols. A precursor of the present paper, entitled 'One hundred prisoners and a lightbulb - logic and computation' (van Ditmarsch et ai, 2010), was presented at KR 2010, Toronto. The differences with the present contribution are as follows: the former contains a section with computational results (expected runtime of different protocols before termination), whereas the focus of the present paper is the verification of one of the presented protocols in the former.
机译：这是关于知识表示和动态认知协议验证的案例研究。我们分析了“一百名囚犯和一个灯泡”难题。在这个难题中，与代理人（囚犯）所知道的有关，他们的知识如何由于观察而改变，以及他们如何通过改变事实（即通过他们的行动）来影响世界状况。这些动作取决于先前动作和观察的历史。它的部分兴趣是所有动作都是本地的，即不是公开可观察到的，因此，部分问题是如何将本地结果传播给其他主体，并使它们全球化。难题的各种解决方案以协议（从代理的本地状态，动作历史到动作历史的迭代功能）的形式表示。本文由三部分组成。首先，我们介绍了不同版本的拼图及其解决方案。这包括一个概率版本和一个假定同步的版本（囚犯审问之间的间隔是已知的）。后者对囚犯很有帮助，并且允许使用不同的协议（预期更快的终止）。然后，我们在认知逻辑中对难题进行建模，该逻辑结合了动态运算符以应对信息更改事件的影响。这样的事件既包括提供信息的动作（事实使主体更了解世界的不变状态），也包括事实的变化（事实和描述世界的事实也随之改变）。最后，我们验证了解决此问题的基本协议。本文的新颖贡献包括：首先是协议2和协议4。其次，是动态认知逻辑的整体建模-我们不知道在非公开事件中结合了事实和信息动态的案例研究，或在动态认知逻辑中处理异步行为的类似建议。第三，我们通过对这些协议的可能无限执行序列进行推理来验证动态认知协议的方法。本论文的前驱题为“一百名囚犯和一个灯泡-逻辑与计算”（van Ditmarsch等，2010），在多伦多的KR 2010上发表。与本贡献的区别如下：前者包含一个具有计算结果的部分（终止之前不同协议的预期运行时间），而本文的重点是对前一种协议的验证。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号