Publications
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.