PSPACE-completeness of bimodal transitive weak-density logic

TL;DR

This paper demonstrates that adding transitivity to bimodal weak-density logic results in both satisfiability and validity problems being PSPACE-complete, using windows to develop polynomial algorithms.

Contribution

It introduces a novel approach combining windows with existing algorithms to establish PSPACE-completeness for the extended bimodal weak-density logic.

Findings

Satisfiability and validity are PSPACE-complete for these logics.

Windows enable polynomial algorithms for the extended logic.

The approach revisits and extends previous results on bimodal K4 logic.

Abstract

Windows have been introduce in \cite{BalGasq25} as a tool for designing polynomial algorithms to check satisfiability of a bimodal logic of weak-density. In this paper, after revisiting the ``folklore'' case of bimodal $\K4$ already treated in \cite{Halpern} but which is worth a fresh review, we show that windows allow to polynomially solve the satisfiability problem when adding transitivity to weak-density, by mixing algorithms for bimodal K together with windows-approach. The conclusion is that both satisfiability and validity are PSPACE-complete for these logics.