Advertisement

Generalized Bisimulation Metrics

  • Konstantinos Chatzikokolakis
  • Daniel Gebler
  • Catuscia Palamidessi
  • Lili Xu
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8704)

Abstract

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.

Keywords

Dual Form Parallel Composition Process Algebra Probabilistic Process Total Variation Distance 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Bacci, G., Bacci, G., Larsen, K.G., Mardare, R.: Computing Behavioral Distances, Compositionally. In: Chatterjee, K., Sgall, J. (eds.) MFCS 2013. LNCS, vol. 8087, pp. 74–85. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  2. 2.
    Bacci, G., Bacci, G., Larsen, K.G., Mardare, R.: On-the-fly exact computation of bisimilarity distances. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 1–15. Springer, Heidelberg (2013)Google Scholar
  3. 3.
    Barthe, G., Köpf, B., Olmedo, F., Béguelin, S.Z.: Probabilistic relational reasoning for differential privacy. In: Proc. of POPL. ACM (2012)Google Scholar
  4. 4.
    van Breugel, F., Worrell, J.B.: An algorithm for quantitative verification of probabilistic transition systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 336–350. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  5. 5.
    van Breugel, F., Worrell, J.B.: Towards quantitative verification of probabilistic transition systems. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 421–432. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  6. 6.
    van Breugel, F., Worrell, J.: A behavioural pseudometric for probabilistic transition systems. Theor. Comp. Sci. 331(1), 115–142 (2005)CrossRefzbMATHGoogle Scholar
  7. 7.
    van Breugel, F., Worrell, J.: Approximating and computing behavioural distances in probabilistic transition systems. Theor. Comp. Sci. 360(1-3), 373–385 (2006)CrossRefzbMATHGoogle Scholar
  8. 8.
    Cai, X., Gu, Y.: Measuring anonymity. In: Bao, F., Li, H., Wang, G. (eds.) ISPEC 2009. LNCS, vol. 5451, pp. 183–194. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  9. 9.
    Chatterjee, K., de Alfaro, L., Majumdar, R., Raman, V.: Algorithms for Game Metrics. In: FSTTCS, vol. 2, pp. 107–118. Leibniz-Zentrum fuer Informatik (2008)Google Scholar
  10. 10.
    Chatzikokolakis, K., Andrés, M.E., Bordenabe, N.E., Palamidessi, C.: Broadening the scope of Differential Privacy using metrics. In: De Cristofaro, E., Wright, M. (eds.) PETS 2013. LNCS, vol. 7981, pp. 82–102. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  11. 11.
    Chatzikokolakis, K., Gebler, D., Palamidessi, C., Xu, L.: Generalized bisimulation metrics. Tech. rep., INRIA (2014)Google Scholar
  12. 12.
    Chen, D., van Breugel, F., Worrell, J.: On the complexity of computing probabilistic bisimilarity. In: Birkedal, L. (ed.) FOSSACS 2012. LNCS, vol. 7213, pp. 437–451. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  13. 13.
    Comanici, G., Precup, D.: Basis function discovery using spectral clustering and bisimulation metrics. In: Vrancx, P., Knudson, M., Grześ, M. (eds.) ALA 2011. LNCS, vol. 7113, pp. 85–99. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  14. 14.
    D’Argenio, P.R., Gebler, D., Lee, M.D.: Axiomatizing Bisimulation Equivalences and Metrics from Probabilistic SOS Rules. In: Muscholl, A. (ed.) FOSSACS 2014. LNCS, vol. 8412, pp. 289–303. Springer, Heidelberg (2014)Google Scholar
  15. 15.
    Deng, Y., Du, W.: The kantorovich metric in computer science: A brief survey. ENTCS 253(3), 73–82 (2009)Google Scholar
  16. 16.
    Deng, Y., Palamidessi, C., Pang, J.: Weak probabilistic anonymity. In: Proc. of SecCo. ENTCS, vol. 180 (1), pp. 55–76. Elsevier (2007)Google Scholar
  17. 17.
    Desharnais, J., Jagadeesan, R., Gupta, V., Panangaden, P.: The metric analogue of weak bisimulation for probabilistic processes. In: Proc. of LICS, pp. 413–422. IEEE (2002)Google Scholar
  18. 18.
    Desharnais, J., Jagadeesan, R., Gupta, V., Panangaden, P.: Metrics for labelled Markov processes. Theor. Comp. Sci. 318(3), 323–354 (2004)CrossRefzbMATHMathSciNetGoogle Scholar
  19. 19.
    Dwork, C.: Differential privacy. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 1–12. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  20. 20.
    Dwork, C., Kenthapadi, K., McSherry, F., Mironov, I., Naor, M.: Our data, ourselves: Privacy via distributed noise generation. In: Vaudenay, S. (ed.) EUROCRYPT 2006. LNCS, vol. 4004, pp. 486–503. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  21. 21.
    Lee, M.D., Gebler, D., D’Argenio, P.R.: Tree Rules in Probabilistic Transition System Specifications with Negative and Quantitative Premises. In: Proc. EXPRESS/SOS 2012. EPTCS, vol. 89, pp. 115–130 (2012)Google Scholar
  22. 22.
    Reed, J., Pierce, B.C.: Distance makes the types grow stronger: A calculus for differential privacy. In: Proc. of ICFP, pp. 157–168. ACM (2010)Google Scholar
  23. 23.
    Smith, A.: Efficient, differentially private point estimators. arXiv preprint arXiv:0809.4794 (2008)Google Scholar
  24. 24.
    Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics 5(2), 285–309 (1955)CrossRefzbMATHMathSciNetGoogle Scholar
  25. 25.
    Thorsley, D., Klavins, E.: Approximating stochastic biochemical processes with wasserstein pseudometrics. Systems Biology, IET 4(3), 193–211 (2010)CrossRefGoogle Scholar
  26. 26.
    Tschantz, M.C., Kaynar, D., Datta, A.: Formal verification of differential privacy for interactive systems (extended abstract). ENTCS 276, 61–79 (2011)MathSciNetGoogle Scholar
  27. 27.
    Xu, L., Chatzikokolakis, K., Lin, H.: Metrics for differential privacy in concurrent systems. In: Ábrahám, E., Palamidessi, C. (eds.) FORTE 2014. LNCS, vol. 8461, pp. 199–215. Springer, Heidelberg (2014)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Konstantinos Chatzikokolakis
    • 1
    • 2
  • Daniel Gebler
    • 3
  • Catuscia Palamidessi
    • 4
    • 2
  • Lili Xu
    • 2
    • 5
  1. 1.CNRSFrance
  2. 2.LIX, Ecole PolytechniqueFrance
  3. 3.VU University AmsterdamNetherlands
  4. 4.INRIAFrance
  5. 5.Institute of SoftwareChinese Academy of ScienceChina

Personalised recommendations