Prism is a probabilistic model checker, by which, the users can model and analyse real time systems. Prism provides its own modelling language. A user can model a system using this language, see a graphical representation of the model and check the behaviour of the model against the optimal strategy (adversary).

The aim of the project is to enhance the support for strategies, which will enable more flexible/complex types of strategies/checks which are currently not supported. It will also allow the users to visualize the behaviour of the optimal adversary in a more user-friendly way, and to modify it and re-check with the model. And it will enhance the support for the features like exporting, importing and re-verification of strategies, which are already available in the tool, but not with full functionality.





  • Dave Parker
  • Gethin