# Logic for Computer Scientists/Modal Logic/Temporal Logics

## Temporal LogicsEdit

The two modalities ${\displaystyle \square }$  and ${\displaystyle \diamond }$  cannot be used to distinguish between past and future. For this we need a multi-modal logic with the following ${\displaystyle \square }$ -operators

• ${\displaystyle [F]A}$ : ${\displaystyle A}$  holds always in the future
• ${\displaystyle [P]A}$ : ${\displaystyle A}$  holds always in the past
• ${\displaystyle [A]A}$ : ${\displaystyle A}$  holds always

and the corresponding ${\displaystyle \diamond }$ -operators:

• ${\displaystyle \langle F\rangle A}$ : ${\displaystyle A}$  holds somewhere in the future
• ${\displaystyle \langle P\rangle A}$ : ${\displaystyle A}$  holds somewhere in the past
• ${\displaystyle \langle A\rangle A}$ : ${\displaystyle 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.

• ${\displaystyle [F]A\to [F][F]A}$ : Transitivity; an analog axiom holds for the two other ${\displaystyle \square }$ -operators.
• ${\displaystyle A\to [F]\langle P\rangle A}$ : if we go from a time point ${\displaystyle t}$  in the future ${\displaystyle t'}$ , we can go back in the past to the time point where ${\displaystyle A}$  was true.
• ${\displaystyle [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.