Complexity through Translations for Modal Logic with Recursion
Luca Aceto (School of Computer Science, Reykjavik University, Gran, Sasso Science Institute, L'Aquila, Italy), Antonis Achilleos (School of, Computer Science, Reykjavik University), Elli Anastasiadi (School of Computer, Science, Reykjavik University)
TL;DR
This paper explores the complexity of classical and fixed-point modal logics by using translations to transfer results, and introduces a tableau system based on these translations for improved analysis.
Contribution
It presents a novel translation-based approach to analyze complexity and introduces a terminating tableau system for multi-agent modal logics with fixed points.
Findings
Complexity bounds transferred via translations between logics.
A new terminating tableau system for multi-agent modal logics with fixed points.
Unified framework for analyzing modal logic complexity.
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 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 mu-calculus, and the one of Fitting and Massacci for modal logic.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.