A Cancellation Law for Probabilistic Processes
Rob van Glabbeek, Jan Friso Groote, and Erik de Vink

We show a cancellation property for probabilistic choice. If $\mu
\oplus \varrho$ and $\nu \oplus \varrho$ are branching probabilistic
bisimilar, then $\mu$ and~$\nu$ are also branching probabilistic
bisimilar. We do this in the setting of a basic process language
involving non-deterministic and probabilistic choice and define
branching probabilistic bisimilarity on distributions. Despite the
fact that the cancellation property is very elegant and concise, we
failed to provide a short and natural combinatorial proof. Instead we
provide a proof using metric topology. Our major lemma is that every
distribution can be unfolded into an equivalent stable distribution,
where the topological arguments are required to deal with uncountable
branching.