3 years ago

Permutation Games for the Weakly Aconjunctive mu-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 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 O((nk+2)!) and with 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 O((nk+2)!) with 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.

Publisher URL: http://arxiv.org/abs/1710.08996

DOI: arXiv:1710.08996v1

You might also like
Discover & Discuss Important Research

Keeping up-to-date with research can feel impossible, with papers being published faster than you'll ever be able to read them. That's where Researcher comes in: we're simplifying discovery and making important discussions happen. With over 19,000 sources, including peer-reviewed journals, preprints, blogs, universities, podcasts and Live events across 10 research areas, you'll never miss what's important to you. It's like social media, but better. Oh, and we should mention - it's free.

  • Download from Google Play
  • Download from App Store
  • Download from AppInChina

Researcher displays publicly available abstracts and doesn’t host any full article content. If the content is open access, we will direct clicks from the abstracts to the publisher website and display the PDF copy on our platform. Clicks to view the full text will be directed to the publisher website, where only users with subscriptions or access through their institution are able to view the full article.