This work is licensed under the Creative Commons Attribution License. Compositionality of Approximate Bisimulation for Probabilistic Systems

Probabilistic transition system specifications using the rule format ntµfθ/ntµxθ provide structural operational semantics for Segala-type systems and guarantee that probabilistic bisimilarity is a con-gruence. Probabilistic bisimilarity is for many applications too sensitive to the exact probabilities of transitions. Approximate bisimulation provides a robust semantics that is stable with respect to implementation and measurement errors of probabilistic behavior. We provide a general method to quantify how much a process combinator expands the approximate bisimulation distance. As a di-rect application we derive an appropriate rule format that guarantees compositionality with respect to approximate bisimilarity. Moreover, we describe how specification formats for non-standard com-positionality requirements may be derived.