Modal Logics with Composition on Finite Forests: Expressivity and Complexity

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) AExp Pol -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.

• Theory of computation → Modal and temporal logics.