The coalgebraic $\mu$-calculus provides a generic semantic framework for fixpoint logics over systems whose branching type goes beyond the standard relational setup, e.g. probabilistic, weighted, or game-based. Previous work on the coalgebraic $\mu$-calculus includes an exponential-time upper bound on satisfiability checking, which however relies on the availability of tableau rules for the next-step modalities that are sufficiently well-behaved in a formally defined sense; in particular, rule matches need to be representable by polynomial-sized codes, and the sequent duals of the rules need to absorb cut. While such rule sets have been identified for some important cases, they are not known to exist in all cases of interest, in particular ones involving either integer weights as in the graded $\mu$-calculus, or real-valued weights in combination with non-linear arithmetic. In the present work, we prove the same upper complexity bound under more general assumptions, specifically regarding the complexity of the (much simpler) satisfiability problem for the underlying one-step logic, roughly described as the nesting-free next-step fragment of the logic. The bound is realized by a generic global caching algorithm that supports on-the-fly satisfiability checking. Notably, our approach directly accommodates unguarded formulae, and thus avoids use of the guardedness transformation. Example applications include new exponential-time upper bounds for satisfiability checking in an extension of the graded $\mu$-calculus with polynomial inequalities (including positive Presburger arithmetic), as well as an extension of the (two-valued) probabilistic $\mu$-calculus with polynomial inequalities.

翻译：余代数μ-演算为分支类型超越标准关系设置（例如概率型、加权型或博弈型）的系统上的不动点逻辑提供了通用语义框架。前人关于余代数μ-演算的工作包括可满足性检查的指数时间上界，但该上界依赖于下一步模态的表格规则在形式定义意义下具有足够良好的行为特性；特别地，规则匹配必须能够用多项式大小的编码表示，且规则的后件对偶必须能吸收消解。尽管在某些重要情形下已识别出此类规则集，但在所有感兴趣的情形下（特别是涉及分级μ-演算中的整数权重，或涉及实值权重与非线性算术组合的情形）这类规则集是否均存在尚不明确。本研究在更一般的假设下证明了相同的上复杂度界，具体而言，该假设关注底层一步逻辑（大致描述为逻辑的无嵌套下一步片段）的（更简单的）可满足性问题的复杂度。该上界通过支持即时可满足性检查的通用全局缓存算法实现。值得注意的是，我们的方法可直接处理非保护公式，从而避免使用保护性变换。示例应用包括：在扩展了多项式不等式（含正Presburger算术）的分级μ-演算中，以及在扩展了多项式不等式的（二值）概率μ-演算中，均获得了可满足性检查的新指数时间上界。