Formal verification for winning strategy of chess game

This paper presents a formal method to verify the winning strategy in a chess game by means of symbolic model checking, and demonstrate the winning strategy in tic-tac-toe game through the symbolic model checking tool NuSMV improved with the verification algorithm for winning strategy.