【作者】 何青； 骆翔宇； 苏开乐；

【机构】 中山大学计算机科学系；

【摘要】 <正>1 引言在对弈问题的研究中,人们一直都在探询这样的问题:对弈中的某一方是否存在必胜策略,也就是说无论对手如何行棋,该方是否总是能够战胜对手。从搜索技术的角度来看,这将需要对棋局的状态空间进行穷举搜索,因此启发式搜索技术无法很好地解决这个问题。然而从形式化方法的角度来看,这个问题可归结为棋局模型中的形式化验证问题,即更多还原

【Abstract】 In the two-player zero-sum games, verifying whether there exists winning strategies has not been solved properly, since it refers to the exhaust searches of the finite state space. With the development of symbolic model checking, however, verifying large systems becomes possible. In this paper, we present a common method for verifying the winning strategies of games with symbolic model checking, and give a case study for Tic-Tac-Toe using our model checker MCTK.更多还原