Automated Game Analysis via Probabilistic Model Checking: a case study

It has been recognised for some time that there are close links between the various logics developed for the analysis of multi-agent systems and the many game-theoretic models developed for the same purpose. In this paper, we contribute to this burgeoning body of work by showing how a probabilistic model checking tool can be used for the automated analysis of game-like multi-agent systems in which both agents and environments can act with uncertainty. Specifically, we show how a variation of the well-known alternating offers negotiation protocol of Rubinstein can be encoded as a model for the PRISM model checker and its behaviour analysed through automatic verification of probabilistic CTL's properties.