Up-To Techniques for Generalized Bisimulation Metrics

Konstantinos Chatzikokolakis 1, 2 Catuscia Palamidessi 3, 1, 2 Valeria Vignudelli 2, 4, 5
2 COMETE - Concurrency, Mobility and Transactions
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR7161
5 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : Bisimulation metrics allow us to compute distances between the behaviors of probabilistic systems. In this paper we present enhancements of the proof method based on bisimulation metrics, by extending the theory of up-to techniques to (pre)metrics on discrete probabilistic concurrent processes. Up-to techniques have proved to be a powerful proof method for showing that two systems are bisimilar, since they make it possible to build (and thereby check) smaller relations in bisimulation proofs. We define soundness conditions for up-to techniques on metrics, and study compatibility properties that allow us to safely compose up-to techniques with each other. As an example, we derive the soundness of the up-to-bisimilarity-metric-and-context technique. The study is carried out for a generalized version of the bisimulation metrics, in which the Kantorovich lifting is parametrized with respect to a distance function. The standard bisimulation metrics, as well as metrics aimed at capturing multiplicative properties such as differential privacy, are specific instances of this general definition.
Type de document :
Communication dans un congrès
27th International Conference on Concurrency Theory (CONCUR 2016), Aug 2016, Québec City, Canada. 59, pp.35:1--35:14, 2016, Leibniz International Proceedings in Informatics (LIPIcs). 〈10.4230/LIPIcs.CONCUR.2016.35〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01335234
Contributeur : Konstantinos Chatzikokolakis <>
Soumis le : dimanche 3 juillet 2016 - 17:45:44
Dernière modification le : samedi 18 février 2017 - 01:13:11
Document(s) archivé(s) le : mardi 4 octobre 2016 - 10:55:21

Fichier

paper.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Konstantinos Chatzikokolakis, Catuscia Palamidessi, Valeria Vignudelli. Up-To Techniques for Generalized Bisimulation Metrics. 27th International Conference on Concurrency Theory (CONCUR 2016), Aug 2016, Québec City, Canada. 59, pp.35:1--35:14, 2016, Leibniz International Proceedings in Informatics (LIPIcs). 〈10.4230/LIPIcs.CONCUR.2016.35〉. 〈hal-01335234〉

Partager

Métriques

Consultations de
la notice

510

Téléchargements du document

90