NEW: Version 2.0 of PRISM-games is out, featuring new reward properties, multi-objective strategy synthesis and assume-guarantee reasoning.


PRISM-games [CFK+13] is an extension of PRISM for the verification of probabilistic systems that can incorporate competitive or collaborative behaviour, modelled as (turn-based) stochastic multi-player games (SMGs). These can be seen as a generalisation of Markov decision processes (MDPs) in which nondeterministic choices are under the control of several distinct players.

SMGs are specified in a modelling language, which extends the existing language used by PRISM. Similarly, properties to be checked are represented in temporal logics that extend the ones used by PRISM. We provide various examples here and with the tool itself.

We provide specific instructions for installation and usage of PRISM-games, but the main manual for PRISM will also be a useful reference. You can also look at the list of related publications.

The tool can be downloaded from here. If you have questions or comments, you can use the main PRISM support forum.

PRISM-games has been developed by:

See also here for a list of contributors to PRISM. Details of those that have worked on the techniques implemented in PRISM-games can be found in this publication list.

To cite PRISM-games, please use the TACAS'13 tool paper: