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

I am a developer of the probabilistic model checker Storm

Research Activities

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

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, 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021), Volume 12651 of LNCS, 230-249, Springer, 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},
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, 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},
pages = {22 Seiten},
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, 22 Seiten, 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 = {Theoretical Computer Science and General Issues},
volume = {12078},
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, Tools and Algorithms for the Construction and Analysis of Systems 2020 (TACAS 2020), Volume 12078 of Theoretical Computer Science and General Issues, 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 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 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), 25th 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, 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 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, 5th 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},
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, 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018), Volume 10806 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, 30th 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, 34th 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, 34th 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, 29th 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, 14th International Symposium on Automated Technology for Verification and Analysis (ATVA 2016), Volume 9938 of LNCS, 50-67, Springer, 2016.
2015
DOI [bibtex]
@inbook{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 = {Book Chapter},
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, Volume 9109 of LNCS, 435-452, Springer, 2015.