Abstract Windows have been introduced in 1 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 8, 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 K4 together with windows-approach. The conclusion is that both satisfiability and validity are PSPACE-complete for these logics.
Olivier Gasquet (Sat,) studied this question.