Please use this identifier to cite or link to this item:
https://www.um.edu.mt/library/oar/handle/123456789/131242
Title: | Complexity results for modal logic with recursion via translations and tableaux |
Authors: | Aceto, Luca Achilleos, Antonis Anastasiadi, Elli Francalanza, Adrian Ingólfsdóttir, Anna |
Keywords: | Modality (Logic) Recursive functions Translators (Computer programs) Fixed point theory Calculus -- Computer programs |
Issue Date: | 2024 |
Publisher: | EPIsciences |
Citation: | Aceto, L., Achilleos, A., Anastasiadi, E., Francalanza, A., & Ingólfsdóttir, A. (2024). Complexity results for modal logic with recursion via translations and tableaux. Logical Methods in Computer Science, 20(3), 14:1–14:53. |
Abstract: | This paper studies the complexity of classical modal logics and of their extension with fixed-point operators, using translations to transfer results across logics. In particular, we show several complexity results for multi-agent logics via translations to and from the μ-calculus and modal logic, which allow us to transfer known upper and lower bounds. We also use these translations to introduce terminating and non-terminating tableau systems for the logics we study, based on Kozen’s tableau for the μ-calculus and the one of Fitting and Massacci for modal logic. Finally, we describe these tableaux with μ-calculus formulas, thus reducing the satisfiability of each of these logics to the satisfiability of the μ-calculus, resulting in a general 2EXP upper bound for satisfiability testing. |
URI: | https://www.um.edu.mt/library/oar/handle/123456789/131242 |
Appears in Collections: | Scholarly Works - FacICTCS |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
Complexity results for modal logic with recursion via translations and tableaux 2024.pdf | 718.66 kB | Adobe PDF | View/Open |
Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.