www.prismmodelchecker.org

PRISM-games: Examples

There are example files available in the prism-examples/smgs directory included with downloads of PRISM-games

The simple subdirectory contains some small examples that can be used to test PRISM-games's functionality for rPATL model checking and strategy synthesis:

Other examples included are listed below. See the README file in each directory for more info and links.

  • investor: Future markets investor
  • mdsm: Microgrid demand-side management (see also this case study)
  • cdmsn: Collective decision making for sensor networks
  • team-form: Team formation protocol
  • car: Autonomous vehicle in an urban setting
  • uav: Unmanned aerial vehicle

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

A selection of examples for benchmarking can be found on this page. These include:

PRISM-games