On Composing Finite Forests with Modal Logics

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche

Toggle side column

On Composing Finite Forests with Modal Logics

Bartosz BednarczykBartosz Bednarczyk,  Stéphane DemriStéphane Demri,  Raul FervariRaul Fervari,  Alessio MansuttiAlessio Mansutti
On Composing Finite Forests with Modal Logics


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
  • 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}
}