DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2016.35

Up-To Techniques for Generalized Bisimulation Metrics

Authors: Konstantinos Chatzikokolakis, Catuscia Palamidessi, and Valeria Vignudelli

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

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.

Cite as

Konstantinos Chatzikokolakis, Catuscia Palamidessi, and Valeria Vignudelli. Up-To Techniques for Generalized Bisimulation Metrics. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 35:1-35:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{chatzikokolakis_et_al:LIPIcs.CONCUR.2016.35,
  author =	{Chatzikokolakis, Konstantinos and Palamidessi, Catuscia and Vignudelli, Valeria},
  title =	{{Up-To Techniques for Generalized Bisimulation Metrics}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{35:1--35:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.35},
  URN =		{urn:nbn:de:0030-drops-61793},
  doi =		{10.4230/LIPIcs.CONCUR.2016.35},
  annote =	{Keywords: bisimulation, metrics, up-to techniques, Kantorovich, differential privacy}
}

Search Results

Documents authored by Chatzikokolakis, Konstantinos

Up-To Techniques for Generalized Bisimulation Metrics

Abstract

Cite as

Thanks for your feedback!

Could not send message