EDBT 2026 Demo / reviewers in the wild / expert
Stefanie Mohr
dblp:268/5555
· DBLP profile ↗
9ranked-venue papers
1as first author
8since 2021 · last 2025
0000-0002-8630-3218ORCID · verified
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 6 · 5 since 2021Theory of computation · 3 · 3 since 2021Artificial intelligence and machine learning · 1 · 1 first-author · 1 since 2021
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2025 | Risk-aware Markov Decision Processes Using Cumulative Prospect TheoryabstractCumulative prospect theory (CPT) is the first theory for decision-making under uncertainty that combines full theoretical soundness and empirically realistic features [1], [Page 2]. While CPT was originally considered in one-shot settings for risk-aware decision-making, we consider CPT in sequential decision-making. The most fundamental and well-studied models for sequential decision-making are Markov chains (MCs), and their generalization Markov decision processes (MDPs). The complexity theoretic study of MCs and MDPs with CPT is a fundamental problem that has not been addressed in the literature.Our contributions are as follows: First, we present an alternative viewpoint for the CPT-value of MCs and MDPs. This allows us to establish a connection with multi-objective reachability analysis and conclude the strategy complexity result that memoryless randomized strategies are necessary and sufficient for optimality. Second, based on this connection, we provide an algorithm for computing the CPT-value in MDPs with infinite-horizon objectives. We show that the problem is in EXPTIME and fixed-parameter tractable. Moreover, we provide a polynomial-time algorithm for the special case of MCs. Thomas Brihaye, Krishnendu Chatterjee, Stefanie Mohr, Maximilian Weininger |
LICS | 3 |
| 2025 | 1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization
Muqsit Azeem, Debraj Chakraborty 0002, Sudeep Kanav, Jan Kretínský, MohammadSadegh Mohagheghi, Stefanie Mohr, Maximilian Weininger |
VMCAI (2) | 6 |
| 2024 | Monitizer: Automating Design and Evaluation of Neural Network MonitorsabstractAbstract The behavior of neural networks (NNs) on previously unseen types of data (out-of-distribution or OOD) is typically unpredictable. This can be dangerous if the network’s output is used for decision making in a safety-critical system. Hence, detecting that an input is OOD is crucial for the safe application of the NN. Verification approaches do not scale to practical NNs, making runtime monitoring more appealing for practical use. While various monitors have been suggested recently, their optimization for a given problem, as well as comparison with each other and reproduction of results, remain challenging. We present a tool for users and developers of NN monitors. It allows for (i) application of various types of monitors from the literature to a given input NN, (ii) optimization of the monitor’s hyperparameters, and (iii) experimental evaluation and comparison to other approaches. Besides, it facilitates the development of new monitoring approaches. We demonstrate the tool’s usability on several use cases of different types of users as well as on a case study comparing different approaches from recent literature. Muqsit Azeem, Marta Grobelna, Sudeep Kanav, Jan Kretínský, Stefanie Mohr, Sabine Rieder |
CAV (2) | 5 |
| 2024 | Learning Explainable and Better Performing Representations of POMDP StrategiesabstractAbstract Strategies for partially observable Markov decision processes (POMDP) typically require memory. One way to represent this memory is via automata. We present a method to learn an automaton representation of a strategy using a modification of the $$L^*$$ L ∗ -algorithm. Compared to the tabular representation of a strategy, the resulting automaton is dramatically smaller and thus also more explainable. Moreover, in the learning process, our heuristics may even improve the strategy’s performance. We compare our approach to an existing approach that synthesizes an automaton directly from the POMDP, thereby solving it. Our experiments show that our approach can lead to significant improvements in the size and quality of the resulting strategy representations. Alexander Bork, Debraj Chakraborty 0002, Kush Grover, Jan Kretínský, Stefanie Mohr |
TACAS (2) | 5 |
| 2024 | Stochastic games with lexicographic objectivesabstractAbstract We study turn-based stochastic zero-sum games with lexicographic preferences over objectives. Stochastic games are standard models in control, verification, and synthesis of stochastic reactive systems that exhibit both randomness as well as controllable and adversarial non-determinism. Lexicographic order allows one to consider multiple objectives with a strict preference order. To the best of our knowledge, stochastic games with lexicographic objectives have not been studied before. For a mixture of reachability and safety objectives, we show that deterministic lexicographically optimal strategies exist and memory is only required to remember the already satisfied and violated objectives. For a constant number of objectives, we show that the relevant decision problem is in $$\textsf{NP}\cap \textsf{coNP}$$ NP ∩ coNP , matching the current known bound for single objectives; and in general the decision problem is $$\textsf{PSPACE}$$ PSPACE -hard and can be solved in $$\textsf{NEXPTIME}\cap \textsf{coNEXPTIME}$$ NEXPTIME ∩ coNEXPTIME . We present an algorithm that computes the lexicographically optimal strategies via a reduction to the computation of optimal strategies in a sequence of single-objectives games. For omega-regular objectives, we restrict our analysis to one-player games, also known as Markov decision processes. We show that lexicographically optimal strategies exist and need either randomization or finite memory. We present an algorithm that solves the relevant decision problem in polynomial time. We have implemented our algorithms and report experimental results on various case studies. Krishnendu Chatterjee, Joost-Pieter Katoen, Stefanie Mohr, Maximilian Weininger, Tobias Winkler 0001 |
Formal Methods Syst. Des. | 3 |
| 2023 | Syntactic vs Semantic Linear Abstraction and Refinement of Neural Networks
Calvin Chau, Jan Kretínský, Stefanie Mohr |
ATVA (1) | 3 |
| 2021 | Assessment of Neural Networks for Stream-Water-Temperature PredictionabstractClimate change results in altered air and water temperatures. Increases affect physicochemical properties, such as oxygen concentration, and can shift species distribution and survival, with consequences for ecosystem functioning and services. These ecosystem services have integral value for humankind and are forecasted to alter under climate warming. A mechanistic understanding of the drivers and magnitude of expected changes is essential in identifying system resilience and mitigation measures. In this work, we present a selection of state-of-the-art Neural Networks (NN) for the prediction of water temperatures in six streams in Germany. We show that the use of methods that compare observed and predicted values, exemplified with the Root Mean Square Error (RMSE), is not sufficient for their assessment. Hence we introduce additional analysis methods for our models to complement the state-of-the-art metrics. These analyses evaluate the NN’s robustness, possible maximal and minimal values, and the impact of single input parameters on the output. We thus contribute to understanding the processes within the NN and help applicants choose architectures and input parameters for reliable water temperature prediction models. Stefanie Mohr, Konstantina Drainas, Jürgen Geist |
ICMLA | 1 |
| 2021 | Gaussian-Based Runtime Detection of Out-of-distribution Inputs for Neural Networks
Vahid Hashemi, Jan Kretínský, Stefanie Mohr, Emmanouil Seferis |
RV | 3 |
| 2020 | DeepAbstract: Neural Network Abstraction for Accelerating Verification
Pranav Ashok, Vahid Hashemi, Jan Kretínský, Stefanie Mohr |
ATVA | 4 |