Compositionality of Approximate Bisimulation for Probabilistic Systems

Daniel Gebler
(Department of Computer Science, VU University Amsterdam)
Simone Tini
(Department of Scienza e Alta Tecnologia, University of Insubria)

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.

In Johannes Borgström and Bas Luttik: Proceedings Combined 20th International Workshop on Expressiveness in Concurrency and 10th Workshop on Structural Operational Semantics (EXPRESS/SOS 2013), Buenos Aires, Argentina, 26th August, 2013, Electronic Proceedings in Theoretical Computer Science 120, pp. 32–46.
Published: 26th July 2013.

ArXived at: http://dx.doi.org/10.4204/EPTCS.120.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org