Compositionality of Approximate Bisimulation for Probabilistic Systems

Autor: Daniel Gebler, Simone Tini
Jazyk: angličtina
Rok vydání: 2013
Předmět:
Zdroj: Electronic Proceedings in Theoretical Computer Science, Vol 120, Iss Proc. EXPRESS/SOS 2013, Pp 32-46 (2013)
Druh dokumentu: article
ISSN: 2075-2180
DOI: 10.4204/EPTCS.120.4
Popis: 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.
Databáze: Directory of Open Access Journals