Verifying Maze-Like Game Levels With Model Checker SPIN

Date

2022-06-01

Author

Tekik, Onur
Sürer, Elif
Betin Can, Aysu

Metadata

Show full item record

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

Item Usage Stats

162
views

0
downloads

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.

URI

https://ieeexplore.ieee.org/abstract/document/9802094
https://hdl.handle.net/11511/98355

Journal

IEEE ACCESS

DOI

https://doi.org/10.1109/access.2022.3185109

Collections

Graduate School of Informatics, Article

Suggestions

OpenMETU
Core

Optimization of Speed Control Hump Profiles BAŞLAMIŞLI, SELAHATTİN ÇAĞLAR; Ünlüsoy, Yavuz Samim (2009-05-01) In this study, the goal attainment method is implemented for the optimization of speed control hump profiles. Basic dimensions for a number of hump profile functions are optimized for single vehicles classified in five categories and for a specified distribution of these vehicles. Objective functions are selected as combinations of the longitudinal and vertical acceleration components at pre-specified points on the vehicle body. The main objective is to minimize vehicle response functions below the hump cro...
Determination of Rainfall – Runoff Relationship in Yenicegoruce Basin with HEC-HMS Hydrologic Model MESTA, BUKET; KARGI, PINAR GÖKÇE; TEZYAPAR, İPEK; AYVAZ, MUSTAFA TAMER; GÖKTAŞ, RECEP KAYA; Kentel Erdoğan, Elçin; TEZEL, ULAŞ (2019-01-01) The goal of this study is to model rainfall-runoff process using HEC-HMS developed by U.S. Army Corps of Engineers for the 10,508 km2 catchment that has E01A012-Yenicegörüce stream gage at its outlet which is located just at the upstream of the point where Meric and Ergene Rivers meet. This study is conducted as a part of 115Y064 numbered “Development of a geographical information systems based decision-making tool for water quality management of Ergene watershed using pollutant fingerprints” project funded...
Sampling Performance of Multiple Independent Molecular Dynamics Simulations of an RNA Aptamer Yan, Shuting; Peck, Jason M.; İlgü, Müslüm; Nilsen-Hamilton, Marit; Lamm, Monica H. (2020-08-01) Using multiple independent simulations instead of one long simulation has been shown to improve the sampling performance attained with the molecular dynamics (MD) simulation method. However, it is generally not known how long each independent simulation should be, how many independent simulations should be used, or to what extent either of these factors affects the overall sampling performance achieved for a given system. The goal of the present study was to assess the sampling performance of multiple indep...
Application of genetic algorithms to calibration and verification of QUAL2E Göktaş, Recep Kaya; Aksoy, Ayşegül; Department of Environmental Engineering (2004) The objective of this study is to develop a calibration and verification tool for the QUAL2E Model by using Genetic Algorithms. In the developed optimization model, an objective function that is formulated on the basis of the sum-of-least squares approach aiming at minimizing the difference between the observed and simulated quantities was used. In order to perform simultaneous calibration and verification, verification of the calibrated results was treated as a constraint and inserted into the objective fu...
Composition Capability of Component-Oriented Development Kaya, Muhammed Çağrı; Çetinkaya, Anıl; Doğru, Ali Hikmet (2017-10-30) This research enhances component-oriented development approaches with the capability to represent the dynamic behavior of the final system through a process model. For an executable system, ordering of the message invocations should also be specified besides the definition of a set of components which only presents a static view. Components, however, are usually server kind software units that respond when a request is made. A central application can be expected to trigger some of the methods while some com...

Citation Formats

O. Tekik, E. Sürer, and A. Betin Can, “Verifying Maze-Like Game Levels With Model Checker SPIN,” IEEE ACCESS, vol. 10, pp. 66492–66510, 2022, Accessed: 00, 2022. [Online]. Available: https://ieeexplore.ieee.org/abstract/document/9802094.