 A very natural class of instant-based models of time is the class of linear models, and soon after Prior’s invention of Tense Logic several extensions of TL over linear time have been proposed. In this section, we discuss two such extensions of Prior’s basic temporal logic: the extension of TL by a Next Time operator over discrete, linear models of time and the introduction of the operators Since and Until. These operators also form the basis of the linear time temporal logic LTL, which has widespread applications in computer science.