Highly Incremental: A Simple Programmatic Approach for Many Objectives (Extended Version)
Philipp Schr\"oer, Joost-Pieter Katoen

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, Reasoning, and Knowledge · Advanced Software Engineering Methodologies
