Ernst Moritz Hahn (韩墨锐)'s Homepage

Contact

• Office: Room A219, Building 5
• Telephone: +86 10-62661604
• Address: South Fourth Street 4#, Zhong Guan Cun, Beijing
• email: <lastname> [at] ios.ac.cn

About me

I am Associate Research Professor at State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences. Previously, I was postdoc at Department of Computer Science, University of Oxford and Ph.D. student at Dependable Systems and Software, Universität des Saarlandes. My main research interest is probabilistic model checking. This involves topics such as:

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

Professional activities

• PC member ICSE 2017 Student Research Competition
• Member of HSCC 2016 Repeatability Evaluation Committee
• Member of HSCC 2014 Repeatability Evaluation Committee
• PC member ValueTools 2013
• Referee for the following journals, conferences, and workshops:
  • Applied Dynamical Systems, SIAM Journal on (SIADS)
  • Applied Mathematics, Journal of (JAM)
  • Automata, Languages and Programming (ICALP)
  • Automated Technology for Verification and Analysis (ATVA)
  • Automated Verification of Critical Systems (AVOCS)
  • Computational Methods in Systems Biology (CMSB)
  • Computer Aided Verification (CAV)
  • Computer Science and Technology, Journal of (JCST)
  • Conference on Concurrency Theory (CONCUR)
  • Dependable Software Engineering: Theories, Tools, and Applications (SETTA)
  • Design, Modeling and Evaluation of Cyber Physical Systems (CyPhy)
  • European Journal of Control (EJCON)
  • Formal Methods (FM)
  • Formal Methods in System Design (FMSD)
  • Formal Modelling and Analysis of Timed Systems (FORMATS)
  • Foundations of Software Technology and Theoretical Computer Science (FSTTCS)
  • Hybrid Systems: Computation and Control (HSCC)
  • Information and Computation, Journal (I&C)
  • Interdisciplinary Sciences: Computational Life Sciences (INSC)
  • Measurement, Modelling and Evaluation of Computing Systems and Dependability and Fault Tolerance (MMB & DFT)
  • NASA Formal Methods (NFM)
  • Quantitative Evaluation of SysTems (QEST)
  • Reachability Problems (RP)
  • Science of Computer Programming, Journal (SCICO)
  • Scientific Research and Essays, Journal (SRE)
  • Theoretical Computer Science, Journal (TCS)
  • Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
  • Transactions of Software Engineering, Journal (TSE)
  • Verification, Model Checking, and Abstract Interpretation (VMCAI)

Publications

• Ying Liu, Andrea Turrini, Ernst Moritz Hahn (), Bai Xue (), Lijun Zhang: Scenario Approach for Parametric Markov Models. In Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Singapore, October 24-27, 2023, Proceedings, Part I, volume 14215 of Lecture Notes in Computer Science, pages 158-180, 2023. DOI BIB
• Chen Fu, Ernst Moritz Hahn (), Yong Li, Sven Schewe (), Meng Sun (), Andrea Turrini, Lijun Zhang: EPMC Gets Knowledge in Multi-agent Systems. In Verification, Model Checking, and Abstract Interpretation - 23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16-18, 2022, Proceedings, volume 13182 of Lecture Notes in Computer Science, pages 93-107, 2022. DOI BIB
• Meilun Li, Andrea Turrini, Ernst Moritz Hahn (), Zhikun She, Lijun Zhang: Probabilistic Preference Planning Problem for Markov Decision Processes. In IEEE Trans. Software Eng. 48(5):1545-1559, 2022. DOI BIB
• 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). In Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III, volume 11429 of Lecture Notes in Computer Science, pages 69-92, 2019. DOI BIB
• Ernst Moritz Hahn (), Vahid Hashemi, Holger Hermanns (), Morteza Lahijanian, Andrea Turrini: Interval Markov Decision Processes with Multiple Objectives: From Robust Strategies to Pareto Curves. In ACM Trans. Model. Comput. Simul. 29(4):27:1-27:31, 2019. DOI BIB
• Ernst Moritz Hahn (), Mateo Perez, Sven Schewe (), Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak: Omega-Regular Objectives in Model-Free Reinforcement Learning. In Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part I, volume 11427 of Lecture Notes in Computer Science, pages 395-412, 2019. DOI BIB
• Carlos E. Budde, Christian Dehnert, Ernst Moritz Hahn (), Arnd Hartmanns (), Sebastian Junges (), Andrea Turrini: JANI: Quantitative Model and Tool Interaction. In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part II, volume 10206 of Lecture Notes in Computer Science, pages 151-168, 2017. DOI BIB
• Yuan Feng (), Ernst Moritz Hahn (), Andrea Turrini, Shenggang Ying: Model Checking Omega-regular Properties for Quantum Markov Chains. In 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany, volume 85 of LIPIcs, pages 35:1-35:16, 2017. DOI BIB
• Ernst Moritz Hahn (), Vahid Hashemi, Holger Hermanns (), Morteza Lahijanian, Andrea Turrini: Multi-objective Robust Strategy Synthesis for Interval Markov Decision Processes. In Quantitative Evaluation of Systems - 14th International Conference, QEST 2017, Berlin, Germany, September 5-7, 2017, Proceedings, volume 10503 of Lecture Notes in Computer Science, pages 207-223, 2017. DOI BIB
• Ernst Moritz Hahn (), Sven Schewe (), Andrea Turrini, Lijun Zhang: Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games. In Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings, volume 10145 of Lecture Notes in Computer Science, pages 266-287, 2017. DOI BIB
• Vahid Hashemi, Andrea Turrini, Ernst Moritz Hahn (), Holger Hermanns (), Khaled M. Elbassioni: Polynomial-Time Alternating Probabilistic Bisimulation for Interval MDPs. In Dependable Software Engineering. Theories, Tools, and Applications - Third International Symposium, SETTA 2017, Changsha, China, October 23-25, 2017, Proceedings, volume 10606 of Lecture Notes in Computer Science, pages 25-41, 2017. Best paper. DOI BIB
• Ernst Moritz Hahn (), Vahid Hashemi, Holger Hermanns (), Andrea Turrini: Exploiting Robust Optimization for Interval Probabilistic Bisimulation. In Quantitative Evaluation of Systems - 13th International Conference, QEST 2016, Quebec City, QC, Canada, August 23-25, 2016, Proceedings, volume 9826 of Lecture Notes in Computer Science, pages 55-71, 2016. DOI BIB
• Ernst Moritz Hahn (), Sven Schewe (), Andrea Turrini, Lijun Zhang: A Simple Algorithm for Solving Qualitative Probabilistic Parity Games. In Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II, volume 9780 of Lecture Notes in Computer Science, pages 291-311, 2016. DOI BIB
• Yong Li, Wanwei Liu, Andrea Turrini, Ernst Moritz Hahn (), Lijun Zhang: An Efficient Synthesis Algorithm for Parametric Markov Chains Against Linear Time Properties. In Dependable Software Engineering: Theories, Tools, and Applications - Second International Symposium, SETTA 2016, Beijing, China, November 9-11, 2016, Proceedings, volume 9984 of Lecture Notes in Computer Science, pages 280-296, 2016. DOI BIB
• Zhimin Wu, Ernst Moritz Hahn (), Akin Günay, Lijun Zhang, Yang Liu: GPU-Accelerated Value Iteration for the Computation of Reachability Probabilities in MDPs. In ECAI 2016 - 22nd European Conference on Artificial Intelligence, 29 August-2 September 2016, The Hague, The Netherlands - Including Prestigious Applications of Artificial Intelligence (PAIS 2016),, volume 285 of Frontiers in Artificial Intelligence and Applications, pages 1726-1727, 2016. DOI BIB
• Tom van Dijk (), Ernst Moritz Hahn (), David N. Jansen (), Yong Li, Thomas Neele (), Mariëlle Stoelinga (), Andrea Turrini, Lijun Zhang: A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking. In Dependable Software Engineering: Theories, Tools, and Applications - First International Symposium, SETTA 2015, Nanjing, China, November 4-6, 2015, Proceedings, volume 9409 of Lecture Notes in Computer Science, pages 35-51, 2015. DOI BIB
• Yuan Feng (), Ernst Moritz Hahn (), Andrea Turrini, Lijun Zhang: QPMC: A Model Checker for Quantum Programs and Protocols. In FM 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings, volume 9109 of Lecture Notes in Computer Science, pages 265-272, 2015. DOI BIB
• Ernst Moritz Hahn (), Holger Hermanns (), Ralf Wimmer (), Bernd Becker (): Transient Reward Approximation for Continuous-Time Markov Chains. In IEEE Trans. Reliab. 64(4):1254-1275, 2015. DOI BIB
• Ernst Moritz Hahn (), Guangyuan Li, Sven Schewe (), Andrea Turrini, Lijun Zhang: Lazy Probabilistic Model Checking without Determinisation. In 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015, volume 42 of LIPIcs, pages 354-367, 2015. DOI BIB
• Ernst Moritz Hahn (), Arnd Hartmanns (), Holger Hermanns (): Reachability and Reward Checking for Stochastic Timed Automata. In Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 70, 2014. DOI BIB
• Ernst Moritz Hahn (), Yi Li, Sven Schewe (), Andrea Turrini, Lijun Zhang: IscasMc: A Web-Based Probabilistic Model Checker. In FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings, volume 8442 of Lecture Notes in Computer Science, pages 312-317, 2014. DOI BIB
• David Spieler, Ernst Moritz Hahn (), Lijun Zhang: Model Checking CSL for Markov Population Models. In Proceedings Twelfth International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2014, Grenoble, France, 12-13 April 2014, volume 154 of EPTCS, pages 93-107, 2014. DOI BIB
• Taolue Chen (), Ernst Moritz Hahn (), Tingting Han, Marta Z. Kwiatkowska, Hongyang Qu, Lijun Zhang: Model Repair for Markov Decision Processes. In Seventh International Symposium on Theoretical Aspects of Software Engineering, TASE 2013, 1-3 July 2013, Birmingham, UK, pages 85-92, 2013. DOI BIB
• Frits Dannenberg, Ernst Moritz Hahn (), Marta Z. Kwiatkowska: Computing Cumulative Rewards Using Fast Adaptive Uniformisation. In Computational Methods in Systems Biology - 11th International Conference, CMSB 2013, Klosterneuburg, Austria, September 22-24, 2013. Proceedings, volume 8130 of Lecture Notes in Computer Science, pages 33-49, 2013. DOI BIB
• Yang Gao, Ernst Moritz Hahn (), Naijun Zhan (), Lijun Zhang: CCMC: A Conditional CSL Model Checker for Continuous-Time Markov Chains. In Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings, volume 8172 of Lecture Notes in Computer Science, pages 464-468, 2013. DOI BIB
• Lijun Zhang, Zhikun She, Stefan Ratschan, Holger Hermanns (), Ernst Moritz Hahn (): Safety Verification for Probabilistic Hybrid Systems. In Eur. J. Control 18(6):572-587, 2012. DOI BIB
• Peter Buchholz, Ernst Moritz Hahn (), Holger Hermanns (), Lijun Zhang: Model Checking Algorithms for CTMDPs. In Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 225-242, 2011. DOI BIB
• Martin Fränzle, Ernst Moritz Hahn (), Holger Hermanns (), Nicolás Wolovick, Lijun Zhang: Measurability and safety verification for stochastic hybrid systems. In Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, IL, USA, April 12-14, 2011, pages 43-52, 2011. DOI BIB
• Ernst Moritz Hahn (), Holger Hermanns (), Lijun Zhang: Probabilistic reachability for parametric Markov models. In Int. J. Softw. Tools Technol. Transf. 13(1):3-19, 2011. DOI BIB
• Ernst Moritz Hahn (), Tingting Han, Lijun Zhang: Synthesis for PCTL in Parametric Markov Decision Processes. In NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings, volume 6617 of Lecture Notes in Computer Science, pages 146-161, 2011. DOI BIB
• Ernst Moritz Hahn (), Gethin Norman, David Parker, Björn Wachter, Lijun Zhang: Game-based Abstraction and Controller Synthesis for Probabilistic Hybrid Systems. In Eighth International Conference on Quantitative Evaluation of Systems, QEST 2011, Aachen, Germany, 5-8 September, 2011, pages 69-78, 2011. DOI BIB
• Joost-Pieter Katoen (), Ivan S. Zapreev, Ernst Moritz Hahn (), Holger Hermanns (), David N. Jansen (): The ins and outs of the probabilistic model checker MRMC. In Perform. Evaluation 68(2):90-104, 2011. DOI BIB
• Georgel Calin, Pepijn Crouzen, Pedro R. D'Argenio, Ernst Moritz Hahn (), Lijun Zhang: Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains. In Model Checking Software - 17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010. Proceedings, volume 6349 of Lecture Notes in Computer Science, pages 193-211, 2010. DOI BIB
• Ernst Moritz Hahn (), Holger Hermanns (), Björn Wachter, Lijun Zhang: PARAM: A Model Checker for Parametric Markov Models. In Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, volume 6174 of Lecture Notes in Computer Science, pages 660-664, 2010. DOI BIB
• Ernst Moritz Hahn (), Holger Hermanns (), Björn Wachter, Lijun Zhang: PASS: Abstraction Refinement for Infinite Probabilistic Models. In Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6015 of Lecture Notes in Computer Science, pages 353-357, 2010. DOI BIB
• Lijun Zhang, Zhikun She, Stefan Ratschan, Holger Hermanns (), Ernst Moritz Hahn (): Safety Verification for Probabilistic Hybrid Systems. In Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, volume 6174 of Lecture Notes in Computer Science, pages 196-211, 2010. DOI BIB
• Ernst Moritz Hahn (), Holger Hermanns (), Björn Wachter, Lijun Zhang: Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains. In Fundam. Informaticae 95(1):129-155, 2009. DOI BIB
• Ernst Moritz Hahn (), Holger Hermanns (), Björn Wachter, Lijun Zhang: INFAMY: An Infinite-State Markov Model Checker. In Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, volume 5643 of Lecture Notes in Computer Science, pages 641-647, 2009. DOI BIB
• Ernst Moritz Hahn (), Holger Hermanns (), Lijun Zhang: Probabilistic Reachability for Parametric Markov Models. In Model Checking Software, 16th International SPIN Workshop, Grenoble, France, June 26-28, 2009. Proceedings, volume 5578 of Lecture Notes in Computer Science, pages 88-106, 2009. DOI BIB
• Joost-Pieter Katoen (), Ivan S. Zapreev, Ernst Moritz Hahn (), Holger Hermanns (), David N. Jansen (): The Ins and Outs of the Probabilistic Model Checker MRMC. In QEST 2009, Sixth International Conference on the Quantitative Evaluation of Systems, Budapest, Hungary, 13-16 September 2009, pages 167-176, 2009. DOI BIB
• Lijun Zhang, Holger Hermanns (), Ernst Moritz Hahn (), Björn Wachter: Time-bounded model checking of infinite-state continuous-time Markov chains. In 8th International Conference on Application of Concurrency to System Design (ACSD 2008), Xi'an, China, June 23-27, 2008, pages 98-107, 2008. DOI BIB

Google Scholar page

Thesis

• Ernst Moritz Hahn (): Model checking stochastic hybrid systems. Saarland University, 2013. URL BIB.

Student projects

• Christian Josef Köhl: Probabilistische Aspekte – AspectKP – ein verteiltes Prozesskalkül

Teaching activities

• SS11: Tutor for the lecture Data Networks by Prof. Dr.-Ing. Holger Hermanns ()
• WS10/11: Assistant for the proseminar Im Zoo der Automaten by Prof. Dr.-Ing. Holger Hermanns ()
• SS10: Assistant for the advanced course Quantitative Model Checking by Prof. Dr.-Ing. Holger Hermanns ()
• SS09: Assistant for the advanced course Quantitative Model Checking by Dr. Lijun Zhang
• WS08/09: Assistant for the advanced course Testing Techniques by Prof. Dr.-Ing. Holger Hermanns () and Dr. Julien Schmaltz
• WS08/09: Assistant for the proseminar Im Zoo der Automaten by Prof. Dr.-Ing. Holger Hermanns ()
• SS08: Student assistant for the lecture Nebenläufige Programmierung by Prof. Dr.-Ing. Holger Hermanns ()
• SS07: Student assistant for the lecture Embedded Systems by Prof. Bernd Finkbeiner, Ph.D.

Participation in tool development

I have contributed to the development of the following tools:

• IscasMC (main developer)
• CCMC (participation in tool paper and internal review of homepage)
• PARAM (main developer)
• ProHVer (main developer)
• INFAMY (main developer)
• PASS (improvements on value iteration and code cleanup)
• PRISM (integration of parametric analysis and an extension of the fast adaptive uniformisation, see the development version 4.1.dev.r7596)
• MRMC (integration of two algorithms on continuous-time Markov decision processes)

My work also involves several smaller tools developed for single publications.

Participation in Projects in the past

• CAP - “Composition, Abstraction, and Parametrization for the Verification of Probabilistic Hybrid Systems”, Chinesisch-Deutsches Zentrum für Wissenschaftsförderung (CDZ)
• VERIWARE (University of Oxford)
• AVACS (S2, S3, H4) (Universität des Saarlandes)
• Quasimodo (Universität des Saarlandes)
• ROCKS (Universität des Saarlandes)
• ISAAC (OFFIS)

Education

• May 2013: Doctoral degree (Dr.-Ing.) “summa cum laude” from Universität des Saarlandes (defence: 21.12.2012)
• Apr. 2008: Second degree in Computer Science (Master) “with honours” received from Universität des Saarlandes
• Sept. 2005: First degree in Computer Science (Bachelor) received from Carl von Ossietzky Universität Oldenburg
• May 2008 – Oct. 2012: Studying Computer Science (Ph.D.) at Universität des Saarlandes
• Oct. 2006 – Apr. 2008: Studied Computer Science (Master) at Universität des Saarlandes
• Oct. 2002 – Sept. 2005: Studied Computer Science (Bachelor) with minors in Mathematics at Carl von Ossietzky Universität Oldenburg
• Aug. 1995 – Jun. 2002: Abitur at Altes Gymnasium Oldenburg

Professional appointments

• Jun. 2013 - Oct. 2017: Associate Research Professor at State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
• Oct. 2012 – May 2013: Research Assistant at University of Oxford
• May 2010 – Oct. 2012: Research Assistant at Universität des Saarlandes
• Oct. 2005 – Oct. 2006: Research Assistant at OFFIS, Safety Analysis & Verification (Oldenburg)

Scholarships and affiliations

• since Dec. 2013: Project “Model Checking of Complex and Hybrid Stochastic Systems”, Grant No. 61350110518, 61450110461, 61550110506 of Research Fund for International Young Scientists (extended two times)
• since Jun. 2013: Chinese Academy of Sciences fellowship for young international scientists, Grant No. 2013Y1GB0006 (extended two times)
• Jan. 2013 – May 2013: Member of Common Room of Wolfson College, Oxford
• Feb. 2010 – Apr. 2010: 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 Innovacíon Productiva (MINCyT)
• May 2008 – Apr. 2010: Scholarship of the graduate school “Leistungsgarantien für Rechnersysteme” of the Deutsche Forschungsgemeinschaft
• 2009: Faculty Nomination for a stipend of the “Deutsche Telekom Stiftung”

Personal data

• Full name: Ernst Moritz Hahn
• Date of birth: October 3rd, 1982
• Place of birth: Fernwald, Germany (Hesse)

Language proficiency

• German: native speaker
• English: highly proficient in spoken and written language
• Chinese (Mandarin): good command