Tobias Winkler: Programming and Verifying Uncertain Phenomena


Tobias Winkler’s research is focused on the algorithmic analysis of stochastic models in a broad sense. As student assistant in UNRAVEL, he established (together with Junges) complexity results for parameter synthesis. In particular, it was shown that most parameter synthesis problems are as hard as deciding whether a formula in the existential theory of reals (ETR) is satisfiable or not. Winkler established determinacy of such games and presented strategy and computational complexity results for stochastic two-player games with lexicographic reachability and safety objectives. Lexicographic order allows to consider multiple objectives with a strict preference order over the satisfaction of the objectives. His algorithm computes the lexicographically optimal strategies via a reduction to computation of optimal strategies in a sequence of single-objectives games. Winkler also developed an algorithm to approximate the Pareto frontier of the achievable values to a given precision for a stochastic game with multiple objectives. Winkler currently considers reduction techniques based on static analysis for Markov decision processes and on the automated verification of recursive probabilistic programs.