PRISM-games extends the existing PRISM modelling language to support the specification of stochastic multi-player games (SMGs), building upon 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, [send1], [send2] endplayer player p2 client endplayer module host h : [0..2] init 0; [send1] h=0 -> (h'=1); // send message 1 [send2] h=0 -> (h'=2); // send message 2  c=0 -> (h'=0); // restart endmodule module client c : [0..2] init 0; [send1] c=0 -> 0.85 : (c'=1) + 0.15 : (c'=0); // receive message 1 [send2] c=0 -> 0.85 : (c'=2) + 0.15 : (c'=0); // receive message 2  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.