Email Gateway (Dec 28 2021 at 15:03): Email Gateway (Dec 28 2021 at 15:03):From: Lawrence Paulson <lp15@cam.ac.uk>
I’m happy to announce two new entries, both by Maximilian Schäffeler and Mohammad Abdulaziz:
Markov Decision Processes with Rewards
Verified Algorithms for Solving Markov Decision Processes
From the Abstract:
We present a formalization of algorithms for solving Markov Decision Processes (MDPs) with formal guarantees on the optimality of their solutions. In particular we build on our analysis of the Bellman operator for discounted infinite horizon MDPs. From the iterator rule on the Bellman operator we directly derive executable value iteration and policy iteration algorithms to iteratively solve finite MDPs. … Our formalization is based on chapters 5 and 6 in Puterman's book "Markov Decision Processes: Discrete Stochastic Dynamic Programming”.
Both now available at https://www.isa-afp.org !
Larry Paulson
Last updated: Jul 15 2022 at 23:21 UTC