計算機科學家邏輯/模態邏輯/時態邏輯
兩個模態和無法用於區分過去和未來。為此，我們需要一個具有以下運算子的多模態邏輯
- : 始終在未來成立
- : 始終在過去成立
- : 始終成立
![{\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)
以及相應的運算子
- : 在未來某個地方成立
- : 在過去某個地方成立
- : 在某個地方成立
然後語義像以前一樣給出，透過給出三個可達性關係的約束，或者透過給出適當的公理，例如
- : 傳遞性；一個類似的公理對另外兩個運算子成立。
- : 如果我們從未來 的時間點 開始，我們可以回到過去，回到 為真的時間點。
- : 過去與未來的連線。
![{\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)
此外，時態邏輯還有許多其他方面。例如，可以區分左線性和右線性結構，或區分密集時間結構和離散時間結構。