Advertisement

Statistical Epistemic Logic

  • Yusuke KawamotoEmail author
Chapter
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11760)

Abstract

We introduce a modal logic for describing statistical knowledge, which we call statistical epistemic logic. We propose a Kripke model dealing with probability distributions and stochastic assignments, and show a stochastic semantics for the logic. To our knowledge, this is the first semantics for modal logic that can express the statistical knowledge dependent on non-deterministic inputs and the statistical significance of observed results. By using statistical epistemic logic, we express a notion of statistical secrecy with a confidence level. We also show that this logic is useful to formalize statistical hypothesis testing and differential privacy in a simple and abstract manner.

Keywords

Epistemic logic Possible world semantics Divergence Statistical hypothesis testing Differential privacy 

Notes

Acknowledgments

When I was a postdoctoral researcher with Catuscia Palamidessi in 2014, I tried to work alone on this research, but could not manage. Through my collaboration with her on quantitative information flow for the last several years, I obtained missing pieces of techniques needed to develop my ideas into this paper. I am grateful to her for our research collaboration and her helpful advice until today.

I would like to thank the reviewers for their helpful and insightful comments. I am also grateful to Ken Mano, Gergei Bana, and Ryuta Arisaka for their useful comments on preliminary manuscripts.

References

  1. 1.
    Ábrahám, E., Bonakdarpour, B.: HyperPCTL: a temporal logic for probabilistic hyperproperties. In: McIver, A., Horvath, A. (eds.) QEST 2018. LNCS, vol. 11024, pp. 20–35. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-99154-2_2CrossRefGoogle Scholar
  2. 2.
    Bana, G.: Models of objective chance: an analysis through examples. In: Hofer-Szabó, G., Wroński, L. (eds.) Making it Formally Explicit. ESPS, vol. 6, pp. 43–60. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-55486-0_3CrossRefGoogle Scholar
  3. 3.
    Barthe, G., Gaboardi, M., Arias, E.J.G., Hsu, J., Kunz, C., Strub, P.: Proving differential privacy in Hoare logic. In: Proceedings of CSF, pp. 411–424 (2014)Google Scholar
  4. 4.
    Baskar, A., Ramanujam, R., Suresh, S.P.: Knowledge-based modelling of voting protocols. In: Proceedings of TARK, pp. 62–71 (2007)Google Scholar
  5. 5.
    Biondi, F., Kawamoto, Y., Legay, A., Traonouez, L.: Hybrid statisticalestimation of mutual information and its application to information flow. Formal Asp. Comput. 31(2), 165–206 (2019).  https://doi.org/10.1007/s00165-018-0469-zMathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Chadha, R., Delaune, S., Kremer, S.: Epistemic logic for the applied pi calculus. In: Lee, D., Lopes, A., Poetzsch-Heffter, A. (eds.) FMOODS/FORTE -2009. LNCS, vol. 5522, pp. 182–197. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-02138-1_12CrossRefGoogle Scholar
  7. 7.
    Chatzikokolakis, K., Gebler, D., Palamidessi, C., Xu, L.: Generalized bisimulation metrics. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 32–46. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-662-44584-6_4CrossRefGoogle Scholar
  8. 8.
    Chatzikokolakis, K., Knight, S., Palamidessi, C., Panangaden, P.: Epistemic strategies and games on concurrent processes. ACM Trans. Comput. Logic 13(4), 28:1–28:35 (2012).  https://doi.org/10.1145/2362355.2362356MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Chatzikokolakis, K., Palamidessi, C., Panangaden, P.: Anonymity protocols as noisy channels. Inf. Comput. 206(2–4), 378–401 (2008).  https://doi.org/10.1016/j.ic.2007.07.003MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Dechesne, F., Mousavi, M.R., Orzan, S.: Operational and epistemic approaches to protocol analysis: bridging the gap. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 226–241. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-75560-9_18CrossRefzbMATHGoogle Scholar
  11. 11.
    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).  https://doi.org/10.1007/11787006_1CrossRefGoogle Scholar
  12. 12.
    Dwork, C., Roth, A., et al.: The algorithmic foundations of differential privacy. Found. Trends® Theor. Comput. Sci. 9(3–4), 211–407 (2014)MathSciNetzbMATHGoogle Scholar
  13. 13.
    van Eijck, J., Orzan, S.: Epistemic verification of anonymity. Electr. Notes Theor. Comput. Sci. 168, 159–174 (2007).  https://doi.org/10.1016/j.entcs.2006.08.026CrossRefGoogle Scholar
  14. 14.
    Fagin, R., Halpern, J., Moses, Y., Vardi, M.: Reasoning About Knowledge. The MIT Press, Cambridge (1995)zbMATHGoogle Scholar
  15. 15.
    French, T., Gozzard, A., Reynolds, M.: Dynamic aleatoric reasoning in games of bluffing and chance. In: Proceedings of AAMAS, pp. 1964–1966 (2019)Google Scholar
  16. 16.
    Pearson, K.: On the criterion that a given system of deviations from the probable in the case of a correlated system of variables is such that it can be reasonably supposed to have arisen from random sampling. Lond. Edinb. Dublin Philos. Mag. J. Sci. 50(302), 157–175 (1900)CrossRefGoogle Scholar
  17. 17.
    Garcia, F.D., Hasuo, I., Pieters, W., van Rossum, P.: Provable anonymity. In: Proceedings of FMSE, pp. 63–72 (2005).  https://doi.org/10.1145/1103576.1103585
  18. 18.
    Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic programming. In: Proceedings of FOSE, pp. 167–181 (2014).  https://doi.org/10.1145/2593882.2593900
  19. 19.
    Halpern, J.Y.: An analysis of first-order logics of probability. Artif. Intell. 46(3), 311–350 (1990).  https://doi.org/10.1016/0004-3702(90)90019-VMathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Halpern, J.Y.: Reasoning About Uncertainty. The MIT Press, Cambrdige (2003)zbMATHGoogle Scholar
  21. 21.
    Halpern, J.Y., O’Neill, K.R.: Anonymity and information hiding in multiagent systems. In: Proceedings of CSFW, pp. 75–88 (2003)Google Scholar
  22. 22.
    Hughes, D., Shmatikov, V.: Information hiding, anonymity and privacy: a modular approach. J. Comput. Secur. 12(1), 3–36 (2004)CrossRefGoogle Scholar
  23. 23.
    Jonker, H.L., Pieters, W.: Receipt-freeness as a special case of anonymity in epistemic logic. In: Proceedings of Workshop On Trustworthy Elections (WOTE 2006), June 2006Google Scholar
  24. 24.
    Kawamoto, Y.: Towards logical specification of statistical machine learning. In: Proceedings of SEFM (2019, to appear)CrossRefGoogle Scholar
  25. 25.
    Kawamoto, Y., Mano, K., Sakurada, H., Hagiya, M.: Partial knowledge of functions and verification of anonymity. Trans. Jpn. Soc. Ind. Appl. Math. 17(4), 559–576 (2007).  https://doi.org/10.11540/jsiamt.17.4_559. (in Japanese)CrossRefGoogle Scholar
  26. 26.
    Kawamoto, Y., Murakami, T.: On the anonymization of differentially private location obfuscation. In: Proceedings of ISITA, pp. 159–163 (2018)Google Scholar
  27. 27.
    Kawamoto, Y., Murakami, T.: Local obfuscation mechanisms for hiding probability distributions. In: Proceedings of ESORICS (2019, to appear)Google Scholar
  28. 28.
    Kooi, B.P.: Probabilistic dynamic epistemic logic. J. Log. Lang. Inf. 12(4), 381–408 (2003).  https://doi.org/10.1023/A:1025050800836MathSciNetCrossRefzbMATHGoogle Scholar
  29. 29.
    Kripke, S.A.: Semantical analysis of modal logic i normal modal propositional calculi. Math. Log. Q. 9(5–6), 67–96 (1963)MathSciNetCrossRefGoogle Scholar
  30. 30.
    Küsters, R., Truderung, T.: An epistemic approach to coercion-resistance for electronic voting protocols. In: Proceedings of S&P, pp. 251–266 (2009).  https://doi.org/10.1109/SP.2009.13
  31. 31.
    Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 122–135. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-16612-9_11CrossRefGoogle Scholar
  32. 32.
    Lewis, D.: A subjectivist’s guide to objective chance. In: Harper, W.L., Stalnaker, R., Pearce G. (eds)Studies in Inductive Logic and Probability, vol. II, pp. 263–293. University of California Press, Berkeley (1980)Google Scholar
  33. 33.
    Lin, J.: Divergence measures based on the Shannon entropy. IEEE Trans. Inf. Theory 37(1), 145–151 (1991).  https://doi.org/10.1109/18.61115MathSciNetCrossRefzbMATHGoogle Scholar
  34. 34.
    Mano, K., Kawabe, Y., Sakurada, H., Tsukada, Y.: Role interchange for anonymity and privacy of voting. J. Log. Comput. 20(6), 1251–1288 (2010).  https://doi.org/10.1093/logcom/exq013MathSciNetCrossRefzbMATHGoogle Scholar
  35. 35.
    van der Meyden, R., Su, K.: Symbolic model checking the knowledge of the dining cryptographers. In: Proceedings of CSFW, p. 280 (2004).  https://doi.org/10.1109/CSFW.2004.19
  36. 36.
    Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 202–215. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-27813-9_16CrossRefGoogle Scholar
  37. 37.
    Syverson, P.F., Stubblebine, S.G.: Group principals and the formalization of anonymity. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 814–833. Springer, Heidelberg (1999).  https://doi.org/10.1007/3-540-48119-2_45CrossRefGoogle Scholar
  38. 38.
    Vaserstein, L.: Markovian processes on countable space product describing large systems of automata. Probl. Peredachi Inf. 5(3), 64–72 (1969)zbMATHGoogle Scholar
  39. 39.
    von Wright, G.H.: An Essay in Modal Logic. North-Holland Pub. Co., Amsterdam (1951)zbMATHGoogle Scholar
  40. 40.
    Younes, H.L.: Verification and planning for stochastic processes with asynchronous events. Ph.D. thesis, Carnegie Mellon University (2005)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.National Institute of Advanced Industrial Science and Technology (AIST)TsukubaJapan

Personalised recommendations