Abstract: In the research of two-player zero-sum games，verifying whether there exists winning strategy has not been solved properly，since it refers to the search of the grand scale state space.With the development of the symbolic model checking，however，verifying large systems becomes possible.This paper presents a common method of verifying the winning strategy of games with symbolic model checking，and gives a case study of Tic-Tac-Toe.

摘要： 在对弈的研究中，验证对弈双方是否存在必胜策略的问题一直没能很好地解决，因为这涉及到超大规模的状态空间搜索。而随着符号化模型检测技术的发展，大规模系统的验证成为了可能。给出了使用符号化模型检测来验证对弈必胜策略的一般方法，并给出了一个井字棋必胜策略验证的实例。