论文标题
具有有限森林组成的模态逻辑：表现力和复杂性（额外的材料）
Modal Logics with Composition on Finite Forests: Expressivity and Complexity (Extra Material)
论文作者
论文摘要
我们研究了配备有操作员的有限森林上两个模态逻辑的表达和计算复杂性，以推理子模型。逻辑ML（|）用构图操作员扩展了基本的模态逻辑ML |从静态环境逻辑中，而ML（ *）包含与分离逻辑的分离连词 *。尽管两个运算符本质上都是二阶的，但我们表明ML（|）与分级的模态逻辑GML（在有限树上）一样表现力，而ML（*）严格位于ML和GML之间。此外，我们确定ML（*）的满足性问题是塔式完整的，而对于ML（|）是（仅）Aexppol-Complete。作为副产品，我们解决了与姐妹逻辑有关的几个开放问题，例如静态环境逻辑，模态分离逻辑和有限树上的二阶模态逻辑。
We investigate the expressivity and computational complexity of two modal logics on finite forests equipped with operators to reason on submodels. The logic ML(|) extends the basic modal logic ML with the composition operator | from static ambient logic, whereas ML(*) contains the separating conjunction * from separation logic. Though both operators are second-order in nature, we show that ML(|) is as expressive as the graded modal logic GML (on finite trees) whereas ML(*) lies strictly between ML and GML. Moreover, we establish that the satisfiability problem for ML(*) is Tower-complete, whereas for ML(|) is (only) AExpPol-complete. As a by-product, we solve several open problems related to sister logics, such as static ambient logic, modal separation logic, and second-order modal logic on finite trees.
