In the setting of an elementary probabilistic process language we consider branching bisimilarity for distributions. In earlier work its
axiomatization included a semantic condition for the probabilistic counterparts of the B-axiom. In this talk we introduce the syntactic notion of probabilistic inclusion. We further discuss how to replace the semantic condition by the requirement of probabilistic inclusion, and how, in turn, probabilistic inclusion can be dispensed with at the cost of an infinitary theory.
Joint work with Rob van Glabbeek and Jan Friso Groote