一句话：证明有限森林上两种带复合算子的模态逻辑的表达力与可满足性复杂度，并解决相关公开问题。
论文研究在有限森林上解释、并带有用于推理子模型的标准模态词的两类模态逻辑 ML(|) 与 ML(*)。ML(|) 在模态逻辑 K 上加入 ambient logic 的复合算子 |，ML(*) 则加入分离逻辑的分离合取 *，两者本质上都是二阶算子。作者比较了它们的表达力：ML(|) 与树上的 graded modal logic GML 表达力相同，而 ML(*) 严格弱于 GML。可满足性方面，ML(*) 是 Tower-完全的，ML(|) 仅为 AExpPol-完全的，这一反差在表达力对比下出人意料。作为副产品，还解决了静态 ambient logic 与模态分离逻辑等姊妹逻辑的若干公开问题。
We study the expressivity and complexity of two modal logics interpreted on finite forests and equipped with standard modalities to reason on submodels. The logic ML(|) extends the modal logic K with the composition operator | from ambient logic, whereas ML(*) features the separating conjunction * from separation logic. Both operators are second-order in nature. We show that ML(|) is as expressive as the graded modal logic GML (on trees) whereas ML(*) is strictly less expressive than GML. Moreover, we establish that the satisfiability problem is Tower-complete for ML(*), whereas it is (only) AExpPol-complete for ML(|), a result which is surprising given their relative expressivity. As by-products, we solve open problems related to sister logics such as static ambient logic and modal separation logic.