In this paper, we develop model checking procedures for three ways of combining (temporal) logics:
temporalization, independent combination, and join.We prove that they are terminating, sound, and complete, we
analyze their computational complexity, and we report on experiments with implementations.We take a close look
at mobile systems and show how the proposed combined model checking framework can be successfully applied
to the specification and verification of their properties.
