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 a terminating tableau system 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 show how to encode the tableaux we introduced into $\mu$-calculus formulas. This encoding provides upper bounds for the satisfiability checking of the few logics we previously did not have algorithms for.

翻译：本文利用跨逻辑的翻译方法，研究经典模态逻辑及其带不动点算子扩展的复杂性。具体而言，我们通过多主体逻辑与μ演算及模态逻辑之间的双向翻译，展示多项复杂性结果，从而迁移已知的上界与下界。同时，基于Kozen的μ演算表格法以及Fitting与Massacci的模态逻辑表格法，利用这些翻译为所研究的逻辑引入一个可终止的表格系统。最后，我们展示如何将所引入的表格编码为μ演算公式。该编码为先前缺乏算法的少数逻辑提供了可满足性检测的上界。