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
For example doing an action
a with probability
1/3 and an action
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
1 is reached with probability
2 is reached with probability
2/7, and state
3 is reached
with the remaining probability
dist d:D[f(d)].p is chosen as it also allows the domain
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.