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

TL;DR

This paper introduces a simple, programmatic method for reasoning about multiple probabilistic objectives by transforming programs with reward-based modifications, enabling unified analysis of various reward-related properties.

Contribution

It proposes a novel, incremental transformation technique that extends probabilistic reasoning to a wide range of objectives within a unified framework.

Findings

The approach can express higher moments and threshold probabilities.

Automated verification was successfully demonstrated with Caesar.

The method simplifies reasoning about complex probabilistic objectives.

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.