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

## TL;DR

This paper introduces ESPACE-algorithms that establish the EXPSPACE-completeness of satisfiability problems for product logics K4xS5, S4xS5, and the logic of subset spaces, improving previous complexity bounds.

## Contribution

It presents the first ESPACE-algorithms for these problems, proving their EXPSPACE-completeness and refining the understanding of their computational complexity.

## Key findings

- Established ESPACE-algorithms for the problems
- Proved the problems are EXPSPACE-hard
- Confirmed the problems are EXPSPACE-complete

## Abstract

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