「モデル検査入門」でググると上位に京大の数理研 2009 年の講義ノートと思われる PDF が見つかるので読んでみた．自分用のまとめなので他人の参考にならないかもしれない．詳しくは PDF 探して読んでください．

モデル検査入門

ここでは「モデル検査入門」の PDF を読んだ所感をかく．

第 1 章　モデル検査とは？

形式手法について簡単な記載．仕様書やプログラムで書いた内容に'バグがない'状態をつくりたい．その一つの方法として，

• 数学的に
• バグがないことを証明

することが考えられる．それを形式検証や形式手法という．

紙面では「仕様書やプログラムで書いた内容に」という記述はないけれどもおおよそそういう風に読んでいいと思う．これは形式手法について記載されたいろんなドキュメントから思ったこと．例えば，仕様を書くだけでもプログラマと設計者の意思疎通がうまくいくとかそういうことが考えられる．もっと言うと，仕様書からバグ（というか仕様の矛盾）を取り除ける（仕様書のデバッグ！）も考えられる．

「数学的に」，「バグがないことを証明」するというのが具体的に何を指しているかは次の分類に依存しそう．

手法は大きく分けて二つに分けられる：

• 定理証明：
  数学的な証明を書き下す（自動 or 手動）．定理証明器や証明支援器というものがある．B メソッドについて調べていると，どうも完全に全自動とは行かないらしい．（ここでいう証明とは DR や MP のこと？私にはまだわからない）

• モデル検査：
  システムを表す構造を定義し，その中である性質が成り立つかを検証する方法．具体的には，Kripke 構造 M の中で性質 \varphi が成り立つか（M\models\varphi が成り立つか）を調べる．しらみつぶしなので場合によっては現実的な時間内に終わらない．ここで，M は形式手法で記載する全体像，\varphi は検査したい性質を表していて，M\models\varphi であればうまく設計ができていると考えるんだと思われる．

モデル検査は「この先どういう状態になるか」とか「この先起こりうる状態で hoge は成り立つか」とかを調べる手法（らしい）なので，否定，論理和，論理積，含意以外の要素も含んだ文法とその意味論を展開する必要がある．

論理については第 2 章以降で扱われる．命題論理→様相理論 K → CTL* → CTL, LTL の順に展開される．

第 2 章　命題論理

論理式の構文論（syntax）と意味論（semantics）について．

構文はあくまで文字列の文法であって，true とか false は考えない．なので，(\varphi \land \psi)\land \xi と \varphi \land (\psi \land \xi) は別物．

意味論では，原子論理式から \{\top,\,\bot\} への写像を与えることで論理式全体の true, false を定めることができる．
含意については前提が偽なら全体も偽になる．数学を大学でやっていれば常識かもしれないが理由はいまいちよくわかっていなかった．これは別途調べたところ，前提が偽の場合に全体を真にしておかないと，「逆もまた真なり」の状況が起こってしまい，意図した体系にならないからだと思われる．

続きはまた今度．
（KaTeX で数式が赤になってしまう…．）