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).

Microgrid demand-side management [CFK+13b, Sim14]SMG
Non-repudiation protocol [NPS13, KNP19]PTATPTG
Task-graph scheduling [NPS13, KNP19]PTATPTG
Jamming multi-channel radio systems [KNPS18]CSG
Power control in cellular networks [KNPS19]CSG
Public good game [KNPS20]CSG
Trust models for user-centric networks [KPS13, KNPS18]SMGCSG
Robot coordination [KNPS19]CSG
Intrusion detection policies [KNPS18]CSG
Aloha protocol [KNPS19, KNPS20]CSG

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:

SMGs [CFK+13b], CSGs (zero-sum) [KNPS18], CSGs (equilibria) [KNPS19]