完全情報ゲームの必勝戦略の構築は莫大な計算量を必要とする問題である。本論文では、ソフトウェアの性質を検証するために利用されるモデル検査器を用いることで、必勝戦略を発見的に見つけることを目指す。具体的には、どうぶつしょうぎの必勝戦略をモデル検査器を用いて見つけ出すことを実験的に行い、必勝戦略の構築の可能性について調べた。