08/07/2020

Modal Logics with Composition on Finite Forests: Expressivity and Complexity

Bartosz Bednarczyk, Stéphane Demri, Raul Fervari, Alessio Mansutti

Keywords: static ambient logic, separation logic, graded modal logic, expressive power, complexity, modal logic on trees

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.

 0
 0
 0
 0
This is an embedded video. Talk and the respective paper are published at ICALP 2020 virtual conference. If you are one of the authors of the paper and want to manage your upload, see the question "My papertalk has been externally embedded..." in the FAQ section.

Comments

Post Comment
no comments yet
code of conduct: tbd

Similar Papers