The product of converse PDL and polymodal K

The product of two modal logics L1 and L2 is the modal logic determined by the class of frames of the form F \Theta G such that F and G validate L1 and L2 , respectively. This paper proves the decidability of the product of converse PDL and polymodal K. Decidability results for products of modal logics of knowledge as well as temporal logics and polymodal K are discussed. All those products form rather expressive but still decidable fragments of modal predicate logics. Based on the equivalence of polymodal K and the description logic ALC we shall discuss the obtained fragments, extend the expressive power a bit, and compare them with other modal description logics