Generating Functions for Probabilistic Programs

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.

Authors

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

Keywords

No keywords are indexed for this paper.