Complexity results for modal logic with recursion via translations and tableaux

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 $\mu$-calculus and modal logi...

Full description

Saved in:
Bibliographic Details
Published in:Logical methods in computer science 2024-01, Vol.20, Issue 3 (3)
Main Authors: Aceto, Luca, Achilleos, Antonis, Anastasiadi, Elli, Francalanza, Adrian, Ingólfsdóttir, Anna
Format: Article
Language:English
Subjects:
computer science - logic in computer science
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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 $\mu$-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 $\mu$-calculus and the one of Fitting and Massacci for modal logic. Finally, we describe these tableaux with $\mu$-calculus formulas, thus reducing the satisfiability of each of these logics to the satisfiability of the $\mu$-calculus, resulting in a general 2EXP upper bound for satisfiability testing.
ISSN:1860-5974
1860-5974
DOI:10.46298/lmcs-20(3:14)2024