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
Article
2019
1 Citation (Scopus)
14 Downloads (Pure)

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
Multiple Objectives
Markov Decision Process
Pareto
Transition Probability
Curve
2015
3 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

Stochastic models
Markov processes
Chemical reactions
Chemical analysis
Statistical Models
2 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

Computer viruses
Reliability analysis
Electric network analysis
Computer networks
Markov processes
2014
14 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
Model checking
Real time systems
Hybrid systems
Statistical Models
2013
54 Citations (Scopus)

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

Hybrid systems
Hybrid Systems
Stochastic Systems
Modeling
High level languages
14 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

Model checking
Temporal logic
Stochastic models
2012
14 Citations (Scopus)

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

Hybrid systems
2011
87 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

Rational functions
Finite automata
Markov processes
138 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

Model checking
Reward
Probabilistic Model
Discrete event simulation
Model Checking
2009
12 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

Model checking
Markov processes
Availability
Explosions