User Manual

Model formulation

Models are given in an extended version of the PRISM language. For an overview of the PRISM language, please refere to their homepage. PARAM extends the PRISM language by the possibility to specify a <parameter> via

param float <parameter>;

and later usage of such parameters in the probability distributions in the commands of the model. In PARAM 2, parameters can be assigned an interval [<p1>,...,<p2>] of valid values using the syntax

param <parameter> : [<p1>..<p2>];

By default, the interval is assumed to be [0,1].

PARAM 1 supports discrete-time Markov chains and a (with some restrictions) continuous-time Markov chains. PARAM 2 also support discrete-time Markov decision processes. We also allow the definition of reward structures, but the usage for several reward structures is not supported for earlier versions of PARAM.

Properties are given in PCTL using the notion of PRISM PARAM 1 supports non-nested PCTL formulae of the following form, where <A> and <B> are expressions over the model variables and <bound> is a natural number:

• P=? [ <A> U <B> ] (unbounded until)
• P=? [ <A> U<=<bound> <B> ] (bounded until)
• R=? [ F <A> ] (expected accumulated reward)

For the expected accumulated reward, you must make sure that always finally the set of states in which <A> holds will be reached. Otherwise, the result is undefined.

PARAM 2 also supports nested PCTL. We aim at completeness there, however as there was only limited testing on the new version, there are still some restrictions.

Usage

PARAM is invoked from the command line by

<param> <model-file> <property-file> <options>

where <param> is the command to start PARAM, <model-file> is the model file and <property-file> is the formula file, with the restrictions described above. Depending on the PARAM version, there are different possible options for <options>. Please use

<param> --help

to print a list of available options. Notice that the set of command line options is not stable, and new command line options may be added or existing ones changed, as the development of the tool continues. After calling PARAM, the result of the analysis is written to the file result.out, if not specified differently.