Research On Game Model Checking Based On Alternating-time Temporal Logic And Its Application In Game Of Go

Model Checking is an automatic validation technique for finite state concurrent systems,which is put forward by American professor Edmund M.Clarke et al.This technique use model checking algorithm based on exhaustive state space search to determine whether a system model satisfies the desired properties.However,state space grows rapidly with the increase of systems,symbolic model checking is put forward to alleviate state space explosion.Whether there is a winning strategy in a zero-sum game is a major area in game theory.Model checking can be applied to the verification of games because of high efficiency of the symbolic technique.Alternating-time temporal logic can be used to describe system properties,so that system model can be verified by symbolic model checking algorithm.However,state space of some games are too large to search.Therefore,more research is needed to expand the search scale.Our group has introduced model checking in the game of Go to search exhaustively in small board.However,the main restriction of model checking in Go is the state space.How to reduce the state space of game model is the main problem.Based on the above backgrounds,the main work of this thesis is as follow:1)We model and analysis the winning strategy of the traditional game tic-tac-toe.The experiment results are consistent with the results of other methods,which show that ATL can be used in the game verification.2)We study the symmetry technique of model checking and use it in game model checking.According to the repeated character of game,we can reduce the state space of the game model with the symmetry technique.3)We reduce the game model of game Go and verify the winning strategy in small board by symbolic model checking algorithm.The experiment results show that model checking in small board is feasible.