LOPSTR Conference 2020 Conference Paper
Generating Functions for Probabilistic Programs
- Lutz Klinkenberg
- Kevin Batz
- Benjamin Lucien Kaminski
- Joost-Pieter Katoen
- Joshua Moerman
- Tobias Winkler 0001
Abstract 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.