Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops

Lecture notes in computer science, pp. 314–343

Abstract

A fundamental computational task in probabilistic programming is to infer a program’s output (posterior) distribution from a given initial (prior) distribution. This problem is challenging, especially for expressive languages that feature loops or unbounded recursion. While most of the existing literature focuses on statistical approximation, in this paper we address the problem of mathematically exact inference. To achieve this for programs with loops, we rely on a relatively underexplored type of probabilistic loop invariant, which is linked to a loop’s so-called occupation measure . The occupation measure associates program states with their expected number of visits, given the initial distribution. Based on this, we derive the notion of an occupation invariant . Such invariants are essentially dual to probabilistic martingales, the predominant technique for formal probabilistic loop analysis in the literature. A key feature of occupation invariants is that they can take the initial distribution into account and often yield a proof of positive almost sure termination as a by-product. Finally, we present an automatic, template-based invariant synthesis approach for occupation invariants by encoding them as generating functions . The approach is implemented and evaluated on a set of benchmarks.

Authors 7

1. Darion Haase corresponding Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

2. Kevin Batz

   Cornell University · University College London

   Affiliation as printed

   Cornell University, Ithaca, NY, USA

   University College London, London, United Kingdom

3. Adrian Gallus
   Affiliation as printed

   Independent Researcher, Aachen, Germany

4. Benjamin Lucien Kaminski

   University College London · Saarland University

   Affiliation as printed

   Saarland University, Saarbrücken, Germany

   University College London, London, United Kingdom

5. Joost-Pieter Katoen Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

6. Lutz Klinkenberg Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

7. Tobias Winkler Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany