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 alternation-free fixpoint operators as well as the universal modality; the resulting logic – the alternation-free monotone mu-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.
CITATION STYLE
Hausmann, D., & Schröder, L. (2020). NP Reasoning in the Monotone$$\mu $$ -Calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12166 LNAI, pp. 482–499). Springer. https://doi.org/10.1007/978-3-030-51074-9_28
Mendeley helps you to discover research relevant for your work.