Generating Functions for Probabilistic Programs

Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman, Tobias Winkler

Research output: Working paper / PreprintPreprintAcademic


This paper investigates the usage of generating functions (GFs) encoding measures over the program variables for reasoning about discrete probabilistic programs. To that end, we define a denotational GF-transformer semantics for probabilistic while-programs, and show that it instantiates Kozen’s seminal distribution transformer semantics. We then study the effective usage of GFs for program analysis. We show that finitely expressible GFs enable checking super-invariants by means of computer algebra tools, and that they can be used to determine termination probabilities. The paper concludes by characterizing a class of — possibly infinite-state — programs whose semantics is a rational GF encoding a discrete phase-type distribution.
Original languageEnglish
PublisherCornell University - arXiv
Publication statusPublished - Jul 2020
Externally publishedYes


Dive into the research topics of 'Generating Functions for Probabilistic Programs'. Together they form a unique fingerprint.
  • Generating Functions for Probabilistic Programs

    Klinkenberg, L., Batz, K., Kaminski, B. L., Katoen, J-P., Moerman, J. & Winkler, T., 13 Feb 2021, Logic-Based Program Synthesis and Transformation: 30th International Symposium, LOPSTR 2020, Bologna, Italy, September 7–9, 2020, Proceedings. Maribel Fernández (ed.). 1 ed. Cham: Springer, p. 231-248 18 p. (Lecture Notes in Computer Science, Vol. 12561).

    Research output: Chapter in Book/Report/Conference proceedingConference Article in proceedingAcademicpeer-review

Cite this