第 3 章 様相理論 K
様相理論は「今後どうなる」みたいな時相を取り扱うことになる．
そのために，K-論理式を定義して（論理演算子 \Box を追加する）おく．
状態遷移を取り扱うため，Kripke フレームというものを定義する．これは '状態' と '遷移可否' を表す構造で，遷移可否については二項関係で表される．簡単に言うと，同一頂点への有向枝を許す有効グラフである（Kripke フレーム）．さらに，各頂点である論理式が成り立つかどうかを定義する写像も合わせて，Kripke モデルという．遷移可能性については，計算過程と思うこともできる．
M,\,s \models \Box \varphi が「モデル M の中の状態 s の後の状態では，必ず \varphi が成り立つ」と定義されることからも，時相を念頭に置いた定義がされていることがわかる．
3.3 は後ろの議論に出てこなかったので読み飛ばした．気が向いたら（？）読みます．
第 4 章 システムの Kripke モデルによる表現
電子レンジの例．各ノードの '~hoge' は「hoge の状態にない」とか「hoge が偽」とかそういう意味だと思う．
図の左側の縦二つ（ドアが閉まってない状態で温めスタートし，エラーとなった状態）の状態で，ひたすらドアを開け閉めしてしまうという状態が含まれている．これはこの後の章への布石っぽい．
第 5 章 様相理論 LTL, CTL, CTL*
CTL*
パス（状態遷移の無限列）や各状態に対する構文と意味論が展開される．たとえば，E\varphi は「あるパスが存在して \varphi が成り立つ」という意味で，パスに関する論理式であり，X\varphi は「パス上の次の状態で \varphi が成り立つ」を表しているので，状態に関する論理式である．
状態論理式やパス論理式の定義に論理積 \wedge がない．これは \varphi \wedge \psi=\neg(\neg\varphi\vee\neg\psi) と思えばいいから？？と思うことにする．意味論のなかで証明が必要な気がするけど特に書いてなかった．ちなみに，別途ググった結果，CTL* においても \wedge を含んだ定義をしている PDF を見つけた．
CTL
定義は書いてある通り．
命題 5.8 の通り，状態論理式は独立して定義できて，パス論理式は状態論理式に E や A をつけたものと考えることもできるので，結局状態論理式がメインになる体系と思っていい．言い換えると，パス論理は状態に対する論理ということになる．「状態論理式とパス論理式の区別はあまり意味がない」というのはこういうこと？
そう考えておけば，CTL の遷移図が木構造になるのも納得できる．
LTL
これも定義は書いてる通り．
CTL とは逆に，パス論理式が独立に定義できて，状態論理は各パスについての論理ということになる．
線形というのはここからきているんだと思う．その証拠に，「あるパスで hoge」がなく，「全てのパスで hoge」としか言えない．言い換えると，パスの分岐を考えないので，一つのパスを表すだけだから「全てのパスで」だけ言えればいいということと思われる．
コメント