English

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 \K4\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.

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

R2 v1 2026-07-01T04:09:55.755Z