PRISM-games: Examples

The following example model and properties files can be used to test PRISM-games's functionality for rPATL model checking and strategy synthesis.

The example files are also available in the examples directory included with downloads of PRISM-games

A selection of larger benchmark examples can be found on this page. These include:

  • mdsm: Microgrid Demand-Side Management (see also this case study)
  • cdmsn: Collective Decision Making for Sensor Networks
  • investor: Future Markets Investor
  • team-form: Team Formation Protocol

See also the PRISM-games publications list for papers describing various case studies that illustrate the application of PRISM-games.