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

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.