Skip to main content
SpringerLink
Log in
Book cover

The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy pp 344–362Cite as

Statistical Epistemic Logic

  • Chapter
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,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.

This work was supported by JSPS KAKENHI Grant Number JP17K12667, and by Inria under the project LOGIS.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    It is left for future work to investigate the case of infinite numbers of states.

  2. 2.

    Since \(\mathcal {W}\) is not a multiset, each world in \(\mathcal {W}\) is a different distribution of states. However, this is still expressive enough when we take \(\mathcal {S}\) to be sufficiently large.

  3. 3.

    Since the relation \(\mathcal {R}_{\!\varepsilon }\) is symmetric, the symmetry axiom (B) also holds.

References

  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_2

    Chapter  Google Scholar 

  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_3

    Chapter  Google Scholar 

  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. Baskar, A., Ramanujam, R., Suresh, S.P.: Knowledge-based modelling of voting protocols. In: Proceedings of TARK, pp. 62–71 (2007)

    Google Scholar 

  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-z

    Article  MathSciNet  MATH  Google Scholar 

  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_12

    Chapter  Google Scholar 

  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_4

    Chapter  Google Scholar 

  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.2362356

    Article  MathSciNet  MATH  Google Scholar 

  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.003

    Article  MathSciNet  MATH  Google Scholar 

  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_18

    Chapter  MATH  Google Scholar 

  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_1

    Chapter  Google Scholar 

  12. Dwork, C., Roth, A., et al.: The algorithmic foundations of differential privacy. Found. Trends® Theor. Comput. Sci. 9(3–4), 211–407 (2014)

    MathSciNet  MATH  Google Scholar 

  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.026

    Article  Google Scholar 

  14. Fagin, R., Halpern, J., Moses, Y., Vardi, M.: Reasoning About Knowledge. The MIT Press, Cambridge (1995)

    MATH  Google Scholar 

  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. 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)

    Article  Google Scholar 

  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. 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. 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-V

    Article  MathSciNet  MATH  Google Scholar 

  20. Halpern, J.Y.: Reasoning About Uncertainty. The MIT Press, Cambrdige (2003)

    MATH  Google Scholar 

  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. Hughes, D., Shmatikov, V.: Information hiding, anonymity and privacy: a modular approach. J. Comput. Secur. 12(1), 3–36 (2004)

    Article  Google Scholar 

  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 2006

    Google Scholar 

  24. Kawamoto, Y.: Towards logical specification of statistical machine learning. In: Proceedings of SEFM (2019, to appear)

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

  26. Kawamoto, Y., Murakami, T.: On the anonymization of differentially private location obfuscation. In: Proceedings of ISITA, pp. 159–163 (2018)

    Google Scholar 

  27. Kawamoto, Y., Murakami, T.: Local obfuscation mechanisms for hiding probability distributions. In: Proceedings of ESORICS (2019, to appear)

    Google Scholar 

  28. Kooi, B.P.: Probabilistic dynamic epistemic logic. J. Log. Lang. Inf. 12(4), 381–408 (2003). https://doi.org/10.1023/A:1025050800836

    Article  MathSciNet  MATH  Google Scholar 

  29. Kripke, S.A.: Semantical analysis of modal logic i normal modal propositional calculi. Math. Log. Q. 9(5–6), 67–96 (1963)

    Article  MathSciNet  Google Scholar 

  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. 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_11

    Chapter  Google Scholar 

  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. Lin, J.: Divergence measures based on the Shannon entropy. IEEE Trans. Inf. Theory 37(1), 145–151 (1991). https://doi.org/10.1109/18.61115

    Article  MathSciNet  MATH  Google Scholar 

  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/exq013

    Article  MathSciNet  MATH  Google Scholar 

  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. 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_16

    Chapter  Google Scholar 

  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_45

    Chapter  Google Scholar 

  38. Vaserstein, L.: Markovian processes on countable space product describing large systems of automata. Probl. Peredachi Inf. 5(3), 64–72 (1969)

    MATH  Google Scholar 

  39. von Wright, G.H.: An Essay in Modal Logic. North-Holland Pub. Co., Amsterdam (1951)

    MATH  Google Scholar 

  40. Younes, H.L.: Verification and planning for stochastic processes with asynchronous events. Ph.D. thesis, Carnegie Mellon University (2005)

    Google Scholar 

Download references

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.

Author information

Authors and Affiliations

  1. National Institute of Advanced Industrial Science and Technology (AIST), Tsukuba, Japan

    Yusuke Kawamoto

Authors
  1. Yusuke Kawamoto
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Yusuke Kawamoto .

Editor information

Editors and Affiliations

  1. Universidade Federal de Minas Gerais, Belo Horizonte, Brazil

    Mário S. Alvim

  2. University of Athens, Athens, Greece

    Kostas Chatzikokolakis

  3. Federal University of Rio Grande do Norte - UFRN, Natal, Brazil

    Carlos Olarte

  4. CNRS & University Javeriana Cali, Palaiseau, France

    Frank Valencia

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Kawamoto, Y. (2019). Statistical Epistemic Logic. In: Alvim, M., Chatzikokolakis, K., Olarte, C., Valencia, F. (eds) The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy. Lecture Notes in Computer Science(), vol 11760. Springer, Cham. https://doi.org/10.1007/978-3-030-31175-9_20

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-31175-9_20

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-31174-2

  • Online ISBN: 978-3-030-31175-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation