4日で学ぶ モデル検査

ずいぶん前に購入していたのですが、忙しくて感想を書けていませんでした。

結論としましては、ツールとしてのモデル検査に興味がある方には実践的かな、と。

モデル検査の代表的なツールである NuSMV と SPIN の両者で、さまざまな演習課題を解いてみる、というスタイルで何題も続く感じの構成になっています。実際のセミナー教材を元に作られた本だけあって、確かに偽り無く4日でやっていけそうな分量ですね。

モデル検査って言葉だけ聞くけど、実際にツールとしてどんな風に使うのよ？という疑問には答えられそうです。LTL の簡単な説明もありますので、演習用の例題を解くには困らないでしょう。

ただ、実際にモデル検査の理論やアルゴリズムなどを知りたい方には向かない本かもしれません。そして、僕にとって一番残念だったのは LTL しか対応していなかったということ。AG EF が書けない LTL には（僕の使いたい応用では）用はございません！

やはり、CTL を素で使ってしまうと、fairness (常に無限回成立すること) が表現できないのが、よくある応用にとって致命的なのでしょうね……。マルチプロセスの系で延々と片方のプロセスだけ動き続けるといったことがなく、両方のプロセスが常に無限回実行され続けることを保証するためなどに用いられる概念です。ただ、CTL に fairness を導入するという話はいろいろありますし、回避可能な弱点ではないかと考えてます。

個人的には branching time logic の方が好きなんですよね。ハマり状態の表現に AG EF という様相演算子が必須だという理由も大きいんですが、そもそも非決定性の根源がユーザからの入力であるような状態遷移系の検証において検証したい事柄は branching time のほうが似合っている気がします。無限に状態が遷移していって、その中で fairness を議論しつつ性質を検証する、なんて話なら linear time のほうがあっているのでしょうけど。

なにはともあれ、次は CTL も扱った日本語のモデル検査の本が出ることを期待しつつ。