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为μ演算设计的tableau系统以及Fitting与Massacci为模态逻辑设计的tableau系统，我们利用这些翻译为所研究的逻辑引入了终止性tableau系统。最后，我们展示了如何将所引入的tableau编码为μ演算公式。该编码为先前缺乏算法的少数逻辑提供了可满足性检测的上界。