Publications

You may click on the items listed below for further details.

16. On probability-raising causality in Markov decision processes (with C. Baier, J. Piribauer, and R. Ziemek)

    Proceedings of FoSSaCS'22, LNCS 13242, 40-60, 2022.

    Abstract: The purpose of this paper is to introduce a notion of causality in Markov decision processes based on the probability-raising principle and to analyze its algorithmic properties. The latter includes algorithms for checking cause-effect relationships and the existence of probability-raising causes for given effect scenarios. Inspired by concepts of statistical analysis, we study quality measures (recall, coverage ratio and f-score) for causes and develop algorithms for their computation. Finally, the computational complexity for finding optimal causes with respect to these measures is analyzed.

17. Probabilistic causes in Markov chains (with C. Baier, S. Jantsch, J. Piribauer, and R. Ziemek)

    Journal version: Innovations Syst Softw Eng, 2022.

    Abstract: By combining two of the central paradigms of causality, namely counterfactual reasoning and probability-raising, we introduce a probabilistic notion of cause in Markov chains. Such a cause consists of finite executions of the probabilistic system after which the probability of an ω-regular effect exceeds a given threshold. The cause, as a set of executions, then has to cover all behaviors exhibiting the effect. With these properties, such causes can be used for monitoring purposes where the aim is to detect faulty behavior before it actually occurs. In order to choose which cause should be computed, we introduce multiple types of costs to capture the consumption of resources by the system or monitor from different perspectives, and study the complexity of computing cost-minimal causes.

    Conference version: Proceedings of ATVA'21, LNCS 12971, 205-221, 2021.

    Abstract: The paper studies a probabilistic notion of causes in Markov chains that relies on the counterfactuality principle and the probability-raising property. This notion is motivated by the use of causes for monitoring purposes where the aim is to detect faulty or undesired behaviours before they actually occur. A cause is a set of finite executions of the system after which the probability of the effect exceeds a given threshold. We introduce multiple types of costs that capture the consumption of resources from different perspectives, and study the complexity of computing cost-minimal causes.

18. The Orbit Problem for Parametric Linear Dynamical Systems (with C. Baier, S. Jantsch, T. Karimov, E. Lefaucheux, F. Luca, J. Ouaknine, D. Purser, M. A. Whiteland, and J. Worrell)

    Proceedings of CONCUR'21, LIPIcs 203, 2021.

    Abstract: We study a parametric version of the Kannan-Lipton Orbit Problem for linear dynamical systems. We show decidability in the case of one parameter and Skolem-hardness with four or more parameters.

    More precisely, consider M a d-dimensional square matrix whose entries are rational functions in one or more real variables. Given initial and target vectors u, v ∈ Q^d, the parametrised point-to-point reachability problem asks whether there exist values of the parameters giving rise to a concrete matrix N ∈ Q^d×d, and a positive integer n, such that Nⁿu=v.

    We show decidability in the case where M depends only upon a single parameter, and we exhibit a reduction from the well-known Skolem problem for linear recurrence sequences, indicating intractability in the case of four or more parameters.

19. From Verification to Causality-Based Explications (with C. Baier, C. Dubslaff, S. Jantsch, R. Majumdar, J. Piribauer, and R. Ziemek)

    Proceedings of ICALP'21, LIPIcs 198, 2021.

    Abstract: In view of the growing complexity of modern software architectures, formal models are increasingly used to understand why a system works the way it does, opposed to simply verifying that it behaves as intended. This paper surveys approaches to formally explicate the observable behavior of reactive systems. We describe how Halpern and Pearl's notion of actual causation inspired verification-oriented studies of cause-effect relationships in the evolution of a system. A second focus lies on applications of the Shapley value to responsibility ascriptions, aimed to measure the influence of an event on an observable effect. Finally, formal approaches to probabilistic causation are collected and connected, and their relevance to the understanding of probabilistic systems is discussed.

20. Causality-Based Game Solving (with C. Baier, N. Coenen, B. Finkbeiner, S. Jantsch, and J. Siber)

    Proceedings of CAV'21, LNCS 12759, 894-917, 2021

    Abstract: We present a causality-based algorithm for solving two-player reachability games represented by logical constraints. These games are a useful formalism to model a wide array of problems arising, e.g., in program synthesis. Our technique for solving these games is based on the notion of subgoals, which are slices of the game that the reachability player necessarily needs to pass through in order to reach the goal. We use Craig interpolation to identify these necessary sets of moves and recursively slice the game along these subgoals. Our approach allows us to infer winning strategies that are structured along the subgoals. If the game is won by the reachability player, this is a strategy that progresses through the subgoals towards the final goal; if the game is won by the safety player, it is a permissive strategy that completely avoids a single subgoal. We evaluate our prototype implementation on a range of different games. On multiple benchmark families, our prototype scales dramatically better than previously available tools.

21. A Game-Theoretic Account of Responsibility Allocation (with C. Baier and R. Majumdar)

    Proceedings of IJCAI'21, 1773-1779, 2021

    Abstract: When designing or analyzing multi-agent systems, a fundamental problem is responsibility ascription: to specify which agents are responsible for the joint outcome of their behaviors and to which extent. We model strategic multi-agent interaction as an extensive form game of imperfect information and define notions of forward (prospective) and backward (retrospective) responsibility. Forward responsibility identifies the responsibility of a group of agents for an outcome along all possible plays, whereas backward responsibility identifies the responsibility along a given play. We further distinguish between strategic and causal backward responsibility, where the former captures the epistemic knowledge of players along a play, while the latter formalizes which players -- possibly unknowingly -- caused the outcome. A formal connection between forward and backward notions is established in the case of perfect recall. We further ascribe quantitative responsibility through cooperative game theory. We show through a number of examples that our approach encompasses several prior formal accounts of responsibility attribution.

22. Responsibility and verification: Importance value in temporal logics (with C. Mascle, C. Baier, S. Jantsch, and S. Kiefer)

    Proceedings of LICS'21, 2021.

    Abstract: We aim at measuring the influence of the nondeterministic choices of a part of a system on its ability to satisfy a specification. For this purpose, we apply the concept of Shapley values to verification as a means to evaluate how important a part of a system is. The importance of a component is measured by giving its control to an adversary, alone or along with other components, and testing whether the system can still fulfill the specification. We study this idea in the framework of model-checking with various classical types of linear-time specification, and propose several ways to transpose it to branching ones. We also provide tight complexity bounds in almost every case.

23. Responsibility Attribution in Parameterized Markovian Models (with C. Baier and R. Majumdar)

    Proceedings of AAAI-21, 11734-11743, 2021.

    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 path-based 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. Path-based attribution schemes include the well-studied Aumann-Shapley and the Shapley-Shubik 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 path-based attribution schemes. Our main technical result is an algorithm for deciding if a path-based attribution scheme for a rational (ratios of polynomials) cost function is over a rational threshold. In particular, it is decidable if the Aumann-Shapley 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 long-run average rewards, as well as specifications in temporal logic.

24. 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 point-to-point reachability - whether a given target y ∈ Q^d belongs to O - is PSPACE-complete when no eigenvalue of M has modulus one. We also establish decidability without any restrictions on eigenvalues for several natural classes of rounding functions.

25. Minimal witnesses for probabilistic timed automata (with S. Jantsch and C. Baier)

    Proceedings of ATVA'20, LNCS 12302, 501-517, 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 finite-state 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.

26. SWITSS: Computing Small Witnessing Subsystems (with S. Jantsch, H. Harder and C. Baier)

    Proceedings of FMCAD'20, 236-244, 2020.

    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.

27. Farkas certificates and minimal witnesses for probabilistic reachability constraints (with S. Jantsch and C. Baier)

    Proceedings of TACAS'20, LNCS 12078, 324-345, 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 MDP-variant 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 state-of-the-art 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 NP-complete even for acyclic Markov chains.

28. The integral polytope group

    Advances in Geometry 21 (2021), 45-62.

    Abstract: We show that the Grothendieck group associated to integral polytopes in Rⁿ is free-abelian 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ⁿ.

29. The L²-torsion polytope of amenable groups

    Documenta Mathematica 23 (2018), 1969-1993.

    Abstract: We introduce the notion of groups of polytope class and show that torsion-free amenable groups satisfying the Atiyah Conjecture possess this property. A direct consequence is the homotopy invariance of the L²-torsion polytope among G-CW-complexes for these groups. As another application we prove that the L²-torsion polytope of an amenable group vanishes provided that it contains a non-abelian elementary amenable normal subgroup.

30. Alexander and Thurston norms, and the Bieri-Neumann-Strebel invariants for free-by-cyclic groups (with D. Kielak)

    Geometry and Topology 22 (2018), 2647-2696.

    Abstract: We investigate Friedl--Lück's universal L²-torsion for descending HNN extensions of finitely generated free groups, and so in particular for F_n-by-Z groups. This invariant induces a semi-norm on the first cohomology of the group which is an analogue of the Thurston norm for 3-manifold groups.

    We prove that this Thurston semi-norm is an upper bound for the Alexander semi-norm defined by McMullen, as well as for the higher Alexander semi-norms 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²-torsion of a descending HNN extension of F₂ locally determine the Bieri-Neumann-Strebel invariant of the group. We give an explicit means of computing the BNS invariant for such groups. As a corollary, we prove that the Bieri-Neumann-Strebel invariant of a descending HNN extension of F₂ 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²-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.

31. The Grothendieck groups of polytopes of norms (with J. C. Cha and S. Friedl)

    Münster Journal of Mathematics 10 (2017), 75-81.

    Abstract: Polytopes in Rⁿ 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.