Verification of General Games with Imperfect Information Using Strategy Logic

The Game Description Language with Imperfect Information (GDL-II) is a lightweight formalism for representing the rules of arbitrary games, including those where players have private information. Its purpose is to build general game-playing systems, that is, automated players that can understand the rules of games and learn how to play them without human intervention. Epistemic Strategy Logic (SLK), on the other hand, is a rich logical framework for reasoning about multi-agent systems and the strategic behavior of agents with partial observability. To enable a general game-playing system to take advantage of this rich formalism for the automatic verification of properties of games, we present a formal translation from GDL-II to SLK models. We prove the correctness of this translation and show how crucial properties of general games, including playability and the existence of Nash equilibria, can be expressed as formulas in SLK. Finally, we demonstrate the application of an existing model-checking system for SLK to verify the properties of GDL-II games.