講座內容：Differential privacy has been an increasingly hot topic in academic, ever since proposed by Dwork, to protect the privacy of every single individual. Although there are a large number of works on it, few attempts have been made on reasoning about differential privacy at a system level that considers differential privacy for continual observation and several parts of the system as a whole. In this talk, we introduce a formal framework to verify differential privacy in the context of probabilistic systems. We model probabilistic systems by probabilistic labeled transition systems and formalize differential privacy by the ratio of the probabilities in the distributions after the same labeled transitions of relevant states. Furthermore, we propose a two-level logic, a privacy variant of the familiar Hennessy-Milner logic, to characterize differential privacy in our framework, which gives an approach to measuring the distance in the infimum metric logically. Our results have close relations to probabilistic bisimilarity as well.