Undecidability and Temporal Logic: Some Landmarks from Turing to the Present

This is a selective survey and discussion of some of the landmark undecidability results in temporal logic, beginning with Turing´s undecidability of the Halting problem which, in retrospect, can be regarded as the historically first undecidability result for a suitable temporal logic over configuration graphs of Turing machines. I will discuss some of the natural habitats of undecidable temporal logics, such as first-order, interval-based and real time temporal logics, as well as some extensions that often lead to undecidability, such as two-dimensional temporal logics and temporal-epistemic logics.