A Complete Axiomatization of Branching Bisimilarity for a Simple Process Language with Probabilistic Choice (extended abstract)
R.J. van Glabbeek, J.F. Groote & E.P.~de Vink

This paper proposes a notion of branching bisimilarity for non-deterministic
probabilistic processes. In order to characterize the corresponding notion of
rooted branching probabilistic bisimilarity, an equational theory is proposed
for a basic, recursion-free process language with non-deterministic as well as
probabilistic choice. The proof of completeness of the axiomatization builds on
the completeness of strong probabilistic bisimilarity on the one hand and on
the notion of a concrete process, i.e. a process that does not display
(partially) inert $\tau$-moves, on the other hand. The approach is first
presented for the non-deterministic fragment of the calculus and next
generalized to incorporate probabilistic choice, too.