On Composing Finite Forests with Modal Logics

Bartosz BednarczykBartosz Bednarczyk, Stéphane DemriStéphane Demri, Raul FervariRaul Fervari, Alessio MansuttiAlessio Mansutti

ISSN: 1529-3785
Download
DOI Link

Bartosz Bednarczyk, Stéphane Demri, Raul Fervari, Alessio Mansutti
On Composing Finite Forests with Modal Logics
ACM Transactions on Computational Logic, 24(2), April 2023

Details
Bibtex

KurzfassungAbstract
We study the expressivity and complexity of two modal logics interpreted on inite 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 satisiability problem is Tower-complete for ML(∗), whereas it is (only) AExpPolcomplete 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.
Weitere Informationen unter:Further Information: Link
Forschungsgruppe:Research Group: Computational LogicComputational Logic

@article{BDFM2023,
  author    = {Bartosz Bednarczyk and St{\'{e}}phane Demri and Raul Fervari and
               Alessio Mansutti},
  title     = {On Composing Finite Forests with Modal Logics},
  journal   = {ACM Transactions on Computational Logic},
  volume    = {24},
  number    = {2},
  publisher = {Association for Computing Machinery},
  year      = {2023},
  month     = {April},
  doi       = {10.1145/3569954}
}