Photo of Moritz Hahn
  • Room 01.004 - Computer Science Building

    United Kingdom

Accepting PhD Students

PhD projects

I am open to PhD projects related to the area of (stochastic/probabilistic) model checking and generally formal methods such as but not limited to - very large or infinitely large models (using state-space truncation, finite-state projection, (multi-terminal) binary decision diagrams (BDDs), satisfiability modulo theories (SMT), and similar approaches) - analysis of parametric and interval Markov models - stochastic parity games - stochastic hybrid (discrete-continuous) systems - efficient algorithms for deciding linear time logic properties (omega-regular properties) - learning of Markov models - real-world applications of such methods

20062019

Research output per year

If you made any changes in Pure these will be visible here soon.

Research Output

2019

ARCH-COMP19 Category Report: Stochastic Modelling

Abate, A., Blom, H., Cauchi, N., Degiorgio, K., Fränzle, M., Hahn, E. M., Haesaert, S., Ma, H., Oishi, M., Pilch, C., Remke, A., Salamati, M., Soudjani, S., Huijgevoort, B. V. & Vinod, A. P., 2019, ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systemsi, part of CPS-IoT Week 2019, Montreal, QC, Canada, April 15, 2019.. p. 62-102 41 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Interval Markov Decision Processes with Multiple Objectives: from Robust Strategies to Pareto Curves

Hahn, E. M., Hashemi, V., Hermanns, H., Lahijanian, M. & Turrini, A., 18 Nov 2019, In : ACM Transactions on Modeling and Computer Simulation. 29, 4, 31 p., 27.

Research output: Contribution to journalArticle

Open Access
File
1 Citation (Scopus)
26 Downloads (Pure)

Omega-Regular Objectives in Model-Free Reinforcement Learning

Hahn, E. M., Perez, M., Schewe, S., Somenzi, F., Trivedi, A. & Liverpool, U., 04 Apr 2019, TACAS: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer Lecture Notes in Computer Science (LNCS), Vol. 11427. p. 395-412 (Lecture Notes in Computer Science; vol. 11427).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Open Access
File
6 Citations (Scopus)
74 Downloads (Pure)

The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models - (QComp 2019 Competition Report)

Hahn, E. M., Hartmanns, A., Hensel, C., Klauck, M., Klein, J., Kretínský, J., Parker, D., Quatmann, T., Ruijters, E. & Steinmetz, M., 2019, 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: TOOLympics, Held as Part of ETAPS 2019, Proceedings. Steffen, B., Kordon, F., Beyer, D. & Huisman, M. (eds.). p. 69-92 24 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

6 Citations (Scopus)
2018

Accelerated Model Checking of Parametric Markov Chains

Gainer, P., Hahn, E. M. & Schewe, S., 30 Sep 2018, International Symposium on Automated Technology for Verification and Analysis, 2018. p. 300-316 17 p. (Lecture notes in Computer Science; vol. 11138).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Open Access
File
4 Citations (Scopus)
156 Downloads (Pure)

Incremental Verification of Parametric and Reconfigurable Markov Chains

Gainer, P., Hahn, E. M., Liverpool, U. & Schewe, S., 2018, Quantitative Evaluation of Systems - 15th International Conference, QEST 2018, Beijing, China, September 4-7, 2018: Proceedings. Springer, Vol. 11024. p. 140-156 17 p. (Lecture Notes in Computer Science; vol. 11024).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Open Access
File
2 Citations (Scopus)
65 Downloads (Pure)
2017

JANI: Quantitative Model and Tool Interaction

Budde, C. E., Dehnert, C., Hahn, E. M., Hartmanns, A., Junges, S. & Turrini, A., 01 May 2017, TACAS: International Conference on Tools and Algorithms for the Construction and Analysis of Systems: 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. Springer, p. 151-168 18 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Open Access
File
16 Citations (Scopus)
17 Downloads (Pure)

Model Checking Omega-regular Properties for Quantum Markov Chains

Feng, Y., Hahn, E. M., Turrini, A. & Ying, S., 25 Aug 2017, 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Vol. 85. p. 35:1-35:16

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Open Access
File
1 Citation (Scopus)
6 Downloads (Pure)

Multi-objective Robust Strategy Synthesis for Interval Markov Decision Processes

Hahn, E. M., Hashemi, V., Hermanns, H., Lahijanian, M. & Turrini, A., 01 Dec 2017, Quantitative Evaluation of Systems - 14th International Conference, QEST 2017, Berlin, Germany, September 5-7, 2017, Proceedings. Springer, Vol. 10503. p. 207-223 17 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Citations (Scopus)

Polynomial-Time Alternating Probabilistic Bisimulation for Interval MDPs

Hashemi, V., Turrini, A., Hahn, E. M., Hermanns, H. & Elbassioni, K., 01 Nov 2017, Dependable Software Engineering. Theories, Tools, and Applications: Dependable Software Engineering. Theories, Tools, and Applications - Third International Symposium, SETTA 2017, Changsha, China, October 23-25, 2017, Proceedings. Springer, p. 25-41 17 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games

Hahn, E. M., Schewe, S., Turrini, A. & Zhang, L., 01 Feb 2017, Verification, Model Checking, and Abstract Interpretation : 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings. Springer, p. 266-287 22 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)
2016

A Comparison of Time- and Reward-Bounded Probabilistic Model Checking Techniques

Hahn, E. M. & Hartmanns, A., 06 Oct 2016, Dependable Software Engineering: Theories, Tools, and Applications - Second International Symposium, SETTA 2016, Beijing, China, November 9-11, 2016, Proceedings. Springer, p. 85-100 16 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

5 Citations (Scopus)

An Efficient Synthesis Algorithm for Parametric Markov Chains Against Linear Time Properties

Li, Y., Liu, W., Turrini, A., Hahn, E. M. & Zhang, L., 06 Oct 2016, Dependable Software Engineering: Theories, Tools, and Applications - Second International Symposium, SETTA 2016, Beijing, China, November 9-11, 2016, Proceedings. Springer, Vol. 9984. p. 280-296 (Lecture Notes in Computer Science ; vol. 9984).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

A Simple Algorithm for Solving Qualitative Probabilistic Parity Games

Hahn, E. M., Schewe, S., Turrini, A. & Zhang, L., 2016, p. 291. 311 p.

Research output: Contribution to conferencePaper

4 Citations (Scopus)

Exploiting Robust Optimization for Interval Probabilistic Bisimulation

Hahn, E. M., Hashemi, V., Hermanns, H. & Turrini, A., 2016, Quantitative Evaluation of Systems - 13th International Conference, QEST 2016, Quebec City, QC, Canada, August 23-25, 2016, Proceedings. p. 55-71 17 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)

GPU-Accelerated Value Iteration for the Computation of Reachability Probabilities in MDPs

Wu, Z., Hahn, E. M., Günay, A., Zhang, L. & Liu, Y., 02 Sep 2016, 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). IOS Press, Vol. 285. p. 1726-1727 2 p. (Frontiers in Artificial Intelligence and Applications; vol. 285).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Open Access
File
1 Citation (Scopus)
27 Downloads (Pure)
2015

A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking

Dijk, T. V., Hahn, E. M., Jansen, D. N., Li, Y., Neele, T., Stoelinga, M., Turrini, A. & Zhang, L., 2015, Dependable Software Engineering: Theories, Tools, and Applications - First International Symposium, SETTA 2015, Nanjing, China, November 4-6, 2015, Proceedings. p. 35-51 17 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

8 Citations (Scopus)

Computing Cumulative Rewards Using Fast Adaptive Uniformization

Dannenberg, F., Hahn, E. M. & Kwiatkowska, M. Z., 06 Apr 2015, In : ACM Transactions on Modeling and Computer Simulation. 25, 2, 23 p., 9.

Research output: Contribution to journalArticle

3 Citations (Scopus)

Lazy Probabilistic Model Checking without Determinisation

Hahn, E. M., Li, G., Liverpool, U., Turrini, A. & Zhang, L., 2015, 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015. p. 354-367 14 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

17 Citations (Scopus)

QPMC: A Model Checker for Quantum Programs and Protocols

Feng, Y., Hahn, E. M., Turrini, A. & Zhang, L., 2015, FM 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings. p. 265-272 8 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

9 Citations (Scopus)

Transient Reward Approximation for Continuous-Time Markov Chains

Hahn, E. M., Hermanns, H., Wimmer, R. & Becker, B., 01 Dec 2015, In : IEEE Transactions on Reliability . 64, 4, p. 1254-1275

Research output: Contribution to journalArticle

2 Citations (Scopus)
2014

iscasMc: A Web-Based Probabilistic Model Checker

Hahn, E. M., Li, Y., Liverpool, U., Turrini, A. & Zhang, L., 2014, FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings. p. 312-317 6 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

42 Citations (Scopus)

Model Checking CSL for Markov Population Models

Spieler, D., Hahn, E. M. & Zhang, L., 2014, Proceedings Twelfth International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2014, Grenoble, France, 12-13 April 2014.. p. 93-107 15 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)

Reachability and Reward Checking for Stochastic Timed Automata

Hahn, E. M., Hartmanns, A. & Hermanns, H., 2014, In : ECEASST. 70, 15 p.

Research output: Contribution to journalArticle

Open Access
File
14 Citations (Scopus)
2013

A compositional modelling and analysis framework for stochastic hybrid systems

Hahn, E. M., Hartmanns, A., Hermanns, H. & Katoen, J-P., 2013, In : Formal Methods in System Design. 43, 2, p. 191-232 42 p.

Research output: Contribution to journalArticle

56 Citations (Scopus)

CCMC: A Conditional CSL Model Checker for Continuous-Time Markov Chains

Gao, Y., Hahn, E. M., Zhan, N. & Zhang, L., 2013, Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings. p. 464-468 5 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

Computing Cumulative Rewards Using Fast Adaptive Uniformisation

Dannenberg, F., Hahn, E. M. & Kwiatkowska, M. Z., 2013, Computational Methods in Systems Biology - 11th International Conference, CMSB 2013, Klosterneuburg, Austria, September 22-24, 2013. Proceedings. p. 33-49 17 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

5 Citations (Scopus)

Model checking for performability

Baier, C., Hahn, E. M., Haverkort, B. R., Hermanns, H. & Katoen, J-P., Aug 2013, In : Mathematical Structures in Computer Science. 23, 4, p. 751-795 45 p.

Research output: Contribution to journalArticle

14 Citations (Scopus)

Model checking stochastic hybrid systems

Hahn, E. M., 2013

Research output: Book/ReportCommissioned report

Model Repair for Markov Decision Processes

Chen, T., Hahn, E. M., Han, T., Kwiatkowska, M. Z., Qu, H. & Zhang, L., 2013, Seventh International Symposium on Theoretical Aspects of Software Engineering, TASE 2013, 1-3 July 2013, Birmingham, UK. p. 85-92 8 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

44 Citations (Scopus)

Rewarding probabilistic hybrid automata

Hahn, E. M. & Hermanns, H., 2013, Proceedings of the 16th international conference on Hybrid systems: computation and control, HSCC 2013, April 8-11, 2013, Philadelphia, PA, USA. p. 313-322 10 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)
2012

Safety Verification for Probabilistic Hybrid Systems

Zhang, L., She, Z., Ratschan, S., Hermanns, H. & Hahn, E. M., 2012, In : Eur. J. Control. 18, 6, p. 572-587 16 p.

Research output: Contribution to journalArticle

15 Citations (Scopus)

Variable Probabilistic Abstraction Refinement

Fioriti, L. M. F., Hahn, E. M., Hermanns, H. & Wachter, B., 2012, Automated Technology for Verification and Analysis - 10th International Symposium, ATVA 2012, Thiruvananthapuram, India, October 3-6, 2012. Proceedings. p. 300-316 17 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)
2011

Bounded Fairness for Probabilistic Distributed Algorithms

Crouzen, P., Hahn, E. M., Hermanns, H., Dhama, A., Theel, O. E., Wimmer, R., Braitling, B. & Becker, B., 2011, 11th International Conference on Application of Concurrency to System Design, ACSD 2011, Newcastle Upon Tyne, UK, 20-24 June, 2011. p. 89-97 9 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Citations (Scopus)

Game-based Abstraction and Controller Synthesis for Probabilistic Hybrid Systems

Hahn, E. M., Norman, G., Parker, D., Wachter, B. & Zhang, L., 2011, Eighth International Conference on Quantitative Evaluation of Systems, QEST 2011, Aachen, Germany, 5-8 September, 2011. p. 69-78 10 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

17 Citations (Scopus)

Measurability and safety verification for stochastic hybrid systems

Fränzle, M., Hahn, E. M., Hermanns, H., Wolovick, N. & Zhang, L., 2011, Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, IL, USA, April 12-14, 2011. p. 43-52 10 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

42 Citations (Scopus)

Model Checking Algorithms for CTMDPs

Buchholz, P., Hahn, E. M., Hermanns, H. & Zhang, L., 2011, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings. p. 225-242 18 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

24 Citations (Scopus)

Probabilistic reachability for parametric Markov models

Hahn, E. M., Hermanns, H. & Zhang, L., 2011, In : STTT. 13, 1, p. 3-19 17 p.

Research output: Contribution to journalArticle

89 Citations (Scopus)

Reachability analysis for incomplete networks of Markov decision processes

Wimmer, R., Hahn, E. M., Hermanns, H. & Becker, B., 2011, 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign, MEMOCODE 2011, Cambridge, UK, 11-13 July, 2011. p. 151-160 10 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Synthesis for PCTL in Parametric Markov Decision Processes

Hahn, E. M., Han, T. & Zhang, L., 2011, NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings. p. 146-161 16 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

41 Citations (Scopus)

The ins and outs of the probabilistic model checker MRMC

Katoen, J-P., Zapreev, I. S., Hahn, E. M., Hermanns, H. & Jansen, D. N., 2011, In : Perform. Eval.. 68, 2, p. 90-104 15 p.

Research output: Contribution to journalArticle

141 Citations (Scopus)
2010

PARAM: A Model Checker for Parametric Markov Models

Hahn, E. M., Hermanns, H., Wachter, B. & Zhang, L., 2010, Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings. p. 660-664 5 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

68 Citations (Scopus)

PASS: Abstraction Refinement for Infinite Probabilistic Models

Hahn, E. M., Hermanns, H., Wachter, B. & Zhang, L., 2010, 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. p. 353-357 5 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

22 Citations (Scopus)

Safety Verification for Probabilistic Hybrid Systems

Zhang, L., She, Z., Ratschan, S., Hermanns, H. & Hahn, E. M., 2010, Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings. p. 196-211 16 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

30 Citations (Scopus)

Symblicit Calculation of Long-Run Averages for Concurrent Probabilistic Systems

Wimmer, R., Braitling, B., Becker, B., Hahn, E. M., Crouzen, P., Hermanns, H., Dhama, A. & Theel, O. E., 2010, QEST 2010, Seventh International Conference on the Quantitative Evaluation of Systems, Williamsburg, Virginia, USA, 15-18 September 2010. p. 27-36 10 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

18 Citations (Scopus)

Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains

Calin, G., Crouzen, P., D'Argenio, P. R., Hahn, E. M. & Zhang, L., 2010, Model Checking Software - 17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010. Proceedings. p. 193-211 19 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Citations (Scopus)
2009

INFAMY: An Infinite-State Markov Model Checker

Hahn, E. M., Hermanns, H., Wachter, B. & Zhang, L., 2009, Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings. p. 641-647 7 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

18 Citations (Scopus)

Probabilistic Reachability for Parametric Markov Models

Hahn, E. M., Hermanns, H. & Zhang, L., 2009, Model Checking Software, 16th International SPIN Workshop, Grenoble, France, June 26-28, 2009. Proceedings. p. 88-106 19 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

27 Citations (Scopus)

The Ins and Outs of the Probabilistic Model Checker MRMC

Katoen, J-P., Zapreev, I. S., Hahn, E. M., Hermanns, H. & Jansen, D. N., 2009, QEST 2009, Sixth International Conference on the Quantitative Evaluation of Systems, Budapest, Hungary, 13-16 September 2009. p. 167-176 10 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

73 Citations (Scopus)

Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains

Hahn, E. M., Hermanns, H., Wachter, B. & Zhang, L., 2009, In : Fundam. Inform.. 95, 1, p. 129-155 27 p.

Research output: Contribution to journalArticle

12 Citations (Scopus)