Compositionality of Approximate Bisimulation for Probabilistic Systems

TL;DR

This paper develops a method to quantify and ensure compositionality of approximate bisimulation in probabilistic systems, making the semantics more robust to implementation errors.

Contribution

It introduces a general approach to measure how process combinators affect approximate bisimulation distance and derives rule formats for compositionality.

Findings

Provides a method to quantify the expansion of approximate bisimulation distance.

Derives rule formats guaranteeing compositionality for approximate bisimilarity.

Addresses non-standard compositionality requirements in probabilistic process specifications.

Abstract

Probabilistic transition system specifications using the rule format ntmuft-ntmuxt provide structural operational semantics for Segala-type systems and guarantee that probabilistic bisimilarity is a congruence. 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 direct application we derive an appropriate rule format that guarantees compositionality with respect to approximate bisimilarity. Moreover, we describe how specification formats for non-standard compositionality requirements may be derived.