risk = nil;

時相論理には，様々なタイプがある．時間を離散的と捉えるか・連続的と捉えるか．未来のみを扱うか・過去も扱うか．時間の分岐（可能な未来）をモデル化するか否か．

ここでは，要求に関連しそうな基本的なところのみを扱う．また，ここでは，時間軸上の順番のみを問題にする．3msecから 5msecの間といった時間を論理で扱うことは難しい．

ここでは，Manna氏とPnueli氏による教科書 ¹から．

いま，状態の列をσとし，その j 番目が式 φ を満足しているとき，次の様に記述することとする．

(σ, j) ⊧ φ.

「否定」演算子　¬

(σ,  j)  ⊧ ¬φ   iff   (σ,  j) ⊭ φ.

 j 番目が p でないということは，p であることが正しくない．”iff C” は「もし，C ならば，かつ C の時に限り」という意味である．いわゆる必要十分条件を示す．

「選言」演算子　 ∨ 

(σ, j)   ⊧   φ ∨ ψ   iff   (σ,  j) ⊧ φ or (σ, j) ⊧ ψ.

これも問題ないと思う．否定と選言から，∧（連言），→（含意），↔（同等）も導出できる．

「次」演算子　○

ここから，時相論理特有の記号の使い方である．

(σ, j) ⊧ ○ φ   iff   (σ, j+1) ⊧ φ.

p の次の状態を指す．簡単な例だと次になる．「悲しい」∧ ¬「金銭的に恵まれている」⇒　○「悲しい」

「⇒」の意味は，後に記述する．

簡単なようで，少し間違えやすい．もう少し複雑な例を考える．(x=0) ∧○(x=1)の真偽がどう変化するかを考えてみる．状態列の番号と x を混同しないように．

横軸が時間の進行を示している．xの値は，適当に与えている．○(x=1) は，x=1 の次の状態であるから，一つ先を見る．x = 1 の真偽を一つ先取りすることになる．

次回は，未来に関する演算子の残りである．

(nil)