Multiobjective Preexpectation Reasoning for Probabilistic Programs

arXiv (Cornell University)

Abstract

Probabilistic programs with nondeterminism model planning problems in which a strategy resolves the nondeterminism to optimize an expected outcome. We study the multiobjective setting, optimizing several outcomes at once along a Pareto front, and provide a deductive, program-level account of strategy synthesis. Its core is a multiobjective preexpectation transformer mapping a tuple of postexpectations to the set of simultaneously achievable values, an element of the convex Hoare powerdomain. It conservatively extends weakest preexpectations and lifts standard loop rules. We develop rules to synthesize witnessing strategies as mixed determinizations that randomize over non-probabilistic determinizations. We prove the transformer and synthesis rules sound against an operational MDP semantics, without requiring a finite state space: our approach can be seen as a symbolic approach - at program level - for multiobjective optimization over infinite MDPs. We demonstrate our machinery using various case studies.

Authors 6

1. Lena Verscht

   Cornell University

   Affiliation as printed

   Cornell University , USA

2. Hannah Mertens

   Cornell University

   Affiliation as printed

   Cornell University , USA

3. Kevin Batz

   Cornell University

   Affiliation as printed

   Cornell University , USA

4. Sebastian Junges

   Cornell University

   Affiliation as printed

   Cornell University , USA

5. Benjamin Lucien Kaminski Aachen

   University College London · RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , Aachen , Germany,

   University College London , London , UK;

6. Joost-Pieter Katoen

   Cornell University

   Affiliation as printed

   Cornell University , USA