Logic for Computer Scientists/Modal Logic/Temporal Logics

From Wikibooks, open books for an open world
< Logic for Computer Scientists‎ | Modal Logic
Jump to: navigation, search

Temporal Logics[edit]

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.