We study which standard operators of probabilistic process calculi allow for#N#compositional reasoning with respect to bisimulation metric semantics. We argue#N#that uniform continuity (generalizing the earlier proposed property of#N#non-expansiveness) captures the essential nature of compositional reasoning and#N#allows now also to reason compositionally about recursive processes. We#N#characterize the distance between probabilistic processes composed by standard#N#process algebra operators. Combining these results, we demonstrate how#N#compositional reasoning about systems specified by continuous process algebra#N#operators allows for metric assume-guarantee like performance validation.
['Daniel Gebler', 'Kim Guldstrand Larsen', 'Simone Tini']
Compositional bisimulation metric reasoning with Probabilistic Process Calculi