### Abstract

We present a formalization of Markov Decision Processes with rewards. In particular we first build on Hölzl's formalization of MDPs (AFP entry: Markov_Models) and extend them with rewards. We proceed with an analysis of the expected total discounted reward criterion for infinite horizon MDPs. The central result is the construction of the iteration rule for the Bellman operator. We prove the optimality equations for this operator and show the existence of an optimal stationary deterministic solution. The analysis can be used to obtain dynamic programming algorithms such as value iteration and policy iteration to solve MDPs with formal guarantees. Our formalization is based on chapters 5 and 6 in Puterman's book "Markov Decision Processes: Discrete Stochastic Dynamic Programming".

### License

BSD License

### Topics

- Mathematics/Probability theory

### Session MDP-Rewards

- Bounded_Functions
- Blinfun_Util
- MDP_reward_Util
- MDP_cont
- MDP_disc
- MDP_reward

### Used by

- Verified Algorithms for Solving Markov Decision Processes

## Cite

×

MDP-Rewards-AFP

    @article{MDP-Rewards-AFP,
      author  = {Maximilian Schäffeler and Mohammad Abdulaziz},
      title   = {Markov Decision Processes with Rewards},
      journal = {Archive of Formal Proofs},
      month   = {December},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/MDP-Rewards.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 28, 2021 : Isabelle2021-1