# Probabilistic processes

It is possible to model probabilistic processes in mCRL2, although this is still an experimental extension.

The tool mcrl22lps linearises the process to a stochastic linear process. Using lps2lts a probabilistic state space can be generated and ltspbisim allows to reduce this state space. The tool ltsgraph supports visualisation of probabilistic processes by drawing probabilistic states with a thicker circle. There are experimental tools to evaluate probabilistic modal formulas, but these are not included in the toolset.

Probabilistic processes are specified using the `dist d:D[f(d)].p` operator. This operator selects a variable `d` of sort `D` with probability `f(d)`. For example doing an action `a` with probability `1/3` and an action `b` with probability `2/3` can be denoted by `dist d:Bool[if(d,1/3,2/3)](d -> a <> b)`.

A larger example is the following:

```% Below a process is modelled where a can happen with probability 1/7, b with
% probability 2/7, a (again) now with probability 3/7 and c with probabilty 1/7.
% The c action goes back to the initial process. Example is provided by  Susmoy Das.

act a,b,c;
proc P = dist n:Pos[if(n==1,1/7,if(n==2,2/7, if(n==3,3/7,if(n==4,1/7,0))))].
((n==1)->a. Q +
(n==2)->b. R +
(n==3)->a. S +
(n==4)->c. P);
Q = delta;
R = delta;
S = delta;

init P;
```

The generated state space for this example is

```des (0 1/7 1 3/7 2 2/7 3,4,5)
(0,"a",4)
(1,"a",4)
(2,"b",4)
(3,"c",0 1/7 1 3/7 2 2/7 3)
```

In this state space, `0 1/7 1 3/7 2 2/7 3` means that state `0` is reached with probability `1/7`, state `1` is reached with probability `3/7`, state `2` is reached with probability `2/7`, and state `3` is reached with the remaining probability `1/7`.

The notation `dist d:D[f(d)].p` is chosen as it also allows the domain `D` and the distribution to range over infinite domains, and as such supports both discrete and continuous distributions. As it stands the tools do not support continuous distributions. A major reason is that the combination of continous probability distribution in combination with nondeterminism over uncountable domains is not properly understood as it stands.