Tim Quatmann

Email: tim.quatmann@cs.rwth-aachen.de
Address: Room 4206
Ahornstraße 55
D-52074 Aachen
Phone: +49 241 80 21210

Research Topics

My research interests include:

Probabilistic model checking
Multi-objective optimization
Synthesis of parametric probabilistic systems
Systems with partial observability

I am a developer of the probabilistic model checker Storm

Research Activities

Year	Activity
2023	Artifact Evaluation Co-Chair for QEST 2023
2022	Member of the Artifact Evaluation Committee for TACAS 2022
2021	Member of the Artifact Evaluation Committee for CAV 2021
2020	Member of the Artifact Evaluation Committee for TACAS 2020
2019	Co-organizer of the Comparison of Tools for the Analysis of Quantitative Formal Models (QComp)

Teaching Activities

Semester	Course
WS 2023	Modeling and Verification of Probabilistic Systems
SS 2023	Model Checking
SS 2022	Model Checking
WS 2021	Theoretical Foundations of the UML
WS 2020	Model Checking
SS 2020	Datenstrukturen und Algorithmen
SS 2019	Formale Systeme, Automaten, Prozesse
WS 2018	Modeling and Verification of Probabilistic Systems
SS 2018	Datenstrukturen und Algorithmen
WS 2017	Theoretical Foundations of the UML
WS 2016	Advanced Model Checking

Publications

Own publications

Supervised theses

2026

Bachelor’s thesis
Belief-tracking policies for partially observable MDPs via randomized finite-state controllers
Ole Dannemeyer
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Tim Quatmann
Consultants: Tobias Winkler, Lisa Pühl
RWTH record for Belief-tracking policies for partially observable MDPs via randomized finite-state controllers BibTeX for Belief-tracking policies for partially observable MDPs via randomized finite-state controllers
Bachelor’s thesis
Semantic equivalences of probabilistic programs and their underlying Markov chains
Philip Strüwer
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Tim Quatmann
Consultants: Daniel Johannes Zilken, Jan-Gustav Michnia
RWTH record for Semantic equivalences of probabilistic programs and their underlying Markov chains BibTeX for Semantic equivalences of probabilistic programs and their underlying Markov chains
Bachelor’s thesis
Integrating KoAT’s push-button probabilistic cost analysis into Caesar
Mats Eblenkamp
RWTH Aachen University
Advisers: Jürgen Giesl, Tim Quatmann
Consultants: Philipp Schroer, Nils Michael Lommen
PDF of Integrating KoAT’s push-button probabilistic cost analysis into Caesar RWTH record for Integrating KoAT’s push-button probabilistic cost analysis into Caesar BibTeX for Integrating KoAT’s push-button probabilistic cost analysis into Caesar

2023

Master’s thesis
Approximate probabilistic bisimulations and quotienting
Timm Spork
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tim Quatmann
RWTH record for Approximate probabilistic bisimulations and quotienting BibTeX for Approximate probabilistic bisimulations and quotienting
Master’s thesis
Representing Markov models by extending the intermediate model checking language
Jialei Yao
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tim Quatmann
RWTH record for Representing Markov models by extending the intermediate model checking language BibTeX for Representing Markov models by extending the intermediate model checking language
Bachelor’s thesis
Automatic algorithm selection for probabilistic model checking using machine learning
Umut Yigit Dural
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tim Quatmann, Alexander Nikolai Bork
RWTH record for Automatic algorithm selection for probabilistic model checking using machine learning BibTeX for Automatic algorithm selection for probabilistic model checking using machine learning
Bachelor’s thesis
Comparison of symbolic maximal end component decomposition algorithms
Felix Faber
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tim Quatmann
RWTH record for Comparison of symbolic maximal end component decomposition algorithms BibTeX for Comparison of symbolic maximal end component decomposition algorithms

2022

Bachelor’s thesis
Verifying parametric Markov models using decision diagrams
Jan Erik Karuc
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tim Quatmann
RWTH record for Verifying parametric Markov models using decision diagrams BibTeX for Verifying parametric Markov models using decision diagrams
Master’s thesis
Markow-Entscheidungsprozesse mit mehreren Agenten : Ein Überblick mit Fokus auf effiziente Aufgabenverteilung
Denis Kuksaus
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tim Quatmann
RWTH record for Markow-Entscheidungsprozesse mit mehreren Agenten : Ein Überblick mit Fokus auf effiziente Aufgabenverteilung BibTeX for Markow-Entscheidungsprozesse mit mehreren Agenten : Ein Überblick mit Fokus auf effiziente Aufgabenverteilung

2021

Master’s thesis
Underapproximations for indefinite-horizon POMDPS
Alexander Nikolai Bork
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Gerhard Lakemeyer
Consultants: Tim Quatmann
RWTH record for Underapproximations for indefinite-horizon POMDPS BibTeX for Underapproximations for indefinite-horizon POMDPS
Master’s thesis
Efficient analysis of time-bounded reachability in markov automata
Mengying Xue
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tim Quatmann
RWTH record for Efficient analysis of time-bounded reachability in markov automata BibTeX for Efficient analysis of time-bounded reachability in markov automata

All records on RWTH Publications

Tim Quatmann

Research Topics

Research Activities

Teaching Activities

Publications

Own publications

2026

2025

2024

2023

2022

2021

Supervised theses

2026

2023

2022

2021