Email

tobias.winkler at cs.rwth-aachen.de

Address

Room 4231
Ahornstraße 55
D-52074 Aachen

I am a PhD candidate in the Software Modeling and Verification Group headed by Professor Joost-Pieter Katoen. Moreover, I am associated with the research training group UnRAVel.

Research

My research focuses on formal verification of probabilistic systems, both from a theoretical and practical point of view. More specifically, my research interests include:

• Probabilistic Model Checking: Probabilistic Pushdown Automata, Markov Decision Processes, Stochastic Games, Multi-Objective Controller Synthesis, Temporal Logics, Certificates
• Quantitative Program Analysis: Probabilistic Programs, Weighted Programs, Semi-automatic Loop Verification, Strategy Synthesis, Termination Analysis

Thesis projects

If you are interested in writing a Bachelor/Master’s thesis in any of the areas mentioned above please contact thesis at i2.informatik.rwth-aachen.de for a general request. I am currently supervising or have supervised the following thesis projects:

Ongoing thesis projects

• An Automata-based Semantics for the Probabilistic ReDiP Language (working title) – Master’s thesis.

Past thesis projects

• Distributional Invariants for Probabilistic Programs – Daniel Zilken, Master’s thesis. 2024. (Joint supervision with Kevin Batz).
• Most Probable Explanations in Bayesian Networks via Weighted Programming – Dinis Vitorino, Bachelor’s thesis. 2024. (Joint supervision with Kevin Batz).
• Model Checking Probabilistic PDA vs Unambiguous Automata – Anastasiia Petrova, Bachelor’s thesis. 2023.
• Invariant-based Strategy Synthesis for Nondeterministic Probabilistic Programs – Tom Biskup, Master’s thesis. 2022. (Joint supervision with Kevin Batz)
  Tom has received the Berthold Vöcking Master Award for his thesis.
• Pushdown and Expectation Transformer Semantics of Probabilistic Recursive Programs with Nested Conditioning – Johannes Lehmann, Master’s thesis. 2022.
• POMDP-based Execution Models for Probabilistic Programs with Partial Observability – Christina Gehnen, Master’s thesis. 2022. (Joint supervision with Alex Bork)
• Automatic Verification of Loop Invariants in Weighted Programs – Ben Sturgis, Bachelor’s thesis. 2022. (Joint supervision with Kevin Batz)
• Inference in Discrete Probabilistic Programs using Probability Generating Functions – Christian Blumenthal, Master’s thesis. 2022. (Joint supervision with Lutz Klinkenberg)
• Implementation of an LTL Model Checker for Probabilistic Pushdown Automata – Laura Bamberger, Bachelor’s thesis. 2022.
• Proving Termination of Probabilistic Recursive Programs via SMT-Solving – Leo Mommers, Bachelor’s thesis. 2022.
• Compositional Control-Flow Reduction for Probabilistic Model Checking – Naomi Barth, Bachelor’s thesis. 2021.
• Automata-based Model Checking of Recursive Systems – Christina Gehnen, Bachelor’s thesis. 2020.
  Christina has received an award from the Fachgruppe Informatik for her thesis.
  

Student assistants

I am not supervising any research student assistants at the moment. In the past, I have supervised our research student assistants Johannes Lehmann, Christina Gehnen, Adrian Gallus, Tom Biskup, Samuel Rode, and our DAAD RISE intern Arman Ozcan.

Teaching

Past semesters

• Formale Sprachen, Automaten und Prozesse (“FoSAP”; Vorlesung) SS24
• Theoretical Foundations of the UML (Lecture) WS23/24
• Datenstrukturen und Algorithmen (“DSAL”; Vorlesung) SS23
• Probabilistic Programming (Lecture) WS22/23
• Probabilistic Programming (Seminar) WS22/23
• Static Program Analysis (Lecture) SS22
• Formal Verification Meets Machine Learning (Seminar) WS21/22
• Modelling and Verification of Probabilistic Systems (“MVPS”; Lecture) SS21
• Probabilistic Programming (Lecture) WS20/21
• Probabilistic Programming (Seminar) WS20/21
• Datenstrukturen und Algorithmen (“DSAL”; Vorlesung) SS20
• Introduction to Program Analysis (Proseminar) SS20

Awards

• Our paper Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains with Hannah Mertens, Joost-Pieter Katoen and Tim Quatmann has received the EAPLS best paper award at ETAPS 2024.
• Our paper Generating Functions for Probabilistic Programs with Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen and Joshua Moerman) has received the best paper award at LOPSTR 2020.
• I was awarded the Springorum Medal in 2020 for receiving a master’s degree with distinction.

Peer Review

Journals

• Logical Methods in Computer Science (LMCS) 2022 (reviewer)
• Formal Methods in System Design (FMSD) 2021 (external reviewer)

Conferences & Workshops

• TACAS 2025 (external reviewer)
• STACS 2025 (external reviewer)
• IJCAR 2024 (external reviewer)
• CAV 2024 (PC member Artifact Evaluation / external reviewer)
• AAMAS 2024 (external reviewer)
• SODA 2024 (external reviewer)
• MFCS 2023 (external reviewer)
• ATVA 2023 (external reviewer)
• SYNT 2023 @CAV 2023 (PC member)
• POPL 2023 (external reviewer)
• ICTAC 2022 (external reviewer)
• CONCUR 2022 (external reviewer)
• ICALP 2022 (external reviewer)
• LICS 2022 (external reviewer)
• CAV 2022 (PC member Artifact Evaluation / external reviewer)
• POPL 2022 (external reviewer)
• CONCUR 2021 (external reviewer)
• CAV 2021 (PC member Artifact Evaluation / external reviewer)
• FoSSaCS 2021 (external reviewer)

Selected Talks

• Certifying Positive Almost Sure Termination of Probabilistic Pushdown Automata. Conference talk at Highlights 2024. Bordeaux, France.
• Programmtic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs. Conference talk at POPL 2024. London, UK.
• Probabilistic Language Inclusion Problems. Guest Talk at IMDEA Software Institute, 2023. Madrid, Spain.
• On Certificates, Expected Runtimes, and Termination in Probabilistic Pushdown Automata. Conference talk at LICS 2023. Boston, USA.
• Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration. Conference talk at TACAS 2023. Paris, France.
• Model Checking Temporal Properties of Probabilistic Recursive Programs. Conference talk at FoSSaCS 2022. Munich, Germany.
• Out of Control: Reducing Probabilistic Models by Control State Elimination. Conference talk at VMCAI 2022. Philadelphia, USA.
• On the Complexity of Reachability in Parametric MDPs. Conference talk at CONCUR 2019. Amsterdam, The Netherlands.

Publications

You can also find me on dblp and Google Scholar.

2025
[bibtex] @inbook{JPMFP2025, title = {J-P: MDP. FP. PP}, author = {Kevin Batz and Benjamin Lucien Kaminski and Christoph Matheja and Tobias Winkler}, publisher = {Springer}, booktitle = {LNCS}, volume = {15260}, pages = {255-302}, type = {Book Chapter}, year = {2025}, doi = {10.1007/978-3-031-75783-9_11}, url = { https://publications.rwth-aachen.de/record/999819}, }× [issue]	Kevin Batz, Benjamin Lucien Kaminski, Christoph Matheja, Tobias Winkler. J-P: MDP. FP. PP, Volume 15260 of LNCS, 255-302, Springer, 2025.
2024
[bibtex] @article{PSSRNPP2024, title = {Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs}, author = {Kevin Batz and Tom Jannik Biskup and Joost-Pieter Katoen and Tobias Winkler}, publisher = {ACM}, journal = {Proceedings of the ACM on programming languages}, volume = {8}, pages = {pages 93}, type = {Journal Article}, year = {2024}, doi = {10.1145/3632935}, url = { https://publications.rwth-aachen.de/record/979194}, }× [issue]	Kevin Batz, Tom Jannik Biskup, Joost-Pieter Katoen, Tobias Winkler. Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs, Proceedings of the ACM on programming languages 8, pages 93, ACM, 2024.
[bibtex] @masterthesis{C2024, title = {Complexity and decidability of multi-objective stochastic games}, author = {Tobias Winkler}, publisher = {RWTH Aachen University}, institution = {RWTH Aachen University}, pages = {1 Online-Ressource : Illustrationen}, type = {Master Thesis}, year = {2024}, doi = {10.18154/RWTH-2024-02592}, url = { https://publications.rwth-aachen.de/record/980848}, }× [issue]	Tobias Winkler. Complexity and decidability of multi-objective stochastic games, Master Thesis, RWTH Aachen University, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2024.
[bibtex] @conference{ACEVTSDMC2024, title = {Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains}, author = {Hannah Mertens and Joost-Pieter Katoen and Tim Quatmann and Tobias Winkler}, publisher = {Springer}, booktitle = {LNCS}, volume = {14571}, pages = {237-257}, type = {Conference Paper}, year = {2024}, doi = {10.1007/978-3-031-57249-4_12}, url = { https://publications.rwth-aachen.de/record/990356}, }× [issue]	Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann, Tobias Winkler. Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains, 30. International Conference TACAS (TACAS 2024), Volume 14571 of LNCS, 237-257, Springer, 2024.
[bibtex] @conference{MDPSPMRO2024, title = {Markov Decision Processes with Sure Parity and Multiple Reachability Objectives}, author = {Raphael Jean Berthon and Joost-Pieter Katoen and Tobias Winkler}, publisher = {Springer}, booktitle = {LNCS}, volume = {15050}, pages = {203-220}, type = {Conference Paper}, year = {2024}, doi = {10.1007/978-3-031-72621-7_14}, url = { https://publications.rwth-aachen.de/record/997143}, }× [issue]	Raphael Jean Berthon, Joost-Pieter Katoen, Tobias Winkler. Markov Decision Processes with Sure Parity and Multiple Reachability Objectives, 18. International Conference on Reachability Problems (RP 2024), Volume 15050 of LNCS, 203-220, Springer, 2024.
Show all