Generating Functions for Probabilistic Programs

TL;DR

This paper explores the use of generating functions to analyze discrete probabilistic programs, enabling reasoning about invariants and termination probabilities through algebraic methods.

Contribution

It introduces a denotational GF-transformer semantics for probabilistic while-programs, connecting it to Kozen's distribution transformer semantics and enabling algebraic analysis.

Findings

Finitely expressible GFs facilitate invariant checking with computer algebra tools.

GFs can determine termination probabilities of probabilistic programs.

Characterization of programs with rational GFs encoding phase-type distributions.

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.