Logic for Computer Scientists/Modal Logic/Temporal Logics

Temporal Logics

The two modalities $◻$ and $\diamond$ cannot be used to distinguish between past and future. For this we need a multi-modal logic with the following $◻$-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:

• $⟨F⟩A$: $A$ holds somewhere in the future
• $⟨P⟩A$: $A$ holds somewhere in the past
• $⟨A⟩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 $◻$-operators.
• $A\to [F]⟨P⟩A$: if we go from a time point $t$ in the future $t^{\prime }$, we can go back in the past to the time point where $A$ was true.
• $[A]A\leftrightarrow [F]A\wedge [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.