Case studies of application of probabilistic and statistical model checking in game design

We propose probabilistic/statistical model checking as a tool for game design. Models of games under design can be used for the early evaluation of properties related with game duration, existence of different successful strategies, and balancing of the game core mechanics. To show the usefulness of model checking in game design we consider and develop three case studies in which model checking is used to answer specific game design questions.