In this talk I will present two algorithmical approaches to static partial order reduction for Markov Decision Processes. These techniques can be used to alleviate the state space explosion problem associated to Model Checking of probabilistic systems. These techniques only use information obtained by a static analysis over the behaviour of the programs and, therefore, can be combined with Symbolic model checking, which has outperformed explicit model checking with respect to the size of systems tractable. The talk is aimed at anyone interested in formal verification. Basic notions about model checking and partial order reductions will be provided, so no prior knowledge is required.

Those algorithms are also joint work with Frank Ciesinski and Christel Baier, from Technische Universität Dresden.