"Sometimes" and "Not Never" Revisited: On Branching Versus Linear Time

Abstract

Temporal logic ([PR57], [PR67]) provides a formalism for describing the occurrence of events in time which is suitable for reasoning about concurrent programs (cf. [PN77]). In defining temporal logic, there are two possible views regarding the underlying nature of time. One is that time is linear: at each moment there is only one possible future. The other is that time has a branching, tree-like nature: at each moment, time may split into alternate courses representing different possible futures. Depending upon which view is chosen, we classify (cf. [RU71]) a system of temporal logic as either a linear time logic in which the semantics of the time structure is linear, or a system of branching time logic based on the semantics corresponding to a branching time structure. The modalities of a temporal logic system usually reflect the semantics regarding the nature of time. Thus,in a logic of linear time, temporal operators are provided for describing events along a single time path (cf. [GPSS80]). In contract, in a logic of branching time the operators reflect the branching nature of time by allowing quantification over possible futures cf. [AB80],[EC80]).