モデル検査入門の PDF を読んだまとめ 3（完結）

モデル検査入門の PDF を読んだまとめ 2の続きです．

第 6 章　CTL モデル検査

モデル検査を実施するためには，

• 検証したいシステムを Kripke モデル M として表現し，
• 検証したい性質を状態論理式 \varphi で表し（\mathbf{AG}(\mathrm{hoge} \rightarrow \mathbf{AF}\mathrm{fuga})みたいな感じ），
• 状態の集合 \{s\mid M,\, s\models \varphi\} を求め，初期状態がこれに含まれるかを調べる

という手順を踏む．

これを求めるためのアルゴリズムが記載されている．ここでは補題 6.7 についてだけ備忘録を書いておく．

状態 s からスタートして，式 \mathsf{EG}\psi が成り立つかどうかを調べるには，

1. s において \psi が成り立つこと
2. \psi が真となる部分グラフが強連結成分 C を持っていて，かつ s から C へ至るパスが存在すること

が成り立つかどうかを調べればよい（必要十分）．

この二つ目は，「s からスタートして，\psi が成り立つ強連結成分にトラップされ得る」ことを表している．
なので，強連結成分を求めるアルゴリズムが使える（グラフ理論）！

第 7 章　公平性（fairness）

公平性とは，特定の状態ばかりが起こる状態を良しとせず，いくつか状態（の部分集合）の集合 \mathsf{FC}\subseteq 2^S を選んで，FC のどの状況にも無限回現れることを要請して特定の状況への偏りをなくすことを目的としているように思う．

注意 7.1 の状態を左から順に a,\,s,\,b とすれば，\mathsf{FC}=\{\{a\},\,\{b\}\} と選びたい…はず．
例 4.2 では，正常に操作している状態，つまり start かつ close かつ not error である状態を FC に入れておけばよい．
ちなみに，例 7.8 は \mathsf{FC}=\{\{ s\mid s\models \mathsf{Start}\wedge \mathsf{Close} \wedge \neg \mathsf{Error}\}\} のこと？

とりあえず，読んでみた感想をまとめてみました．誤った解釈をしている可能性があるのでご指摘いただければ～～～．