Verifying Maze-Like Game Levels With Model Checker SPIN

Tekik O., Surer E., Can A. B.

IEEE Access, vol.10, pp.66492-66510, 2022 (Peer-Reviewed Journal) identifier identifier

  • Publication Type: Article / Article
  • Volume: 10
  • Publication Date: 2022
  • Doi Number: 10.1109/access.2022.3185109
  • Journal Name: IEEE Access
  • Journal Indexes: Science Citation Index Expanded, Scopus, Compendex, INSPEC, Directory of Open Access Journals
  • Page Numbers: pp.66492-66510
  • Keywords: Games, Automata, Behavioral sciences, Model checking, Pipelines, Computational modeling, Visualization, Formal verification, model checking, procedural content generation, puzzle games, video game description language


© 2013 IEEE.This study presents a framework that procedurally generates maze-like levels and leverages an automated verification technique called model checking to verify and produce a winning action sequence for that level. By leveraging the counterexample generation feature of the SPIN model checker, one or more solutions to the level-in-test are found, and the solutions are animated using a video game description language, PyVGDL. The framework contains four behavioral templates developed to model the logic of maze-like puzzle games in the modeling language of SPIN. These models automatically are tailored according to the level-in-test. To show the proposed 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 use of the proposed approach to check a game level with respect to requirements. This study also proposes a pipeline to generate maze-like puzzle levels with two levels of cellular automata.