NEW: Version 2.1 of PRISM-games is out, providing simpler installation/compilation, updates from PRISM 4.5 and more. Get it here.
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. Currently, compositional functionality is kept in a separate branch.
PRISM-games has been developed by: