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