TY - GEN
T1 - Generalized bisimulation metrics
AU - Chatzikokolakis, Konstantinos
AU - Gebler, Daniel
AU - Palamidessi, Catuscia
AU - Xu, Lili
PY - 2014/1/1
Y1 - 2014/1/1
N2 - 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.
AB - 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.
U2 - 10.1007/978-3-662-44584-6_4
DO - 10.1007/978-3-662-44584-6_4
M3 - Conference contribution
AN - SCOPUS:84906735843
SN - 9783662445839
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 32
EP - 46
BT - Concurrency Theory - 25th International Conference, CONCUR 2014, Proceedings
PB - Springer Verlag
T2 - 25th International Conference on Concurrency Theory, CONCUR 2014
Y2 - 2 September 2014 through 5 September 2014
ER -