Publications
Backward Responsibility in Transition Systems Beyond Safety (2025)
Accepted at FMICS 2025 Previous work has focussed on responsibility for models with safety objectives. This paper analyses responsibility for reachability, Büchi and parity objectives and provides complexity bounds. In particular, we provide a polynomial algorithm for determining the set of responsible states for Büchi objectives. Additionally, we introduce a novel refinement algorithm that significantly reduces computation times in suitable models.
Responsibility in Actor-Based Systems (2025)
Essays Dedicated to Marjan Sirjani on the Occasion of Her 60th Birthday Computing responsibility for individual states is often neither tractable nor very insightful. In this paper, we show how Shapley values can be used to compute responsibility for state groups (“actors”). The paper focusses on extracting actors automatically from features of a reactive-modules style modelling language. We present techniques to generate actors for every module, every action and every variable value. We have implemented these techniques and investigate their performance and usefulness.
Backward Responsibility in Transition Systems Using General Power Indices (2024)
AAAI-24 We present a novel method for computing responsibility in a transition system. Using general power indices, we assign a numeric responsibility value to each state. This indicates how much impact that state had on whether a specific system failure occured.
Towards a Formal Account on Negative Latency (2023)
AISoLA 2023 In this paper, we approach negative latency as anticipatory networking with formal guarantees. We first establish a formal framework for modeling predictions on goal-directed behaviors in Markov decision processes. Then, we present and characterise methods to synthesise predictions with formal quality criteria that can be turned into negative latency.
Pushdown and Expectation Transformer Semantics of Probabilistic Recursive Programs with Nested Conditioning (2023)
Master's thesis Conditioning is a common feature in probabilistic programming. Nested conditioning is particularly is useful to express “Reasoning about reasoning”. We present an imperative language with recursion and nested conditioning. We define operational semantics based on probabilistic pushdown automata, provide weakest-preexpectation transformer semantics and show the equivalence of these two semantics. We show that conditioning does not increase the expressiveness of the language and highlight that two definitions of conditioning exist that differ in how they handle termination. Based on the operational semantics, we have implemented nested conditioning in the model checker Pray.
Out of Control: Reducing Probabilistic Models by Control-State Elimination (2022)
VMCAI-22 We develop a novel technique that works on the program flow graph before it is given to the model checker. For this, we "unfold" some variables and then perform simplifications of the program flow graph. This reduces the size of the state space of the final model. We have implemented the technique in the model checker Storm and developed heuristics to fully automate the unfolding and simplification.
Exact Minimisation of ω-Automata (2020)
Bachelor's thesis We summarise several results from the field of Büchi automaton minimisation, including a proof of NP-completeness, two minimisation techniques that use SAT solving, and a polynomial-time algorithm for minimisation of transition-based good-for-games Co-Büchi automata.