Logic for Computer Scientists/Modal Logic/Temporal Logics

From Wikibooks, open books for an open world
Jump to navigation Jump to search

Temporal Logics[edit | edit source]

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

  • : holds always in the future
  • : holds always in the past
  • : holds always

and the corresponding -operators:

  • : holds somewhere in the future
  • : holds somewhere in the past
  • : holds somewhere

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

  • : Transitivity; an analog axiom holds for the two other -operators.
  • : if we go from a time point in the future , we can go back in the past to the time point where was true.
  • : 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.