通过翻译与表列系统的带递归模态逻辑复杂性结果

本文研究经典模态逻辑及其带不动点算子扩展的复杂性，利用翻译在不同逻辑间传递结果。特别地，我们通过对 $\mu$-演算与模态逻辑的来回翻译，展示了多智能体逻辑的若干复杂性结果，从而得以传递已知的上界与下界。我们还利用这些翻译，基于 Kozen 的 $\mu$-演算表列以及 Fitting 和 Massacci 的模态逻辑表列，引入我们所研究逻辑的中止与非中止表列系统。最后，我们用 $\mu$-演算公式描述这些表列，从而将各逻辑的满足性问题归约到 $\mu$-演算的满足性问题，得到满足性检验的一般 2EXP 上界。