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.