Skip to content
Date: 27th August 2021
Time: 14:00 - 16:00
Location: Online

Title: A Formalisation of Markov Decision Processes
Speaker: Mark Chevallier

In this talk I will discuss my formalisation of Markov Decision Processes. I will talk about the formalised model, formal proofs of value convergence and of the existence of an optimal policy by vector representation of functions on the states. My approach was based on Martin Puterman’s proof, and in the process of formalisation I found a small flaw in it, which was addressed and fixed.