Johannes Hölzl
Post-doc at the Technical University of Munich
Markov Chains and Markov Decision Processes in Isabelle/HOL
Abstract:
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).
Bio: 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.