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
If you made any changes in Pure these will be visible here soon.

Research Output 2006 2019

Filter
Conference contribution
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

4 Citations (Scopus)
48 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
Reinforcement learning
Learning algorithms
6 Citations (Scopus)

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

Markov processes
Statistical Models
2018
4 Citations (Scopus)
131 Downloads (Pure)

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
Model checking
Markov processes
Data structures
Sales
Specifications
2 Citations (Scopus)
44 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
Markov processes
Chemical analysis
Costs
2017
13 Citations (Scopus)
17 Downloads (Pure)

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
Model checking
Network protocols
User interfaces
Interfaces (computer)
Modeling languages
1 Citation (Scopus)
3 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
Model Checking
Markov chain
Connected Components
State Space
Operator
6 Citations (Scopus)

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

Uncertainty

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

Polynomials
Linear programming
Computational complexity
Controllers
Uncertainty
1 Citation (Scopus)

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

2016
5 Citations (Scopus)

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

Model checking
Scalability
Linear programming
Statistical Models
1 Citation (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

Markov processes
Surface mount technology
2 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

Model checking
Explosions
Polynomials
Uncertainty
1 Citation (Scopus)
14 Downloads (Pure)

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
2015
8 Citations (Scopus)

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

Binary decision diagrams
Model checking
Data structures
Experiments
16 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

Model checking
Markov processes
Specifications
Chemical analysis
Experiments
8 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

commands
2014
40 Citations (Scopus)

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

Markov processes
Specifications
Statistical Models
2 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

Model checking
Biological systems
Markov processes
Semantics
2013
1 Citation (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

Markov processes
5 Citations (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

Stochastic models
Markov processes
Chemical reactions
Chemical analysis
Statistical Models
42 Citations (Scopus)

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

Repair
Computer viruses
Costs
Sampling
1 Citation (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

Wireless sensor networks
Energy utilization
Bandwidth
Data storage equipment
Costs
2012
2 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

Markov processes
Sensor networks
2011
4 Citations (Scopus)

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

Parallel algorithms
Model checking
Sensor networks
16 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

Hybrid systems
Controllers
38 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

Hybrid systems
Probability distributions
Wireless sensor networks
Differential equations
Semantics
24 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

Model checking
Stochastic systems

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

40 Citations (Scopus)

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

Markov processes
Concretes
Specifications
2010
68 Citations (Scopus)

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

Markov processes
Rational functions
Algebra
Polynomials
22 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

Numerical methods
Surface mount technology
Interpolation
Engines
Network protocols
29 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

Hybrid systems
Real time control
18 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

Markov processes
Binary decision diagrams
Linear equations
Data structures
Data storage equipment
3 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

Nonlinear programming
Polynomials
2009
18 Citations (Scopus)

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

Markov processes
Model checking
Explosions
27 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

Regular Expressions
Parametric Model
Reachability
Markov Model
Nondeterminism
73 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

Model checking
Discrete event simulation
Statistical Models
2008
10 Citations (Scopus)

Time-bounded model checking of infinite-state continuous-time Markov chains

Zhang, L., Hermanns, H., Hahn, E. M. & Wachter, B., 2008, 8th International Conference on Application of Concurrency to System Design (ACSD 2008), Xi'an, China, June 23-27, 2008. p. 98-107 10 p.

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

Model checking
Markov processes
Availability
Explosions
Systems analysis
2006
18 Citations (Scopus)

Towards a Unified Model-Based Safety Assessment

Peikenkamp, T., Cavallo, A., Valacca, L., Böde, E., Pretzer, M. & Hahn, E. M., 2006, Computer Safety, Reliability, and Security, 25th International Conference, SAFECOMP 2006, Gdansk, Poland, September 27-29, 2006, Proceedings. p. 275-288 14 p.

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

Reusability
Failure modes
Aircraft
Specifications