Tim Quatmann

quatmann-2
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

2023Artifact Evaluation Co-Chair for QEST 2023
2022Member of the Artifact Evaluation Committee for TACAS 2022
2021Member of the Artifact Evaluation Committee for CAV 2021
2020Member 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 2023Modeling and Verification of Probabilistic Systems
SS 2023Model Checking
SS 2022Model Checking
WS 2021Theoretical Foundations of the UML
WS 2020Model Checking
SS 2020Datenstrukturen und Algorithmen
SS 2019Formale Systeme, Automaten, Prozesse
WS 2018Modeling and Verification of Probabilistic Systems
SS 2018Datenstrukturen und Algorithmen
WS 2017Theoretical Foundations of the UML
WS 2016Advanced Model Checking

2023
DOI fulltext PDF [bibtex]
@phdthesis{VM2023,
title = {Verification of multi-objective Markov models},
author = {Tim Quatmann},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource : Illustrationen},
type = {PhD Thesis},
year = {2023},
doi = {10.18154/RWTH-2023-09669},
url = { https://publications.rwth-aachen.de/record/971553},
}×
[issue] 		Tim Quatmann. Verification of multi-objective Markov models, PhD Thesis, RWTH Aachen University, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2023.
DOI [bibtex]
@conference{APGMMCA2023,
title = {A Practitioner’s Guide to MDP Model Checking Algorithms},
author = {Arnd Hartmanns and Sebastian Junges and Tim Quatmann and Maximilian Weininger},
publisher = {Springer},
booktitle = {LNCS},
volume = {13993},
pages = {469-488},
type = {Conference Paper},
year = {2023},
doi = {10.1007/978-3-031-30823-9_24},
url = { https://publications.rwth-aachen.de/record/972074},
}×
[issue] 		Arnd Hartmanns, Sebastian Junges, Tim Quatmann, Maximilian Weininger. A Practitioner’s Guide to MDP Model Checking Algorithms, International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), Volume 13993 of LNCS, 469-488, Springer, 2023.
2022
DOI fulltext PDF [bibtex]
@conference{UAETRP2022,
title = {Under-Approximating Expected Total Rewards in POMDPs},
author = {Alexander Nikolai Bork and Joost-Pieter Katoen and Tim Quatmann},
publisher = {Springer},
booktitle = {LNCS},
volume = {13244},
pages = {22-40},
type = {Conference Paper},
year = {2022},
doi = {10.1007/978-3-030-99527-0_2},
url = { https://publications.rwth-aachen.de/record/844526},
}×
[issue] 		Alexander Nikolai Bork, Joost-Pieter Katoen, Tim Quatmann. Under-Approximating Expected Total Rewards in POMDPs, 28. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022), Volume 13244 of LNCS, 22-40, Springer, 2022.
2021
DOI [bibtex]
@article{M2021,
title = {Markov automata with multiple objectives},
author = {Tim Quatmann and Sebastian Junges and Joost-Pieter Katoen},
publisher = {Springer},
journal = {Formal methods in system design},
volume = {60(1)},
pages = {pages 33-86},
type = {Journal Article},
year = {2021},
doi = {10.1007/s10703-021-00364-6},
url = { https://publications.rwth-aachen.de/record/816671},
}×
[issue] 		Tim Quatmann, Sebastian Junges, Joost-Pieter Katoen. Markov automata with multiple objectives, Formal methods in system design 60 (1), pages 33-86, Springer, 2021.
DOI fulltext PDF [bibtex]
@conference{MOLATR2021,
title = {Multi-objective Optimization of Long-run Average and Total Rewards},
author = {Tim Quatmann and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {12651},
pages = {230-249},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-72016-2_13},
url = { https://publications.rwth-aachen.de/record/817768},
}×
[issue] 		Tim Quatmann, Joost-Pieter Katoen. Multi-objective Optimization of Long-run Average and Total Rewards, 27. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021), Volume 12651 of LNCS, 230-249, Springer, 2021.
DOI fulltext PDF [bibtex]
@article{TS2021,
title = {The probabilistic model checker STORM},
author = {Hans Christian Hensel and Sebastian Junges and Joost-Pieter Katoen and Tim Quatmann and Matthias Volk},
publisher = {Springer},
journal = {International journal on software tools for technology transfer},
volume = {24(4)},
pages = {pages 589-610},
type = {Journal Article},
year = {2021},
doi = {10.1007/s10009-021-00633-z},
url = { https://publications.rwth-aachen.de/record/822059},
}×
[issue] 		Hans Christian Hensel, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, Matthias Volk. The probabilistic model checker STORM, International journal on software tools for technology transfer 24 (4), pages 589-610, Springer, 2021.
DOI [bibtex]
@conference{OCPPQVQCR2021,
title = {On Correctness, Precision, and Performance in Quantitative Verification: QComp 2020 Competition Report},
author = {Carlos E. Budde and Arnd Hartmanns and Michaela Klauck and Jan Křetínský and David Parker and Tim Quatmann and Andrea Turrini and Zhen Zhang},
publisher = {Springer},
booktitle = {LNCS},
volume = {12479},
pages = {216-241},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-83723-5_15},
url = { https://publications.rwth-aachen.de/record/834796},
}×
[issue] 		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, 9. International Symposium on Leveraging Applications of Formal Methods (ISoLA 2020), Volume 12479 of LNCS, 216-241, Springer, 2021.
2020
DOI fulltext PDF [bibtex]
@conference{SSMOM2020,
title = {Simple Strategies in Multi-Objective MDPs},
author = {Florent Delgrange and Joost-Pieter Katoen and Tim Quatmann and Mickael Randour},
publisher = {Springer},
booktitle = {LNCS},
volume = {12078, Theoretical Computer Science and General Issues},
pages = {346-364},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-45190-5_19},
url = { https://publications.rwth-aachen.de/record/792348},
}×
[issue] 		Florent Delgrange, Joost-Pieter Katoen, Tim Quatmann, Mickael Randour. Simple Strategies in Multi-Objective MDPs, 26. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020), Volume 12078, Theoretical Computer Science and General Issues of LNCS, 346-364, Springer, 2020.
DOI fulltext PDF [bibtex]
@article{MBTAM2020,
title = {Multi-cost Bounded Tradeoff Analysis in MDP},
author = {Arnd Hartmanns and Sebastian Junges and Joost-Pieter Katoen and Tim Quatmann},
publisher = {Springer},
journal = {Journal of automated reasoning},
volume = {64(7)},
pages = {pages 1483-1522},
type = {Journal Article},
year = {2020},
doi = {10.1007/s10817-020-09574-9},
url = { https://publications.rwth-aachen.de/record/794977},
}×
[issue] 		Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann. Multi-cost Bounded Tradeoff Analysis in MDP, Journal of automated reasoning 64 (7), pages 1483-1522, Springer, 2020.
DOI [bibtex]
@conference{VIHP2020,
title = {Verification of Indefinite-Horizon POMDPs},
author = {Alexander Nikolai Bork and Sebastian Junges and Joost-Pieter Katoen and Tim Quatmann},
publisher = {Springer},
booktitle = {LNCS},
volume = {12302},
pages = {288-304},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-59152-6_16},
url = { https://publications.rwth-aachen.de/record/814779},
}×
[issue] 		Alexander Nikolai Bork, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann. Verification of Indefinite-Horizon POMDPs, International Symposium on Automated Technology for Verification and Analysis (ATVA 2020), Volume 12302 of LNCS, 288-304, Springer, 2020.
2019
DOI fulltext PDF [bibtex]
@conference{TCTAQFMQCR2019,
title = {The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models: (QComp 2019 Competition Report)},
author = {Ernst Moritz Hahn and Arnd Hartmanns and Hans Christian Hensel and Michaela Klauck and Joachim Klein and Jan Křetínský and David Parker and Tim Quatmann and Enno Ruijters and Marcel Steinmetz},
publisher = {Springer},
booktitle = {LNCS},
volume = {11429},
pages = {69-92},
type = {Conference Paper},
year = {2019},
doi = {10.1007/978-3-030-17502-3_5},
url = { https://publications.rwth-aachen.de/record/759255},
}×
[issue] 		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), 25. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019), Volume 11429 of LNCS, 69-92, Springer, 2019.
DOI fulltext PDF [bibtex]
@conference{TQVBS2019,
title = {The Quantitative Verification Benchmark Set},
author = {Arnd Hartmanns and Michaela Klauck and David Parker and Tim Quatmann and Enno Ruijters},
publisher = {Springer},
booktitle = {LNCS},
volume = {11427},
pages = {344-350},
type = {Conference Paper},
year = {2019},
doi = {10.1007/978-3-030-17462-0_20},
url = { https://publications.rwth-aachen.de/record/759258},
}×
[issue] 		Arnd Hartmanns, Michaela Klauck, David Parker, Tim Quatmann, Enno Ruijters. The Quantitative Verification Benchmark Set, 25. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019), Volume 11427 of LNCS, 344-350, Springer, 2019.
DOI [bibtex]
@conference{CP2019,
title = {Correct-by-construction policies for POMDPs},
author = {Nils Jansen and Sebastian Junges and Joost-Pieter Katoen and Tim Quatmann and Bernd Becker and Ralf Wimmer and Leonore Winterer},
publisher = {ACM Press},
booktitle = {ACM Digital Library},
pages = {6-8},
type = {Conference Paper},
year = {2019},
doi = {10.1145/3313149.3313366},
url = { https://publications.rwth-aachen.de/record/764541},
}×
[issue] 		Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, Bernd Becker, Ralf Wimmer, Leonore Winterer. Correct-by-construction policies for POMDPs, 5. International Workshop on Symbolic-Numeric Methods for Reasoning about CPS and IoT (SNR) held as part of the 12th Cyber-Physical Systems and Internet-of-Things Week (CPS-IoT Week) (SNR '19), ACM Digital Library, 6-8, ACM Press, 2019.
2018
DOI fulltext PDF [bibtex]
@conference{MBRM2018,
title = {Multi-cost Bounded Reachability in MDP},
author = {Arnd Hartmanns and Sebastian Junges and Joost-Pieter Katoen and Tim Quatmann},
publisher = {Springer},
booktitle = {LNCS},
volume = {10806, Part 2},
pages = {320-339},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-89963-3_19},
url = { https://publications.rwth-aachen.de/record/745801},
}×
[issue] 		Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann. Multi-cost Bounded Reachability in MDP, 24. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018), Volume 10806, Part 2 of LNCS, 320-339, Springer, 2018.
DOI fulltext PDF [bibtex]
@conference{SVI2018,
title = {Sound Value Iteration},
author = {Tim Quatmann and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {10981},
pages = {643-661},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-96145-3_37},
url = { https://publications.rwth-aachen.de/record/753074},
}×
[issue] 		Tim Quatmann, Joost-Pieter Katoen. Sound Value Iteration, 30. International Conference on Computer Aided Verification (CAV 2018), Volume 10981 of LNCS, 643-661, Springer, 2018.
fulltext PDF [bibtex]
@conference{FSCPPS2018,
title = {Finite-State Controllers of POMDPs using Parameter Synthesis},
author = {Sebastian Junges and Nils Jansen and Ralf Wimmer and Tim Quatmann and Leonore Winterer and Joost-Pieter Katoen and Bernd Becker},
publisher = {AUAI Press},
pages = {519-529},
type = {Conference Paper},
year = {2018},
url = { https://publications.rwth-aachen.de/record/754534},
}×
[issue] 		Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen, Bernd Becker. Finite-State Controllers of POMDPs using Parameter Synthesis, 34. Conference on Uncertainty in Artificial Intelligence (UAI 34), 519-529, AUAI Press, 2018.
[bibtex]
@conference{FSCPPS2018,
title = {Finite-State Controllers of POMDPs using Parameter Synthesis},
author = {Sebastian Junges and Nils Jansen and Ralf Wimmer and Tim Quatmann and Leonore Winterer and Joost-Pieter Katoen and Bernd Becker},
publisher = {Curran Associates, Inc.},
pages = {519-529},
type = {Conference Paper},
year = {2018},
url = { https://publications.rwth-aachen.de/record/794908},
}×
[issue] 		Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen, Bernd Becker. Finite-State Controllers of POMDPs using Parameter Synthesis, 34. Conference on Uncertainty in Artificial Intelligence (UAI 34), 519-529, Curran Associates, Inc., 2018.
2017
DOI [bibtex]
@conference{MAMO2017,
title = {Markov Automata with Multiple Objectives},
author = {Tim Quatmann and Sebastian Junges and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {10426},
pages = {140-159},
type = {Conference Paper},
year = {2017},
doi = {10.1007/978-3-319-63387-9_7},
url = { https://publications.rwth-aachen.de/record/713574},
}×
[issue] 		Tim Quatmann, Sebastian Junges, Joost-Pieter Katoen. Markov Automata with Multiple Objectives, 29. International Conference on Computer-Aided Verification (CAV 2017), Volume 10426 of LNCS, 140-159, Springer, 2017.
2016
DOI [bibtex]
@conference{PSMMFTE2016,
title = {Parameter Synthesis for Markov Models: Faster Than Ever},
author = {Tim Quatmann and Hans Christian Dehnert and Nils Jansen and Sebastian Junges and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {9938},
pages = {50-67},
type = {Conference Paper},
year = {2016},
doi = {10.1007/978-3-319-46520-3_4},
url = { https://publications.rwth-aachen.de/record/681503},
}×
[issue] 		Tim Quatmann, Hans Christian Dehnert, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen. Parameter Synthesis for Markov Models: Faster Than Ever, 14. International Symposium on Automated Technology for Verification and Analysis (ATVA 2016), Volume 9938 of LNCS, 50-67, Springer, 2016.
2015
DOI [bibtex]
@conference{CER2015,
title = {Counterexamples for Expected Rewards},
author = {Tim Quatmann and Nils Jansen and Hans Christian Dehnert and Ralf Wimmer and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker},
publisher = {Springer},
booktitle = {LNCS},
volume = {9109},
pages = {435-452},
type = {Conference Paper},
year = {2015},
doi = {10.1007/978-3-319-19249-9_27},
url = { https://publications.rwth-aachen.de/record/541095},
}×
[issue] 		Tim Quatmann, Nils Jansen, Hans Christian Dehnert, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Counterexamples for Expected Rewards, 20. international symposium Formal Methods (FM 2015), Volume 9109 of LNCS, 435-452, Springer, 2015.