Kripkeモデル
W: 有限集合
元が可能世界(possible world)
R: W上の
2項関係
到達可能関係(accessibility relation)
からなるK=(W, R)を
Kripke構造
という
直感的には
有向グラフ
Kripke構造に真偽の概念を追加するとKripkeモデルになる:
Kripke構造 (W, R)
IはWの部分集合(初期状態の集合と思えば良い)
AP:
原子論理式
の集合
V: WとAPの直積から
$ \top, \bot
への関数
システムが指定した状態にあるときの原子論理式の真偽を返す関数
valuation
#モデル検査