L. Aceto, A. Ingólfsdóttir, P. B. Levy, and J. Sack, Characteristic formulae for fixed-point semantics: a general framework, Mathematical Structures in Computer Science, vol.22, issue.2, pp.125-173, 2012.

G. Bacci, G. Bacci, K. G. Larsen, and R. Mardare, Converging from branching to linear metrics on Markov chains, Proceedings of ICTAC 2015, vol.9399, pp.349-367, 2015.

C. Baier, On algorithmic verification methods for probabilistic systems, 1998.

G. Barthe, M. Gaboardi, E. J. Arias, J. Hsu, C. Kunz et al., Proving differential privacy in hoare logic, Proc. of CSF, pp.411-424, 2014.

G. Barthe, M. Gaboardi, B. Grégoire, J. Hsu, and P. Strub, Proving differential privacy via probabilistic couplings, Proc. of LICS '16, pp.749-758, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01411097

G. Barthe, B. Köpf, F. Olmedo, and S. Z. Béguelin, Probabilistic relational reasoning for differential privacy, Proc. of POPL, 2012.

M. Bernardo, R. De-nicola, and M. Loreti, Revisiting trace and testing equivalences for nondeterministic and probabilistic processes, Logical Methods in Computer Science, vol.10, issue.1, 2014.

B. Bloom, W. J. Fokkink, and R. J. Van-glabbeek, Precongruence formats for decorated trace semantics, ACM Trans. Comput. Log, vol.5, issue.1, pp.26-78, 2004.

V. Castiglioni, Trace and testing metrics on nondeterministic probabilistic processes, Proceedings of EX-PRESS/SOS 2018, vol.276, pp.19-36, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01966950

V. Castiglioni, K. Chatzikokolakis, and C. Palamidessi, A logical characterization of differential privacy via behavioral metrics, Proceedings of FACS 2018, vol.11222, pp.75-96, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01966870

V. Castiglioni, D. Gebler, and S. Tini, Logical characterization of bisimulation metrics, Proceedings of QAPL'16, vol.227, pp.44-62, 2016.

V. Castiglioni and S. Tini, Logical characterization of trace metrics, Proceedings of QAPL@ETAPS 2017, vol.250, pp.39-74, 2017.

V. Castiglioni and S. Tini, Logical characterization of branching metrics for nondeterministic probabilistic transition systems, Inf. Comput, vol.268, 2019.

K. Chatzikokolakis, M. E. Andrés, N. E. Bordenabe, and C. Palamidessi, Broadening the scope of differential privacy using metrics, Proceedings of PETS 2013, vol.7981, pp.82-102, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00767210

K. Chatzikokolakis, D. Gebler, C. Palamidessi, and L. Xu, Generalized bisimulation metrics, Proceedings of CONCUR 2014, vol.8704, pp.32-46, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01011471

D. Chaum, The dining cryptographers problem: Unconditional sender and recipient untraceability, J. Cryptology, vol.1, issue.1, pp.65-75, 1988.

D. Chistikov, A. S. Murawski, and D. Purser, Asymmetric distances for approximate differential privacy, Proceedings of CONCUR 2019, vol.140, 2019.

P. Daca, T. A. Henzinger, J. K?etínský, and T. Petrov, Linear distances between Markov chains, Proceedings of CONCUR 2016, vol.59, p.15, 2016.

L. De-alfaro, M. Faella, and M. Stoelinga, Linear and branching system metrics, IEEE Trans. Software Eng, vol.35, issue.2, pp.258-273, 2009.

L. De-alfaro, T. A. Henzinger, and R. Majumdar, Discounting the Future in Systems Theory, Proceedings of ICALP'03, vol.2719, pp.1022-1037, 2003.

L. De-alfaro, R. Majumdar, V. Raman, and M. Stoelinga, Game refinement relations and metrics, Logical Methods in Computer Science, vol.4, issue.3, 2008.

Y. Deng, T. Chothia, C. Palamidessi, and J. Pang, Metrics for action-labelled quantitative transition systems, Electr. Notes Theor. Comput. Sci, vol.153, issue.2, pp.79-96, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00201087

Y. Deng and W. Du, Logical, metric, and algorithmic characterisations of probabilistic bisimulation, 2011.

Y. Deng, C. Palamidessi, and J. Pang, Weak probabilistic anonymity, ENTCS, vol.180, issue.1, pp.55-76, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00200912

Y. Deng and R. J. Van-glabbeek, Characterising probabilistic processes logically -(extended abstract), Proceedings of LPAR-17, pp.278-293, 2010.

J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden, Approximating labelled Markov processes, Inf. Comput, vol.184, issue.1, pp.51-59, 2003.

J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden, Metrics for labelled Markov processes, Theor. Comput. Sci, vol.318, issue.3, pp.323-354, 2004.

J. Desharnais, R. Jagadeesan, V. Gupta, and P. Panangaden, The metric analogue of weak bisimulation for probabilistic processes, Proceedings of LICS 2002, pp.413-422, 2002.

J. Dong, A. Roth, and W. J. Su, Gaussian differential privacy, 2019.

W. Du, Y. Deng, and D. Gebler, Behavioural pseudometrics for nondeterministic probabilistic systems, Proceedings of SETTA 2016, vol.9984, pp.67-84, 2016.

J. C. Duchi, M. I. Jordan, and M. J. Wainwright, Local privacy and statistical minimax rates, Proceedings of the 54th Annual IEEE Symposium on Foundations of Computer Science (FOCS), pp.429-438, 2013.

C. Dwork, Differential privacy, Proceedings of ICALP 2006, vol.4052, pp.1-12, 2006.

Ú. Erlingsson, V. Pihur, and A. Korolova, RAPPOR: randomized aggregatable privacy-preserving ordinal response, Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security (CCS), pp.1054-1067, 2014.

M. Gaboardi, A. Haeberlen, J. Hsu, A. Narayan, and B. C. Pierce, Linear dependent types for differential privacy, POPL, pp.357-370, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00909340

A. Ghosh, T. Roughgarden, and M. Sundararajan, Universally utility-maximizing privacy mechanisms, Proceedings of the 41st annual ACM Symposium on Theory of Computing (STOC), pp.351-360, 2009.

A. Giacalone, C. Jou, and S. A. Smolka, Algebraic reasoning for probabilistic concurrent systems, Proceedings of IFIP Work, Conf. on Programming, pp.443-458, 1990.

J. A. Goguen and J. Meseguer, Unwinding and inference control, Proc. of the 1984 IEEE Symposium on Security and Privacy, pp.75-87, 1984.

S. Graf and J. Sifakis, A modal characterization of observational congruence on finite terms of CCS, Information and Control, vol.68, issue.1-3, pp.125-145, 1986.

H. Hansson and B. Jonsson, A logic for reasoning about time and reliability, FAC, vol.6, issue.5, pp.512-535, 1994.

M. Hennessy and R. Milner, Algebraic laws for nondeterminism and concurrency, J. Assoc. Comput. Mach, vol.32, pp.137-161, 1985.

H. Hermanns, A. Parma, R. Segala, B. Wachter, and L. Zhang, Probabilistic logical characterization, Inf. Comput, vol.209, issue.2, pp.154-172, 2011.

R. M. Keller, Formal verification of parallel programs, Commun. ACM, vol.19, issue.7, pp.371-384, 1976.

S. Kiefer, On computing the total variation distance of hidden markov models, Proceedings of ICALP 2018, vol.107, 2018.

M. Z. Kwiatkowska and G. Norman, Probabilistic metric semantics for a simple language with recursion, Proceedings of MFCS'96, vol.1113, pp.419-430, 1996.

K. G. Larsen, Proof systems for satisfiability in Hennessy-Milner logic with recursion, Theor. Comput. Sci, vol.72, issue.2&3, pp.265-288, 1990.

K. G. Larsen and A. Skou, Bisimulation through probabilistic testing, Inf. Comput, vol.94, issue.1, pp.1-28, 1991.

A. Machanavajjhala, D. Kifer, J. M. Abowd, J. Gehrke, and L. Vilhuber, Privacy: Theory meets practice on the map, Proceedings of ICDE 2008, pp.277-286, 2008.

I. Mironov, Rényi differential privacy, Proceedings of CSF 2017, pp.263-275, 2017.

A. Narayanan and V. Shmatikov, De-anonymizing social networks, Proceedings of S&P 2009, pp.173-187, 2009.

J. Reed and B. C. Pierce, Distance makes the types grow stronger: a calculus for differential privacy, Proc. of ICFP. ACM, pp.157-168, 2010.

J. Sack and L. Zhang, A general framework for probabilistic characterizing formulae, Proceedings of VMCAI 2012, pp.396-411, 2012.

R. Segala, Modeling and verification of randomized distributed real-time systems, 1995.

L. Song, Y. Deng, and X. Cai, Towards automatic measurement of probabilistic processes, Proceedings of QSIC 2007, pp.50-59, 2007.

M. C. Tschantz, D. Kaynar, and A. Datta, Formal verification of differential privacy for interactive systems, ENTCS, vol.276, pp.61-79, 2011.

F. Van-breugel, On behavioural pseudometrics and closure ordinals, Inf. Process. Lett, vol.112, pp.715-718, 2012.

F. Van-breugel and J. Worrell, A behavioural pseudometric for probabilistic transition systems, Theor. Comput. Sci, vol.331, issue.1, pp.115-142, 2005.

L. Xu, K. Chatzikokolakis, and H. Lin, Metrics for differential privacy in concurrent systems, Proc. of FORTE, vol.8461, pp.199-215, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00879140

, 1) and Equation (B.2) taken together prove the thesis. Proof of Lemma 1. Immediate from Definition 10, Definition 11 and Proposition 3. Proof of Proposition 4. We expand only the case of the additive total variation distance. The general case can be obtained by proving the two inequalities separately