risk = nil;

ここでは，原書にある例を幾つか見る．

要求1

列車のドアは，プラットフォーム（駅）間では，閉まっていなければならない．但し，緊急事態のためにプラットフォーム間で停止している間は除く．

対応する様相論理記述

∀tr: Train, pl: Platform

（●At(tr, pl) ∧ ¬At(tr, pl) ⇒ tr.Doors = ‘closed’ W [At(tr, next(pl))  ∨  Alarm  (tr)  ∧ ¬Moving(tr)]）

「一つ前ではプラットフォームにいるが，いまはいない」というのが条件部分である．このとき，列車のドアは，「閉まっている．それは，列車が次の駅に到着するか，停止してアラームがあるときまで続く」というのが，この文の解釈である．

最初の束縛変数の定義部分（∀tr: Train, pl: Platform）は，これまで説明していない．集合の要素と捉えてもよいし，なじみの抽象データ型とインスタンスというとらえ方でも良い．いずれ説明したい．trというのはある列車を，plはあるプラットフォーム（駅）を示している．いま全称限量子で束縛しているので，一つ前に駅にいて，いまはその駅にいない列車という条件になっている．ある列車を考えたときに，全ての駅に同時に存在することはできないので，「前に」ある駅にいた列車がいまはいないという制約が，●At(tr,pl)の部分である．●で十分かは，議論があるだろうが，何らかの制約は必要になる．

要求2

列車は，次のプラットフォームに5分以内に到着しなくてはならない．

対応する様相論理記述

∀tr: Train, pl:Platform (At(tr, pl) ⇒ ◇_≤5m At(tr, next(pl))

◇_≤5mという記述法は，始めて出てきている．◇は，いつか生じるということである．いつかというのは，あまりにも漠としているので，制約を加えている．時間（間隔）制約を書くときには，比較的よく見る記法となる．論理的な取扱に関して，実践的な方法はすくない ¹．ここでは，あくまで要求としてどう表現するかというレベルで考える．

次回も引き続き原書の例について考える．

(nil)