PRISM-games: Case Studies

PRISM-games has been used for verification and strategy synthesis in many different application domains.

Here is a list of cases studies, for which we have developed web pages to explain the modelling and analysis performed. The list is annotated with the types of models used; game models include SMGs (turn-based stochastic multi-player games), CSGs (concurrent stochastic multi-player games) and TPTGs (turn-based probabilistic timed games).

We further list (non-exhaustively) other PRISM-games case studies where details are available in publications. (See also the PRISM-games publications list)

  • Collective decision making for sensor networks (files here) [CFK+13b, Sim14]SMG
  • Team formation protocol (files here) [CKPS11]SMG
  • Attack-defence scenarios in RFID goods management system (files here) [ANP16]SMG
  • Human-in-the-loop UAV mission planning [FWHT15]SMG
  • Autonomous urban driving [CKSW13]SMG
  • Aircraft power distribution [BKTW15]SMG
  • Self-adaptive software architectures [GCSG15, CGSP15]SMG
  • DNS bandwidth amplification attack [DKSS14]SMG
  • Safe robot navigation among humans [JJK+18]SMG

We are always happy to include details of externally developed case studies. If you would like to contribute content about your work with PRISM-games, or you want us to add a pointer to a relevant publication, please contact us.

If you are interested in benchmarking, you can also find the files used for some of these case studies (and others) online:


7,737 downloads of PRISM-games to date.