Temporal Logic

Temporal logic is based on modal logic which uses the standard two modalities □ and ◊ interpreted as “necessity” and “possibility”. Kripke [1963] elaborated a formal semantics for modal logic. Prior [1957] first suggested a temporal interpretation of the modalities, “always” for □ and “sometimes” for ◊. Following von Wright [1965] a new modality, the “next” time operator, denoted by o, was added to □ and ◊, and the temporal logic obtained was investigated in Prior [1967]. Prior’s temporal logic contains operators for referring to both past and future. From Prior’s work different temporal logics have been developed with different temporal operators. These logics realize different views of time such as the linear or branching time view; for example Pnueli [1977] adapted Prior’s temporal logic with the linear time view to describe program properties following an idea of Burstall [1974]. This temporal logic uses the future fragment only and it contains the temporal operators “sometimes” , “always” and “next”. The time view is linear and semantically represented by natural numbers.