Logic for Computer Scientists/Modal Logic/Temporal Logics

Temporal Logics

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.

Last modified on 13 July 2009, at 14:10

Logic for Computer Scientists/Modal Logic/Temporal Logics

Temporal Logics

Wikibooks ™