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算术）的分级μ演算扩展，以及带多项式不等式的（二值）概率μ演算扩展的可满足性检验新指数时间上界。