DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2025.35

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

Authors: Leandro Gomes, Patrick Baillot, and Marco Gaboardi

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{gomes_et_al:LIPIcs.CSL.2025.35,
  author =	{Gomes, Leandro and Baillot, Patrick and Gaboardi, Marco},
  title =	{{A Kleene Algebra with Tests for Union Bound Reasoning About Probabilistic Programs}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{35:1--35:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.35},
  URN =		{urn:nbn:de:0030-drops-227929},
  doi =		{10.4230/LIPIcs.CSL.2025.35},
  annote =	{Keywords: Kleene algebras with tests, Hoare logic, equational reasoning, probabilistic programs, union bound, formal verification}
}

Search Results

Documents authored by Gomes, Leandro

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

Abstract

Cite as

Thanks for your feedback!

Could not send message