PRISM-games is an extension of PRISM for the verification of probabilistic systems that can incorporate competitive 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.
PRISM-games extends the existing PRISM modelling language to support the specification of SMGs, extending the usual modelling of MDPs. SMG models are indicated by including the keyword smg. Each probability distribution in the model is assigned to exactly one player. The set of all players and the distributions under their control is specified using one or more player ... endplayer constructs, as in the example below.
smg player p1 host, [send] endplayer player p2 client endplayer module host h : [0..2] init 0; [send] h=0 -> (h'=1); // send message 1 [send] h=0 -> (h'=2); // send message 2 [] c=0 -> (h'=0); endmodule module client c : [0..2] init 0; [send] c=0 -> 0.85 : (c'=h) + 0.15 : (c'=0); // receive message [] c!=0 -> (c'=0); // request another message [] c!=0 -> true; // wait endmodule
For example, the above model has two players, p1 and p2. The former controls synchronous transitions labelled with send and any asynchronous transitions from module host. Currently, PRISM-games only supports turn-based SMGs, in which all the distributions available in a given state are controlled by the same player. Violation of this condition results in an error. Unlike the standard version of PRISM, modification of global variables is allowed by synchronous transitions in PRISM-games models; it is up to the modeller to ensure that transitions update global variables consistently.
At the moment, PRISM-games supports model checking of properties specified in the logic rPATL [CFK+12], which combines elements of the probabilistic temporal logic PCTL for MDPs and the logic ATL for games and agent-based systems. A typical rPATL property is:
<<1>> P>=0.99 [F "end"]
which states that player 1 has a strategy to ensure that "end"-labelled states are reached with probability at least 0.99, regardless of the strategies of any other player.
Further example properties are listed below:
<<1,2,3>> P>0.5 ["a" U "b"] <<1,3>> Pmax=? [F "end"] <<4,5>> P<0.95 [F<=100 "end"] <<1>> R{"r"}max=? [F "success"] <<>> R>100 [F0 "finished"] <<2,5>> Rmin=? [Fc "fail"]
To specify the rPATL coalition one can use either the player names or their indices separated by commas. Player numbering is determined by the order or their specification in the model file, starting from 1. To specify the empty set of players, use <<>>.
Once you have downloaded PRISM-games (see below), it can be compiled and installed by following the standard instructions for PRISM.
PRISM-games is built on top of PRISM's (prototype) explicit model checking engine. It is available both via the command-line and GUI versions of PRISM. To run from the command-line, use:
prism <model.prism> <specification.props>
where <model.prism> is the location of the SMG PRISM model file and <specification.props> is the location of the file containing rPATL properties. Stardard PRISM parameters can be specified from the command line, e.g., -const for constants.
We are currently distributing a beta release of PRISM-games, in source code form. Download it here:
You can find some example model/property files in the directory examples/smg.
For further details about the examples, see this page and this case study.
For further details about the underlying models, logics and algorithms, see [CFK+12].
PRISM-games in currently under development. Please contact:
regarding any problems or suggestions for extensions and improvements.
Site hosted at the Department of Computer Science, University of Oxford