A Cancellation Law for Probabilistic Processes

We show a cancellation property for probabilistic choice. If µ ⊕ ρ and ν ⊕ ρ are branching probabilistic bisimilar, then µ and ν 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.