论文标题
单调$μ$ -calculus中的NP推理
NP Reasoning in the Monotone $μ$-Calculus
论文作者
论文摘要
已知对单调模量逻辑的满足性检查是（仅）NP完整的。我们表明，当逻辑与无尖和交替的固定点运算符以及通用模态扩展时，这仍然是正确的。所得的逻辑 - 带有通用模态的无尖端单调$μ$ $ $ $ $ $ $ $ - 既包含并发的命题动力学逻辑（CPDL），也包含游戏逻辑的无交替片段作为片段。我们通过通过多个eloise节点的Büchi游戏来表征令人满意的表征。
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 aconjunctive and alternation-free fixpoint operators as well as the universal modality; the resulting logic -- the aconjunctive alternation-free monotone $μ$-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.
