Compositionality of approximate bisimulation for probabilistic systems. (English) Zbl 1464.68245
Borgström, Johannes (ed.) et al., Combined 20th international workshop on expressiveness in concurrency and 10th workshop on structured operational semantics, Buenos Aires, Argentina, August, 26, 2013. Proceedings. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 120, 32-46 (2013).
Summary: Probabilistic transition system specifications using the rule format \(nt\mu f\theta/nt\mu x\theta\) 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.
For the entire collection see [Zbl 1415.68016].
For the entire collection see [Zbl 1415.68016].
MSC:
68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
68Q87 | Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) |