Basic temporal logic

The reading of the operator $\Box$ as ``always in the future'' (and accordingly, $\diamond$ 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 K$_t$4, with the subscript $t$ 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].