Verifying maze-like game levels with model checker SPIN

Download

qq-combined.pdf

Date

2021-11-5

Author

Tekik, Onur

Metadata

Show full item record

This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

Item Usage Stats

344
views

98
downloads

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.

Subject Keywords

Procedural content generation, Model checking, Formal verification, Video game description language, Puzzle games

URI

https://hdl.handle.net/11511/94575

Collections

Graduate School of Informatics, Thesis

Suggestions

OpenMETU
Core

Enhancing the Monte Carlo Tree Search Algorithm for Video Game Testing Arıyürek, Sinan; Betin Can, Aysu; Sürer, Elif (2020-03-01) In this paper, we study the effects of several Monte Carlo Tree Search (MCTS) modifications for video game testing. Although MCTS modifications are highly studied in game playing, their impacts on finding bugs are blank. We focused on bug finding in our previous study where we introduced synthetic and human-like test goals and we used these test goals in Sarsa and MCTS agents to find bugs. In this study, we extend the MCTS agent with several modifications for game testing purposes. Furthermore, we present a...
Theory of Action Phases in Video Games: Effects of Deliberative and Implemental Mindset Differences in Video Game Design Kosa, Mehmet (2016-10-19) This paper describes the studies I have undertaken so far and states the next steps for my PhD. After a brief introduction, I state the motivation for the study. Then, the application of a well-established theory in psychology domain on a video game is articulated. The theory is "Theory of Action Phases" and it simply claims that people happen to be in deliberative mindset while selecting goals and in implemental mindset while pursuing them. In order to test the theory in the gaming domain, a lab experiment...
Verifying Maze-Like Game Levels With Model Checker SPIN Tekik, Onur; Sürer, Elif; Betin Can, Aysu (2022-06-01) 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-...
Electromagnetic modeling of split-ring resonators Gurel, Levent; Unal, Alper; Ergül, Özgür Salih (2006-09-15) In this paper, we report our efforts to model split-ring resonators (SRRs) and their large arrays accurately and efficiently in a sophisticated simulation environment based on recent advances in the computational electromagnetics. The resulting linear system obtained from the simultaneous discretization of the geometry and Maxwell's equations is solved iteratively with the multilevel fast multipole algorithm. As an example, we present an array of 125 SRRs showing a negative effective permeability about 92 GHz.
Machine learning methods for opponent modeling in games of imperfect information Şirin, Volkan; Yarman Vural, Fatoş Tunay; Department of Computer Engineering (2012) This thesis presents a machine learning approach to the problem of opponent modeling in games of imperfect information. The efficiency of various artificial intelligence techniques are investigated in this domain. A sequential game is called imperfect information game if players do not have all the information about the current state of the game. A very popular example is the Texas Holdem Poker, which is used for realization of the suggested methods in this thesis. Opponent modeling is the system that enabl...

Citation Formats

O. Tekik, “Verifying maze-like game levels with model checker SPIN,” M.S. - Master of Science, Middle East Technical University, 2021.