Permutation Games for the Weakly Aconjunctive \mu μ -Calculus

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ü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.