Showing 1–18 of 18 results for author: Hausmann, D

Efficient Model Checking for the Alternating-Time μ-Calculus via Effectivity Frames

Authors: Daniel Hausmann, Merlin Humml, Simon Prucker, Lutz Schröder

Abstract: 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 information required to interpret AMC formulas is equivalently represented in terms of effectivity frames in the sense of Pauly; in many cases, this representation is more compact than the corresponding CGF, and in princi… ▽ More 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 information required to interpret AMC formulas is equivalently represented in terms of effectivity frames in the sense of Pauly; in many cases, this representation is more compact than the corresponding CGF, and in principle allows for faster evaluation of coalitional modalities. In the present work, we investigate whether implementing a model checker based on effectivity frames leads to better performance in practice. We implement the translation from concurrent game frames to effectivity frames and analyse performance gains in model checking based on corresponding instantiations of a generic model checker for coalgebraic μ-calculi, using dedicated benchmark series as well as random systems and formulas. In the process, we also compare performance to the state-of-the-art ATL model checkerMCMAS. Our results indicate that on large systems, the overhead involved in converting a CGF to an effectivity frame is often outweighed by the benefits in subsequent model checking. △ Less

Submitted 1 June, 2025; originally announced June 2025.

Distribution of Reconfiguration Languages maintaining Tree-like Communication Topology

Authors: Daniel Hausmann, Mathieu Lehaut, Nir Piterman

Abstract: We study how to distribute trace languages in a setting where processes communicate via reconfigurable communication channels. That is, the different processes can connect and disconnect from channels at run time. We restrict attention to communication via tree-like communication architectures. These allow channels to connect more than two processes in a way that maintains an underlying spanning t… ▽ More We study how to distribute trace languages in a setting where processes communicate via reconfigurable communication channels. That is, the different processes can connect and disconnect from channels at run time. We restrict attention to communication via tree-like communication architectures. These allow channels to connect more than two processes in a way that maintains an underlying spanning tree and keeps communication continuous on the tree. We make the reconfiguration explicit in the language allowing both a centralized automaton as well as the distributed processes to share relevant information about the current communication configuration. We show that Zielonka's seminal result regarding distribution of regular languages for asynchronous automata can be generalized in this setting, incorporating both reconfiguration and more than binary tree architectures. △ Less

Submitted 20 August, 2024; originally announced August 2024.

Alternating Nominal Automata with Name Allocation

Authors: Florian Frank, Daniel Hausmann, Stefan Milius, Lutz Schröder, Henning Urbat

Abstract: Formal languages over infinite alphabets serve as abstractions of structures and processes carrying data. Automata models over infinite alphabets, such as classical register automata or, equivalently, nominal orbit-finite automata, tend to have computationally hard or even undecidable reasoning problems unless stringent restrictions are imposed on either the power of control or the number of regis… ▽ More Formal languages over infinite alphabets serve as abstractions of structures and processes carrying data. Automata models over infinite alphabets, such as classical register automata or, equivalently, nominal orbit-finite automata, tend to have computationally hard or even undecidable reasoning problems unless stringent restrictions are imposed on either the power of control or the number of registers. This has been shown to be ameliorated in automata models with name allocation such as regular nondeterministic nominal automata, which allow for deciding language inclusion in elementary complexity even with unboundedly many registers while retaining a reasonable level of expressiveness. In the present work, we demonstrate that elementary complexity survives under extending the power of control to alternation: We introduce regular alternating nominal automata (RANAs), and show that their non-emptiness and inclusion problems have elementary complexity even when the number of registers is unbounded. Moreover, we show that RANAs allow for nearly complete de-alternation, specifically de-alternation up to a single deadlocked universal state. As a corollary to our results, we improve the complexity of model checking for a flavour of Bar-$μ$TL, a fixed-point logic with name allocation over finite data words, by one exponential level. △ Less

Submitted 19 May, 2025; v1 submitted 7 August, 2024; originally announced August 2024.

MSC Class: 68Q45 ACM Class: F.4.3

Faster and Smaller Solutions of Obliging Games

Authors: Daniel Hausmann, Nir Piterman

Abstract: Obliging games have been introduced in the context of the game perspective on reactive synthesis in order to enforce a degree of cooperation between the to-be-synthesized system and the environment. Previous approaches to the analysis of obliging games have been small-step in the sense that they have been based on a reduction to standard (non-obliging) games in which single moves correspond to sin… ▽ More Obliging games have been introduced in the context of the game perspective on reactive synthesis in order to enforce a degree of cooperation between the to-be-synthesized system and the environment. Previous approaches to the analysis of obliging games have been small-step in the sense that they have been based on a reduction to standard (non-obliging) games in which single moves correspond to single moves in the original (obliging) game. Here, we propose a novel, large-step view on obliging games, reducing them to standard games in which single moves encode long-term behaviors in the original game. This not only allows us to give a meaningful definition of the environment winning in obliging games, but also leads to significantly improved bounds on both strategy sizes and the solution runtime for obliging games. △ Less

Submitted 16 July, 2024; originally announced July 2024.

Comments: extended version of paper accepted for publication at CONCUR 2024

Faster Game Solving by Fixpoint Acceleration

Authors: Daniel Hausmann

Abstract: We propose a method for solving parity games with acyclic (DAG) sub-structures by computing nested fixpoints of a DAG attractor function that lives over the non-DAG parts of the game, thereby restricting the domain of the involved fixpoint operators. Intuitively, this corresponds to accelerating fixpoint computation by inlining cycle-free parts during the solution of parity games, leading to earli… ▽ More We propose a method for solving parity games with acyclic (DAG) sub-structures by computing nested fixpoints of a DAG attractor function that lives over the non-DAG parts of the game, thereby restricting the domain of the involved fixpoint operators. Intuitively, this corresponds to accelerating fixpoint computation by inlining cycle-free parts during the solution of parity games, leading to earlier convergence. We also present an economic later-appearence-record construction that takes Emerson-Lei games to parity games, and show that it preserves DAG sub-structures; it follows that the proposed method can be used also for the accelerated solution of Emerson-Lei games. △ Less

Submitted 21 April, 2024; originally announced April 2024.

Generic Model Checking for Modal Fixpoint Logics in COOL-MC

Authors: Daniel Hausmann, Merlin Humml, Simon Prucker, Lutz Schröder, Aaron Strahlberger

Abstract: 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 next-step modalities used in formulae. The tool implements generic model checking algorithms developed in coalgebraic logic that are easily adapted to concrete instance logics. Apart from the standard modal $μ$-calculus, CO… ▽ More 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 next-step modalities used in formulae. The tool implements generic model checking algorithms developed in coalgebraic logic that are easily adapted to concrete instance logics. Apart from the standard modal $μ$-calculus, COOL-MC currently supports alternating-time, graded, probabilistic and monotone variants of the $μ$-calculus, but is also effortlessly extensible with new instance logics. The model checking process is realized by polynomial reductions to parity game solving, or, alternatively, by a local model checking algorithm that directly computes the extensions of formulae in a lazy fashion, thereby potentially avoiding the construction of the full parity game. We evaluate COOL-MC on informative benchmark sets. △ Less

Submitted 3 November, 2023; v1 submitted 2 November, 2023; originally announced November 2023.

Comments: Full Version of VMCAI 2024 publication

Fair $ω$-Regular Games

Authors: Daniel Hausmann, Nir Piterman, Irmak Sağlam, Anne-Kathrin Schmuck

Abstract: We consider two-player games over finite graphs in which both players are restricted by fairness constraints on their moves. Given a two player game graph $G=(V,E)$ and a set of fair moves $E_f\subseteq E$ a player is said to play "fair" in $G$ if they choose an edge $e \in E_f$ infinitely often whenever the source vertex of $e$ is visited infinitely often. Otherwise, they play "unfair". We equip… ▽ More We consider two-player games over finite graphs in which both players are restricted by fairness constraints on their moves. Given a two player game graph $G=(V,E)$ and a set of fair moves $E_f\subseteq E$ a player is said to play "fair" in $G$ if they choose an edge $e \in E_f$ infinitely often whenever the source vertex of $e$ is visited infinitely often. Otherwise, they play "unfair". We equip such games with two $ω$-regular winning conditions $α$ and $β$ deciding the winner of mutually fair and mutually unfair plays, respectively. Whenever one player plays fair and the other plays unfair, the fairly playing player wins the game. The resulting games are called "fair $α/β$ games". We formalize fair $α/β$ games and show that they are determined. For fair parity/parity games, i.e., fair $α/β$ games where $α$ and $β$ are given each by a parity condition over $G$, we provide a polynomial reduction to (normal) parity games via a gadget construction inspired by the reduction of stochastic parity games to parity games. We further give a direct symbolic fixpoint algorithm to solve fair parity/parity games. On a conceptual level, we illustrate the translation between the gadget-based reduction and the direct symbolic algorithm which uncovers the underlying similarities of solution algorithms for fair and stochastic parity games, as well as for the recently considered class of fair games where only one player is restricted by fair moves. △ Less

Submitted 20 October, 2023; originally announced October 2023.

COOL 2 -- A Generic Reasoner for Modal Fixpoint Logics

Authors: Oliver Görlitz, Daniel Hausmann, Merlin Humml, Dirk Pattinson, Simon Prucker, Lutz Schröder

Abstract: 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 structures. Coalgebraic logic serves as a unifying semantic and algorithmic framework for such logics. It provides uniform reasoning algorithms that are easily instantiated to particular, concretely given logics. The COOL… ▽ More 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 structures. Coalgebraic logic serves as a unifying semantic and algorithmic framework for such logics. It provides uniform reasoning algorithms that are easily instantiated to particular, concretely given logics. The COOL 2 reasoner provides an implementation of such generic algorithms for coalgebraic modal fixpoint logics. As concrete instances, we obtain in particular reasoners for the aconjunctive and alternation-free fragments of the graded $μ$-calculus and the alternating-time $μ$-calculus. We evaluate the tool on standard benchmark sets for fixpoint-free graded modal logic and alternating-time temporal logic (ATL), as well as on a dedicated set of benchmarks for the graded $μ$-calculus. △ Less

Submitted 15 June, 2023; v1 submitted 18 May, 2023; originally announced May 2023.

Comments: Final version (corrected slight mistake in Rabin-type formula series)

Symbolic Solution of Emerson-Lei Games for Reactive Synthesis

Authors: Daniel Hausmann, Mathieu Lehaut, Nir Pitermann

Abstract: 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 Emerson-Lei objectives can be analyzed in two different ways. First, we show that the Zielonka tree of the Emerson-Lei condition gives rise naturally to a new reduction to parity games. This reduction, however, does not re… ▽ More 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 Emerson-Lei objectives can be analyzed in two different ways. First, we show that the Zielonka tree of the Emerson-Lei condition gives rise naturally to a new reduction to parity games. This reduction, however, does not result in optimal analysis. Second, we show based on the first reduction (and the Zielonka tree) how to provide a direct fixpoint-based characterization of the winning region. The fixpoint-based characterization allows for symbolic analysis. It generalizes the solutions of games with known winning conditions such as Büchi, GR[1], parity, Streett, Rabin and Muller objectives, and in the case of these conditions reproduces previously known symbolic algorithms and complexity results. We also show how the capabilities of the proposed algorithm can be exploited in reactive synthesis, suggesting a new expressive fragment of LTL that can be handled symbolically. Our fragment combines a safety specification and a liveness part. The safety part is unrestricted and the liveness part allows to define Emerson-Lei conditions on occurrences of letters. The symbolic treatment is enabled due to the simplicity of determinization in the case of safety languages and by using our new algorithm for game solving. This approach maximizes the number of steps solved symbolically in order to maximize the potential for efficient symbolic implementations. △ Less

Submitted 25 October, 2023; v1 submitted 4 May, 2023; originally announced May 2023.

Coalgebraic Satisfiability Checking for Arithmetic $μ$-Calculi

Authors: Daniel Hausmann, Lutz Schröder

Abstract: The coalgebraic $μ$-calculus provides a generic semantic framework for fixpoint logics over systems whose branching type goes beyond the standard relational setup, e.g. probabilistic, weighted, or game-based. Previous work on the coalgebraic $μ$-calculus includes an exponential-time upper bound on satisfiability checking, which however relies on the availability of tableau rules for the next-step… ▽ More The coalgebraic $μ$-calculus provides a generic semantic framework for fixpoint logics over systems whose branching type goes beyond the standard relational setup, e.g. probabilistic, weighted, or game-based. Previous work on the coalgebraic $μ$-calculus includes an exponential-time upper bound on satisfiability checking, which however relies on the availability of tableau rules for the next-step modalities that are sufficiently well-behaved in a formally defined sense; in particular, rule matches need to be representable by polynomial-sized codes, and the sequent duals of the rules need to absorb cut. While such rule sets have been identified for some important cases, they are not known to exist in all cases of interest, in particular ones involving either integer weights as in the graded $μ$-calculus, or real-valued weights in combination with non-linear arithmetic. In the present work, we prove the same upper complexity bound under more general assumptions, specifically regarding the complexity of the (much simpler) satisfiability problem for the underlying one-step logic, roughly described as the nesting-free next-step fragment of the logic. The bound is realized by a generic global caching algorithm that supports on-the-fly satisfiability checking. Notably, our approach directly accommodates unguarded formulae, and thus avoids use of the guardedness transformation. Example applications include new exponential-time upper bounds for satisfiability checking in an extension of the graded $μ$-calculus with polynomial inequalities (including positive Presburger arithmetic), as well as an extension of the (two-valued) probabilistic $μ$-calculus with polynomial inequalities. △ Less

Submitted 22 July, 2024; v1 submitted 21 December, 2022; originally announced December 2022.

MSC Class: 03B70; 03B44 ACM Class: F.4.1

Journal ref: Logical Methods in Computer Science, Volume 20, Issue 3 (July 23, 2024) lmcs:10532

A Survey on Satisfiability Checking for the $μ$-Calculus through Tree Automata

Authors: Daniel Hausmann, Nir Piterman

Abstract: 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 checking acceptance by tree automata and satisfiability to checking their emptiness. The first reduces directly to the solution of parity games but the second is more complicated. We review the non-emptiness checking of al… ▽ More 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 checking acceptance by tree automata and satisfiability to checking their emptiness. The first reduces directly to the solution of parity games but the second is more complicated. We review the non-emptiness checking of alternating tree automata by a reduction to solving parity games of a certain structure, so-called emptiness games. Since the emptiness problem for alternating tree automata is EXPTIME-complete, the size of these games is exponential in the number of states of the input automaton. We show how the construction of the emptiness games combines a (fixed) structural part with (history-)determinization of parity word automata. For tree automata with certain syntactic structures, simpler methods may be used to handle the treatment of the word automata, which then may be asymptotically smaller than in the general case. These results have direct consequences in satisfiability and validity checking for (various fragments of) the modal $μ$-calculus. △ Less

Submitted 23 August, 2022; v1 submitted 1 July, 2022; originally announced July 2022.

Comments: 28 pages

Nominal Büchi Automata with Name Allocation

Authors: Henning Urbat, Daniel Hausmann, Stefan Milius, Lutz Schröder

Abstract: 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 infinite alphabets in the setting of nominal sets, and study languages of infinite bar strings, i.e. infinite sequences of names that feature binding of fresh names; binding corresponds roughly to reading letters from inpu… ▽ More 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 infinite alphabets in the setting of nominal sets, and study languages of infinite bar strings, i.e. infinite sequences of names that feature binding of fresh names; binding corresponds roughly to reading letters from input words in automata models with registers. We introduce regular nominal nondeterministic Büchi automata (Büchi RNNAs), an automata model for languages of infinite bar strings, repurposing the previously introduced RNNAs over finite bar strings. Our machines feature explicit binding (i.e. resource-allocating) transitions and process their input via a Büchi-type acceptance condition. They emerge from the abstract perspective on name binding given by the theory of nominal sets. As our main result we prove that, in contrast to most other nondeterministic automata models over infinite alphabets, language inclusion of Büchi RNNAs is decidable and in fact elementary. This makes Büchi RNNAs a suitable tool for applications in model checking. △ Less

Submitted 10 July, 2021; v1 submitted 7 July, 2021; originally announced July 2021.

A Linear-Time Nominal $μ$-Calculus with Name Allocation

Authors: Daniel Hausmann, Stefan Milius, Lutz Schröder

Abstract: 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 tightly to formalisms over nominal sets, such as nondetermininistic orbit-finite automata (NOFAs), where names play the role of data. Reasoning problems in such formalisms tend to be computationally hard. Name-binding no… ▽ More 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 tightly to formalisms over nominal sets, such as nondetermininistic orbit-finite automata (NOFAs), where names play the role of data. Reasoning problems in such formalisms tend to be computationally hard. Name-binding nominal automata models such as regular nondeterministic nominal automata (RNNAs) have been shown to be computationally more tractable. In the present paper, we introduce a linear-time fixpoint logic Bar-muTL for finite words over an infinite alphabet, which features full negation and freeze quantification via name binding. We show by a nontrivial reduction to extended regular nondeterministic nominal automata that even though Bar-muTL allows unrestricted nondeterminism and unboundedly many registers, model checking Bar-muTL over RNNAs and satisfiability checking both have elementary complexity. For example, model checking is in 2ExpSpace, more precisely in parametrized ExpSpace, effectively with the number of registers as the parameter. △ Less

Submitted 20 August, 2021; v1 submitted 21 October, 2020; originally announced October 2020.

Comments: Extended version (shorter version published at MFCS 2021)

NP Reasoning in the Monotone $μ$-Calculus

Authors: Daniel Hausmann, Lutz Schröder

Abstract: 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 fixpoint operators as well as the universal modality; the resulting logic -- the aconjunctive alternation-free monotone $μ$-calculus with the universal modality -- contains both concurrent propositional dynamic logic (C… ▽ More 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 fixpoint operators as well as the universal modality; the resulting logic -- the aconjunctive alternation-free monotone $μ$-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. △ Less

Submitted 3 May, 2020; v1 submitted 12 February, 2020; originally announced February 2020.

Comments: Longer version of IJCAR 2020 paper

Quasipolynomial Computation of Nested Fixpoints

Authors: Daniel Hausmann, Lutz Schröder

Abstract: It is well-known that the winning region of a parity game with $n$ nodes and $k$ priorities can be computed as a $k$-nested fixpoint of a suitable function; straightforward computation of this nested fixpoint requires $\mathcal{O}(n^{\frac{k}{2}})$ iterations of the function. Calude et al.'s recent quasipolynomial-time parity game solving algorithm essentially shows how to compute the same fixpoin… ▽ More It is well-known that the winning region of a parity game with $n$ nodes and $k$ priorities can be computed as a $k$-nested fixpoint of a suitable function; straightforward computation of this nested fixpoint requires $\mathcal{O}(n^{\frac{k}{2}})$ iterations of the function. Calude et al.'s recent quasipolynomial-time parity game solving algorithm essentially shows how to compute the same fixpoint in only quasipolynomially many iterations by reducing parity games to quasipolynomially sized safety games. Universal graphs have been used to modularize this transformation of parity games to equivalent safety games that are obtained by combining the original game with a universal graph. We show that this approach naturally generalizes to the computation of solutions of systems of \emph{any} fixpoint equations over finite lattices; hence, the solution of fixpoint equation systems can be computed by quasipolynomially many iterations of the equations. We present applications to modal fixpoint logics and games beyond relational semantics. For instance, the model checking problems for the energy $μ$-calculus, finite latticed $μ$-calculi, and the graded and the (two-valued) probabilistic $μ$-calculus -- with numbers coded in binary -- can be solved via nested fixpoints of functions that differ substantially from the function for parity games but still can be computed in quasipolynomial time; our result hence implies that model checking for these $μ$-calculi is in QP. Moreover, we improve the exponent in known exponential bounds on satisfiability checking. △ Less

Submitted 19 March, 2021; v1 submitted 16 July, 2019; originally announced July 2019.

Comments: extended version of conference paper

Optimal Satisfiability Checking for Arithmetic $μ$-Calculi

Authors: Daniel Hausmann, Lutz Schröder

Abstract: The coalgebraic $μ$-calculus provides a generic semantic framework for fixpoint logics with branching types beyond the standard relational setup, e.g. probabilistic, weighted, or game-based. Previous work on the coalgebraic $μ$-calculus includes an exponential time upper bound on satisfiability checking, which however requires a well-behaved set of tableau rules for the next-step modalities. Such… ▽ More The coalgebraic $μ$-calculus provides a generic semantic framework for fixpoint logics with branching types beyond the standard relational setup, e.g. probabilistic, weighted, or game-based. Previous work on the coalgebraic $μ$-calculus includes an exponential time upper bound on satisfiability checking, which however requires a well-behaved set of tableau rules for the next-step modalities. Such rules are not available in all cases of interest, in particular ones involving either integer weights as in the graded $μ$-calculus, or real-valued weights in combination with non-linear arithmetic. In the present paper, we prove the same upper complexity bound under more general assumptions, specifically regarding the complexity of the (much simpler) satisfiability problem for the underlying so-called one-step logic, roughly described as the nesting-free next-step fragment of the logic. We also present a generic global caching algorithm that is suitable for practical use and supports on-the-fly satisfiability checking. Example applications include new exponential-time upper bounds for satisfiability checking in an extension of the graded $μ$-calculus with Presburger arithmetic, as well as an extension of the (two-valued) probabilistic $μ$-calculus with polynomial inequalities. As a side result, we moreover obtain a new upper bound $\mathcal{O}(((nk)!)^2)$ on minimum model size for satisfiable formulas for all coalgebraic $μ$-calculi, where $n$ is the size of the formula and $k$ its alternation depth. △ Less

Submitted 15 January, 2019; originally announced January 2019.

Permutation Games for the Weakly Aconjunctive $μ$-Calculus

Authors: Daniel Hausmann, Lutz Schröder, Hans-Peter Deifel

Abstract: 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 fragment of the $μ$-calculus. To this end we devise a method that determinizes limit-deterministic parity automata of size $n$ with $k$ priorities through limit-deterministic Büchi automata to deterministic parity automata o… ▽ More 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 fragment of the $μ$-calculus. To this end we devise a method 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 $μ$-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. △ Less

Submitted 14 March, 2018; v1 submitted 24 October, 2017; originally announced October 2017.

Global Caching for the Alternation-free $μ$-Calculus

Authors: Daniel Hausmann, Lutz Schröder, Christoph Egger

Abstract: We present a sound, complete, and optimal single-pass tableau algorithm for the alternation-free $μ$-calculus. The algorithm supports global caching with intermediate propagation and runs in time $2^{\mathcal{O}(n)}$. In game-theoretic terms, our algorithm integrates the steps for constructing and solving the Büchi game arising from the input tableau into a single procedure; this is done on-the-fl… ▽ More We present a sound, complete, and optimal single-pass tableau algorithm for the alternation-free $μ$-calculus. The algorithm supports global caching with intermediate propagation and runs in time $2^{\mathcal{O}(n)}$. In game-theoretic terms, our algorithm integrates the steps for constructing and solving the Büchi game arising from the input tableau into a single procedure; this is done on-the-fly, i.e. may terminate before the game has been fully constructed. This suggests a slogan to the effect that global caching = game solving on-the-fly. A prototypical implementation shows promising initial results. △ Less

Submitted 20 September, 2016; originally announced September 2016.