System Reduction Based on Symmetry in Game Model Checking

Abstract

In the research of two-player games, verifying whether there exists winning strategy is a major problem of game theory. Based on the high efficiency of symbol model checking, model checking can be applied to game verification. However, some games like game of Go have large state space, so reduction of system model is a key issue to improve the scale and efficiency of verification. This paper presents a method of reducing system model of Alternating-time Temporal Logic (ATL) model checking based on symmetry and gives two experiments on tic-tac-toe and go in small board.