Epistemic GDL: A logic for representing and reasoning about imperfect information games

This paper proposes a logical framework for representing and reasoning about imperfect information games. We first extend Game Description Language (GDL) with the standard epistemic operators and provide it with a semantics based on the epistemic state transition model. We then demonstrate how to use the language to represent the rules of an imperfect information game and formalize common game properties as well as epistemic properties. We also show how to use the framework to reason about players' own and each others' knowledge during game playing. Furthermore, we prove that the model-checking problem of the framework is in Δ2P, even though its lower bound is Θ2P. These results indicate that the framework makes a good balance between expressive power and computational efficiency. Finally we provide a sound and complete axiomatic system for this logic. With action, temporal and epistemic operators, the completeness proof requires a novel combination of techniques used for completeness of dynamic logic and epistemic temporal logics. The proof theory provides a feasible tool to analyze properties of a family of games.