We study complete axiomatizations for different notions of probabilistic bisimulation on a recursion free process algebra
with probability and nondeterminism under alternating and non-alternating semantics. The axioms that do not involve probability
coincide with the original axioms of Milner. The axioms that involve probability differ depending on the bisimulation under
examination and on the semantics that is used, thus revealing the implications of the different choices.
Supported by MURST project TOSCA