EXPSPACE-Completeness of the Logics K4xS5 and S4xS5 and the Logic of\n Subset Spaces, Part 1: ESPACE-Algorithms

2019/08/09 by Peter Hertling, Hertling, Peter, Gisela Krommes +1
Computer Science · #03B45 #68Q17 #68Q25 #Advanced Algebra and Logic #Computational Complexity (cs.CC) #FOS: Computer and information sciences #FOS: Mathematics #Formal Methods in Verification #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems

paper · pdf · doi:10.48550/arxiv.1908.03501

openalex publication_date 2019/08/09 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

It is known that the satisfiability problems of the product logics K4xS5 and\nS4xS5 and of the logic SSL of subset spaces are in N2EXPTIME. We improve this\nupper bound for the complexity of these problems by presenting\nESPACE-algorithms for these problems. In another paper we show that these\nproblems are EXPSPACE-hard. This shows that all three problems are\nEXPSPACE-complete.\n

Related

• EXPSPACE-Completeness of the Logics K4xS5 and S4xS5 and the Logic of Subset Spaces, Part 2: EXPSPACE-Hardness
• Characterizing the NP-PSPACE Gap in the Satisfiability Problem for Modal Logic
• Logics with the axiom of convergence: complexity with a small number of variables in the language (extended version)
• The Complexity of Satisfiability for Sub-Boolean Fragments of ALC
• Characterizing the Exponential-Space Hierarchy Via Partial Fixpoints