Article3088

PublikationenPublications

• Nach AutorBy Author
  • Bartosz BednarczykBartosz Bednarczyk
• Nach ForschungsgruppeBy Research Group
  • Computational LogicComputational Logic

Toggle side column

On Composing Finite Forests with Modal Logics

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

• ISSN: 1529-3785
• DOI Link

Bartosz Bednarczyk, Stéphane Demri, Raul Fervari, Alessio Mansutti
On Composing Finite Forests with Modal Logics
ACM Transactions on Computational Logic, December 2022

• 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{BDFM2022,
  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},
  publisher = {Association for Computing Machinery},
  year      = {2022},
  month     = {December},
  doi       = {10.1145/3569954}
}