Fixed-point Characterization of Compositionality Properties of Probabilistic Processes Combinators

TL;DR

This paper introduces a method to compute the compositionality properties of probabilistic process operators, enabling the derivation of process distance bounds based solely on operator specifications.

Contribution

It provides a systematic way to determine the modulus of continuity for probabilistic process operators from SOS specifications.

Findings

Method to compute operator compositionality properties

Allows deriving process distance bounds from operator structure

Applicable to any SOS specification of probabilistic processes

Abstract

Bisimulation metric is a robust behavioural semantics for probabilistic processes. Given any SOS specification of probabilistic processes, we provide a method to compute for each operator of the language its respective metric compositionality property. The compositionality property of an operator is defined as its modulus of continuity which gives the relative increase of the distance between processes when they are combined by that operator. The compositionality property of an operator is computed by recursively counting how many times the combined processes are copied along their evolution. The compositionality properties allow to derive an upper bound on the distance between processes by purely inspecting the operators used to specify those processes.