학술논문
Verifying Maze-Like Game Levels With Model Checker SPIN
Document Type
Periodical
Author
Source
IEEE Access Access, IEEE. 10:66492-66510 2022
Subject
Language
ISSN
2169-3536
Abstract
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.