A Cancellation Law for Probabilistic Processes

TL;DR

This paper establishes a cancellation law for probabilistic choice in process languages, showing that bisimilarity is preserved when removing a common distribution, using a topological proof approach.

Contribution

It introduces a cancellation property for probabilistic bisimilarity and provides a novel topological proof in the context of probabilistic process languages.

Findings

Cancellation property holds for probabilistic bisimilar distributions

Topological proof approach handles uncountable branching

Distribution unfolding into stable distributions is key

Abstract

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.