通过翻译和表格法对具有递归的模态逻辑进行复杂性结果的研究
摘要：经典模态逻辑及其带固定点运算符扩展的复杂性研究：通过翻译结果在逻辑之间传递，本文研究了经典模态逻辑及其带固定点运算符扩展的复杂性。特别是通过与μ-演算和模态逻辑之间的翻译，我们展示了一些多代理逻辑的复杂性结果，可以转移已知的上界和下界。我们还利用这些翻译引入了一个基于Kozen的μ-演算表格和Fitting和Massacci的模态逻辑表格的终止表格系统来研究我们的逻辑。最后，我们展示了如何将我们引入的表格编码为μ-演算公式。这种编码为我们之前没有算法的一些逻辑的可满足性检查提供了上界。
作者：Luca Aceto, Antonis Achilleos, Elli Anastasiadi, Adrian Francalanza, Anna Ing''olfsd''ottir
论文ID：2306.16881
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-30