Permutation Games for the Weakly Aconjunctive $\mu$-Calculus

TL;DR

This paper introduces a novel automata-based approach for constructing satisfiability games for the weakly aconjunctive fragment of the $d$-calculus, leveraging limit-deterministic parity automata to improve complexity and efficiency.

Contribution

It presents a new method to determinize limit-deterministic parity automata using partial permutations, avoiding full Safra/Piterman constructions, and applies this to satisfiability games for the weakly aconjunctive $d$-calculus.

Findings

Automata determinization method reduces complexity compared to Safra/Piterman.

Constructed satisfiability games have size $O((nk)!)$ with $O(nk)$ priorities.

Prototype implementation shows promising initial results in solving these games.

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 $\mu$-calculus. To this end we devise a method that determinizes limit-deterministic parity automata of size $n$ with $k$ priorities through limit-deterministic B\"uchi 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.