A Kleene Algebra with Tests for Union Bound Reasoning About Probabilistic Programs

Authors Leandro Gomes , Patrick Baillot , Marco Gaboardi



PDF
Thumbnail PDF

File

LIPIcs.CSL.2025.35.pdf
  • Filesize: 0.9 MB
  • 19 pages

Document Identifiers

Author Details

Leandro Gomes
  • Université de Lille, CNRS, Inria, Centrale Lille, UMR 9189 CRIStAL, F-59000, France
Patrick Baillot
  • Université de Lille, CNRS, Inria, Centrale Lille, UMR 9189 CRIStAL, F-59000, France
Marco Gaboardi
  • Boston University, MA, USA

Cite As Get BibTex

Leandro Gomes, Patrick Baillot, and Marco Gaboardi. A Kleene Algebra with Tests for Union Bound Reasoning About Probabilistic Programs. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 35:1-35:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CSL.2025.35

Abstract

Kleene Algebra with Tests (KAT) provides a framework for algebraic equational reasoning about imperative programs. The recent variant Guarded KAT (GKAT) allows to reason on non-probabilistic properties of probabilistic programs. Here we introduce an extension of this framework called approximate GKAT (aGKAT), which equips GKAT with a partially ordered monoid (real numbers) enabling to express satisfaction of (deterministic) properties except with a probability up to a certain bound. This allows to represent in equational reasoning "à la KAT" proofs of probabilistic programs based on the union bound, a technique from basic probability theory. We show how a propositional variant of approximate Hoare Logic (aHL), a program logic for union bound, can be soundly encoded in our system aGKAT. We then illustrate the use of aGKAT with an example of accuracy analysis from the field of differential privacy.

Subject Classification

ACM Subject Classification
  • Theory of computation → Algebraic semantics
  • Theory of computation → Pre- and post-conditions
  • Theory of computation → Logic and verification
  • Theory of computation → Hoare logic
Keywords
  • Kleene algebras with tests
  • Hoare logic
  • equational reasoning
  • probabilistic programs
  • union bound
  • formal verification

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. D. Kozen A. Angus. Kleene algebra with tests and program schematology. Technical report, Computer Science Department, Cornell University, Ithaca, NY 14853-7501, USA, July 2001. Technical Report TR2001-1844. Google Scholar
  2. Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. NetKAT: semantic foundations for networks. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 113-126. ACM, 2014. URL: https://doi.org/10.1145/2535838.2535862.
  3. Timos Antonopoulos, Eric Koskinen, Ton Chanh Le, Ramana Nagasamudram, David A. Naumann, and Minh Ngo. An algebra of alignment for relational verification. Proc. ACM Program. Lang., 7(POPL):573-603, 2023. URL: https://doi.org/10.1145/3571213.
  4. Gilles Barthe, François Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, and Pierre-Yves Strub. Easycrypt: A tutorial. In Alessandro Aldini, Javier López, and Fabio Martinelli, editors, Foundations of Security Analysis and Design VII - FOSAD 2012/2013 Tutorial Lectures, volume 8604 of Lecture Notes in Computer Science, pages 146-166. Springer, 2013. URL: https://doi.org/10.1007/978-3-319-10082-1_6.
  5. Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. A program logic for union bounds. In Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi, editors, 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, volume 55 of LIPIcs, pages 107:1-107:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.ICALP.2016.107.
  6. Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella Béguelin. Probabilistic relational reasoning for differential privacy. ACM Trans. Program. Lang. Syst., 35(3):9:1-9:49, 2013. URL: https://doi.org/10.1145/2492061.
  7. Jerry den Hartog and Erik P. de Vink. Verifying probabilistic programs using a Hoare like logic. Int. J. Found. Comput. Sci., 13(3):315-340, 2002. URL: https://doi.org/10.1142/S012905410200114X.
  8. Easycrypt development team. Easycrypt, 2024. URL: https://formosa-crypto.org/projects/.
  9. Cynthia Dwork and Aaron Roth. The algorithmic foundations of differential privacy. Found. Trends Theor. Comput. Sci., 9(3-4):211-407, 2014. URL: https://doi.org/10.1561/0400000042.
  10. Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, and Tetsuya Sato. Graded hoare logic and its categorical semantics. In Nobuko Yoshida, editor, Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, volume 12648 of Lecture Notes in Computer Science, pages 234-263. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72019-3_9.
  11. L. Gomes, A. Madeira, and L. S. Barbosa. Generalising KAT to verify weighted computations. Scient. Annals of Comp. Sc., 29(2):141-184, 2019. URL: https://doi.org/10.7561/SACS.2019.2.141.
  12. Leandro Gomes, Patrick Baillot, and Marco Gaboardi. BiGKAT: an algebraic framework for relational verification of probabilistic programs. working paper or preprint, March 2023. URL: https://hal.science/hal-04017128.
  13. Leandro Gomes, Patrick Baillot, and Marco Gaboardi. A Kleene algebra with tests for union bound reasoning about probabilistic programs. working paper or preprint, July 2024. URL: https://hal.science/hal-04196675.
  14. Leandro Gomes, Alexandre Madeira, and Luís Soares Barbosa. A semantics and a logic for fuzzy arden syntax. Soft Comput., 25(9):6789-6805, 2021. URL: https://doi.org/10.1007/s00500-021-05593-9.
  15. Ichiro Hasuo, Yuichiro Oyabu, Clovis Eberhart, Kohei Suenaga, Kenta Cho, and Shin-ya Katsumata. Control-data separation and logical condition propagation for efficient inference on probabilistic programs. J. Log. Algebraic Methods Program., 136:100922, 2024. URL: https://doi.org/10.1016/J.JLAMP.2023.100922.
  16. Claire Jones. Probabilistic non-determinism. PhD thesis, University of Edinburgh, UK, 1990. URL: https://hdl.handle.net/1842/413.
  17. Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo. Weakest precondition reasoning for expected runtimes of randomized algorithms. J. ACM, 65(5):30:1-30:68, 2018. URL: https://doi.org/10.1145/3208102.
  18. Tobias Kappé, Paul Brunet, Alexandra Silva, Jana Wagemaker, and Fabio Zanasi. Concurrent kleene algebra with observations: From hypotheses to completeness. In Proceedings of FOSSACS 2020, volume 12077 of LNCS, pages 381-400. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-45231-5_20.
  19. Michael J. Kearns and Umesh V. Vazirani. An Introduction to Computational Learning Theory. MIT Press, 1994. URL: https://mitpress.mit.edu/books/introduction-computational-learning-theory.
  20. Juraj Kolcák, Jérémy Dubut, Ichiro Hasuo, Shin-ya Katsumata, David Sprunger, and Akihisa Yamada. Relational differential dynamic logic. In Armin Biere and David Parker, editors, Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I, volume 12078 of Lecture Notes in Computer Science, pages 191-208. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-45190-5_11.
  21. D. Kozen. Kleene algebra with tests. ACM Trans. on Prog. Lang. and Systems, 19(3):427-443, 1997. URL: https://doi.org/10.1145/256167.256195.
  22. D. Kozen. On Hoare logic and Kleene algebra with tests. ACM Trans. on Comp. Logic, 1(212):1-14, 2000. URL: https://doi.org/10.1109/LICS.1999.782610.
  23. Dexter Kozen. A probabilistic PDL. J. Comput. Syst. Sci., 30(2):162-178, 1985. URL: https://doi.org/10.1016/0022-0000(85)90012-1.
  24. Dexter Kozen and Maria-Christina Patron. Certification of compiler optimizations using Kleene algebra with tests. In John W. Lloyd, Verónica Dahl, Ulrich Furbach, Manfred Kerber, Kung-Kiu Lau, Catuscia Palamidessi, Luís Moniz Pereira, Yehoshua Sagiv, and Peter J. Stuckey, editors, Computational Logic - CL 2000, First International Conference, London, UK, 24-28 July, 2000, Proceedings, volume 1861 of Lecture Notes in Computer Science, pages 568-582. Springer, 2000. URL: https://doi.org/10.1007/3-540-44957-4_38.
  25. Annabelle McIver and Carroll Morgan. Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, 2005. URL: https://doi.org/10.1007/B138392.
  26. David Molnar, Matt Piotrowski, David Schultz, and David A. Wagner. The program counter security model: Automatic detection and removal of control-flow side channel attacks. In Dongho Won and Seungjoo Kim, editors, Information Security and Cryptology - ICISC 2005, 8th International Conference, Seoul, Korea, December 1-2, 2005, Revised Selected Papers, volume 3935 of Lecture Notes in Computer Science, pages 156-168. Springer, 2005. URL: https://doi.org/10.1007/11734727_14.
  27. Rajeev Motwani and Prabhakar Raghavan. Randomized Algorithms. Cambridge University Press, 1995. URL: https://doi.org/10.1017/cbo9780511814075.
  28. Damien Pous. Kleene algebra with tests and coq tools for while programs. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, volume 7998 of Lecture Notes in Computer Science, pages 180-196. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39634-2_15.
  29. Wojciech Rozowski, Tobias Kappé, Dexter Kozen, Todd Schmid, and Alexandra Silva. Probabilistic guarded KAT modulo bisimilarity: Completeness and complexity. In Kousha Etessami, Uriel Feige, and Gabriele Puppis, editors, 50th International Colloquium on Automata, Languages, and Programming, ICALP 2023, July 10-14, 2023, Paderborn, Germany, volume 261 of LIPIcs, pages 136:1-136:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.ICALP.2023.136.
  30. Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, and Alexandra Silva. Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time. Proc. ACM Program. Lang., 4(POPL):61:1-61:28, 2020. URL: https://doi.org/10.1145/3371129.
  31. Jana Wagemaker, Nate Foster, Tobias Kappé, Dexter Kozen, Jurriaan Rot, and Alexandra Silva. Concurrent NetKAT - modeling and analyzing stateful, concurrent networks. In Ilya Sergey, editor, Programming Languages and Systems - 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, volume 13240 of Lecture Notes in Computer Science, pages 575-602. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99336-8_21.
  32. Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi. On incorrectness logic and Kleene algebra with top and tests. Proc. ACM Program. Lang., 6(POPL):1-30, 2022. URL: https://doi.org/10.1145/3498690.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail