Inproceedings3250: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Bartosz Bednarczyk (Diskussion | Beiträge) Keine Bearbeitungszusammenfassung |
Bartosz Bednarczyk (Diskussion | Beiträge) Keine Bearbeitungszusammenfassung |
||
| Zeile 11: | Zeile 11: | ||
|Month=Juni | |Month=Juni | ||
|Booktitle=Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2020) | |Booktitle=Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2020) | ||
|Pages=167--180 | |||
|Publisher=ACM | |||
|Editor=Holger Hermanns, Lijun Zhang, Naoki Kobayashi, Dale Miller | |||
}} | }} | ||
{{Publikation Details | {{Publikation Details | ||
|Abstract=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. | |Abstract=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. | ||
|Download=BBE-LICS20.pdf | |Download=BBE-LICS20.pdf | ||
|Link=https:// | |Link=https://dl.acm.org/doi/10.1145/3373718.3394787 | ||
|DOI Name=10.1145/3373718.3394787 | |DOI Name=10.1145/3373718.3394787 | ||
|Forschungsgruppe=Computational Logic | |Forschungsgruppe=Computational Logic | ||
Aktuelle Version vom 9. September 2022, 18:41 Uhr
Modal Logics with Composition on Finite Forests: Expressivity and Complexity
Bartosz BednarczykBartosz Bednarczyk, Stéphane DemriStéphane Demri, Raul FervariRaul Fervari, Alessio MansuttiAlessio Mansutti
Bartosz Bednarczyk, Stéphane Demri, Raul Fervari, Alessio Mansutti
Modal Logics with Composition on Finite Forests: Expressivity and Complexity
In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, Dale Miller, eds., Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2020), 167--180, June 2020. ACM
Modal Logics with Composition on Finite Forests: Expressivity and Complexity
In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, Dale Miller, eds., Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2020), 167--180, June 2020. ACM
- 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. - Weitere Informationen unter:Further Information: Link
- Forschungsgruppe:Research Group: Computational LogicComputational Logic
@inproceedings{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},
editor = {Holger Hermanns and Lijun Zhang and Naoki Kobayashi and Dale
Miller},
booktitle = {Proceedings of the 35th Annual {ACM/IEEE} Symposium on Logic in
Computer Science (LICS 2020)},
publisher = {ACM},
year = {2020},
month = {June},
pages = {167--180},
doi = {10.1145/3373718.3394787}
}
