Model-Checking in Hide and Seek Games with Imperfect Information
摘要
We consider a logical framework to express reasoning about actions and strategies in a hide and seek game with imperfect information. In this version of the game, the seeker(s) and the hider move alternately with the seekers moving simultaneously on their turn. A win for the seekers is described in terms of the information they have about the position of the hider. We assume limited observational powers of the players. We provide model-checking algorithms for the proposed framework, and analyze the complexity of those algorithms. We also showcase an implementation of a model-checking tool that can be used for verifying winning strategies in these games.