Institutional Repository
| Generalized bisimulation metrics | |
| Chatzikokolakis, Konstantinos (1); Gebler, Daniel (3); Palamidessi, Catuscia (2); Xu, Lili (2) | |
| 2014 | |
| Conference Name | 25th International Conference on Concurrency Theory, CONCUR 2014 |
| Pages | 32-46 |
| Conference Date | September 2, 2014 - September 5, 2014 |
| Conference Place | Rome, Italy |
| Indexed Type | EI |
| Publish Place | Springer Verlag |
| ISSN | 3029743 |
| ISBN | 9783662445839 |
| Department | (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 |
| English Abstract | 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. |
| Language | 英语 |
| Content Type | 会议论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/16583 |
| Collection | 中国科学院软件研究所 |
| Recommended Citation GB/T 7714 | Chatzikokolakis, Konstantinos ,Gebler, Daniel ,Palamidessi, Catuscia ,et al. Generalized bisimulation metrics[C]. Springer Verlag,2014:32-46. |
| Files in This Item: | There are no files associated with this item. | |||||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment