Verifying maze-like game levels with model checker SPIN

Tekik, Onur
In this thesis, we present a new methodology that includes procedural generation and verification of maze-like game levels. The methodology employs a model checker, called SPIN, to both produce a winning sequence of actions and to formally verify custom game design properties. To verify a game level, we propose automated tailoring on template game models, considering the level-in-test, specifically designed according to the game rules. By leveraging the counterexample generation feature of SPIN, we find one or more solutions to the level-in-test and use PyVGDL to animate the solutions. To show this methodology’s effectiveness, we conducted five different experiments. These experiments include performance comparisons in level solving between the proposed and existing methodologies —A* Search and Monte Carlo Tree Search—and demonstrations of the proposed approach’s usage to verify a game level with respect to existing requirements. The work also includes a pipeline for the generation of maze-like puzzle levels that includes two levels of cellular automata.
Citation Formats
O. Tekik, “Verifying maze-like game levels with model checker SPIN,” M.S. - Master of Science, Middle East Technical University, 2021.