We show that the satisfiability problems of the bimodal product logics K4xS5 and S4xS5 and of the bimodal logic of subset spaces SSL are EXPSPACE-complete. In fact, on the one hand we construct for these three problems decision algorithms working even in ESPACE. The heart of the proof, that on the other hand these problems are EXPSPACE-hard, is a reduction, computable in logarithmic space, of the word problem for so called Alternating Turing machines working in exponential time to the satisfiability problem for the logic SSL. It is known, that these machines accept exactly the languages accepted by usual Turing machines working in exponential space. We show EXPSPACE-hardness of S4xS5 and K4xS5 by translating on the one hand SSL-formulas to equisatisfiable S4xS5-formulas and finally by translating S4xS5-formulas to equisatisfiable K4xS5-formulas, where both translations are computable in logarithmic space as well.    «

We show that the satisfiability problems of the bimodal product logics K4xS5 and S4xS5 and of the bimodal logic of subset spaces SSL are EXPSPACE-complete. In fact, on the one hand we construct for these three problems decision algorithms working even in ESPACE. The heart of the proof, that on the other hand these problems are EXPSPACE-hard, is a reduction, computable in logarithmic space, of the word problem for so called Alternating Turing machines working in exponential time to the satisfiabili...    »