Characteristic formulae for fixed-point semantics: a general framework, Mathematical Structures in Computer Science, vol.22, issue.2, pp.125-173, 2012. ,
Converging from branching to linear metrics on Markov chains, Proceedings of ICTAC 2015, vol.9399, pp.349-367, 2015. ,
On algorithmic verification methods for probabilistic systems, 1998. ,
Proving differential privacy in hoare logic, Proc. of CSF, pp.411-424, 2014. ,
Proving differential privacy via probabilistic couplings, Proc. of LICS '16, pp.749-758, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01411097
Probabilistic relational reasoning for differential privacy, Proc. of POPL, 2012. ,
Revisiting trace and testing equivalences for nondeterministic and probabilistic processes, Logical Methods in Computer Science, vol.10, issue.1, 2014. ,
Precongruence formats for decorated trace semantics, ACM Trans. Comput. Log, vol.5, issue.1, pp.26-78, 2004. ,
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
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
Logical characterization of bisimulation metrics, Proceedings of QAPL'16, vol.227, pp.44-62, 2016. ,
Logical characterization of trace metrics, Proceedings of QAPL@ETAPS 2017, vol.250, pp.39-74, 2017. ,
Logical characterization of branching metrics for nondeterministic probabilistic transition systems, Inf. Comput, vol.268, 2019. ,
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
Generalized bisimulation metrics, Proceedings of CONCUR 2014, vol.8704, pp.32-46, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-01011471
The dining cryptographers problem: Unconditional sender and recipient untraceability, J. Cryptology, vol.1, issue.1, pp.65-75, 1988. ,
Asymmetric distances for approximate differential privacy, Proceedings of CONCUR 2019, vol.140, 2019. ,
Linear distances between Markov chains, Proceedings of CONCUR 2016, vol.59, p.15, 2016. ,
Linear and branching system metrics, IEEE Trans. Software Eng, vol.35, issue.2, pp.258-273, 2009. ,
Discounting the Future in Systems Theory, Proceedings of ICALP'03, vol.2719, pp.1022-1037, 2003. ,
Game refinement relations and metrics, Logical Methods in Computer Science, vol.4, issue.3, 2008. ,
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
Logical, metric, and algorithmic characterisations of probabilistic bisimulation, 2011. ,
Weak probabilistic anonymity, ENTCS, vol.180, issue.1, pp.55-76, 2007. ,
URL : https://hal.archives-ouvertes.fr/inria-00200912
Characterising probabilistic processes logically -(extended abstract), Proceedings of LPAR-17, pp.278-293, 2010. ,
Approximating labelled Markov processes, Inf. Comput, vol.184, issue.1, pp.51-59, 2003. ,
Metrics for labelled Markov processes, Theor. Comput. Sci, vol.318, issue.3, pp.323-354, 2004. ,
The metric analogue of weak bisimulation for probabilistic processes, Proceedings of LICS 2002, pp.413-422, 2002. ,
Gaussian differential privacy, 2019. ,
Behavioural pseudometrics for nondeterministic probabilistic systems, Proceedings of SETTA 2016, vol.9984, pp.67-84, 2016. ,
Local privacy and statistical minimax rates, Proceedings of the 54th Annual IEEE Symposium on Foundations of Computer Science (FOCS), pp.429-438, 2013. ,
Differential privacy, Proceedings of ICALP 2006, vol.4052, pp.1-12, 2006. ,
RAPPOR: randomized aggregatable privacy-preserving ordinal response, Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security (CCS), pp.1054-1067, 2014. ,
Linear dependent types for differential privacy, POPL, pp.357-370, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00909340
Universally utility-maximizing privacy mechanisms, Proceedings of the 41st annual ACM Symposium on Theory of Computing (STOC), pp.351-360, 2009. ,
Algebraic reasoning for probabilistic concurrent systems, Proceedings of IFIP Work, Conf. on Programming, pp.443-458, 1990. ,
Unwinding and inference control, Proc. of the 1984 IEEE Symposium on Security and Privacy, pp.75-87, 1984. ,
A modal characterization of observational congruence on finite terms of CCS, Information and Control, vol.68, issue.1-3, pp.125-145, 1986. ,
A logic for reasoning about time and reliability, FAC, vol.6, issue.5, pp.512-535, 1994. ,
Algebraic laws for nondeterminism and concurrency, J. Assoc. Comput. Mach, vol.32, pp.137-161, 1985. ,
Probabilistic logical characterization, Inf. Comput, vol.209, issue.2, pp.154-172, 2011. ,
Formal verification of parallel programs, Commun. ACM, vol.19, issue.7, pp.371-384, 1976. ,
On computing the total variation distance of hidden markov models, Proceedings of ICALP 2018, vol.107, 2018. ,
Probabilistic metric semantics for a simple language with recursion, Proceedings of MFCS'96, vol.1113, pp.419-430, 1996. ,
Proof systems for satisfiability in Hennessy-Milner logic with recursion, Theor. Comput. Sci, vol.72, issue.2&3, pp.265-288, 1990. ,
Bisimulation through probabilistic testing, Inf. Comput, vol.94, issue.1, pp.1-28, 1991. ,
Privacy: Theory meets practice on the map, Proceedings of ICDE 2008, pp.277-286, 2008. ,
Rényi differential privacy, Proceedings of CSF 2017, pp.263-275, 2017. ,
De-anonymizing social networks, Proceedings of S&P 2009, pp.173-187, 2009. ,
Distance makes the types grow stronger: a calculus for differential privacy, Proc. of ICFP. ACM, pp.157-168, 2010. ,
A general framework for probabilistic characterizing formulae, Proceedings of VMCAI 2012, pp.396-411, 2012. ,
Modeling and verification of randomized distributed real-time systems, 1995. ,
Towards automatic measurement of probabilistic processes, Proceedings of QSIC 2007, pp.50-59, 2007. ,
Formal verification of differential privacy for interactive systems, ENTCS, vol.276, pp.61-79, 2011. ,
On behavioural pseudometrics and closure ordinals, Inf. Process. Lett, vol.112, pp.715-718, 2012. ,
A behavioural pseudometric for probabilistic transition systems, Theor. Comput. Sci, vol.331, issue.1, pp.115-142, 2005. ,
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