NEW: Version 3.0 of PRISM-games is out, providing concurrent stochastic games, equilibria, real-time models and more. Get it here.
PRISM-games is an extension of PRISM for the verification of probabilistic systems that can incorporate competitive or collaborative behaviour, modelled as stochastic multi-player games. The tool supports several variants of the model:
Stochastic multi-player games are specified in the PRISM-games modelling language, which extends the existing language used by PRISM. There are many illustrations of using the language in our case studies section and also some detailed examples with explanations.
For verification and strategy synthesis on stochastic games, a property specification language is used that again extends the core version found in PRISM. This based on the logic rPATL (probabilistic alternating temporal logic with rewards) [CFK+13b], which is extended to also include multi-objective and equilibria-based properties.
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 PRISM-games case studies and related publications. Currently, compositional functionality is kept in a separate branch.
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: Dave Parker, Marta Kwiatkowska, Gethin Norman, Gabriel Santos, Clemens Wiltsche, Mateusz Ujma, Vojtěch Forejt and Aistis Simaitis. It builds upon PRISM, for which there is also a list of contributors. Details of those that have worked on the techniques implemented in PRISM-games can be found in this publication list.