# 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.