 The ontological nature and properties of time give rise to fundamental philosophical questions, which find their expression in the rich variety of formal models of time employed in temporal logics. For example, is time instant-based or interval-based? Is it discrete, dense, or continuous? Does time have a beginning or an end? Is it linear, branching, or circular? Before we turn to the formal languages of temporal logics and their semantics, we briefly introduce below the two most basic types of formal models of time together with some of their pertinent properties: instant-based and interval-based models.