University of Twente Student Theses


Analysis of Stochastic Behaviour in Sokoban

Hagens, B. (2022) Analysis of Stochastic Behaviour in Sokoban.

[img] PDF
Abstract:Sokoban is a challenging puzzle game for both humans and computers. By modifying the game to include stochastic elements, Sokoban can be used to benchmark different probabilistic model checkers. Probabilistic model checkers are used to analyse systems that exhibit probabilistic behaviour. To improve the real-world performance of these tools, being able to benchmark them with a large variety of models is essential. This research introduces a novel tool that can generate probabilistic models from Sokoban levels in the PRISM and JANI formats. With tens of thousands of Sokoban levels readily available online, many models can easily be generated and can be used as a part of a more extensive benchmarking suite, which in turn can be used to determine and compare various performance aspects of probabilistic model checkers during probabilistic model checker competitions. Additionally, the paper includes preliminary benchmarks for the Storm, Modest and PRISM model checkers, as well as an analysis of their performance and the properties of the models.
Item Type:Essay (Bachelor)
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science BSc (56964)
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page