Modal Logics with Composition on Finite Forests: Expressivity and Complexity (Extra Material)

TL;DR

This paper explores the expressivity and computational complexity of two modal logics with composition operators on finite forests, revealing their relative power and solving open problems in related logics.

Contribution

It characterizes the expressivity of ML(|) and ML(*) and determines their satisfiability complexities, advancing understanding of modal logics with composition operators.

Findings

ML(|) is as expressive as graded modal logic GML on finite trees

ML(*) is strictly between ML and GML in expressivity

Satisfiability for ML(*) is Tower-complete, for ML(|) is AExpPol-complete

Abstract

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.