www.prismmodelchecker.org

Download PRISM

PRISM is free and open source software, distributed under the GNU General Public License (GPL), version 2.


Download:

PRISM should run on 32/64-bit versions of all major operating systems.

We distribute various pre-built binaries:

For non-Windows platforms, it is usually easy to build from source code:

Older versions are available on the GitHub releases page.


Latest version: 4.11

The current version of PRISM is 4.11 (first released 9 October 2026).

The main changes since the last major release (4.10.1) are listed below. See the CHANGELOG for full details.

  • Expanded support for reward properties
    • full support for total reward (R[C])
    • discounted rewards for DTMCs/MDPs
    • extra support for MTBDD/hybrid engines

  • Other model checking improvements
    • SCC/EC computation optimisations (iterative Tarjan, speed/memory fixes)
    • MDP solution via linear programming in explicit engine (-lp)
    • counterexamples/witnesses for E[F], A[G] in the explicit engine
    • various fixes and extensions to optimal strategy generation

  • Import/export functionality
    • new combined explicit model format (.pexp): single file with transitions, states, labels, rewards, observations
    • explicit exports all include (optional) comment headers
    • import/export of zipped (gzip/xz) explicit model files
    • strategy export to full (annotated) induced model, e.g. .pexp, .umb
    • -exporttrans, -exportstates, etc. take options (e.g. precision=x)
    • faster, lower-memory import/export of UMB files

Installation

See the installation instructions, included in the PRISM manual (which is also distributed with the tool).

If you have any problems, first check the list of common problems and questions.

If you are still stuck, post a message in the forum.

Once you have installed PRISM, you might want to look at:

Downloads