www.prismmodelchecker.org

PRISM-games: Modelling Language

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
View: printable version          Download: smg_example.prism

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.

From version 2.0, PRISM-games supports additional compositional modelling features for the purposes of assume-guarantee strategy synthesis.

PRISM-games