Raiders of the lost equivalence: Probabilistic branching bisimilarity

Probabilistic branching bisimilarity allows us to compare process behaviour with respect to their branching structure and probabilistic features, while abstracting away from those computation steps that can be marked as irrelevant to the analysis at hand. To the best of our knowledge, in the context of nondeterministic probabilistic processes, no proof of probabilistic branching bisimilarity being an equivalence has been provided so far. Since, as happened in the fully nondeterministic case, some researchers are using such a result by taking it for granted, we decided to dedicate this note to a formal proof of it. More precisely, we extend and adapt the proof strategy used by Basten in the fully nondeterministic case. Thus, we introduce the probabilistic analogue to the notion of semi-branching bisimilarity and to van Glabbeek and Weijland's Stuttering Lemma to prove that probabilistic branching bisimilarity is indeed an equivalence relation.