Axiomatizations for Probabilistic Bisimulation?

Abstract. We study complete axiomatizations for dierent notions of probabilistic bisimulation on a recursion free process algebra with prob-ability and nondeterminism under alternating and non-alternating se-mantics. The axioms that do not involve probability coincide with the original axioms of Milner. The axioms that involve probability dier de-pending on the bisimulation under examination and on the semantics that is used, thus revealing the implications of the dierent choices.