Bio 
I am a postdoc at the Chair of Algebraic and Logic Foundations of Computer Science of the Technical University Dresden, headed by Christel Baier. I am also a member of the Collaborative Research Center ("Sonderforschungsbereich") 248 Center for Perspicuous Computing, funded by the Deutsche Forschungsgemeinschaft DFG.
Prior to settling in theoretical computer science, I obtained my Ph.D. in pure mathematics from the University of Bonn, supervised by Wolfgang Lück. Between Ph.D. and postdoc, I worked at Fraunhofer on applied artificial intelligence.

Papers 
Responsibility Attribution in Parameterized Markovian Models (with C. Baier and R. Majumdar)
Accepted for publication at AAAI21
Abstract:
We consider the problem of responsibility attribution in the setting of parametric Markov chains. Given a family of Markov chains over a set of parameters, and a property, responsibility attribution asks how the difference in the value of the property should be attributed to the parameters when they change from one point in the parameter space to another.
We formalize responsibility as pathbased attribution schemes studied in cooperative game theory. An attribution scheme in a game determines how a value (a surplus or a cost) is distributed among a set of participants. Pathbased attribution schemes include the wellstudied AumannShapley and the ShapleyShubik schemes. In our context, an attribution scheme measures the responsibility of each parameter on the value function of the parametric Markov chain.
We study the decision problem for pathbased attribution schemes. Our main technical result is an algorithm for deciding if a pathbased attribution scheme for a rational (ratios of polynomials) cost function is over a rational threshold. In particular, it is decidable if the AumannShapley value for a player is at least a given rational number. As a consequence, we show that responsibility attribution is decidable for parametric Markov chains and for a general class of properties that include expectation and variance of discounted sum and longrun average rewards, as well as specifications in temporal logic.
Reachability in Dynamical Systems with Rounding (with C. Baier, S. Jantsch, T. Karimov, E. Lefaucheux, J. Ouaknine, A. Pouly, D. Purser, and M. A. Whiteland)
Proceedings of FSTTCS'20, LIPIcs 182, 2020.
Abstract:
We consider reachability in dynamical systems with discrete linear updates, but with fixed decimal precision, i.e., such that values of the system are rounded at each step. Given a matrix M ∈ Q^{d×d},
an initial vector x ∈ Q^{d}, a granularity
g ∈ Q_{+} and a rounding operation [] projecting a vector of Q^{d} onto another vector whose every entry is a multiple of g, we are interested in the behaviour of the orbit O = <[x], [M[x]],
[M[M[x]]],
... >, i.e., the trajectory of a linear dynamical system in which the state is rounded after each step. For arbitrary rounding functions with bounded effect, we show that the complexity of deciding pointtopoint reachability  whether a given target y ∈ Q^{d} belongs to O  is PSPACEcomplete when no eigenvalue of M has modulus one. We also establish decidability without any restrictions on eigenvalues for several natural classes of rounding functions.
Minimal witnesses for probabilistic timed automata (with S. Jantsch and C. Baier)
Proceedings of ATVA'20, LNCS 12302, 501517, 2020.
Abstract:
Witnessing subsystems have proven to be a useful concept in the analysis of probabilistic systems, for example as diagnostic informa tion on why a given property holds or as input to refinement algorithms. This paper introduces witnessing subsystems for reachability problems in probabilistic timed automata (PTA). Using a new operation on differ ence bounds matrices, it is shown how Farkas certificates of finitestate bisimulation quotients of a PTA can be translated into witnessing subsys tems. We present algorithms for the computation of minimal witnessing subsystems under three notions of minimality, which capture the timed behavior from different perspectives, and discuss their complexity.
SWITSS: Computing Small Witnessing Subsystems (with S. Jantsch, H. Harder and C. Baier)
Proceedings of FMCAD'20, 236244.
Abstract:
Witnessing subsystems for probabilistic reachability thresholds in discrete Markovian models are an important concept both as diagnostic information on why a property holds, and as input to refinement algorithms. We present SWITSS, a tool for the computation of Small WITnessing SubSystems. SWITSS implements exact and heuristic approaches based on reducing the problem to (mixed integer) linear programming. Returned subsystems can automatically be rendered graphically and are accompanied with a certificate which proves that the subsystem is indeed a witness.
Farkas certificates and minimal witnesses for probabilistic reachability constraints (with S. Jantsch and C. Baier)
Proceedings of TACAS'20, LNCS 12078, 324345, 2020.
Abstract:
This paper introduces Farkas certificates for lower and upper bounds on minimal and maximal reachability probabilities in Markov decision processes (MDP), which we derive using an MDPvariant of Farkas' Lemma. The set of all such certificates is shown to form a polytope whose points correspond to witnessing subsystems of the model and the property. This allows translating the problem of finding minimal witnesses to the problem of finding vertices with a maximal number of zeros. While computing such vertices is computationally hard in general, we derive new heuristics from our formulations that exhibit competitive performance compared to stateoftheart techniques and apply to more situations. As an argument that asymptotically better algorithms cannot be hoped for, we show that the decision version of finding minimal witnesses is NPcomplete even for acyclic Markov chains.
The integral polytope group
to appear in Advances in Geometry
Abstract:
We show that the Grothendieck group associated to integral polytopes in $\R^n$ is freeabelian by providing an explicit basis. Moreover, we identify the involution on this polytope group given by reflection about the origin as a sum of Euler characteristic type. We also compute the kernel of the norm map sending a polytope to its induced seminorm on the dual of $\R^n$.
The L²torsion polytope of amenable groups
Documenta Mathematica 23 (2018), 19691993
Abstract:
We introduce the notion of groups of polytope class and show that torsionfree amenable groups satisfying the Atiyah Conjecture possess this property. A direct consequence is the homotopy invariance of the $L^2$torsion polytope among $G$CWcomplexes for these groups. As another application we prove that the $L^2$torsion polytope of an amenable group vanishes provided that it contains a nonabelian elementary amenable normal subgroup.
Alexander and Thurston norms, and the BieriNeumannStrebel invariants for freebycyclic groups (with D. Kielak)
Geometry and Topology 22 (2018), 26472696
Abstract:
We investigate FriedlLück's universal $L^2$torsion for descending HNN extensions of finitely generated free groups, and so in particular for $F_n$by$\Z$ groups. This invariant induces a seminorm on the first cohomology of the group which is an analogue of the Thurston norm for $3$manifold groups.
We prove that this Thurston seminorm is an upper bound for the Alexander seminorm defined by McMullen, as well as for the higher Alexander seminorms defined by Harvey. The same inequalities are known to hold for $3$manifold groups.
We also prove that the Newton polytopes of the universal $L^2$torsion of a descending HNN extension of $F_2$ locally determine the BieriNeumannStrebel invariant of the group. We give an explicit means of computing the BNS invariant for such groups. As a corollary, we prove that the BieriNeumannStrebel invariant of a descending HNN extension of $F_2$ has finitely many connected components.
When the HNN extension is taken over $F_n$ along a polynomially growing automorphism with unipotent image in $\GL(n, \Z)$, we show that the Newton polytope of the universal $L^2$torsion and the BNS invariant completely determine one another. We also show that in this case the Alexander norm, its higher incarnations, and the Thurston norm all coincide.
The Grothendieck groups of polytopes of norms (with J. C. Cha and S. Friedl)
Münster Journal of Mathematics 10 (2017), 7581
Abstract:
Polytopes in $\mathbb{R}^n$ with integral vertices form a monoid under the Minkowski sum, and the Grothendieck construction gives rise to an abelian group. Symmetric polytopes generate a subgroup. Similarly, difference bodies (which we refer to as norms) also generate a subgroup. We show that for every $n$ the two subgroups agree.
