 The most prominent notion in hybrid temporal logics is that of a nominal. Nominals are special atomic propositions in that they are considered to be true at exactly one instant of the temporal model. Hence, one can think of a nominal \(a\) as saying “It is \(a\) o’clock now”. For this reason, nominals are sometimes also called ‘clock variables’. The idea of nominals can be traced back to Prior (1967, Chapter V; 1968, Chapter XI), who considered the possibility of identifying instants with instant-propositions: an instant can be conceived of as the conjunction of all those propositions that are true at that instant. A first systematic treatment of hybrid temporal logic was given in Bull (1970). In addition to nominals, hybrid languages are often augmented by further syntactic mechanisms, such as a satisfaction operator, nominal quantifiers, and reference pointers, which we briefly discuss below. The former two mechanisms can already be found in Prior’s work (see Blackburn 2006) and were reinvented independently in Passy and Tinchev (1985). Reference pointers were introduced only much later in Goranko (1996), and a similar referencing mechanism is found in Alur and Henzinger (1994).