PSPACE-completeness of bimodal transitive weak-density logic
Logic in Computer Science
2025-07-22 v1
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 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.
Keywords
Cite
@article{arxiv.2507.14949,
title = {PSPACE-completeness of bimodal transitive weak-density logic},
author = {Philippe Balbiani and Olivier Gasquet},
journal= {arXiv preprint arXiv:2507.14949},
year = {2025}
}
Comments
arXiv admin note: substantial text overlap with arXiv:2507.11238