1 citations · 1 across the 13 of their papers we have counts for
14 papers
Efficient Model Checking for the Alternating-Time μ-Calculus via Effectivity Frames
Daniel Hausmann, Merlin Humml, Simon Prucker +1
The semantics of alternating-time temporal logic (ATL) and the more expressive alternating-time μ-calculus (AMC) is standardly given in terms of concurrent game frames (CGF). The i…
Alternating Nominal Automata with Name Allocation
Florian Frank, Daniel Hausmann, Stefan Milius +2
Formal languages over infinite alphabets serve as abstractions of structures and processes carrying data. Automata models over infinite alphabets, such as classical register automa…
Generic Model Checking for Modal Fixpoint Logics in COOL-MC
Daniel Hausmann, Merlin Humml, Simon Prucker +2
We report on COOL-MC, a model checking tool for fixpoint logics that is parametric in the branching type of models (nondeterministic, game-based, probabilistic etc.) and in the nex…
COOL 2 -- A Generic Reasoner for Modal Fixpoint Logics
Oliver Görlitz, Daniel Hausmann, Merlin Humml +3
There is a wide range of modal logics whose semantics goes beyond relational structures, and instead involves, e.g., probabilities, multi-player games, weights, or neighbourhood st…
Symbolic Solution of Emerson-Lei Games for Reactive Synthesis
Daniel Hausmann, Mathieu Lehaut, Nir Pitermann
Emerson-Lei conditions have recently attracted attention due to their succinctness and compositionality properties. In the current work, we show how infinite-duration games with Em…
Coalgebraic Satisfiability Checking for Arithmetic -Calculi
Daniel Hausmann, Lutz Schröder
The coalgebraic -calculus provides a generic semantic framework for fixpoint logics over systems whose branching type goes beyond the standard relational setup, e.g. probabilist…
A Survey on Satisfiability Checking for the -Calculus through Tree Automata
Daniel Hausmann, Nir Piterman
Algorithms for model checking and satisfiability of the modal -calculus start by converting formulas to alternating parity tree automata. Thus, model checking is reduced to chec…
Nominal Büchi Automata with Name Allocation
Henning Urbat, Daniel Hausmann, Stefan Milius +1
Infinite words over infinite alphabets serve as models of the temporal development of the allocation and (re-)use of resources over linear time. We approach omega-languages over in…
A Linear-Time Nominal -Calculus with Name Allocation
Daniel Hausmann, Stefan Milius, Lutz Schröder
Logics and automata models for languages over infinite alphabets, such as Freeze LTL and register automata, serve the verification of processes or documents with data. They relate…
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…
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…
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…
Permutation Games for the Weakly Aconjunctive -Calculus
Daniel Hausmann, Lutz Schröder, Hans-Peter Deifel
We introduce a natural notion of limit-deterministic parity automata and present a method that uses such automata to construct satisfiability games for the weakly aconjunctive frag…
Global Caching for the Alternation-free -Calculus
Daniel Hausmann, Lutz Schröder, Christoph Egger
We present a sound, complete, and optimal single-pass tableau algorithm for the alternation-free -calculus. The algorithm supports global caching with intermediate propagation a…