Email

tobias.winkler at cs.rwth-aachen.de

Address

Room 4206
Ahornstraße 55
D-52074 Aachen

Phone

+49 241 80 21210

I am a PhD student in the Software Modeling and Verification Group headed by Professor J.-P. Katoen. Moreover, I am an associated doctoral researcher in the research training group UnRAVel.

Research

My research is situated in the formal automatic analysis of probabilistic systems. In particular, my current research goals and interests include:

• Parametric Markov Models
  In parametric Markov models such as Markov chains or MDPs, concrete probabilities may be replaced by real variables – the parameters. Parametric models are key to analyse situations were transition probabilities are unknown but not unrelated across the whole model; or to synthesise such probabilities in a way that a certain property holds. The main theoretical and practical difficulty are the global dependencies between the parameters. One of my research goals is to establish the theoretical complexity of pMDPs and to identify interesting tractable subclasses.
• Stochastic Games
  In my Master’s thesis, I have been working on stochastic two-person games with multiple objectives. In the context of probabilistic model checking, stochastic games are commonly used as a powerful abstraction mechanism to obtain sound bounds on quantitative properties of otherwise huge Markovian models. I have investigated such games under lexicographic reachability objectives and conjunctions of thresholds on reachability properties.
• Probabilistic Programming
  … is nowadays a common paradigm in machine learning. The increasing number of programmers and engineers writing such programs calls for rigorous automatic program analysis, just like for traditional software.
  

Thesis projects

If you are interested in writing a Bachelor/Master’s thesis in any of the areas mentioned above, don’t hesitate to contact me. You can also check our list of open topics.

Current thesis projects

I am currently supervising the following projects:

• Theoretical Aspects of Parametric Markov Decision Processes – Pascal Pauselli, Bachelor’s thesis.
• Model Checking Probabilistic Pushdown Automata beyond omega-Regularity (working title) – Christina Gehnen, Bachelor’s thesis.

Teaching

I’m currently involved in the following teaching activities:

• Datenstrukturen und Algorithmen SS20

2019
[bibtex]	Tobias Winkler, Sebastian Junges, Guillermo A. Pérez, Joost-Pieter Katoen. On the Complexity of Reachability in Parametric Markov Decision Processes, CONCUR 2019, Volume 140 of Leibniz international proceedings in informatics : LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing, August, 2019.