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.

翻译：余代数μ-演算为不动点逻辑提供了一个通用的语义框架，适用于分支类型超出标准关系结构的系统，例如概率系统、加权系统或基于博弈的系统。先前关于余代数μ-演算的研究已给出可满足性检验的指数时间上界，但该结果依赖于能够获得在形式化定义意义上表现足够良好的下一步模态表规则；具体而言，规则匹配需能由多项式规模的编码表示，且规则的序列对偶需能吸收切割。虽然此类规则集已在某些重要案例中得到确认，但并非所有关注案例（特别是涉及整数权重（如分级μ-演算）或实值权重结合非线性算术的情形）中均已知其存在性。在本研究中，我们在更一般的假设条件下证明了相同的复杂度上界，特别是关于底层单步逻辑（大致描述为该逻辑的无嵌套下一步片段）这一（更简单的）可满足性问题的复杂度。该上界通过支持即时可满足性检验的通用全局缓存算法实现。值得注意的是，我们的方法直接支持非保护公式，从而避免使用保护性变换。示例应用包括：对扩展了多项式不等式（包括正普雷斯伯格算术）的分级μ-演算，以及扩展了多项式不等式的（二值）概率μ-演算，进行可满足性检验的新指数时间上界。