Abstract

Model checkers can be used to solve mathematical problems, without the need of having prior knowledge on the technical solution to those problems. This paper focuses on the practical usage of the tool SCOOP, which uses several optimization techniques for state space reduction in probabilistic automata. SCOOP can be used in collaboration with probabilistic model checkers such as PRISM to solve a given probabilistic problem, so that a manual approach is unnecessary. Three case studies are examined to show how to use SCOOP and, more importantly, to give an understanding of when to choose a model checking approach instead of trying to calculate a solution manually. The case studies are specifically focused on probabilistic games because of the ease of understanding and the freedom of applying variations. The N-Player ruin, Yahtzee and the Game of the Goose are the games that are analyzed. Scaling and other alterations are applied to find out to what extent these affect the state space and time used as well as the mathematical interpretation. The usage of SCOOP’s optimization techniques is investigated to find out if and how these reduce the state space and time used to solve the problems more efficiently. The results will show that in some cases, a model checking approach provides results that are not realistically obtainable with alternative techniques.

References

1. SCOOP (Digital version available here)
2. PRISM (Digital version available here)
3. MRMC (Digital version available here)

Additional Resources

1. The paper