This paper studies the complexity of classical modal logics and of their extension with fixed-point operators, using translations to transfer results across logics. In particular, we show several complexity results for multi-agent logics via translations to and from the $\mu$-calculus and modal logic, which allow us to transfer known upper and lower bounds. We also use these translations to introduce terminating and non-terminating tableau systems for the logics we study, based on Kozen's tableau for the $\mu$-calculus and the one of Fitting and Massacci for modal logic. Finally, we describe these tableaux with $\mu$-calculus formulas, thus reducing the satisfiability of each of these logics to the satisfiability of the $\mu$-calculus, resulting in a general 2EXP upper bound for satisfiability testing.

翻译：本文通过翻译方法在逻辑间传递结果，研究了经典模态逻辑及其不动点算子扩展的复杂性。特别地，我们通过$\mu$-演算与模态逻辑之间的双向翻译，展示了多智能体逻辑的若干复杂性结论，这使得我们能够迁移已知的上界与下界结果。基于Kozen为$\mu$-演算设计的表列系统以及Fitting与Massacci为模态逻辑构建的表列方法，我们进一步利用这些翻译为我们研究的逻辑引入了可终止与不可终止的表列系统。最后，我们使用$\mu$-演算公式描述这些表列系统，从而将各逻辑的可满足性问题归约为$\mu$-演算的可满足性问题，最终为可满足性检测建立了一个通用的2EXP上界。