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

A generalized least fixed point characterization of expected rewards in MDPs without restrictions is developed and it is demonstrated how said characterization can be leveraged to prove weakest-preexpectation-style calculi sound with respect to an operational MDP model.

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.

Figures (5)

• Figure 1: Example MDP with infinite state space. Omitted probabilities are 1. Numbers in boxes next to states -- like $r\newline$ or $2$ -- are rewards (see \ref{['sec:expected_rewards_def']}).
• Figure 2: An MDP where no max-optimal scheduler exist at any state $s_i$, $i \in \mathbb{N}$.
• Figure 3: An example $\mathsf{pGCL}$ program. We assume that $r \in \mathbb{Q}_{\geq 0}^{\infty}$ is a constant.
• Figure 4: A reachable fragment of $\mathsf{pGCL}$'s operational MDP $\mathcal{O}$ for the loop from \ref{['fig:running-example-pgcl']}. Program states are denoted by conjunctions of equalities, i.e. $x = n \wedge y=m$ indicates that the current state $\sigma$ satisfies $\sigma(x)=n$ and $\sigma(y)=m$.
• Figure 5: Rules defining the small-step execution relation $\xrightarrow{}$.

Theorems & Definitions (52)

• definition 1: MDPs
• definition 2: Paths
• definition 3: Schedulers
• definition 4: Path Probabilities
• remark 1
• definition 5: Reward Functions
• definition 6: Expected Rewards
• definition 7: Reachability Probabilities
• definition 8: Partial Orders
• definition 9: Complete Lattices