💻 computer science

Multiobjective Preexpectation Reasoning for Probabilistic Programs

This paper introduces a deductive, program-level framework for multiobjective strategy synthesis in probabilistic programs with nondeterminism, utilizing a multiobjective preexpectation transformer that maps postexpectations to achievable value sets within a convex Hoare powerdomain to soundly handle infinite-state Markov Decision Processes without requiring finite state spaces.

Original authors: Lena Verscht, Hannah Mertens, Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen

Published 2026-08-14

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Lena Verscht, Hannah Mertens, Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are the captain of a spaceship navigating a chaotic nebula. You have two goals: get to your destination as fast as possible, and keep your ship's hull from getting damaged by space debris. But here's the catch: the faster you go, the more likely you are to crash, and the safer you drive, the longer the trip takes. In the world of computer science, this is a classic "planning problem." We write computer programs that make decisions, but sometimes those programs have to deal with two types of uncertainty: randomness (like flipping a coin to decide a route) and nondeterminism (where the program has to choose between options, but we don't know which one it will pick yet).

To make sure these programs work correctly, scientists use a tool called a "predicate transformer." Think of this as a magical crystal ball that looks at a program before it runs and tells you what the expected outcome will be. If you tell the crystal ball, "I want to know the chance of arriving safely," it calculates the best possible strategy to maximize that safety. For a long time, these crystal balls could only look at one goal at a time. But in real life, we rarely just want one thing; we want a balance. We want to know the trade-off: "If I want to arrive 10% faster, how much safety do I lose?" This is the realm of multiobjective optimization, where the goal isn't a single perfect number, but a whole map of possible compromises, known as a Pareto front.

This paper introduces a new, upgraded crystal ball designed specifically for these multi-goal scenarios. The authors, a team of computer scientists, have developed a mathematical framework called the multiobjective preexpectation transformer (or "mop" for short). Instead of giving you a single number, this tool gives you a shape—a cloud of all the possible outcomes you can achieve by mixing different strategies. It works like a sophisticated recipe book: it takes a program with uncertain choices and calculates the entire "menu" of possible results, showing exactly which combinations of speed and safety are achievable and which are impossible.

The paper proves that this new tool is mathematically sound, meaning it accurately reflects how the program would behave in the real world, even if the program could run forever or have an infinite number of states. They show that you can use this tool to not only predict outcomes but also to synthesize strategies. In other words, if you say, "I want a result that is 60% fast and 40% safe," the system can mathematically construct a specific plan (a "mixed determinization") to get you there. This plan might involve flipping a coin at the start to decide between two different pure strategies, effectively randomizing the choice to hit that perfect middle ground.

The researchers tested their method on several examples, including a robot trying to reach a goal without breaking down and a gambler trying to maximize winnings without losing everything. In the robot example, they showed that the best strategy isn't always "always go fast" or "always go slow." Sometimes, the optimal move is to go slow for most of the trip and then sprint at the very end, or to mix these approaches. The paper demonstrates that their "mop" tool can calculate these complex trade-offs symbolically, without needing to simulate every single possible path the robot could take.

However, the authors are careful to note that while they can find strategies that get arbitrarily close to any desired point on the trade-off map, finding a strategy that hits a specific point exactly is sometimes impossible if that point is a "sharp corner" on the map that no single strategy can touch. In those cases, the best they can do is get very, very close. They also point out that their current method works best for simple programs and doesn't yet handle complex features like recursive functions or continuous probability distributions, leaving those as challenges for future research.

Ultimately, this work bridges the gap between high-level program code and the complex mathematics of decision-making under uncertainty. It provides a way to reason about multiple goals simultaneously, turning the vague idea of "finding a balance" into a precise, calculable science. By treating the set of all possible outcomes as a geometric shape, the authors give programmers a powerful new lens to design systems that are not just safe or fast, but smartly balanced.

Technical Summary: Multiobjective Preexpectation Reasoning for Probabilistic Programs

Problem Statement

Probabilistic programs with nondeterminism model planning and control problems where a strategy (or controller) must resolve nondeterministic choices to optimize expected outcomes. While classical approaches focus on optimizing a single quantity (e.g., expected fuel level or termination probability), many real-world scenarios require optimizing multiple, often conflicting, objectives simultaneously (e.g., maximizing success probability while minimizing resource consumption).

In the multiobjective setting, improving one objective often degrades another. The set of optimal trade-offs is captured by the Pareto front. Existing methods for multiobjective optimization in Markov Decision Processes (MDPs) are largely restricted to finite-state models. However, probabilistic programs often induce infinite-state MDPs. Furthermore, there is a lack of a deductive, program-level calculus capable of reasoning about multiple expectations simultaneously, synthesizing strategies, and handling infinite state spaces without resorting to explicit state enumeration.

This paper addresses three core questions:

Q1: What is the set of simultaneously achievable value tuples (the multiobjective preexpectation) for a given program, and can it be computed via a mechanizable, program-level calculus?
Q2: Given an achievable target trade-off, how can we synthesize a program refinement (strategy) that realizes it?
Q3: How do these program-level constructs relate to and extend the theory of (possibly infinite-state) multiobjective MDPs?

Methodology

The authors develop a multiobjective preexpectation transformer (denoted mop) that operates at the program level. This approach extends the classical weakest preexpectation (wp) calculus to handle vectors of expectations.

1. The Multiobjective Preexpectation Transformer (`mop`)

The core innovation is mapping a tuple of postexpectations $(f_1, \dots, f_n)$ to a set of simultaneously achievable values.

Domain: The transformer operates on the convex Hoare powerdomain of $\mathbb{R}_{\ge 0}^n$ $R_{\geq 0}^{n}$ . Elements of this domain are subsets of $\mathbb{R}_{\ge 0}^n$ $R_{\geq 0}^{n}$ that are:
- Non-empty: Always containing the zero vector.
- Downward closed: If a value vector is achievable, any vector dominated by it is also achievable.
- Convex closed: Mixing strategies (randomizing over determinizations) allows achieving any convex combination of their outcomes.
- Scott closed: Captures "almost achievable" points (limits of sequences of achievable points), ensuring completeness for infinite-state systems where suprema may not be attained by a single strategy.
Semantics: The transformer is defined inductively over the program structure (skip, assignment, sequential composition, probabilistic choice, guarded nondeterministic choice, and loops).
- For guarded nondeterministic choice, mop takes the pointwise supremum in the powerdomain, which corresponds to the Scott-closed and convex-closed union of the branches.
- For loops, mop is defined as the least fixed point (lfp) of a characteristic function, guaranteed to exist due to the $\omega$ -continuity of the transformer.

2. Strategy Synthesis via Scalarization

To synthesize a strategy (a determinization) that achieves a specific point on the Pareto front, the authors employ scalarization:

Weighted Sums: A weight vector $w$ combines multiple objectives into a single scalar expectation $w \cdot f$ .
Reduction: The problem of finding a strategy for a specific trade-off is reduced to finding an optimal strategy for a weighted sum objective. Existing single-objective programmatic strategy synthesis techniques (e.g., [Batz et al. 2024a]) can be used to find a pure determinization $C_w$ that maximizes $w \cdot f$ .
Mixed Determinizations: Since a single deterministic strategy may not achieve every point on the Pareto front (especially non-exposed points), the authors introduce mixed determinizations. These are programs that perform an initial coin flip to select between different pure determinizations. The set of achievable points is shown to be the closure of the convex hull of the outcomes of these pure determinizations.

3. Loop Reasoning and Termination

The paper provides rules for reasoning about loops using invariants:

Upper Bounds: Derived via Park induction using superinvariants.
Lower Bounds: Derived using subinvariants under specific termination conditions:
- Demonic Almost-Sure Termination (dAST): Every resolution of nondeterminism terminates with probability 1.
- Demonic Certain Termination (dCT): All executions terminate within a bounded number of steps.
- $\omega$ -invariants: A sequence of invariants tracking unrolling depth, applicable without termination assumptions but requiring infinitely many proof obligations.

4. Operational Correspondence

The authors establish a rigorous connection between the program-level mop transformer and the operational semantics of probabilistic programs as countable-state, finite-action MDPs.

They define a generalized Bellman operator on the convex Hoare powerdomain for MDPs.
They prove that the mop transformer coincides exactly with the least fixed point of this Bellman operator, characterizing the set of almost achievable expected reward vectors. This correspondence holds without assuming a finite state space.

Key Contributions

Multiobjective Preexpectation Transformer: Introduction of mop, a well-defined, monotone, and $\omega$ -continuous transformer on the convex Hoare powerdomain that conservatively extends weakest preexpectations to the multiobjective setting.
Invariant-Based Reasoning: Lifting of invariant-based loop reasoning to the multiobjective setting, providing rules for both upper and lower bounds, including conditions for exactness (dAST/dCT).
Strategy Synthesis: Development of rules to synthesize witnessing strategies. The paper demonstrates that while pure determinizations may not suffice for all Pareto optimal points, mixed determinizations (randomizing over pure determinizations) can achieve any point in the Scott-closed convex hull of the achievable set.
Operational Soundness: Proof of an exact correspondence between the mop transformer and a generalized Bellman operator on operational MDP semantics, valid for countable-state (infinite) MDPs. This generalizes seminal multiobjective MDP verification results which were previously restricted to finite states.
Case Studies: Application of the machinery to three case studies:
- Robot: A risk vs. speed trade-off, demonstrating the calculation of Pareto fronts and synthesis of mixed strategies.
- Casino: A gambling scenario with unbounded rewards, illustrating reasoning with $\omega$ -invariants and dAST.
- Queue: An adaptive server system, showing how the framework can symbolically characterize trade-offs under varying environmental parameters.

Results and Significance

The paper claims that mop provides a symbolic, program-level approach for multiobjective optimization over infinite MDPs.

Completeness: The transformer captures the set of almost achievable points exactly. The Pareto front is identified as the boundary of this set.
Synthesis Capability: The framework allows for the mechanical construction of strategies (determinizations) that achieve specific trade-offs, provided the target point is "exposed" (optimizable by a weighted sum) or can be approximated by such points. For non-exposed points, the paper notes that while exact synthesis via a single weighted sum may fail, the point can be approximated arbitrarily closely by exposed points (Straszewicz's Theorem).
Limitations: The authors modestly note that the sufficient conditions for the existence of exact optimal determinizations (Scott-closedness of achievable sets) are not always easy to verify. Furthermore, the current framework is limited to a simple imperative language (pGCL) and does not yet support procedures, recursion, heap manipulation, or continuous distributions. Objectives like discounted rewards or long-run averages are also outside the current scope.

In summary, this work bridges the gap between deductive program verification and multiobjective MDP theory, offering a unified calculus for reasoning about trade-offs in probabilistic programs with nondeterminism, even in infinite-state settings.