Thursday, January 28, 2016 - 2:00pm to 3:00pm
Location:2109 Gates & Hillman Centers
Speaker:JOHANNES HÖLZL, Post-doctoral Fellow /JOHANNES%20H%C3%96LZL
For More Information, Contact:avigad @ cmu.edu
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).
A distinctive feature of our formalization is the order-theoretic and coalgebraic view on our concepts: we view transition systems as coalgebras, we view traces as coinductive streams, we provide iterative computation rules for expectations, and we define many properties on traces as least or greatest fixed points.
Johannes Hölzl a post-doc at the Technical University of Munich, were hr completed my PhD in 2013. His PhD supervisor was Tobias Nipkow, the topic was the formalization of measure and probability theory in Isabelle/HOL. He is currently interested in the application of interactive theorem proving to probability theory, especially Markov chain theory and probabilistic programming. He is also co-maintaining Isabelle's analysis and probability theory.
Faculty Host: Jeremy Avigad