今回は，過去を示す演算子である．引き続き教科書 1から例をとる．ただ，記号が特殊でテキストでは書きづらいので，記号は，KAOS教科書にあるものを使う．このあたりの記号の豊富さが，絵文字に仲間意識を感じるように，魅力的なところかもしれない．
「前(Previous)」演算子 ●
未来の○に対応する．
(σ, j) ⊧ ● p iff j>0 and (σ, j – 1) ⊧ p.
下記は「前」演算子の真理値である．ゼロから１に変化する場所を示す．「次」演算子も合わせて示している．なお，真になるためには，j>0の条件があるので，最初（j=0）では，無条件で偽になる．
| j | 0 | 1 | 2 | 3 | 4 | 5 | 6 |
| x | 1 | 1 | 0 | 0 | 1 | 1 | 0 |
| (x=1)∧●(x=0) | F | F | F | F | T | F | F |
| (x=0)∧○(x=1) | F | F | F | T | F | F | F |
「以前(Has-alwasy-been)」演算子 ■
(σ, j) ⊧ ■p iff (σ, k) ⊧ p for all k, 0 ≤ k ≤ j.
未来の□に対応する．「ずっと，pであった」ということを意味する．
以下に例を示す．
| j | 0 | 1 | 2 | 3 | 4 | 5 | 6 |
| x | 1 | 2 | 3 | 4 | 5 | 6 | 7 |
| ■ (x ≤ 3) | T | T | T | F | F | F | F |
時刻2までは，式が成立している．
「かつて(Once)」演算子 ◆
(σ, j) ⊧ ◆p iff (σ, k) ⊧ p for some k, 0 ≤ k ≤ j.
「pで真あったことがある」という意味である．
| j | 0 | 1 | 2 | 3 | 4 | 5 | 6 |
| x | 1 | 2 | 3 | 4 | 5 | 6 | 7 |
| ◆ (x = 4) | F | F | F | T | T | T | F |
「以来(Since)」S 演算子
(σ, j) ⊧ p S q iff 0 ≤ k ≤ j となる k があり，(σ, k) ⊧ q が成り立つ．かつ，k < i ≤ j で，全ての i において (σ, i) ⊧ p.
かつて q に出会った．それ以降は p であった．q p … p という列を考えている．
次は，(x ≤ 6) S (x = 3) の例である
| j | 0 | 1 | 2 | 3 | 4 | 5 | 6 |
| x | 1 | 2 | 3 | 4 | 5 | 6 | 7 |
| x ≤ 6 | T | T | T | T | T | T | F |
| x = 3 | F | F | T | F | F | F | F |
| (x ≤ 6) S (x = 3) | F | F | T | T | T | T | F |
「（よわい）以来(Back-to)」B 演算子
(σ, j) ⊧ p B q iff (σ, j) ⊧ p S q or (σ, j) ⊧ ■p.
基本的には，Sと同じである．ただ，q に出会わなくても良い．その場合は，p が続いていた．
ちょうど，U に対するWと同様の関係にある．
次の真理を考える．(x ≠ 4) B (x = 6)
| j | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 |
| x | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 |
| x ≠ 4 | T | T | T | F | T | T | T | T | T |
| x = 6 | F | F | F | F | F | T | F | F | F |
| (x ≠ 4) B (x = 6) | T | T | T | F | F | T | T | T | T |
前半の真の部分は，■ p による．後半は，p S q が機能している．
他にも過去の演算子はあるが，基本的なものは上記になる．
(nil)
Notes:
- Pnueli, Amir, and Zohar Manna. “The temporal logic of reactive and concurrent systems.” , 1992. ↩