Verifying Maze-Like Game Levels With Model Checker SPIN

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

IEEE Access, cilt.10, ss.66492-66510, 2022 (SCI-Expanded) identifier identifier

  • Yayın Türü: Makale / Tam Makale
  • Cilt numarası: 10
  • Basım Tarihi: 2022
  • Doi Numarası: 10.1109/access.2022.3185109
  • Dergi Adı: IEEE Access
  • Derginin Tarandığı İndeksler: Science Citation Index Expanded (SCI-EXPANDED), Scopus, Compendex, INSPEC, Directory of Open Access Journals
  • Sayfa Sayıları: ss.66492-66510
  • Anahtar Kelimeler: Games, Automata, Behavioral sciences, Model checking, Pipelines, Computational modeling, Visualization, Formal verification, model checking, procedural content generation, puzzle games, video game description language
  • Orta Doğu Teknik Üniversitesi Adresli: Evet

Özet

© 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.