Non-primitive recursive decidability of products of modal logics with expanding domains

We show that—unlike products of ‘transitive’ modal logics which are usually undecidable—their ‘expanding domain’ relativisations can be decidable, though not in primitive recursive time. In particular, we prove the decidability and the finite expanding product model property of bimodal logics interpreted in two-dimensional structures where one component—call it the ‘flow of time’—is
•  a finite linear order or a finite transitive tree and the other is composed of structures like
•  transitive trees/partial orders/quasi-orders/linear orders or only finite such structures expanding over time. (It is known that none of these logics is decidable when interpreted in structures where the second component does not change over time.) The decidability proof is based on Kruskal’s tree theorem, and the proof of non-primitive recursiveness is by reduction of the reachability problem for lossy channel systems. The result is used to show that the dynamic topological logic interpreted in topological spaces with continuous functions is decidable (in non-primitive recursive time) if the number of function iterations is assumed to be finite.