Abstract:
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.