On Composing Finite Forests with Modal Logics

Research output: Contribution to journalResearch articleContributedpeer-review

Contributors

  • Bartosz Bednarczyk - , Chair of Computational Logic, University of Wrocław (Author)
  • Stéphane Demri - (Author)
  • Raul Fervari - (Author)
  • Alessio Mansutti - (Author)

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 extends the modal logic K with the composition operator from ambient logic whereas features the separating conjunction from separation logic. Both operators are second-order in nature. We show that is as expressive as the graded modal logic (on trees) whereas is strictly less expressive than . Moreover, we establish that the satisfiability problem is Tower-complete for , whereas it is (only) AExpPol-complete for , a result that 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.

Details

Original languageEnglish
Article number3569954
Number of pages46
JournalACM transactions on computational logic
Volume24
Issue number2
Publication statusPublished - 3 Apr 2023
Peer-reviewedYes

External IDs

Scopus 85152943708

Keywords