We consider a process language featuring both nondeterministic and
probabilistic choice with an operational semantics taking
distributions of processes as basic building blocks. For this langauge
we propose a sound and complete axiomatization of rooted branching
probabilistic bisimulation. Exploiting the notion of a concrete
process and building on the completeness of strong probabilistic
bisimulation, a completeness result for rooted branching probabilistic
bisimulation is obtained.

Joint work with Jan Friso Groote