Ernst Moritz Hahn

About me

I am a Marie Skłodowska Curie Fellow at the Computer Science department of the University of Liverpool. My project is called PaVeCo and targets at developing practically efficient analysis methods for stochastic systems which involve partial control, non-functional requirements, and multi-objective requirements. Previously, I have been working as Associate Research Professor at State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, have been postdoc at Department of Computer Science, University of Oxford and Ph.D. student at Dependable Systems and Software, Universität des Saarlandes.

• Google Scholar: http://scholar.google.de/citations?user=MH7fSVAAAAAJ
• ORCID: https://orcid.org/0000-0002-9348-7684

Research Interests

My main research interest is probabilistic model checking. This involves topics such as:

• parametric Markov models
• stochastic games
• stochastic hybrid systems
• efficient algorithms for deciding linear time logic properties
• continuous-time Markov chains with infinite state-space
• quantum Markov models

Teaching

• 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 of Individual Students

• Reviewer for the graduate award of OLDIES e.V. (Graduate association of the Carl von Ossietzky Universität Oldenburg)
• 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

• 11/2017 - 10/2019: Marie Skłodowska Curie Individual Fellowship “ PaVeCo - Parametrised Verification and Control”, Project ID 753351 (€195 455 total, ≈£174 889)
• 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

• Paul Gainer, Ernst Moritz Hahn, and Sven Schewe. Accelerated model checking of parametric Markov chains. In International Symposium on Automated Technology for Verification and Analysis (ATVA), 2018. To appear.
• Paul Gainer, Ernst Moritz Hahn, and Sven Schewe. Incremental verification of parametric and reconfigurable Markov chains. In International Conference on Quantitative Evaluation of SysTems (QEST), 2018. To appear.
• Vahid Hashemi, Andrea Turrini, Ernst Moritz Hahn, Holger Hermanns, and Khaled Elbassioni. Polynomial-time alternating probabilistic bisimulation for interval MDPs. In Symposium on Dependable Software Engineering (SETTA), pages 25–41, 2017.
• Ernst Moritz Hahn, Vahid Hashemi, Holger Hermanns, Morteza Lahijanian, and Andrea Turrini. Multi-objective robust strategy synthesis for interval MDPs. In International Conference on Quantitative Evaluation of SysTems (QEST), pages 207–223, 2017.
• Andrea Turrini Yuan Feng, Ernst Moritz Hahn and Shenggang Ying. Model checking ω-regular properties for quantum Markov chains. In Conference on Concurrency Theory (CONCUR), pages 35:1–35:16, 2017.
• Carlos E. Budde, Christian Dehnert, Ernst Moritz Hahn, Arnd Hartmanns, Sebastian Junges, and Andrea Turrini. JANI: quantitative model and tool interaction. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 151–168, 2017.
• Ernst Moritz Hahn, Sven Schewe, Andrea Turrini, and Lijun Zhang. Synthesising strategy improvement and recursive algorithms for solving 2.5 player parity games. In Verification, Model Checking, and Abstract Interpretation (VMCAI), pages 266–287, 2017.
• 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 European Conference on Artificial Intelligence (ECAI), pages 1726–1727, 2016.
• Ernst Moritz Hahn and Arnd Hartmanns. A comparison of time- and reward-bounded probabilistic model checking techniques. In Symposium on Dependable Software Engineering (SETTA), 2016.
• 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 Symposium on Dependable Software Engineering (SETTA), pages 280–296, 2016.
• Ernst Moritz Hahn, Vahid Hashemi, Holger Hermanns, and Turrini. Exploiting robust optimization for interval probabilistic bisimulation. In International Conference on Quantitative Evaluation of SysTems (QEST), pages 55–71, 2016.
• Ernst Moritz Hahn, Sven Schewe, Andrea Turrini, and Lijun Zhang. A simple algorithm for solving qualitative probabilistic parity games. In International Conference on Computer Aided Verification (CAV), pages 291–311, 2016.
• 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 Symposium on Dependable Software Engineering (SETTA), pages 35–51, 2015.
• Ernst Moritz Hahn, Guangyuan Li, Sven Schewe, Andrea Turrini, and Lijun Zhang. Lazy probabilistic model checking without determinisation. In Conference on Concurrency Theory (CONCUR), pages 354–367, 2015.
• Yuan Feng, Ernst Moritz Hahn, Andrea Turrini, and Lijun Zhang. QPMC: A model checker for quantum programs and protocols. In International Conference on Formal Methods (FM), pages 265–272, 2015.
• Frits Dannenberg, Ernst Moritz Hahn, and Marta Z. Kwiatkowska. Computing cumulative rewards using fast adaptive uniformization. ACM Transactions on Modeling and Computer Simulation (TOMACS), 25(2):9, 2015.
• Ernst Moritz Hahn, Holger Hermanns, Ralf Wimmer, and Bernd Becker. Transient reward approximation for continuous-time Markov chains. IEEE Transactions on Reliability (TR), 64(4):1254–1275, 2015.
• Ernst Moritz Hahn, Arnd Hartmanns, and Holger Hermanns. Reachability and reward checking for stochastic timed automata. Electronic Communications of the EASST (ECE-ASST), 70, 2014.
• David Spieler, Ernst Moritz Hahn, and Lijun Zhang. Model checking CSL for Markov population models. In International Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL), pages 93–107, 2014.
• Ernst Moritz Hahn, Yi Li, Sven Schewe, Andrea Turrini, and Lijun Zhang. IscasMC: A web-based probabilistic model checker. In International Conference on Formal Methods (FM), pages 312–317, 2014.
• Frits Dannenberg, Ernst Moritz Hahn, and Marta Z. Kwiatkowska. Computing cumulative rewards using fast adaptive uniformisation. In Computational Methods in Systems Biology (CMSB), pages 33–49, 2013.
• Taolue Chen, Ernst Moritz Hahn, Tingting Han, Marta Z. Kwiatkowska, Hongyang Qu, and Lijun Zhang. Model repair for Markov decision processes. In Theoretical Aspects of Software Engineering Conference (TASE), pages 85-92, 2013.
• Yang Gao, Ernst Moritz Hahn, Naijun Zhan, and Lijun Zhang. CCMC: A conditional CSL model checker for continuous-time Markov chains. In International Symposium on Automated Technology for Verification and Analysis (ATVA), pages 464–468, 2013.
• Ernst Moritz Hahn and Holger Hermanns. Rewarding probabilistic hybrid automata. In International Conference on Hybrid Systems: Computation and Control (HSCC), pages 313–322, 2013.
• Ernst Moritz Hahn, Arnd Hartmanns, Holger Hermanns, and Joost-Pieter Katoen. A compositional modelling and analysis framework for stochastic hybrid systems. Formal Methods in System Design (FMSD), 43(2):191–232, 2013. Invited.
• Christel Baier, Ernst Moritz Hahn, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. Model checking for performability. Mathematical Structures in Computer Science (MSCS), 23(4):751–795, 2013.
• Luis María Ferrer Fioriti, Ernst Moritz Hahn, Holger Hermanns, and Björn Wachter. Variable probabilistic abstraction refinement. In International Symposium on Automated Technology for Verification and Analysis (ATVA), pages 300–316, 2012.
• Lijun Zhang, Zhikun She, Stefan Ratschan, Holger Hermanns, and Ernst Moritz Hahn. Safety verification for probabilistic hybrid systems. European Journal of Control (EJCON), 18(6):572–587, 2012.
• Ernst Moritz Hahn, Gethin Norman, David Parker, Björn Wachter, and Lijun Zhang. Game-based abstraction and controller synthesis for probabilistic hybrid systems. In International Conference on Quantitative Evaluation of SysTems (QEST), pages 69–78, 2011.
• Ralf Wimmer, Ernst Moritz Hahn, Holger Hermanns, and Bernd Becker. Reachability analysis for incomplete networks of Markov decision processes. In International Conference on Formal Methods and Models for System Design (MEMOCODE), pages 151–160, 2011.
• Peter Buchholz, Ernst Moritz Hahn, Holger Hermanns, and Lijun Zhang. Model checking algorithms for CTMDPs. In International Conference on Computer Aided Verification (CAV), pages 225–242, 2011.
• 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 International Conference on Application of Concurrency to System Design (ACSD), pages 89–97, 2011. Best Paper Award.
• Ernst Moritz Hahn, Tingting Han, and Lijun Zhang. Synthesis for PCTL in parametric Markov decision processes. In NASA Formal Methods Symposium (NFM), pages 146–161, 2011.
• Martin Fränzle, Ernst Moritz Hahn, Holger Hermanns, Nicolás Wolovick, and Lijun Zhang. Measurability and safety verification for stochastic hybrid systems. In International Conference on Hybrid Systems: Computation and Control (HSCC), pages 43–52, 2011.
• 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. Performance Evaluation (PEVA), 68(2):90–104, 2011. Invited.
• Ernst Moritz Hahn, Holger Hermanns, and Lijun Zhang. Probabilistic reachability for parametric Markov models. International Journal on Software Tools for Technology Transfer (STTT), 13(1):3–19, 2011. Invited.
• 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 International Spin Symposium (SPIN), pages 193–211, 2010.
• 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 International Conference on Quantitative Evaluation of SysTems (QEST), pages 27–36, 2010.
• Lijun Zhang, Zhikun She, Stefan Ratschan, Holger Hermanns, and Ernst Moritz Hahn. Safety verification for probabilistic hybrid systems. In International Conference on Computer Aided Verification (CAV), pages 196–211, 2010.
• Ernst Moritz Hahn, Holger Hermanns, Björn Wachter, and Lijun Zhang. PARAM: A model checker for parametric Markov models. In International Conference on Computer Aided Verification (CAV), pages 660–664, 2010.
• Ernst Moritz Hahn, Holger Hermanns, Björn Wachter, and Lijun Zhang. PASS: Abstraction refinement for infinite probabilistic models. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 353–357, 2010.
• 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 International Conference on Quantitative Evaluation of SysTems (QEST), pages 167–176, 2009.
• Ernst Moritz Hahn, Holger Hermanns, and Lijun Zhang. Probabilistic reachability for parametric Markov models. In International Spin Symposium (SPIN), pages 88–106, 2009.
• Ernst Moritz Hahn, Holger Hermanns, Björn Wachter, and Lijun Zhang. INFAMY: An infinite-state Markov model checker. In International Conference on Computer Aided Verification (CAV), pages 641–647, 2009.
• Ernst Moritz Hahn, Holger Hermanns, Björn Wachter, and Lijun Zhang. Time-bounded model checking of infinite-state continuous-time Markov chains. Fundamenta Informaticae (FUIN), 95(1):129–155, 2009. Invited.
• Lijun Zhang, Holger Hermanns, Ernst Moritz Hahn, and Björn Wachter. Time-bounded model checking of infinite-state continuous-time Markov chains. In International Conference on Application of Concurrency to System Design (ACSD), pages 98–107, 2008.
• Thomas Peikenkamp, Antonella Cavallo, Laura Valacca, Eckard Böde, Matthias Pretzer, and Ernst Moritz Hahn. Towards a unified model-based safety assessment. In International Conference on Computer Safety, Reliability and Security (SAFECOMP), pages 275–288, 2006.

Professional Activities

• AE Chair TACAS 2019
• PC member SETTA 2018
• Publicity Chair CONCUR 2018
• PC member TIME 2017
• PC member ALP4IoT 2017
• PC member ICSE 2017 Student Research Competition
• PC member HSCC Repeatability Evaluation 2014, 2016, 2017, and 2018
• PC member ValueTools 2013
• Visiting Scholar “LCCC Focus Period and Workshop on Formal Verification of Embedded Control Systems” (4/2013 – 5/2013)
• 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 the seminar “Leadership and Communication” lead by Dr. Sphen Paul (10/2009 – 1/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).
• Referee for Journals, Conferences, and Workshops SIADS, JAM, ICALP, ATVA, AVOCS, CMSB, CAV, JCST, CONCUR, SETTA, CyPhy, EJCON, FM, FMSD, FORMATS, FSTTCS, FCS, HSCC, I&C, INSC, KiMfest, MMB & DFT, NFM, QEST, RP, SCICO, SRE, SIMPAT, TCS, TACAS, TSE, VMCAI

Professional Appointments

• since 11/2017: Marie Skłodowska Curie Fellow, University of Liverpool
• 3/2017 - 10/2017: Sabbatical, Saarland University
• 6/2013 - 10/2017: Research Associate Professor, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
• 10/2012 – 5/2013: Research Associate (postdoctoral), University of Oxford
• 5/2010 – 9/2012: Research Associate (PhD student), Saarland University
• 10/2005 – 10/2006: Research Associate, OFFIS, Safety Analysis & Verification (Oldenburg)

Education

• since 4/2018: Studying for a British Certificate in Professional Studies in Learning & Teaching in Higher Education (CPS), 30 ECTS points level 6 (Bachelor) program, leads to Fellowship of British Higher Education Academy (HEA)
• 5/2008 – 9/2012: Studied Computer Science (PhD) at Saarland University, Doctoral degree (Dr.-Ing.) summa cum laude
• 10/2006 – 4/2008: Studied Computer Science (Master) at Saarland University, Second degree in Computer Science (Master) with distinction
• 10/2002 – 9/2005: Studied Computer Science (Bachelor) with a minor in Mathematics at Carl von Ossietzky Universität Oldenburg, First degree in Computer Science (Bachelor)

Honours and Awards

• 1/2013 – 5/2013: Member of the Common Room of Wolfson College, University of Oxford
• 2011: Best Paper Award ACSD 2011
• 2009: Faculty nomination of the computer science department for a stipend of the “Deutsche Telekom Stiftung”

Language Proficiency

• English: fluent
• German: native speaker
• Chinese (Mandarin): good command

Contact Details

Ernst Moritz Hahn
University of Liverpool
Department of Computer Science
Ashton Building
Ashton Street
Liverpool L69 3BX
United Kingdom

Office: Room 307, Ashton Building
email: e.m.hahn@liverpool.ac.uk