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 SizeFormat 
Complexity results for modal logic with recursion via translations and tableaux 2024.pdf718.66 kBAdobe PDFView/Open


Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.