Probabilistic Bisimulation as a Congruence

We propose both an SOS transition rule format for the generative model of probabilistic processes, and an SOS transition rule format for the reactive model of the probabilistic processes. Our rule formats guarantee that probabilistic bisimulation is a congruence with respect to process algebra operations. Moreover, our rule format for generative process algebras guarantees that the probability of the moves of a given process, if there are any, sum up to 1, and the rule format for reactive process algebras guarantees that the probability of the moves of a given process labeled with the same action, if there are any, sum up to 1. We show that most operations of the probabilistic process algebras studied in the literature are captured by our formats, which, therefore, have practical applications.