Tim Quatmann

Email: tim.quatmann at 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

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

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

2023
DOI	Tim Quatmann. Verification of multi-objective Markov models, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2023.
DOI	Arnd Hartmanns, Sebastian Junges, Tim Quatmann, Maximilian Weininger. A Practitioner’s Guide to MDP Model Checking Algorithms, Tools and algorithms for the construction and analysis of systems : 29th international conference, TACAS 2023, held as part of the european joint conferences on theory and practice of software, ETAPS 2022, paris, france, april 22–27, 2023, proceedings, part I / edited by sriram sankaranarayanan, natasha sharygina, 469-488, Springer Nature Switzerland, 2023.
2022
DOI	Tim Quatmann, Sebastian Junges, Joost-Pieter Katoen. Markov automata with multiple objectives, 33-86, Springer Science + Business Media B.V, 2022.
DOI	Hans Christian Hensel, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, Matthias Volk. The probabilistic model checker STORM, 589-610, Springer, 2022.
DOI	Alexander Nikolai Bork, Joost-Pieter Katoen, Tim Quatmann. Under-Approximating Expected Total Rewards in POMDPs, Tools and algorithms for the construction and analysis of systems : 28th international conference, TACAS 2022, held as part of the european joint conferences on theory and practice of software, ETAPS 2022, munich, germany, april 2–7, 2022, proceedings, part II / edited by dana fisman, grigore rosu, 22-40, Springer International Publishing, 2022.
2021
DOI	Tim Quatmann, Joost-Pieter Katoen. Multi-objective Optimization of Long-run Average and Total Rewards, Tools and algorithms for the construction and analysis of systems : 27th international conference, TACAS 2021, held as part of the european joint conferences on theory and practice of software, ETAPS 2021, luxembourg city, luxembourg, march 27 - april 1, 2021, proceedings, part I, 230-249, Springer International Publishing, 2021.
DOI	Carlos E. Budde, Arnd Hartmanns, Michaela Klauck, Jan Křetínský, David Parker, Tim Quatmann, Andrea Turrini, Zhen Zhang. On Correctness, Precision, and Performance in Quantitative Verification : QComp 2020 Competition Report, Leveraging applications of formal methods, verification and validation : Tools and trends : 9th international symposium on leveraging applications of formal methods, ISoLA 2020, rhodes, greece, october 20–30, 2020, proceedings, part IV / edited by tiziana margaria, bernhard steffen, 216-241, Springer International Publishing ; Cham : Imprint: Springer, 2021.
2020
DOI	Florent Delgrange, Joost-Pieter Katoen, Tim Quatmann, Mickael Randour. Simple Strategies in Multi-Objective MDPs, Tools and algorithms for the construction and analysis of systems : 26th international conference, TACAS 2020, held as part of the european joint conferences on theory and practice of software, ETAPS 2020, dublin, ireland, april 25–30, 2020, proceedings, part I / edited by armin biere, david parker, 346-364, Springer International Publishing, 2020.
DOI	Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann. Multi-cost Bounded Tradeoff Analysis in MDP, 1483-1522, Springer Science + Business Media B.V., 2020.
DOI	Alexander Nikolai Bork, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann. Verification of Indefinite-Horizon POMDPs, Automated technology for verification and analysis : 18th international symposium, ATVA 2020, hanoi, vietnam, october 19-23, 2020 : proceedings / dang van hung, oleg sokolsky (eds.), 288-304, Springer, 2020.
2019
DOI	Ernst Moritz Hahn, Arnd Hartmanns, Hans Christian Hensel, Michaela Klauck, Joachim Klein, Jan Křetínský, David Parker, Tim Quatmann, Enno Ruijters, Marcel Steinmetz. The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models : (QComp 2019 Competition Report), Tools and algorithms for the construction and analysis of systems : 25th international conference, TACAS 2019, held as part of the european joint conferences on theory and practice of software, ETAPS 2019, prague, czech republic, april 6-11, 2019 : proceedings. - Part 3: 25 years of TACAS: TOOLympics : held as part of ETAPS 2019, prague, czech republic, april 6-11, 2019 : proceedings / dirk beyer, marieke huisman, fabrice kordon, bernhard steffen (eds.), 69-92, Springer Open, 2019.
DOI	Arnd Hartmanns, Michaela Klauck, David Parker, Tim Quatmann, Enno Ruijters. The Quantitative Verification Benchmark Set, Tools and algorithms for the construction and analysis of systems : 25th international conference, TACAS 2019, held as part of the european joint conferences on theory and practice of software, ETAPS 2019, prague, czech republic, april 6-11, 2019 : proceedings / tomáš vojnar, lijun zhang (eds.). - Part 1, 344-350, Springer Open, 2019.
DOI	Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, Bernd Becker, Ralf Wimmer, Leonore Winterer. Correct-by-construction policies for POMDPs, Proceedings of the fifth international workshop on symbolic-numeric methods for reasoning about CPS and IoT, 6-8, ACM Press, 2019.
2018
DOI	Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann. Multi-cost Bounded Reachability in MDP, Tools and algorithms for the construction and analysis of systems : 24th international conference, TACAS 2018, held as part of the european joint conferences on theory and practice of software, ETAPS 2018, thessaloniki, greece, april 14-20, 2018, proceedings, part II / edited by dirk beyer, marieke huisman, 320-339, Springer International Publishing, 2018.
DOI	Tim Quatmann, Joost-Pieter Katoen. Sound Value Iteration, Computer aided verification : 30th international conference, CAV 2018, held as part of the federated logic conference, FloC 2018, oxford, UK, july 14-17, 2018, proceedings, part I / edited by hana chockler, georg weissenbacher, 643-661, Springer, 2018.
	Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen, Bernd Becker. Finite-State Controllers of POMDPs using Parameter Synthesis, Uncertainty in artificial intelligence : Proceedings of the thirty-fourth conference (2018), august 6-10, 2018, monterey, california, USA / edited by amir globerson, google inc. and tel aviv university; ricardo silva, university college london and the alan turing institute ; general chairs: Gal elidan, google inc. and the hebrew university, israel kristian kersting, TU darmstadt, germany, 519-529, AUAI Press, 2018.
	Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen, Bernd Becker. Finite-State Controllers of POMDPs using Parameter Synthesis, 34th conference on uncertainty in artificial intelligence 2018 : Monterey, california, USA, 6-10 august 2018 / editors: Amir globerson, ricardo silva ; association for uncertainty in artificial intelligence (AUAI). - Volume 1, 519-529, Curran Associates, Inc., 2018.
2017
DOI	Tim Quatmann, Sebastian Junges, Joost-Pieter Katoen. Markov Automata with Multiple Objectives, Computer aided verification : 29th international conference, CAV 2017 : Heidelberg, germany, july 24-28, 2017 : proceedings / rupak majumdar, viktor kunčak (eds.). - Part 1, 140-159, Springer, 2017.
2016
DOI	Tim Quatmann, Hans Christian Dehnert, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen. Parameter Synthesis for Markov Models: Faster Than Ever, Automated technology for verification and analysis : 14th international symposium, ATVA 2016, chiba, japan, october 17-20, 2016, proceedings / edited by cyrille artho, axel legay, doron peled, 50-67, Springer International Publishing, 2016.
2015
DOI	Tim Quatmann, Nils Jansen, Hans Christian Dehnert, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Counterexamples for Expected Rewards, FM 2015: formal methods : 20th international symposium, oslo, norway, june 24 - 26, 2015 ; proceedings / nikolaj bjørner; frank de boer (eds.), 435-452, Springer, 2015.