3 papers
cs.LO2020
NP Reasoning in the Monotone -Calculus
Daniel Hausmann, Lutz Schröder
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 aconjunctive and alternation-free…
cs.CC2019
Quasipolynomial Computation of Nested Fixpoints
Daniel Hausmann, Lutz Schröder
It is well-known that the winning region of a parity game with nodes and priorities can be computed as a -nested fixpoint of a suitable function; straightforward computa…
cs.LO2019
Optimal Satisfiability Checking for Arithmetic -Calculi
Daniel Hausmann, Lutz Schröder
The coalgebraic -calculus provides a generic semantic framework for fixpoint logics with branching types beyond the standard relational setup, e.g. probabilistic, weighted, or g…