Since January 2023, I am working as a research engineer for verification of planning and decision making in autonomous systems at Bosch Research in Renningen.
I successfully defended my PhD thesis entitled “On the Connection of Probabilistic Model Checking, Planning, and Learning” at the chair of Prof. Holger Hermanns in June 2022. In November 2017, I started working at the chair as a PhD student in the area of quantitative verification and Markov decision processes, especially at the interface of these topics to automatic planning and the AI community.
I studied Computer Science at Saarland University where I received my Master’s degree (honor’s degree, Günter-Hotz-Medal) in March 2018 and my Bachelor’s degree in July 2016.
Publications
| Year | Publication |
|---|---|
| 2022 | Timo P. Gros, Holger Hermanns, Jörg Hoffmann, Michaela Klauck, Marcel Steinmetz: Analyzing neural network behavior through deep statistical model checking STTT 2022 |
| 2022 | Arnd Hartmanns, Michaela Klauck: The modest state of learning, sampling, and verifying strategies ISoLA 2022 |
| 2022 | Michaela Klauck: On the Connection of Probabilistic Model Checking, Planning, and Learning for System Verification PhD Thesis at Saarland University |
| 2022 | Timo P. Gros, Holger Hermanns, Joerg Hoffmann, Michaela Klauck, Maximilian A. Köhl, Verena Wolf: MoGym: Using Formal Models for Training and Verifying Decision-making Agents CAV 2022 |
| 2022 | David Groß, Michaela Klauck, Timo P. Gros, Marcel Steinmetz, Jörg Hoffmann, Stefan Gumhold: Glyph-Based Visual Analysis of Q-Learning Based Action Policy Ensembles on Racetrack IV 2022 Best Paper Award |
| 2021 | Michaela Klauck, Holger Hermanns: A Modest Approach to Dynamic Heuristic Search in Probabilistic Model Checking QEST 2021 |
| 2021 | Timo P. Gros, Daniel Höller, Jörg Hoffmann, Michaela Klauck, Hendrik Meerkamp, Verena Wolf: DSMC Evaluation Stages: Fostering Robust and Safe Behavior in Deep Reinforcement Learning QEST 2021 |
| 2021 | Maximilian A. Köhl, Michaela Klauck, Holger Hermanns: Momba: JANI meets Python TACAS (2) 2021 |
| 2020 | Christel Baier, Maria Christakis, Timo P. Gros, David Groß, Stefan Gumhold, Holger Hermanns, Jörg Hoffmann, Michaela Klauck: Lab Conditions for Research on Explainable Automated Decisions TAILOR 2020 Racetrack Website |
| 2020 | Timo P. Gros, David Groß, Stefan Gumhold, Jörg Hoffmann, Michaela Klauck, Marcel Steinmetz: TraceVis: Towards Visualization for Deep Statistical Model Checking ISoLA (4) 2020 |
| 2020 | 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 ISoLA (4) 2020 |
| 2020 | Rasha Faqeh, Christof Fetzer, Holger Hermanns, Jörg Hoffmann, Michaela Klauck, Maximilian A. Köhl, Marcel Steinmetz, Christoph Weidenbach: Towards Dynamic Dependable Systems Through Evidence-Based Continuous Certification ISoLA (2) 2020 |
| 2020 | Christel Baier, Clemens Dubslaff, Holger Hermanns, Michaela Klauck, Sascha Klüppelholz, Maximilian A. Köhl: Components in Probabilistic Systems: Suitable by Construction ISoLA (1) 2020 |
| 2020 | Timo P. Gros, Holger Hermanns, Jörg Hoffmann, Michaela Klauck, Marcel Steinmetz: Deep Statistical Model Checking FORTE 2020 Talk Video |
| 2020 | Michaela Klauck, Marcel Steinmetz, Jörg Hoffmann, Holger Hermanns: Bridging the Gap Between Probabilistic Model Checking and Probabilistic Planning: Survey, Compilations, and Empirical Comparison Journal of Artificial Intelligence Research, Volume 68, 247-310, 2020, (first link includes online appendix) |
| 2020 | Jörg Hoffmann, Holger Hermanns, Michaela Klauck, Marcel Steinmetz, Erez Karpas, Daniele Magazzeni: Let’s Learn their Language? A Case for Planning with Automata-Network Languages from Model Checking AAAI 2020: 13569-13575, Senior Member Track |
| 2019 | Arnd Hartmanns, Michaela Klauck, David Parker, Tim Quatmann, Enno Ruijters: The Quantitative Verification Benchmark Set TACAS (1) 2019: 344-350. |
| 2019 | Ernst Moritz Hahn, Arnd Hartmanns, Christian Hensel, Michaela Klauck, Joachim Klein, Jan Kretí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) TACAS (3) 2019: 69-92. |
| 2018 | Michaela Klauck, Marcel Steinmetz, Jörg Hoffmann, Holger Hermanns: Compiling Probabilistic Model Checking into Probabilistic Planning ICAPS 2018: 150-154. Technical Report The current version of the script to translate JANI MDP models with a restricted syntax into PPDDL used in these papers can be found here. |
| 2017 | Michaela Klauck, Yusuke Sugano, Andreas Bulling: Noticeable or Distractive? A Design Space for Gaze-Contingent User Interface Notifications CHI EA 2017: 1779-1786. |
Tools
Modysh (formerly: Modest FRET-π LRTDP)
We bridged probabilistic planning to probabilistic model checking based on the results of our evaluation in Compiling Probabilistic Model Checking into Probabilistic Planning and Bridging the Gap Between Probabilistic Model Checking and Probabilistic Planning: Survey, Compilations, and Empirical Comparison. We implemented and extended the functionality of FRET-π LRTDP in The Modest Toolset. FRET-π LRTDP has originally been implemented in the probabilistic version of Fast Downward, a planning tool, by Marcel Steinmetz. The latest release of Modysh is integrated in the Modest Toolset and can be downloaded here.
In the paper A Modest Approach to Dynamic Heuristic Search in Probabilistic Model Checkingwe present the tool Modysh which implements the modified, adapted and extended version of the original algorithms with much broader functionality. The current interactive result tables comparing it to other state-of-the-art model checkers and planners like in QComp can be found here for QComp benchmarks and there for additional QVBS benchmarks.
Competitions
I was involved in the development process of QComp, the Comparison of Tools for the Analysis of Quantitative Formal Models, which took place in 2019 at TOOLympics at TACAS for the first time. In 2020, I was part of the organization team and responsible for the technical setup and tool execution of the competition. In addition, I assisted in the development process of the Quantitative Verification Benchmark Set (QVBS).
Center for Perspicuous Systems (CPEC)
I am part of the team working in the Center for Perspicuous Systems (CPEC), the collaborative research center 248 Foundations of Perspicuous Software Systems, funded by the DFG. In this project researchers from TU Dresden, TU Tübingen and Saarland Informatics Campus in Saarbrücken collaborate. More precisely, I am involved in the projects C2, C3 and C6.
Since May 2020 I am the PhD representative on the CPEC Board. All ideas or suggestions which I can present or discuss in the CPEC Board for you are very welcome, just send me a mail.
Community Service
Since 2017, I am a sub-reviewer for TACAS, the International Conference on Tools and Algorithms for the Construction and Analysis of Systems.
In 2020, I was part of the Artifact Evaluation Committee of TACAS.
In addition, I assisted in the organization of The 35th Annual ACM/IEEE Symposium on Logic in Computer Science LICS and The 47th International Colloquium on Automata, Languages and Programming ICALP 2020 held online but hosted in Saarbrücken.
In 2021, I was part of the Repeatability Evaluation Program Committee of ADHS and subreviewer for MEMOCODE.
In 2022, I served in the Artifact Evaluation Committee of QEST and as a reviewer for ISoLA.
Teaching
| 2022 | Teaching Assistant, Nebenläufige Programmierung, Saarland University |
| 2021 | Supportive Teaching Assistant, Nebenläufige Programmierung, Saarland University |
| 2020 | Background helper for Mathematics Precourse, Saarland University |
| 2019 | Organizer and Coach for Mathematics Precourse, Saarland University |
| 2018 | Teaching Assistant, Seminar Probabilistic Models of Concurrency, Saarland University |
| 2018 | Organizer, Lecturer and Coach for Mathematics Precourse, Saarland University |
| 2018 | Teaching Assistant, Mathematische Grundlagen der Computerlinguistik III: Statistische Methoden, Saarland University |
| 2017 | Lecturer and Coach for Mathematics Precourse, Saarland University, received the BESTE award for student initiatives and extraordinary commitment |
| 2016 | Lecturer and Coach for Mathematics Precourse, Saarland University |
| 2016 | Student TA, Nebenläufige Programmierung, Saarland University |
| 2015 | Student TA, Grundzüge der Algorithmen und Datenstrukturen, Saarland University |
| 2014 | Student TA, Programmierung 1, Saarland University |
In addition, I was involved in the supervision of Marcel Vinzent’s Bachelor’s thesis “Dead-End Pattern Databases in PRISM” and his research immersion lab “Implementing FRET/LRTDP in an explicit-state engine for JANI”, as well as in Govinda Sicheneder’s Master’s thesis “Time-bound Latency for Bluetooth Low Energy and Isochronous Channels in a Time-Critical Bicycle Application”.
Contact
If you have any questions feel free to contact me or just come to my office:
| Address: | Campus Saarbrücken, 66123 Saarbrücken |
| Phone: | +49 681 302 5634 |
| Location: | Bldg. E1 3, Room 508 |
| E-mail: | klauck@depend.uni-saarland.de |