Permutation games for the weakly aconjunctive \(\mu \)-calculus

DOI10.1007/978-3-319-89963-3_21zbMATH Open1423.68307arXiv1710.08996OpenAlexW2963537255MaRDI QIDQ2324236

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

Publication date: 16 September 2019

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 $mathcalO((nk)!)$ and with $mathcalO(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 $mathcalO((nk)!)$ with $mathcalO(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.

Full work available at URL: https://arxiv.org/abs/1710.08996

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (4)

Title not available (Why is that?) ⋮ A survey on satisfiability checking for the \(\mu \)-calculus through tree automata ⋮ COOL 2 – A Generic Reasoner for Modal Fixpoint Logics (System Description) ⋮ Coalgebraic satisfiability checking for arithmetic \(\mu\)-calculi

This page was built for publication: Permutation games for the weakly aconjunctive \(\mu \)-calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2324236)