Johannes Hölzl

Date: 16:15, Tuesday, February 23, 2016
Speaker: Johannes Hölzl
Venue: TU Wien

Time: 16:15, Day: Tuesday

I will 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.

Posted in RiSE Seminar