Highly Incremental: A Simple Programmatic Approach for Many Objectives (Extended Version)

TL;DR

A one-fits-all programmatic approach to reason about a plethora of objectives on probabilistic programs using a single existing approach: probabilistic wp-reasoning.

Abstract

We present a one-fits-all programmatic approach to reason about a plethora of objectives on probabilistic programs. The first ingredient is to add a reward-statement to the language. We then define a program transformation applying a monotone function to the cumulative reward of the program. The key idea is that this transformation uses incremental differences in the reward. This simple, elegant approach enables to express e.g., higher moments, threshold probabilities of rewards, the expected excess over a budget, and moment-generating functions. All these objectives can now be analyzed using a single existing approach: probabilistic wp-reasoning. We automated verification using the Caesar deductive verifier and report on the application of the transformation to some examples.

Figures (22)

• Figure 1: Example programs modeling a web server retrying a database call.
• Figure 2: Probability distribution of runtimes of the programs in \ref{['fig:example-programs']}.
• Figure 3: Operational MC for \ref{['fig:example-program-a']}.
• Figure 4: Inductive definition of the weakest pre-expectation semantics for program ${\color{heyvlColor}S}$, $\textsf{\upshape {wp}}\llbracket{{\color{heyvlColor}S}}\rrbracket \colon \mathbb{E} \to \mathbb{E}$ where ${\color{prepostColor}X} \in \mathbb{E}$ is the post-expectation.
• Figure 5: Three different reward models for tracking runtimes for a schematic program consisting of a single while loop. The runtime of interest is the number of times the loop body ${\color{heyvlColor}S'}$ is executed. Only \ref{['fig:incremental-rewards']} tracks the runtime correctly, whereas \ref{['fig:rewards-termination', 'fig:rewards-termination-squared']} have the result zero for a diverging loop ($b = \texttt{true}$).

Theorems & Definitions (21)

• lemma 1: Programmatic Rewards on Termination
• lemma 2: Incremental Runtime Collection
• definition 1: Reward Program Transformation
• theorem 1: Soundness
• theorem 2: Monotonicity
• theorem 3: Linearity
• theorem 4: Ghost Buster
• theorem 5: Composition of Transformations
• definition 2: MC Transformation
• lemma 3