Download PRISM

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

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.

The current version of PRISM is 4.8.1 (first released 13 January 2024).

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

Support for uncertain models:
- interval DTMCs (IDTMCs)
- interval MDPs (IMDPs)
Improved strategy (policy) generation
- switch -exportstrat exports to tra/dot/txt format
- additional export options (restrict/reduce, states, reach)
- strategy generation extended for bounded reachability, LTL, POMDPs
- GUI support for generating, exporting and simulating strategies
Other features/enhancements:
- PTA model checking supports global/non-local variables
- ModelGenerator interface now supports real-time models (e.g., PTAs)
- New -javaparams switch to pass command-line arguments to JVM
Import/export enhancements:
- Model import/export: reward headers, multiple reward structures, export precision, property labels, POMDP observations
- Results export/import to new formats: PRISM comment, dataframe

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: