Modal Logics with Composition on Finite Forests: Expressivity and Complexity

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

Toggle side column

Modal Logics with Composition on Finite Forests: Expressivity and Complexity

Bartosz BednarczykBartosz Bednarczyk,  Stéphane DemriStéphane Demri,  Raul FervariRaul Fervari,  Alessio MansuttiAlessio Mansutti
Modal Logics with Composition on Finite Forests: Expressivity and Complexity


Bartosz Bednarczyk, Stéphane Demri, Raul Fervari, Alessio Mansutti
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), to appear
  • 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 Logic
@article{BDFM2020,
  author  = {Bartosz Bednarczyk and St{\'{e}}phane Demri and Raul Fervari and
             Alessio Mansutti},
  title   = {Modal Logics with Composition on Finite Forests: Expressivity and
             Complexity},
  journal = {Proceedings of the 35th Annual {ACM/IEEE} Symposium on Logic in
             Computer Science (LICS 2020)},
  year    = {2020},
  month   = {June}
}