Both Datalog and Computation Tree Logic (CTL) model checking have been used for declaratively analysing programs. Gottlob et al. (2002) shows how to translate CTL formulae to a subset of Datalog. We extend this by embedding multimodal CTL into the wider Datalog language so that they can be used side-by-side. Further, we extend Datalog with temporal hybrid logic operators to be able to reify and modify the hidden (implicit) time used by the CTL operators in a structured manner. Our system is entirely time agnostic: different notions of time such as a program counter, nodes of a dataflow graph, or versions of software repositories can all be used. Multimodal CTL operators allow various notions of time to be used together within the same clause. We compile our extension into stratified Datalog while preserving properties such as domain independence and well-modedness.