Generalized bisimulation metrics

Abstract : The pseudometric based on the Kantorovich lifting is one of the most popular notion of distance between probabilistic processes proposed in the literature. However, its application in verification is limited to linear properties. We propose a generalization 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 pseudometrics, 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 distance between trace distributions. Finally, we study the instance corresponding to differential privacy, and we show that it has a dual form, easier to compute. We also prove that the typical process-algebra constructs are non-expansive, thus paving the way to a modular approach to verification.
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [33 references]  Display  Hide  Download

https://hal.inria.fr/hal-01011471
Contributor : Catuscia Palamidessi <>
Submitted on : Sunday, July 3, 2016 - 7:02:16 PM
Last modification on : Wednesday, March 27, 2019 - 4:41:28 PM
Document(s) archivé(s) le : Tuesday, October 4, 2016 - 10:51:05 AM

File

concur.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Konstantinos Chatzikokolakis, Daniel Gebler, Catuscia Palamidessi, Lili Xu. Generalized bisimulation metrics. CONCUR - 25th Conference on Concurrency Theory, Sep 2014, Rome, Italy. pp.32-46, ⟨10.1007/978-3-662-44584-6_4⟩. ⟨hal-01011471⟩

Share

Metrics

Record views

928

Files downloads

221