University of Twente Student Theses
Analysis of Stochastic Behaviour in Sokoban
Hagens, B. (2022) Analysis of Stochastic Behaviour in Sokoban.
|
PDF
728kB |
| 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: | https://purl.utwente.nl/essays/91837 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page