We show a cancellation property for probabilistic choice. If distributions mu + rho and nu + rho are branching probabilistic bisimilar, then distributions 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.

翻译：我们研究了概率选择中的消去性质。若分布μ+ρ与ν+ρ是分支概率双相似的，则分布μ与ν也是分支概率双相似的。我们在一个包含非确定选择与概率选择的基本过程语言框架中展开研究，并在分布上定义了分支概率双相似性。尽管消去性质本身非常简洁优美，但我们未能给出简短自然的组合证明，而是借助度量拓扑方法提供了证明。我们的主要引理是：每个分布都可以展开为等价的稳定分布，其中需要利用拓扑论证来处理不可数分支的情形。