J-P: MDP. FP. PP.: Characterizing Total Expected Rewards in Markov Decision Processes as Least Fixed Points with an Application to Operational Semantics of Probabilistic Programs (Technical Report)

TL;DR

This paper generalizes the characterization of expected rewards in Markov decision processes (MDPs) using least fixed points, extending applicability to models with infinite rewards, and applies this to probabilistic program semantics.

Contribution

It introduces a generalized least fixed point framework for expected rewards in MDPs without finiteness restrictions, enabling new verification methods.

Findings

Provides a fixed point characterization for infinite reward MDPs.

Demonstrates soundness of weakest-preexpectation calculi.

Applies the framework to probabilistic program semantics.

Abstract

Markov decision processes (MDPs) with rewards are a widespread and well-studied model for systems that make both probabilistic and nondeterministic choices. A fundamental result about MDPs is that their minimal and maximal expected rewards satisfy Bellmann's optimality equations. For various classes of MDPs - notably finite-state MDPs, positive bounded models, and negative models - expected rewards are known to be the least solution of those equations. However, these classes of MDPs are too restrictive for probabilistic program verification. In particular, they assume that all rewards are finite. This is already not the case for the expected runtime of a simple probabilisitic program modeling a 1-dimensional random walk. In this paper, we develop a generalized least fixed point characterization of expected rewards in MDPs without those restrictions. Furthermore, we demonstrate how said characterization can be leveraged to prove weakest-preexpectation-style calculi sound with respect to an operational MDP model.