Verification of multi-Agent systems with imperfect information and public actions

We analyse the verification problem for synchronous, perfect recall multi-Agent systems with imperfect information against a specification language that includes strategic and epistemic operators. While the verification problem is unde- cidable, we show that if the agents' actions are public, then verification is 2EXPTiME-complete. To illustrate the formal framework we consider two epistemic and strategic puzzles with imperfect information and public actions: The muddy children puzzle and the classic game of battleships.