The reading of the operator as ``always in the future'' (and
accordingly,
as ``sometimes in the future'') has proved
plausible for many modal logics. Those systems are the most simple
temporal (or tense) logics. Semantically, the ``possible worlds'' of a
Kripke model are interpreted as moments in time, and the accessibility
relation is viewed as the the relation ``later than''.
Clearly, not all algebraic properties that can be imposed on binary
relations are meaningful under a temporal interpretation. The most
interesting properties are those characterizing ordering
relations. Transitivity is probably the most basic condition that can
be placed on the relation ``later than'', so it is typically assumed
that temporal structures are transitive. Accordingly, the minimal
temporal logic is axiomatized by adding to system K the axiom
(4), which corresponds to transitivity. That system is
denoted K4, with the subscript
indicating that a
temporal logic is being considered.
More complex logics of time are usually developed on the basis of richer languages. Typically, some past operators are also considered. Different, often incompatible models of time can be developed by adopting appropriate axioms. For example, time can be assumed to be linear or branching, discrete or dense, limited or unlimited. For more complete overviews consult [Bur84], [Eme90].