Johannes Hölzl
Post-doc at the Technical University of Munich

Markov Chains and Markov Decision Processes in Isabelle/HOL

I present an extensive formalization of Markov chains (MCs) and Markov decision processes (MDPs), with discrete time and (possibly infinite) discrete state-spaces. The formalization takes a coalgebraic view on the transition systems representing MCs and constructs their trace spaces. On these trace spaces properties like fairness, reachability, and stationary distributions are formalized. Similar to MCs, MDPs are represented as transition systems with a construction for trace spaces.  These trace spaces provide maximal and minimal expectation over all possible non-deterministic decisions. As applications we provide a certifier for finite reachability problems and we relate the denotational semantics and operational semantics of the probabilistic  guarded command language (pGCL).

I'm a post-doc at the Technical University of Munich, were I completed my PhD in 2013. My PhD supervisor was Tobias Nipkow, the topic was the formalization of measure and probability theory in Isabelle/HOL.
Currently, I'm interested in the application of interactive theorem proving to probability theory, especially Markov chain theory and probabilistic programming. Also, I'm co-maintaining Isabelle's analysis and probability theory.

Thursday, January 28, 2016
2:00 PM
Gates & Hillman Centers 2109

Principles of Programming Seminars