Towards a Unified Model-Based Safety Assessment. - Thomas Peikenkamp; Antonella Cavallo; Laura Valacca; Eckard Böde; Matthias Pretzer; Ernst Moritz Hahn (SAFECOMP, 2006)

INFAMY: An Infinite-State Markov Model Checker. - Ernst Moritz Hahn; Holger Hermanns; Björn Wachter; Lijun Zhang 001 (CAV, 2009)

Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains. - Ernst Moritz Hahn; Holger Hermanns; Björn Wachter; Lijun Zhang 001 (Fundam. Informaticae, 2009)

PARAM: A Model Checker for Parametric Markov Models. - Ernst Moritz Hahn; Holger Hermanns; Björn Wachter; Lijun Zhang 001 (CAV, 2010)

Symblicit Calculation of Long-Run Averages for Concurrent Probabilistic Systems. - Ralf Wimmer 001; Bettina Braitling; Bernd Becker 001; Ernst Moritz Hahn; Pepijn Crouzen; Holger Hermanns; Abhishek Dhama; Oliver E. Theel (QEST, 2010)

Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains. - Georgel Calin; Pepijn Crouzen; Pedro R. D'Argenio; Ernst Moritz Hahn; Lijun Zhang 001 (SPIN, 2010)

PASS: Abstraction Refinement for Infinite Probabilistic Models. - Ernst Moritz Hahn; Holger Hermanns; Björn Wachter; Lijun Zhang 001 (TACAS, 2010)

Bounded Fairness for Probabilistic Distributed Algorithms. - Pepijn Crouzen; Ernst Moritz Hahn; Holger Hermanns; Abhishek Dhama; Oliver E. Theel; Ralf Wimmer 001; Bettina Braitling; Bernd Becker 001 (ACSD, 2011)

Model Checking Algorithms for CTMDPs. - Peter Buchholz 001; Ernst Moritz Hahn; Holger Hermanns; Lijun Zhang 001 (CAV, 2011)

Measurability and safety verification for stochastic hybrid systems. - Martin Fränzle; Ernst Moritz Hahn; Holger Hermanns; Nicolás Wolovick; Lijun Zhang 001 (HSCC, 2011)

Reachability analysis for incomplete networks of Markov decision processes. - Ralf Wimmer 001; Ernst Moritz Hahn; Holger Hermanns; Bernd Becker 001 (MEMOCODE, 2011)

Synthesis for PCTL in Parametric Markov Decision Processes. - Ernst Moritz Hahn; Tingting Han 001; Lijun Zhang 001 (NASA Formal Methods, 2011)

Game-based Abstraction and Controller Synthesis for Probabilistic Hybrid Systems. - Ernst Moritz Hahn; Gethin Norman; David Parker 001; Björn Wachter; Lijun Zhang 001 (QEST, 2011)

The ins and outs of the probabilistic model checker MRMC. - Joost-Pieter Katoen; Ivan S. Zapreev; Ernst Moritz Hahn; Holger Hermanns; David N. Jansen (Perform. Evaluation, 2011)

Probabilistic reachability for parametric Markov models. - Ernst Moritz Hahn; Holger Hermanns; Lijun Zhang 001 (Int. J. Softw. Tools Technol. Transf., 2011)

Variable Probabilistic Abstraction Refinement. - Luis María Ferrer Fioriti; Ernst Moritz Hahn; Holger Hermanns; Björn Wachter (ATVA, 2012)

Transient Reward Approximation for Grids, Crowds, and Viruses - Ernst Moritz Hahn; Holger Hermanns; Ralf Wimmer 001; Bernd Becker 001 (CoRR, 2012)

Safety Verification for Probabilistic Hybrid Systems. - Lijun Zhang 001; Zhikun She; Stefan Ratschan; Holger Hermanns; Ernst Moritz Hahn (Eur. J. Control, 2012)

CCMC: A Conditional CSL Model Checker for Continuous-Time Markov Chains. - Yang Gao; Ernst Moritz Hahn; Naijun Zhan; Lijun Zhang 001 (ATVA, 2013)

Computing Cumulative Rewards Using Fast Adaptive Uniformisation. - Frits Dannenberg; Ernst Moritz Hahn; Marta Z. Kwiatkowska (CMSB, 2013)

Rewarding probabilistic hybrid automata. - Ernst Moritz Hahn; Holger Hermanns (HSCC, 2013)

Model Repair for Markov Decision Processes. - Taolue Chen 001; Ernst Moritz Hahn; Tingting Han 001; Marta Z. Kwiatkowska; Hongyang Qu 001; Lijun Zhang 001 (TASE, 2013)

Lazy Determinisation for Quantitative Model Checking. - Ernst Moritz Hahn; Guangyuan Li; Sven Schewe; Lijun Zhang 001 (CoRR, 2013)

A compositional modelling and analysis framework for stochastic hybrid systems. - Ernst Moritz Hahn; Arnd Hartmanns; Holger Hermanns; Joost-Pieter Katoen (Formal Methods Syst. Des., 2013)

Model checking for performability. - Christel Baier; Ernst Moritz Hahn; Boudewijn R. Haverkort; Holger Hermanns; Joost-Pieter Katoen (Math. Struct. Comput. Sci., 2013)

Model checking stochastic hybrid systems. - Ernst Moritz Hahn (2013)

iscasMc: A Web-Based Probabilistic Model Checker. - Ernst Moritz Hahn; Yi Li; Sven Schewe; Andrea Turrini; Lijun Zhang 001 (FM, 2014)

Model Checking CSL for Markov Population Models - David Spieler; Ernst Moritz Hahn; Lijun Zhang 001 (QAPL, 2014)

Reachability and Reward Checking for Stochastic Timed Automata. - Ernst Moritz Hahn; Arnd Hartmanns; Holger Hermanns (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2014)

Lazy Probabilistic Model Checking without Determinisation. - Ernst Moritz Hahn; Guangyuan Li; Sven Schewe; Andrea Turrini; Lijun Zhang 001 (CONCUR, 2015)

QPMC: A Model Checker for Quantum Programs and Protocols. - Yuan Feng 001; Ernst Moritz Hahn; Andrea Turrini; Lijun Zhang 001 (FM, 2015)

A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking. - Tom van Dijk; Ernst Moritz Hahn; David N. Jansen; Yong Li 031; Thomas Neele; Mariëlle Stoelinga; Andrea Turrini; Lijun Zhang 001 (SETTA, 2015)

Computing Cumulative Rewards Using Fast Adaptive Uniformization. - Frits Dannenberg; Ernst Moritz Hahn; Marta Z. Kwiatkowska (ACM Trans. Model. Comput. Simul., 2015)

Transient Reward Approximation for Continuous-Time Markov Chains. - Ernst Moritz Hahn; Holger Hermanns; Ralf Wimmer 001; Bernd Becker 001 (IEEE Trans. Reliab., 2015)

A Simple Algorithm for Solving Qualitative Probabilistic Parity Games. - Ernst Moritz Hahn; Sven Schewe; Andrea Turrini; Lijun Zhang 001 (CAV (2), 2016)

GPU-Accelerated Value Iteration for the Computation of Reachability Probabilities in MDPs. - Zhimin Wu; Ernst Moritz Hahn; Akin Günay; Lijun Zhang 001; Yang Liu 003 (ECAI, 2016)

Exploiting Robust Optimization for Interval Probabilistic Bisimulation. - Ernst Moritz Hahn; Vahid Hashemi; Holger Hermanns; Andrea Turrini (QEST, 2016)

A Comparison of Time- and Reward-Bounded Probabilistic Model Checking Techniques. - Ernst Moritz Hahn; Arnd Hartmanns (SETTA, 2016)

An Efficient Synthesis Algorithm for Parametric Markov Chains Against Linear Time Properties. - Yong Li 031; Wanwei Liu; Andrea Turrini; Ernst Moritz Hahn; Lijun Zhang 001 (SETTA, 2016)

Efficient Algorithms for Time- and Cost-Bounded Probabilistic Model Checking. - Ernst Moritz Hahn; Arnd Hartmanns (CoRR, 2016)

Model Checking Omega-regular Properties for Quantum Markov Chains . - Yuan Feng 001; Ernst Moritz Hahn; Andrea Turrini; Shenggang Ying (CONCUR, 2017)

Multi-objective Robust Strategy Synthesis for Interval Markov Decision Processes. - Ernst Moritz Hahn; Vahid Hashemi; Holger Hermanns; Morteza Lahijanian; Andrea Turrini (QEST, 2017)

Polynomial-Time Alternating Probabilistic Bisimulation for Interval MDPs. - Vahid Hashemi; Andrea Turrini; Ernst Moritz Hahn; Holger Hermanns; Khaled M. Elbassioni (SETTA, 2017)

JANI: Quantitative Model and Tool Interaction. - Carlos E. Budde; Christian Dehnert; Ernst Moritz Hahn; Arnd Hartmanns; Sebastian Junges; Andrea Turrini (TACAS (2), 2017)

Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games. - Ernst Moritz Hahn; Sven Schewe; Andrea Turrini; Lijun Zhang 001 (VMCAI, 2017)

Accelerated Model Checking of Parametric Markov Chains. - Paul Gainer; Ernst Moritz Hahn; Sven Schewe (ATVA, 2018)

Incremental Verification of Parametric and Reconfigurable Markov Chains. - Paul Gainer; Ernst Moritz Hahn; Sven Schewe (QEST, 2018)

ARCH-COMP19 Category Report: Stochastic Modelling. - Alessandro Abate; Henk A. P. Blom; Nathalie Cauchi; Kurt Degiorgio; Martin Fränzle; Ernst Moritz Hahn; Sofie Haesaert; Hao Ma; Meeko Oishi; Carina Pilch; Anne Remke; Mahmoud Salamati; et al. (ARCH@CPSIoTWeek, 2019)

Limit reachability for model-free reinforcement learning of ω-regular objectives. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (SNR, 2019)

The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models - (QComp 2019 Competition Report). - Ernst Moritz Hahn; Arnd Hartmanns; Christian Hensel; Michaela Klauck; Joachim Klein 001; Jan Kretínský; David Parker 001; Tim Quatmann; Enno Ruijters; Marcel Steinmetz (TACAS (3), 2019)

Omega-Regular Objectives in Model-Free Reinforcement Learning. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (TACAS (1), 2019)

Good-for-MDPs Automata. - Ernst Moritz Hahn; Mateo Perez; Fabio Somenzi; Ashutosh Trivedi 001; Sven Schewe; Dominik Wojtczak (CoRR, 2019)

Interval Markov Decision Processes with Multiple Objectives: From Robust Strategies to Pareto Curves. - Ernst Moritz Hahn; Vahid Hashemi; Holger Hermanns; Morteza Lahijanian; Andrea Turrini (ACM Trans. Model. Comput. Simul., 2019)

Faithful and Effective Reward Schemes for Model-Free Reinforcement Learning of Omega-Regular Objectives. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (ATVA, 2020)

Model-Free Reinforcement Learning for Stochastic Parity Games. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (CONCUR, 2020)

Good-for-MDPs Automata for Probabilistic Analysis and Reinforcement Learning. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (TACAS (1), 2020)

Reward Shaping for Reinforcement Learning with Omega-Regular Objectives. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (CoRR, 2020)

Model-Free Reinforcement Learning for Branching Markov Decision Processes. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (CAV (2), 2021)

Model-Free Reinforcement Learning for Lexicographic Omega-Regular Objectives. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (FM, 2021)

Symblicit exploration and elimination for probabilistic model checking. - Ernst Moritz Hahn; Arnd Hartmanns (SAC, 2021)

The Marriage Between Safety and Cybersecurity: Still Practicing. - Mariëlle Stoelinga; Christina Kolb; Stefano M. Nicoletti; Carlos E. Budde; Ernst Moritz Hahn (SPIN, 2021)

Mungojerrie: Reinforcement Learning of Linear-Time Objectives. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (CoRR, 2021)

Model-free Reinforcement Learning for Branching Markov Decision Processes (Artifact Evaluation for CAV 2021). - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (Zenodo, 2021)

An Impossibility Result in Automata-Theoretic Reinforcement Learning. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (ATVA, 2022)

Alternating Good-for-MDPs Automata. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (ATVA, 2022)

BFL: a Logic to Reason about Fault Trees. - Stefano M. Nicoletti; Ernst Moritz Hahn; Mariëlle Stoelinga (DSN, 2022)

Reinforcement Learning with Guarantees that Hold for Ever. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (FMICS, 2022)

Recursive Reinforcement Learning. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (NeurIPS, 2022)

EPMC Gets Knowledge in Multi-agent Systems. - Chen Fu; Ernst Moritz Hahn; Yong Li 031; Sven Schewe; Meng Sun 002; Andrea Turrini; Lijun Zhang 001 (VMCAI, 2022)

Alternating Good-for-MDP Automata. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (CoRR, 2022)

Probabilistic Preference Planning Problem for Markov Decision Processes. - Meilun Li; Andrea Turrini; Ernst Moritz Hahn; Zhikun She; Lijun Zhang 001 (IEEE Trans. Software Eng., 2022)

Scenario Approach for Parametric Markov Models. - Ying Liu 048; Andrea Turrini; Ernst Moritz Hahn; Bai Xue 001; Lijun Zhang 001 (ATVA (1), 2023)

Omega-Regular Reward Machines. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (ECAI, 2023)

Backdoor Mitigation in Deep Neural Networks via Strategic Retraining. - Akshay Dhonthi; Ernst Moritz Hahn; Vahid Hashemi (FM, 2023)

sfPFL: A Probabilistic Logic for Fault Trees. - Stefano M. Nicoletti; Milan Lopuhaä-Zwakenberg; Ernst Moritz Hahn; Mariëlle Stoelinga (FM, 2023)

Solving Queries for Boolean Fault Tree Logic via Quantified SAT. - Caz Saaltink; Stefano M. Nicoletti; Matthias Volk 001; Ernst Moritz Hahn; Mariëlle Stoelinga (FTSCS, 2023)

sfATM: A Logic for Quantitative Security Properties on Attack Trees. - Stefano M. Nicoletti; Milan Lopuhaä-Zwakenberg; Ernst Moritz Hahn; Mariëlle Stoelinga (SEFM, 2023)

Mungojerrie: Linear-Time Objectives in Model-Free Reinforcement Learning. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (TACAS (1), 2023)

Tools at the Frontiers of Quantitative Verification - QComp 2023 Competition Report. - Roman Andriushchenko; Alexander Bork; Carlos E. Budde; Milan Ceska 002; Kush Grover; Ernst Moritz Hahn; Arnd Hartmanns; Bryant Israelsen; Nils Jansen 001; Joshua Jeppson; Sebastian Junges; Maximilian A. Köhl; et al. (TOOLympics@ETAPS, 2023)

PFL: a Probabilistic Logic for Fault Trees. - Stefano M. Nicoletti; Milan Lopuhaä-Zwakenberg; Ernst Moritz Hahn; Mariëlle Stoelinga (CoRR, 2023)

ATM: a Logic for Quantitative Security Properties on Attack Trees. - Stefano M. Nicoletti; Milan Lopuhaä-Zwakenberg; Ernst Moritz Hahn; Mariëlle Stoelinga (CoRR, 2023)

Multi-objective ω-Regular Reinforcement Learning. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (Formal Aspects Comput., 2023)

Artifact for the ATVA'23 paper "Scenario Approach for Parametric Markov Models". - Ying Liu 048; Andrea Turrini; Ernst Moritz Hahn; Bai Xue 001; Lijun Zhang 001 (Zenodo, 2023)

Omega-Regular Decision Processes. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (AAAI, 2024)

Multi-Agent Reinforcement Learning for Alternating-Time Logic. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (ECAI, 2024)

Autonomous Vehicles Path Planning Under Temporal Logic Specifications. - Akshay Dhonthi; Nicolas Schischka; Ernst Moritz Hahn; Vahid Hashemi (SBMF, 2024)

AGNES: Abstraction-Guided Framework for Deep Neural Networks Security. - Akshay Dhonthi; Marcello Eiermann; Ernst Moritz Hahn; Vahid Hashemi (VMCAI (2), 2024)

Querying Fault and Attack Trees: Property Specification on a Water Network. - Stefano M. Nicoletti; Milan Lopuhaä-Zwakenberg; Ernst Moritz Hahn; Mariëlle Stoelinga (CoRR, 2024)

Tools at the Frontiers of Quantitative Verification. - Roman Andriushchenko; Alexander Bork; Carlos E. Budde; Milan Ceska 002; Kush Grover; Ernst Moritz Hahn; Arnd Hartmanns; Bryant Israelsen; Nils Jansen 001; Joshua Jeppson; Sebastian Junges; Maximilian A. Köhl; et al. (CoRR, 2024)

DODGE: Ontology-Aware Risk Assessment via Object-Oriented Disruption Graphs. - Stefano M. Nicoletti; Ernst Moritz Hahn; Mattia Fumagalli; Giancarlo Guizzardi; Mariëlle Stoelinga (CoRR, 2024)

WATCHDOG: an ontology-aWare risk AssessmenT approaCH via object-oriented DisruptiOn Graphs. - Stefano M. Nicoletti; Ernst Moritz Hahn; Mattia Fumagalli; Giancarlo Guizzardi; Mariëlle Stoelinga (CAiSE (2), 2025)