Instructor “Advanced Logic”
University of Twente
one time a year since 2020
Master programme, in English
Instructor “Probabilistic Model Checking (Software Science)”
University of Twente
one time every two years since 2022
Bachelor programme, in English
Instructor “Languages and Machines”
University of Twente
one time a year since 2020
Bachelor programme, in English
Coordinator of track 3 (FMT) of the BSc research project University of Twente
one time a year since 2020
Bachelor programme, in English
Instructor for “Theory of Computation”
2019 and 2020
Queen’s University Belfast
Bachelor programme, in English
Guest Instructor for “Safety and Dependability”
2018
University of Liverpool Master programme, in English
Instructor for “Data Networks”
summer break 2017
Saarland University
Master programme, advanced elective course, in English
Instructor for “Quantitative Model Checking”
summer term 2017
Saarland University
Master programme, advanced elective course, in English
Teaching about verification of stochastic models as part of Model Checking lecture for Master and PhD students
2016
Beijing University
in English
Designing questions and expected answers for an exam for a lecture about probabilistic model checking.
2012
University of Oxford
in English
Teaching assistant for “Data Networks”
Tutoring exercise groups and grading exercise sheets. summer term 2011
Saarland University
Master programme, advanced elective course, in English
Teaching assistant for “Im Zoo der Automaten”
Discussing slides with students, giving advice for improvement. Participation in grading of final talks.
winter term 2010/2011
Saarland University
Bachelor programme, proseminar, in German
Teaching assistant for “Im Zoo der Automaten”
Discussing slides with students, giving advice for improvement. Participation in grading of final talks.
winter term 2008/2009
Saarland University
Bachelor programme, proseminar, in German
Teaching assistant for “Quantitative Model Checking”
Preparing theoretical and practical exercises for exercise sheets.
Tutoring exercise groups and grading exercise sheets. summer term 2010
Saarland University
Master programme, advanced elective course, in English
Teaching assistant for “Quantitative Model Checking”
Preparing theoretical and practical exercises for exercise sheets. Tutoring exercise groups and grading exercise sheets.
summer term 2009
Saarland University
Master programme, advanced elective course, in English
Teaching assistant for “Testing Techniques”
Tutoring exercise groups and grading exercise sheets. winter term 2008/2009
Saarland University
Master programme, advanced elective course, in English
Teaching assistant for “Nebenläufige Programmierung”
Tutoring exercise groups and grading exercise sheets.
summer term 2008
Saarland University
Bachelor programme, mandatory course, in German
Teaching assistant for “Embededded Systems”
Tutoring exercise groups and grading exercise sheets. Improving course exams.
summer term 2007
Saarland University
Master programme, advanced elective course, in English
Supervision and Evaluation
Daily supervisor of PhD student Akshay Dhonti
joint PhD project with Audi AG
(only full professors can be official supervisors)
University of Twente
Since September 2020
Supervisor of two Master projects (1 finished, 1 ongoing)
University of Twente
since 2020
Supervisor of four Bachelor projects
and several other Bachelor-level student projects.
University of Twente
since 2021
Day supervisor of PhD student Stefano Nicoletti, PhD student of Mariëlle Stoelinga
University of Twente
Since September 2020
Personal tutor of seven Bachelor students
Queen’s University Belfast
2019
Supervisor of five Bachelor projects
Queen’s University Belfast
2019/2020
Reviewer for the graduate award of OLDIES e.V. (Graduate association of the Carl von Ossietzky Universität Oldenburg)
2015, 2023
Second reviewer of Bachelor thesis
“PseuCo meets Java - Code Generation and Execution”
by Lisa Detzler
Saarland University, 2014
Adviser of Bachelor thesis
“Probabilistische Aspekte - AspectKP - ein verteiltes Prozesskalkül”
by Christian Josef Köhl Saarland University, 2012
Adviser of Bachelor thesis
“Analyse Stochastischer Hybrider Systeme”
by Patrick Dubbert Saarland University, 2010
Coadviser of Master thesis
“Approximation of Bisimulation in Probabilistic Metric Systems”
by Fabian Bendun Saarland University, 2010
Coadviser of Master thesis
“Scheduler-Quantified Time-Bounded Reachability for Distributed Input/Output Interactive Probabilistic Chains”
by Georgel Ionut Calin
Saarland University, 2010
Advice concerning individual questions to individual Bachelor and Master students as well as student assistants, including Frits Dannenberg, Zhimin Wu, Yong Li, Fu Chen, Thomas Neele, Frits Dannenberg, Alexander Graf-Brill, Sascha Zickenrott, Ivan Pryvalov, Li Yi, Thomas Karos, Zhechao Lin, Yuliya Butkova and Dmytro Puzhay.
Funding
since 2021:
Industrial PhD project in collaboration with Audi AG Ingolstadt funded by BMWi as part of the KARLI project (grant 19A21031C). This project about safety guarantees for DNN applications runs for 3 years. Audi pays the salary of the candidate as well as an annual fixed price of EUR 17,000 plus 15% IP surcharge (i.e. 19,550EUR per year).
2021:
Established Memorandum of Understanding with Institute of Soft- ware, Chinese Academy of Sciences, to serve as framework for double-degree PhD student projects, to be financed (per PhD stu- dent) by the China Scholarship Council
12/2013 - 12/2016:
PI of the project “Model Checking of Complex and Hybrid Stochastic Systems”, Grant No. 61350110518, 61450110461, 61550110506 of Research Fund for International Young Scientists (extended twice; RMB 200 000/year, ≈£22 840, initially and after first extension; RMB 340 000/year, ≈£38 828, after second extension)
6/2013 - 12/2016:
Chinese Academy of Sciences fellowship for young international scientists,
Grant No. 2013Y1GB0006 (extended twice; RMB 248 000/year, ≈£28 321)
5/2008 – 4/2010:
Stipend of the graduate school “Leistungsgarantien für Rechnersysteme”,
Deutsche Forschungsgemeinschaft (DFG)
Publications
Last updated: 2023-01-18
2022
Meilun Li, Andrea Turrini, Ernst Moritz Hahn, Zhikun She, and Lijun Zhang. Probabilistic Preference Planning Problem for Markov Decision Processes. IEEE TSE,
48(5):1545-1559, 2022 CORE: A* Citations: 2
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtczak. An Impossibility Result in Automata-Theoretic Reinforcement Learning.
In ATVA,
2022, pages 42-57 CORE: A
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtczak. Alternating Good-for-MDPs Automata.
In ATVA,
2022, pages 303-319 CORE: A
Stefano M. Nicoletti, Ernst Moritz Hahn, and Mariëlle Stoelinga. BFL: a Logic to Reason about Fault Trees.
In DSN,
2022, pages 441-452 CORE: A
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtczak. Reinforcement Learning with Guarantees that Hold for Ever.
In FMICS,
2022, pages 3-7 CORE: C
Chen Fu, Ernst Moritz Hahn, Yong Li, Sven Schewe, Meng Sun, Andrea Turrini, and Lijun Zhang. EPMC Gets Knowledge in Multi-agent Systems.
In VMCAI,
2022, pages 93-107 CORE: B Citations: 3
2021
Ernst Moritz Hahn and Arnd Hartmanns. Symblicit exploration and elimination for probabilistic model checking.
In SAC,
2021, pages 1798-1806 Citations: 1
Mariëlle Stoelinga, Christina Kolb, Stefano M. Nicoletti, Carlos E. Budde, and Ernst Moritz Hahn. The Marriage Between Safety and Cybersecurity: Still Practicing.
In SPIN,
2021, pages 3-21 Citations: 2
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtczak. Model-Free Reinforcement Learning for Branching Markov Decision Processes.
In CAV,
2021, pages 651-673 CORE: A* Citations: 2
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtczak. Model-Free Reinforcement Learning for Lexicographic Omega-Regular Objectives.
In FM,
2021, pages 142-159 CORE: A Citations: 2
2020
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtczak. Faithful and Effective Reward Schemes for Model-Free Reinforcement Learning of Omega-Regular Objectives.
In ATVA,
2020, pages 108-124 CORE: A Citations: 13
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtczak. Model-Free Reinforcement Learning for Stochastic Parity Games.
In CONCUR,
2020, pages 21:1-21:16 CORE: A Citations: 9
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtczak. Good-for-MDPs Automata for Probabilistic Analysis and Reinforcement Learning.
In TACAS,
2020, pages 306-323 CORE: A Citations: 19
2019
Ernst Moritz Hahn, Vahid Hashemi, Holger Hermanns, Morteza Lahijanian, and Andrea Turrini. Interval Markov Decision Processes with Multiple Objectives: From Robust Strategies to Pareto Curves. TOMACS,
29(4):27:1-27:31, 2019 CORE: B Citations: 16
Alessandro Abate, Henk Blom, Nathalie Cauchi, Kurt Degiorgio, Martin Fränzle, Ernst Moritz Hahn, Sofie Haesaert, Hao Ma, Meeko Oishi, Carina Pilch, Anne Remke, Mahmoud Salamati, Sadegh Soudjani, Birgit van Huijgevoort, and Abraham P. Vinod. ARCH-COMP19 Category Report: Stochastic Modelling.
In ARCH19,
2019, pages 62-102 Citations: 13
Ernst Moritz Hahn, Arnd Hartmanns, Christian Hensel, Michaela Klauck, Joachim Klein, Jan Křetínský, David Parker, Tim Quatmann, Enno Ruijters, and Marcel Steinmetz. The 2019 Comparison of Tools for the Analysis of Quantitative Formal
Models - (QComp 2019 Competition Report).
In TOOLympics,
2019, pages 69-92 Citations: 52
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtczak. Omega-Regular Objectives in Model-Free Reinforcement Learning.
In TACAS,
2019, pages 395-412 CORE: A Citations: 100
2018
Paul Gainer, Ernst Moritz Hahn, and Sven Schewe. Accelerated Model Checking of Parametric Markov Chains.
In ATVA,
2018, pages 300-316 CORE: A Citations: 19
Paul Gainer, Ernst Moritz Hahn, and Sven Schewe. Incremental Verification of Parametric and Reconfigurable Markov Chains.
In QEST,
2018, pages 140-156 Citations: 11
2017
Vahid Hashemi, Andrea Turrini, Ernst Moritz Hahn, Holger Hermanns, and Khaled M. Elbassioni. Polynomial-Time Alternating Probabilistic Bisimulation for Interval MDPs.
In SETTA,
2017, pages 25-41 Citations: 3
Ernst Moritz Hahn, Vahid Hashemi, Holger Hermanns, Morteza Lahijanian, and Andrea Turrini. Multi-objective Robust Strategy Synthesis for Interval MDPs.
In QEST,
2017, pages 207-223 Citations: 34
Yuan Feng, Ernst Moritz Hahn, Andrea Turrini, and Shenggang Ying. Model Checking ω-regular Properties for Quantum Markov Chains.
In CONCUR,
2017, pages 35:1-35:16 CORE: A Citations: 15
Carlos E. Budde, Christian Dehnert, Ernst Moritz Hahn, Arnd Hartmanns, Sebastian Junges, and Andrea Turrini. JANI: Quantitative Model and Tool Interaction.
In TACAS,
2017, pages 151-168 CORE: A Citations: 99
Ernst Moritz Hahn, Sven Schewe, Andrea Turrini, and Lijun Zhang. Synthesising Strategy Improvement and Recursive Algorithms for Solving
2.5 Player Parity Games.
In VMCAI,
2017, pages 266-287 CORE: B Citations: 4
2016
Wu Zhimin, Ernst Moritz Hahn, Akin Gunay, Li Jun Zhang, and Yang Liu. GPU-accelerated Value Iteration for the Computation of Reachability Probabilities in MDPs.
In ECAI,
2016, pages 1726 - 1727 CORE: A Citations: 2
Ernst Moritz Hahn and Arnd Hartmanns. A Comparison of Time- and Reward-Bounded Probabilistic Model Checking Techniques.
In SETTA,
2016, pages 85-100 Citations: 24
Yong Li, Wanwei Liu, Andrea Turrini, Ernst Moritz Hahn, and Lijun Zhang. An Efficient Synthesis Algorithm for Parametric Markov Chains Against Linear Time Properties.
In SETTA,
2016, pages 280-296 Citations: 7
Ernst Moritz Hahn, Vahid Hashemi, Holger Hermanns, and Turrini. Exploiting Robust Optimization for Interval Probabilistic Bisimulation.
In QEST,
2016, pages 55-71 Citations: 11
Ernst Moritz Hahn, Sven Schewe, Andrea Turrini, and Lijun Zhang. A Simple Algorithm for Solving Qualitative Probabilistic Parity Games.
In CAV,
2016, pages 291-311 CORE: A* Citations: 13
2015
Tom van Dijk, Ernst Moritz Hahn, David N. Jansen, Yong Li, Thomas Neele, Mariëlle Stoelinga, Andrea Turrini, and Lijun Zhang. A Comparative Study of BDD Packages for Probabilistic Symbolic Model
Checking.
In SETTA,
2015, pages 35-51 Citations: 21
Ernst Moritz Hahn, Guangyuan Li, Sven Schewe, Andrea Turrini, and Lijun Zhang. Lazy Probabilistic Model Checking without Determinisation.
In CONCUR,
2015, pages 354-367 CORE: A Citations: 50
Yuan Feng, Ernst Moritz Hahn, Andrea Turrini, and Lijun Zhang. QPMC: A Model Checker for Quantum Programs and Protocols.
In FM,
2015, pages 265-272 CORE: A Citations: 28
Frits Dannenberg, Ernst Moritz Hahn, and Marta Z. Kwiatkowska. Computing Cumulative Rewards Using Fast Adaptive Uniformization. TOMACS,
25(2):9, 2015 CORE: B Citations: 19
Ernst Moritz Hahn, Holger Hermanns, Ralf Wimmer, and Bernd Becker. Transient Reward Approximation for Continuous-Time Markov Chains. IEEE TR,
64(4):1254-1275, 2015 CORE: A Citations: 7
2014
Ernst Moritz Hahn, Arnd Hartmanns, and Holger Hermanns. Reachability and Reward Checking for Stochastic Timed Automata. ECEASST,
70, 2014 Citations: 25
David Spieler, Ernst Moritz Hahn, and Lijun Zhang. Model Checking CSL for Markov Population Models.
In QAPL,
2014, pages 93-107 Citations: 8
Ernst Moritz Hahn, Yi Li, Sven Schewe, Andrea Turrini, and Lijun Zhang. IscasMC: A Web-Based Probabilistic Model Checker.
In FM,
2014, pages 312-317 CORE: A Citations: 104
2013
Frits Dannenberg, Ernst Moritz Hahn, and Marta Z. Kwiatkowska. Computing Cumulative Rewards Using Fast Adaptive Uniformisation.
In CMSB,
2013, pages 33-49
Taolue Chen, Ernst Moritz Hahn, Tingting Han, Marta Z. Kwiatkowska, Hongyang Qu, and Lijun Zhang. Model Repair for Markov Decision Processes.
In TASE,
2013, pages 85-92
Yang Gao, Ernst Moritz Hahn, Naijun Zhan, and Lijun Zhang. CCMC: A Conditional CSL Model Checker for Continuous-Time Markov
Chains.
In ATVA,
2013, pages 464-468 CORE: A Citations: 2
Ernst Moritz Hahn and Holger Hermanns. Rewarding probabilistic hybrid automata.
In HSCC,
2013, pages 313-322 Citations: 1
Ernst Moritz Hahn, Arnd Hartmanns, Holger Hermanns, and Joost-Pieter Katoen. A compositional modelling and analysis framework for stochastic hybrid systems. FMSD,
43(2):191-232, 2013 Citations: 143
Christel Baier, Ernst Moritz Hahn, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. Model checking for performability. MSCS,
23(4):751-795, 2013 CORE: A Citations: 37
2012
Luis María Ferrer Fioriti, Ernst Moritz Hahn, Holger Hermanns, and Björn Wachter. Variable Probabilistic Abstraction Refinement.
In ATVA,
2012, pages 300-316 CORE: A Citations: 5
Lijun Zhang, Zhikun She, Stefan Ratschan, Holger Hermanns, and Ernst Moritz Hahn. Safety Verification for Probabilistic Hybrid Systems. EJCON,
18(6):572-587, 2012 Citations: 29
2011
Ernst Moritz Hahn, Gethin Norman, David Parker, Björn Wachter, and Lijun Zhang. Game-based Abstraction and Controller Synthesis for Probabilistic Hybrid Systems.
In QEST,
2011, pages 69-78 Citations: 31
Ralf Wimmer, Ernst Moritz Hahn, Holger Hermanns, and Bernd Becker. Reachability analysis for incomplete networks of Markov decision processes.
In MEMOCODE,
2011, pages 151-160 Citations: 1
Peter Buchholz, Ernst Moritz Hahn, Holger Hermanns, and Lijun Zhang. Model Checking Algorithms for CTMDPs.
In CAV,
2011, pages 225-242 CORE: A* Citations: 50
Pepijn Crouzen, Ernst Moritz Hahn, Holger Hermanns, Abhishek Dhama, Oliver E. Theel, Ralf Wimmer, Bettina Braitling, and Bernd Becker. Bounded Fairness for Probabilistic Distributed Algorithms.
In ACSD,
2011, pages 89-97 CORE: B Citations: 5
Ernst Moritz Hahn, Tingting Han, and Lijun Zhang. Synthesis for PCTL in Parametric Markov Decision Processes.
In NFM,
2011, pages 146-161 Citations: 104
Martin Fränzle, Ernst Moritz Hahn, Holger Hermanns, Nicolás Wolovick, and Lijun Zhang. Measurability and safety verification for stochastic hybrid systems.
In HSCC,
2011, pages 43-52 Citations: 103
Joost-Pieter Katoen, Ivan S. Zapreev, Ernst Moritz Hahn, Holger Hermanns, and David N. Jansen. The ins and outs of the probabilistic model checker MRMC. PEVA,
68(2):90-104, 2011 CORE: B Citations: 437
Ernst Moritz Hahn, Holger Hermanns, and Lijun Zhang. Probabilistic reachability for parametric Markov models. STTT,
13(1):3-19, 2011 CORE: B Citations: 190
2010
Georgel Calin, Pepijn Crouzen, Pedro R. D'Argenio, Ernst Moritz Hahn, and Lijun Zhang. Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains.
In SPIN,
2010, pages 193-211 Citations: 8
Ralf Wimmer, Bettina Braitling, Bernd Becker, Ernst Moritz Hahn, Pepijn Crouzen, Holger Hermanns, Abhishek Dhama, and Oliver E. Theel. Symblicit Calculation of Long-Run Averages for Concurrent Probabilistic Systems.
In QEST,
2010, pages 27-36 Citations: 32
Lijun Zhang, Zhikun She, Stefan Ratschan, Holger Hermanns, and Ernst Moritz Hahn. Safety Verification for Probabilistic Hybrid Systems.
In CAV,
2010, pages 196-211 CORE: A* Citations: 77
Ernst Moritz Hahn, Holger Hermanns, Björn Wachter, and Lijun Zhang. PARAM: A Model Checker for Parametric Markov Models.
In CAV,
2010, pages 660-664 CORE: A* Citations: 166
Ernst Moritz Hahn, Holger Hermanns, Björn Wachter, and Lijun Zhang. PASS: Abstraction Refinement for Infinite Probabilistic Models.
In TACAS,
2010, pages 353-357 CORE: A Citations: 50
2009
Joost-Pieter Katoen, Ivan S. Zapreev, Ernst Moritz Hahn, Holger Hermanns, and David N. Jansen. The Ins and Outs of the Probabilistic Model Checker MRMC.
In QEST,
2009, pages 167-176
Ernst Moritz Hahn, Holger Hermanns, and Lijun Zhang. Probabilistic Reachability for Parametric Markov Models.
In SPIN,
2009, pages 88-106 Citations: 51
Ernst Moritz Hahn, Holger Hermanns, Björn Wachter, and Lijun Zhang. INFAMY: An Infinite-State Markov Model Checker.
In CAV,
2009, pages 641-647 Citations: 36
Ernst Moritz Hahn, Holger Hermanns, Björn Wachter, and Lijun Zhang. Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains. FUIN,
95(1):129-155, 2009 CORE: B
2008
Lijun Zhang, Holger Hermanns, Ernst Moritz Hahn, and Björn Wachter. Time-bounded model checking of infinite-state continuous-time Markov chains.
In ACSD,
2008, pages 98-107 CORE: B Citations: 37
2006
Thomas Peikenkamp, Antonella Cavallo, Laura Valacca, Eckard Böde, Matthias Pretzer, and Ernst Moritz Hahn. Towards a Unified Model-Based Safety Assessment.
In SAFECOMP,
2006, pages 275-288 CORE: B Citations: 36
Talks
Since 01/07/2020
Talk about "Good-for-MDPs Automata ATVA 2022" at ATVA 2022
Talk about "Faithful and Effective Reward Schemes for Model-Free Reinforcement Learning of Omega-Regular Objectives" at ATVA 2020 PowerPoint PDF
Exchange in Argentina within the programme “Projektbezogener Personenaustausch mit Argentinien (PROALAR)” by the Deutscher Akademischer Austauschdienst (DAAD) and the Ministerio de Ciencia, Tecnología e Innovación Productiva (MINCyT) (2/2010 – 4/2010)
Participation at a business start-up seminar (3/2009).
An introduction into the aspects relevant for the foundation and leadership of small businesses (business administration, accounting, judicial subjects, support programmes, marketing, etc.).
Participation at a consulting course (10/2008 – 2/2009).
A course introducing into the work of a consultant, involving discussions and communication training, business etiquette, as well as several case studies with consulting agencies (Accenture, IDS Scheer, Unity).
Participation at the entrepreneurial planning game “EXIST” (6/2008, 9/2008).
