Daniel Hausmann

KR Conference 2025 Conference Paper

Emerson-Lei and Manna-Pnueli Games for LTLf+ and PPLTL+ Synthesis

• Daniel Hausmann
• Shufang Zhu
• Gianmarco Parretti
• Christoph Weinhuber
• Giuseppe De Giacomo
• Nir Piterman

Recently, the Manna-Pnueli Hierarchy has been used to define the temporal logics LTLf+ and PPLTL+, which allow to use finite-trace LTLf/PPLTL techniques in infinite-trace settings while achieving the expressiveness of full LTL. In this paper, we present the first actual solvers for reactive synthesis in these logics. These are based on games on graphs that leverage DFA-based techniques from LTLf/PPLTL to construct the game arena. We start with a symbolic solver based on Emerson-Lei games, which reduces lower-class properties (guarantee, safety) to higher ones (recurrence, persistence) before solving the game. We then introduce Manna-Pnueli games, which natively embed Manna-Pnueli objectives into the arena. These games are solved by composing solutions to a DAG of simpler Emerson-Lei games, resulting in a provably more efficient approach. We implemented the solvers and practically evaluated their performance on a range of representative formulas. The results show that Manna-Pnueli games often offer significant advantages, though not universally, indicating that combining both approaches could further enhance practical performance.

GandALF Workshop 2025 Workshop Paper

Generalised Reachability Games Revisited

• Sougata Bose
• Daniel Hausmann
• Soumyajit Paul
• Sven Schewe
• Tansholpan Zhanabekova

Classic reachability games on graphs are zero-sum games, where the goal of one player, Eve, is to visit a vertex from a given target set, and that of other player, Adam, is to prevent this. Generalised reachability games, studied by Fijalkow and Horn, are a generalisation of reachability objectives, where instead of a single target set, there is a family of target sets and Eve must visit all of them in any order. In this work, we further study the complexity of solving two-player games on graphs with generalised reachability objectives. Our results are twofold: first, we provide an improved complexity picture for generalised reachability games, expanding the known tractable class from games in which all target sets are singleton to additionally allowing a logarithmic number of target sets of arbitrary size. Second, we study optimisation variants of generalised reachability with a focus on the size of the target sets. For these problems, we show intractability for most interesting cases. Particularly, in contrast to the tractability in the classic variant for singleton target sets, the optimisation problem is NP-hard when Eve tries to maximise the number of singleton target sets that are visited. Tractability can be recovered in the optimisation setting when all target sets are singleton by requiring that Eve pledges a maximum sized subset of target sets that she can guarantee to visit.

Highlights Conference 2025 Conference Abstract

Manna-Pnueli Games for Reactive Synthesis

• Daniel Hausmann

Highlights Conference 2023 Conference Abstract

Solving Emerson-Lei Games via Zielonka Trees

• Daniel Hausmann

We show how Emerson-Lei games can be solved symbolically by providing a fixpoint-based characterization of the winning region, which results from analysis of the Zielonka tree of the winning condition. The proposed algorithm generalizes the solutions of known winning conditions such as parity, Streett, Rabin, and GR[1] objectives, and in the case of these conditions reproduces previously known algorithms and complexity results; the algorithm solves unrestricted Emerson-Lei games with n nodes, m edges and d colors in time O((n^(d/2)) d! m). Contributed talk given by Daniel Hausmann

Highlights Conference 2021 Conference Abstract

Uniform Solving for omega-regular Games

• Daniel Hausmann

We show that fixpoint equation systems over arbitrary finite lattices can be solved with a number of iterations that is quasipolynomial in the lattice height and the alternation-depth of the system. As a side-result, we obtain a highly generic progress measure algorithm that solves fixpoint equation systems over finite lattices and uses universal trees to measure progress. Since the winning regions of various kinds of finite-history omega-regular games can be specified by fixpoint equations, our algorithm instantiates to solving e. g. standard parity games, energy parity games, mean-payoff parity games and stochastic parity games (both qualitative and quantitative). The runtime complexities of the instances of the algorithm typically are quasipolynomial in the number of nodes, the number of priorities, and the maximal size of histories of winning strategies. This work is based on the paper “Quasipolynomial Computation of Nested Fixpoints”, which has been published as joint work with Lutz Schröder at TACAS 2021 (extended version available at https: //arxiv. org/pdf/1907. 07020. pdf).

Highlights Conference 2020 Conference Abstract

NP Reasoning in the Monotone mu-Calculus

• Daniel Hausmann

Satisfiability checking for monotone modal logic is known to be (only) NP-complete. We show that this remains true when the logic is extended with alternation-free fixpoint operators as well as the universal modality; the resulting logic – the alternation-free monotone mu-calculus with the universal modality – contains both concurrent propositional dynamic logic (CPDL) and the alternation-free fragment of game logic as fragments. We obtain our result from a characterization of satisfiability by means of Büchi games with polynomially many Eloise nodes. This work has been published as joint work with Lutz Schröder at IJCAR 2020 under the title “NP Reasoning in the Monotone mu-Calculus”; an extended preprint of the conference paper can be found at https: //arxiv. org/abs/2002. 05075.

Highlights Conference 2018 Conference Abstract

Permutation Games for the Weakly Aconjunctive mu-Calculus

• Daniel Hausmann

ABSTRACT. Satisfiability games for the $\mu$-calculus typically employ determinized parity automata to track fixpoint formulas through pre-tableaux. We introduce a natural notion of limit-deterministic parity automata along with a construction that determinizes limit-deterministic parity automata of size $n$ with $k$ priorities through limit-deterministic Büchi automata to deterministic parity automata of size $\mathcal{O}((nk)!)$ and with $\mathcal{O}(nk)$ priorities. The construction relies on limit-determinism to avoid the full complexity of the Safra/Piterman-construction by using partial permutations of states in place of Safra-Trees. By showing that limit-deterministic parity automata can be used to recognize unsuccessful branches in pre-tableaux for the weakly aconjunctive $\mu$-calculus, we obtain satisfiability games of size $\mathcal{O}((nk)!)$ with $\mathcal{O}(nk)$ priorities for weakly aconjunctive input formulas of size $n$ and alternation-depth $k$. A prototypical implementation that employs a tableau-based global caching algorithm to solve these games on-the-fly shows promising initial results. This work has been published as ``Permutation Games for the Weakly Aconjunctive mu-Calculus'' at TACAS 2018 by Daniel Hausmann, Lutz Schr\"oder and Hans-Peter Deifel (https: //link. springer. com/chapter/10. 1007/978-3-319-89963-3_21).

TCS Journal 2006 Journal Article

A coalgebraic approach to the semantics of the ambient calculus

• Daniel Hausmann
• Till Mossakowski
• Lutz Schröder