Modal Logics with Composition on Finite Forests: Expressivity and Complexity

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

Bartosz Bednarczyk, Stéphane Demri, Alessio Mansutti, Raul Fervari
Modal Logics with Composition on Finite Forests: Expressivity and Complexity
Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2020), June 2020

Details
Bibtex

KurzfassungAbstract
We investigate the expressivity and computational complexity of two modal logics on finite forests equipped with operators to reason on submodels. The logic ML(|) extends the basic modal logic ML with the composition operator | from static ambient logic, whereas ML(∗) contains the separating conjunction ∗ from separation logic. Though both operators are second-order in nature, we show that ML(|) is as expressive as the graded modal logic GML (on finite trees) whereas ML(∗) lies strictly between ML and GML. Moreover, we establish that the satisfiability problem for ML(∗) is Tower-complete, whereas for ML(|) is (only) AExpPol-complete.As a by-product, we solve several open problems related to sister logics, such as static ambient logic, modal separation logic, and second-order modal logic on finite trees.
Forschungsgruppe:Research Group: Computational LogicComputational Logic

@inproceedings{BDMF2020,
  author    = {Bartosz Bednarczyk and St{\'{e}}phane Demri and Alessio Mansutti
               and Raul Fervari},
  title     = {Modal Logics with Composition on Finite Forests: Expressivity and
               Complexity},
  booktitle = {Proceedings of the 35th Annual {ACM/IEEE} Symposium on Logic in
               Computer Science (LICS 2020)},
  year      = {2020},
  month     = {June}
}