www.prismmodelchecker.org

PRISM-games: Compositional Strategy Synthesis

Compositional Modelling

In order to support compositional (assume-guarantee) strategy synthesis, PRISM-games* provides an additional, compositional approach to modelling. This is specifically for the case of stochastic two-player games. Two composition operators are supported. Using the system ... endsystem construct, several subsystems can be composed into a top-level system. Each subsystem comprises several modules, combined using PRISM's usual parallel composition. Rather than using player ... endplayer constructs for player assignments, player 1 transitions are denoted by appending an ! to the action label; similarly, player 2 transitions are those with actions ending in ?. See the example below for a top-level system consisting of two subsystems S1 and S1, each of which consists of one module. 

smg

// top-level system

system "S1" || "S2" endsystem

// subsystem S1

system "S1" G1 endsystem

module G1

	s : [0..2] init 1;

	[d!]  s=0 -> (s'=1);
	[q1!] s=0 -> (s'=1);
	[a?] s=1 -> (s'=2);
	[b?] s=1 -> 0.5 : (s'=1) + 0.5 : (s'=2);
	[] s=2 -> (s'=0);
	[a?] s=2 -> (s'=2);

endmodule

// subsystem S2

system "S2" G2 endsystem

module G2

	t : [0..2] init 1;

	[a!] t=0 -> 0.5 : (t'=1) + 0.5 : (t'=2);
	[q2!] t=0 -> (t'=1);
	[b?] t=1 -> (t'=2);
	[b?] t=1 -> 0.5 : (t'=1) + 0.5 : (t'=2);
	[] t=2 -> (t'=0);

endmodule

// rewards

rewards "r1"
	[a] true : 1;
endrewards

rewards "r2"
	[d] true : 1;
	[b] true : 1;
endrewards

rewards "r3"
	[b] true : 1;
endrewards

rewards "c"
	[a] true : 1;
	[b] true : 1;
endrewards
View: printable version          Download: comp_example.prism

Assume Guarantee

To support compositional (assume-guarantee) synthesis, the comp keyword allows you to specify a property for each subsystem of a top-level system. This allows you, in particular, to display compositional Pareto sets by being able to associate the properties of the respective components with each other.

See the example below for a set of specifications for the compositional model above, indicating synthesis according to the asymmetric synthesis rule of [BKW14]. 

const double v1 = 1/4;
const double v2 = 9/8;
const double v3 = 3/4;

"psi" : comp("phi1", "phi2")

"phi1" : <<1>> (R{"r1"}/{"c"}<=v1 [ C ]=>R{"r2"}/{"c"}>=v2 [ C ])

"phi2" : <<1>> (R{"r1"}/{"c"}<=v1 [ C ]&R{"r3"}/{"c"}<=v3 [ C ])

"phi" : <<1>> (R{"r2"}/{"c"}>=v2 [ C ]&R{"r3"}/{"c"}<=v3 [ C ])

For an example of the compositional strategy synthesis functionality, see the room temperature control case study, described in more detail in [Wil15].

* Currently, compositional functionality is kept in a separate branch of PRISM-games.

PRISM-games