PRISM-games is an extension of PRISM for probabilistic model checking of stochastic multi-player games.

See the website and read the papers for more information.

PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour. It has been used to analyse systems from many different application domains, including communication and multimedia protocols, randomised distributed algorithms, security protocols, biological systems and many others.

Example PRISM graph

PRISM can build and analyse many types of probabilistic models:

  • discrete-time Markov chains (DTMCs)
  • continuous-time Markov chains (CTMCs)
  • Markov decision processes (MDPs)
  • probabilistic automata (PAs)
  • probabilistic timed automata (PTAs)
  • partially observable Markov decision processes (POMDPs)
  • partially observable probabilistic timed automata (POPTAs)

plus extensions of these models with costs and rewards.

Models are described using the PRISM language, a simple, state-based language. PRISM provides support for automated analysis of a wide range of quantitative properties of these models, e.g. "what is the probability of a failure causing the system to shut down within 4 hours?", "what is the worst-case probability of the protocol terminating in error, over all possible initial configurations?", "what is the expected size of the message queue after 30 minutes?", or "what is the worst-case expected time taken for the algorithm to terminate?". The property specification language incorporates the temporal logics PCTL, CSL, LTL and PCTL*, as well as extensions for quantitative specifications and costs/rewards.

PRISM incorporates state-of-the art symbolic data structures and algorithms, based on BDDs (Binary Decision Diagrams) and MTBDDs (Multi-Terminal Binary Decision Diagrams) [KNP04b, Par02]. It also includes a discrete-event simulation engine, providing support for approximate/statistical model checking, and implementations of various different analysis techniques, such as quantitative abstraction refinement and symmetry reduction.

PRISM is free and open source, released under the GNU General Public License (GPL).

To cite PRISM, please use the most recent tool paper, from CAV'11:

Latest News

January 2022: We are looking for 2 motivated Research Associates to play key roles on the FUN2MODEL project. Applications close on 7th February. See here for more details.
November 2021: New survey paper covering MDPs, POMDPs, stochastic games and their support in PRISM and PRISM-games to appear in Annual Review of Control, Robotics, and Autonomous Systems next year,
September 2021: PRISM is 20 years old this month! It's first official release was in 2001. Thanks to all those have used it and who have helped develop it over the years.
March 2021: PRISM 4.7 is now available, including support for POMDPs, improved accuracy reporting and more.

[ more news... ]