Complexity of simple dependent bimodal logics

We characterize the computational complexity of simple dependent bimodal logics. We define an operator +subset of or equal to between logics that almost behaves as the standard joint operator + except that the inclusion axiom [2]p double right arrow [l]p is added. Many multimodal logics from the literature are of this form or contain such fragments. For the standard modal logics K,T,B,S4 and S5 we study the complexity of the satisfiability problem of the joint in the sense of +subset of or equal to. We mainly establish the PSPACE upper bounds by designing tableaux-based algorithms in which a particular attention is given to the formalization of termination and to the design of a uniform framework. Reductions into the packed guarded fragment with only two variables introduced by M. Marx are also used. E. Spaan proved that K+subset of or equal to S5 is EXPTIME-hard. We show that for [L(1), L(2)] is an element of {K, T, B} x {S4, S5}, L(1) +subset of or equal to L(2) is also EXPTIME-hard.