Tools Overview Contact Us Publications Case Studies Manual Home

PARAM Tool Homepage

PARAM is a tool with the purpose of handling parametric variants of models specified in a variant of the PRISM language. PARAM is capable of computing the unbounded reachability probability for parametric discrete-time Markov chains. Apart from this, it can also handle special classes of Markov decision processes, as well as reachability rewards for Markov reward models. To speed up computations, it can compute the (strong and weak) bisimulation quotient of parametric models. The PARAM source code is available under the GNU GENERAL PUBLIC LICENSE (GPL) Version 3.

PARAM has two sisters, PASS and INFAMY, that accept virtually the same language, but have different strengths.

Download and Installation

The latest binaries of PARAM 2 with the improvements of our recent NFM paper [HahnHZ11] can be obtained below. Notice that the version is not tested very well so far. This version includes support for nested PCTL properties and parametric Markov decision processes.


The latest binaries of PARAM 1 [HahnHWZ10] can be obtained here:

Compared to the version described in the STTT journal paper [HahnHZ10], within others the following technical improvements have been done. They should lead to a better performance in the most common use cases, and make the tool easier to be build.

Note: for earlier versions of GiNaC, there is a problem with the cancellation routine. If you get an error message which mentions "mpz_set_str", please use the version of GiNaC from its Git repository. In case problems remain, the latest version still based on CoCoALib is still available.

The PARAM source code is also available (download form).

To build PARAM on Mac OS X, please do the following (thanks to Steffen Märcker):

Use MacPorts GCC >= 4.4 for PARAM and dependencies
(Attention! Dependencies will be incompatible with other ports!)

sudo port install gcc47
sudo port install boost configure.compiler=macports-gcc-4.7
sudo port install ginac configure.compiler=macports-gcc-4.7
sudo port install liblua configure.compiler=macports-gcc-4.7

sudo port select gcc mp-gcc47
sudo port select gcc none

--- Makefile modifications ---
LIB    = -lginac -lcln -lgmpxx -lgmp -lboost_program_options-mt \
-lluajit-5.1 -ldl

INCLUDE_DIRS = -I. -I/opt/local/include
LINK_DIRS = -L/opt/local/lib

FLAGS        = -Wall -O3 -w -DNDEBUG -pipe $(INCLUDE_DIRS) $(LINK_DIRS)

Changes in PARAM 2.3 Alpha

Changes in PARAM 2.2 Alpha


Once you have unzipped the source package, change to the param-vXXXX directory. Delete the existing file "param" there. Type make to compile PARAM. In order to compile PARAM, Boost 1.39.0 or higher must be installed on your system (ideally, the latest version should be installed). Once compilation finishes, the binary may be executed in place. You may have to adopt the Makefile accordingly


There in no installation routine; once you have unzipped the binaries package or compiled PARAM from source, you can run the tool in place. If you wish, you can copy the executables to your bin directory (~/bin as normal user or /usr/bin as root to make PARAM available system-wide).

In case of problems with running the binary or compiling the sources, please contact Ernst Moritz Hahn.


PARAM was developed by Ernst Moritz Hahn, Holger Hermanns, Lijun Zhang and Björn Wachter.


For questions, comments and support requests regarding PARAM, please contact "emh [at] cs [dot] uni [minus] saarland [dot] de".

Valid XHTML 1.1 Valid CSS! Powered by PHP