Last modified on 13 July 2009, at 14:10

Logic for Computer Scientists/Modal Logic/Temporal Logics

Temporal LogicsEdit

The two modalities \square and \diamond cannot be used to distinguish between past and future. For this we need a multi-modal logic with the following \square-operators

  •  [F] A :  A holds always in the future
  •  [P]A:  A holds always in the past
  •  [A]A:  A holds always

and the corresponding \diamond-operators:

  •  \langle F\rangle A :  A holds somewhere in the future
  •  \langle P\rangle A :  A holds somewhere in the past
  •  \langle A\rangle A :  A holds somewhere


The semantics is then given as before, by giving constraints for the three reachability relations or by giving appropriate axioms, e.g.

  • [F] A \to  [F][F]A: Transitivity; an analog axiom holds for the two other \square-operators.
  • A \to [F] \langle P\rangle A: if we go from a time point t in the future t', we can go back in the past to the time point where A was true.
  • [A] A \leftrightarrow [F]A \land[P] A : connection of past with future.

In addition there are many other aspects of temporal logics. E.g. one can distinguish between left- and rightlinear structures or between dense and discrete time structures.