Logic for Computer Scientists/Modal Logic/Temporal Logics
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
![{\displaystyle [F]A}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7f69fcfc5dc6203b75fd0e5104a01db388e07c03)
![{\displaystyle [P]A}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0968f052ba0c5268ee3202e957d8a1a3207a73d7)
![{\displaystyle [A]A}](https://wikimedia.org/api/rest_v1/media/math/render/svg/da90a602fb669508c811d7a03a97d0242acbad1e)
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.
![{\displaystyle [F]A\to [F][F]A}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b71d876be3cf36859a4c61fa9092d93b49b3ec6e)
![{\displaystyle A\to [F]\langle P\rangle A}](https://wikimedia.org/api/rest_v1/media/math/render/svg/474758ba07a8eb514ad457309b987020141deafc)
![{\displaystyle [A]A\leftrightarrow [F]A\land [P]A}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1f6afa0df9f4cf5d74c4e9ffb8a8ca2bab05b9dd)
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.