Equivalences, congruences, and complete axiomatizations for probabilistic processes

We study several notions of process equivalence—viz. trace, failure, ready, and bisimulation equivalence—in the context of probabilistic labeled transition systems. We show that, unlike nondeterministic transition systems, “maximality” of traces and failures does not increase the distinguishing power of trace and failure equivalence, respectively. Thus, in the probabilistic case, trace and maximal trace equivalence coincide, and failure and ready equivalence coincide. We then propose a language PCCS for communicating probabilistic processes, and present its operational semantics. We show that in PCCS, trace equivalence and failure equivalence are not congruences, whereas Larsen-Skou probabilistic bisimulation is. Furthermore, we prove that trace congruence, the largest congruence contained in trace equivalence, lies between failure equivalence and bisimulation equivalence in terms of its distinguishing strength. Finally, we stress the similarity between classical process algebra and probabilistic process algebra by exhibiting sound and complete axiomatizations of bisimulation equivalence for finite and finite state probabilistic processes, which are natural extensions of the classical ones (R. Milner, “A complete inference system for a class of regular behaviours,” Journal of Computer and System Science, Vol. 28, 1984). Of particular interest is the rule for eliminating unguarded recursion, which characterizes the possibility of infinite syntactic substitution as a zero-probability event.