Satisfiability-checking of modal logic with recursion via translations and tableaux

In this work we studied the complexity of classical modal logics and their extension with fixed-point operators, using translations to transfer results across logics. In particular, we showed 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 a terminating tableau system for the logics we study, based on Kozen’s tableau for the μ-calculus, and the one of Fitting and Massacci for modal logic. In the talk I will focus on our method for tackling tableau-based derivations that may not terminate, for achieving decidability and upper complexity bounds, and discuss how we used this method to prove the decidability of certain modal logics that do not have a finite model property. This is joint work with Luca Aceto, Antonis Achilleos, Adrian Francalanza, and Anna Ingolfsdottir.

Authors

• Elli Anastasiadi

Keywords

No keywords are indexed for this paper.