General Game Playing (GGP) is the field of Artificial Intelligence (AI) that investigates generalized techniques for finding winning strategies in games. GGP agents are expected to be able to play a game with no prior knowledge by receiving the game shortly before starting to play. Games with perfect information, such as Tic-Tac-Toe, Chess and Go, can be described in the Game Description Language (GDL), and games with chance and hidden information such as Backgammon and Poker, can be describe in Game Description Language for Incomplete Information (GDL-II), an extension of GDL.

This thesis is mainly concerned with the verification of games in GDL and GDL-II. Games described in these languages may contain bugs, just like the bugs in a program written in C or Java language. E.g., a game may never terminate or a player has a legal move but does not know it. In order to allow GGP agents play games properly, the games need to satisfy a set of {well-formedness} properties. In GDL the properties are Termination, Playability and Winnability and in GDL-II there is also the requirement that agents have sufficient knowledge to derive these properties. Our approach is to utilise model checking, which is a well-known method to check if a program is free from design errors, i.e., satisfying a set of formal properties. We build on an earlier work in verifying games in GDL-II by systematically translating the game descriptions into a system description model and the well-formedness properties of games into a logical language, then feeding them to the model checking program named Model Checking Knowledge (MCK). We refine the existing translation techniques to automatically generate a MCK System Model from an arbitrary game in GDL-II and verify if they satisfy the desirable properties. Our automated translation takes significantly less time to generate models but falls short in efficiency compared with a manual translation. We explore the ways to do further optimisation to increase the efficiency.