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) {\em know}, how their knowledge {\em changes} due to {\em observations}, and how they affect the state of the world by {\em 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 {\em local}, i.e.\ not publicly observable, and part of the problem is therefore how to disseminate local results to other agents, and make them {\em global}. The various solutions to the puzzle are presented as protocols (iterated functions from agent's local states, and histories of actions, to actions)
Additional Metadata
Keywords dynamic epistemic logic, distributed systems, communication protocols
THEME Software (theme 1)
Publisher Hermes Science Publications
Journal Journal of Applied Non Classical Logics
Note accepted for publication; to appear in 2011
Citation
van Eijck, D.J.N, van Ditmarsch, H, & Wu, W. (2011). Verifying one hundred prisoners and a lightbulb . Journal of Applied Non Classical Logics.