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.
Latest version: 4.8
The current version of PRISM is 4.8 (first released 5 July 2023).
The main changes 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
Once you have installed PRISM, you might want to look at: