Compositional bisimulation metric reasoning with Probabilistic Process Calculi.

We study which standard operators of probabilistic process calculi allow forcompositional reasoning with respect to bisimulation metric semantics. We arguethat uniform continuity (generalizing the earlier proposed property ofnon-expansiveness) captures the essential nature of compositional reasoning andallows now also to reason compositionally about recursive processes. Wecharacterize the distance between probabilistic processes composed by standardprocess algebra operators. Combining these results, we demonstrate howcompositional reasoning about systems specified by continuous process algebraoperators allows for metric assume-guarantee like performance validation.