An Axiomatization of Strong Distribution Bisimulation for 
a Language with a Parallel Operator and Probabilistic Choice
J.F. Groote and E.P. de Vink

In the setting of a simple process language featuring non-deterministic choice
and a parallel operator on the one hand and probabilistic choice on the other
hand, we propose an axiomatization capturing strong distribution bisimulation.
Contrary to other process equivalences for probabilistic process languages, in
this paper distributions rather than states are the leading ingredients for
building the semantics and the accompanying equational theory, for which we
establish soundness and completeness.