Generating Functions for Probabilistic Programs

07/13/2020
by   Lutz Klinkenberg, et al.
0

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.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset