On Composing Finite Forests with Modal Logics
Research output: Contribution to journal › Research article › Contributed › peer-review
Contributors
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 language | English |
---|---|
Article number | 3569954 |
Number of pages | 46 |
Journal | ACM transactions on computational logic |
Volume | 24 |
Issue number | 2 |
Publication status | Published - 3 Apr 2023 |
Peer-reviewed | Yes |
External IDs
Scopus | 85152943708 |
---|