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.
PRISM-games has been developed by: