Compositionality of Strict, Approximate and Metric Bisimulation in Probabilistic Systems

We will start by introducing a recently developed Plotkin style SOS specification format for Segala-type probabilistic transition systems that guarantees that probabilistic bisimilarity is a congruence for any operator defined in this format. For many practical applications probabilistic bisimilarity is too sensitive to the exact probabilities of transitions and thus a slight perturbation of the probabilities would make two systems non-bisimilar. Approximate bisimulation and bisimulation metrics provide a robust semantics that is stable with respect to implementation and measurement errors of probabilistic behavior. We provide appropriate SOS rule formats that guarantee compositionality (called non-expansiveness property for approximation semantics compared to the congruence property for strict semantics) with respect to approximate bisimulation and bisimulation metrics. Furthermore, we provide a characterization of the expansivity behavior of operators specified in a more liberal rule format. This allows to derive easily appropriate rule formats for non-standard compositionality criteria.