| The importance of game design and the ability of the computer to respond quickly to the moves made by the player are accepted by the scientific communities as well-known problems. In recent years, many techniques have been employed for game design. Programs have been written in various languages such as C, C++, and JAVA. Although these programs are very satisfactory in terms of accuracy of the results, speed is a factor that can definitely be worked on.;SMV permits automatic verification of programs written in a specialized language for describing concurrent finite state systems and protocols. It builds OBDDs (Ordered Binary Decision Diagrams) and makes calculations based on it. Hence, it is very fast in generating the output.;Key words: SMV, OBDD;In our approach to game design, we employed "Model Checking" techniques. Model Checking is the process of checking whether the given model follows certain specifications. We use the Model Checking approach to design and implement four games: "Missionares and Cannibals Problem," "Bridge-Crossing Problem," "Theseus and the Minotaur Problem," and "Theseus and the Minotaur---Chess Style." Among the games, the "Theseus and the Minotaur---Chess Style" game is new following Dr. Quoc-Nam Tran's ideas. The "Theseus and the Minotaur---Chess Style" game is an interactive puzzle game. It is the type of game Dr. Kwon (Kwon 2006) suggests as an open problem. The interface of the game is built using C and OpenGL. As the player (Theseus) moves around the maze, the computer (Minotaur) tries to either capture the Theseus or block the exit(s). The Minotaur invokes the SMV (Symbolic Model Verifier) program to respond to the Theseus' moves. |
