Open main menu

Wikibooks β

Logic for Computer Scientists/Modal Logic/Temporal Logics

< Logic for Computer Scientists‎ | Modal Logic

Temporal LogicsEdit

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.