Document Open Access Logo

Up-To Techniques for Generalized Bisimulation Metrics

Authors Konstantinos Chatzikokolakis, Catuscia Palamidessi, Valeria Vignudelli

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2016.35.pdf
  • Filesize: 0.5 MB
  • 14 pages

Document Identifiers

Author Details

Konstantinos Chatzikokolakis
Catuscia Palamidessi
Valeria Vignudelli

Cite AsGet BibTex

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)
https://doi.org/10.4230/LIPIcs.CONCUR.2016.35

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.
Keywords
  • bisimulation
  • metrics
  • up-to techniques
  • Kantorovich
  • differential privacy

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. On-the-fly exact computation of bisimilarity distances. In Proc. of TACAS, volume 7795 of LNCS, pages 1-15. Springer, 2013. Google Scholar
  2. Filippo Bonchi, Daniela Petrişan, Damien Pous, and Jurriaan Rot. Coinduction up-to in a fibrational setting. In Proc. of CSL-LICS, pages 20:1-20:9. ACM, 2014. Google Scholar
  3. Konstantinos Chatzikokolakis, Daniel Gebler, Catuscia Palamidessi, and Lili Xu. Generalized bisimulation metrics. In Proc. of CONCUR, volume 8704 of LNCS, pages 32-46. Springer, 2014. Google Scholar
  4. Konstantinos Chatzikokolakis, Catuscia Palamidessi, and Valeria Vignudelli. Up-to techniques for generalized bisimulation metrics. Technical report, INRIA, 2016. URL: https://hal.inria.fr/hal-01335234.
  5. Josee Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labeled markov systems. In Proc. of CONCUR, volume 1664 of LNCS, pages 258-273. Springer, 1999. Google Scholar
  6. Josee Desharnais, Radha Jagadeesan, Vineet Gupta, and Prakash Panangaden. The metric analogue of weak bisimulation for probabilistic processes. In Proc. of LICS, pages 413-422. IEEE, 2002. Google Scholar
  7. Josee Desharnais, Radha Jagadeesan, Vineet Gupta, and Prakash Panangaden. Metrics for labelled Markov processes. Theor. Comp. Sci., 318(3):323-354, 2004. Google Scholar
  8. Cynthia Dwork. Differential privacy. In Proc. of ICALP, volume 4052 of LNCS, pages 1-12. Springer, 2006. Google Scholar
  9. R. Milner. Communication and Concurrency. Series in Comp. Sci. Prentice Hall, 1989. Google Scholar
  10. Damien Pous. Coinduction all the way up. To appear in Proc. of LICS, 2016. Google Scholar
  11. Damien Pous and Davide Sangiorgi. Enhancements of the bisimulation proof method. In Advanced Topics in Bisimulation and Coinduction. Cambridge University Press, 2012. Google Scholar
  12. Davide Sangiorgi. On the bisimulation proof method. Mathematical Structures in Computer Science, 8(5):447-479, 1998. Google Scholar
  13. Franck van Breugel and James Worrell. An algorithm for quantitative verification of probabilistic transition systems. In Proc. of CONCUR, volume 2154 of LNCS, pages 336-350. Springer, 2001. Google Scholar
  14. Franck van Breugel and James Worrell. Towards quantitative verification of probabilistic transition systems. In Proc. of ICALP, volume 2076 of LNCS, pages 421-432. Springer, 2001. Google Scholar
  15. Franck van Breugel and James Worrell. Approximating and computing behavioural distances in probabilistic transition systems. Theor. Comp. Sci., 360(1-3):373-385, 2006. Google Scholar
  16. Franck van Breugel and James Worrell. The complexity of computing a bisimilarity pseudometric on probabilistic automata. In Horizons of the Mind, volume 8464 of LNCS, pages 191-213. Springer, 2014. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact