Generalized bisimulation metrics

ISCAS OpenIR

	Generalized bisimulation metrics
	Chatzikokolakis, Konstantinos (1); Gebler, Daniel (3); Palamidessi, Catuscia (2); Xu, Lili (2)
	2014
会议名称	25th International Conference on Concurrency Theory, CONCUR 2014
页码	32-46
会议日期	September 2, 2014 - September 5, 2014
会议地点	Rome, Italy
收录类别	EI
出版地	Springer Verlag
ISSN	3029743
ISBN	9783662445839
部门归属	(1) CNRS, France; (2) LIX, Ecole Polytechnique, France; (3) VU University Amsterdam, Netherlands; (4) INRIA, France; (5) Institute of Software, Chinese Academy of Science, China
摘要	The bisimilarity pseudometric based on the Kantorovich lifting is one of the most popular metrics for probabilistic processes proposed in the literature. However, its application in verification is limited to linear properties. We propose a generalization of this metric which allows to deal with a wider class of properties, such as those used in security and privacy. More precisely, we propose a family of metrics, parametrized on a notion of distance which depends on the property we want to verify. Furthermore, we show that the members of this family still characterize bisimilarity in terms of their kernel, and provide a bound on the corresponding metrics on traces. Finally, we study the case of a metric corresponding to differential privacy. We show that in this case it is possible to have a dual form, easier to compute, and we prove that the typical constructs of process algebra are non-expansive with respect to this metrics, thus paving the way to a modular approach to verification. © 2014 Springer-Verlag.; The bisimilarity pseudometric based on the Kantorovich lifting is one of the most popular metrics for probabilistic processes proposed in the literature. However, its application in verification is limited to linear properties. We propose a generalization of this metric which allows to deal with a wider class of properties, such as those used in security and privacy. More precisely, we propose a family of metrics, parametrized on a notion of distance which depends on the property we want to verify. Furthermore, we show that the members of this family still characterize bisimilarity in terms of their kernel, and provide a bound on the corresponding metrics on traces. Finally, we study the case of a metric corresponding to differential privacy. We show that in this case it is possible to have a dual form, easier to compute, and we prove that the typical constructs of process algebra are non-expansive with respect to this metrics, thus paving the way to a modular approach to verification. © 2014 Springer-Verlag.
语种	英语
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/16583
专题	中国科学院软件研究所
推荐引用方式 GB/T 7714	Chatzikokolakis, Konstantinos ,Gebler, Daniel ,Palamidessi, Catuscia ,et al. Generalized bisimulation metrics[C]. Springer Verlag,2014:32-46.