モデル検査（５） CTLモデル検査アルゴリズム 表現系工学特論 モデル検査（５） CTLモデル検査アルゴリズム １．CTL の復習 ２．CTL モデル検査 ３．その他のモデル検査アルゴリズム 参考文献 Model Checking, E.M. Clarke, Jr. et al, MIT Press (1999)
モデル検査の概要(復習) モデル検査器 検査結果 モデル （状態遷移系） ＯＫ 反例 性質 モデル記述言語 （安全性，活性） C言語風のもの モデル検査の概要(復習) モデル検査器 モデル （状態遷移系） 検査結果 ＯＫ 反例 性質 （安全性，活性） モデル記述言語 C言語風のもの プロセス代数 性質の記述 時相論理(CTL, LTL) ω-オートマトン
1. CTLの復習 状態遷移系 ⇒ クリプキ構造でモデル化 仕様（性質） ⇒ 時相論理で記述 時相論理には，CTLやLTLがある
クリプキ構造 初期状態 start oven open door cook open door close door done reset start oven start cooking warmup
時相演算子と経路限量子
CTL式
CTL式の例 ready start ready start
モデル検査の問題定義 アルゴリズムの基本設計 アルゴリズムの概要 例題 ２．ＣＴＬモデル検査 モデル検査の問題定義 アルゴリズムの基本設計 アルゴリズムの概要 例題
モデル検査の問題定義
アルゴリズムの基本設計(1/3) 仕様 すべての部分式の集合
仕様
アルゴリズムの基本設計(3/3)
アルゴリズムの概要(1/13)
アルゴリズムの概要(2/13) For all paths: Never exists:
アルゴリズムの概要(3/13) 以下の６通りのみを扱えば十分．
アルゴリズムの概要(4/13)
アルゴリズムの概要(5/13)
アルゴリズムの概要(6/13)
アルゴリズムの概要(7/13)
t s t s
アルゴリズムの概要(9/13) M’
Strongly Connected Component アルゴリズムの概要(10/13) Strongly Connected Component M’ SCC SCC Trivial SCC SCC
アルゴリズムの概要(11/13) M’ SCC
SCC t s
アルゴリズムの概要(13/13)計算量 CheckEUとCheckEGは，O(|S|+|R|). 全体で， O(|f|・(|S|+|R|)).
例題
３．その他のモデル検査アルゴリズム(1/2) グラフ理論に基づくLTLモデル検査アルゴリズム 複雑かつNP-困難 記号モデル検査 状態遷移関係をグラフではなく命題論理式で表現し， BDD（二分決定木）で実装して状態数を削減する．
３．その他のモデル検査アルゴリズム(2/2) ω-オートマトンで仕様を記述 ω-オートマトンはモデルが想定された動作をするか どうか監視する． LTL式の仕様の否定をω-オートマトンに自動変換 することができる． 半順序簡約(partial order reduction) ２つ以上のプロセスのインタリーブを，仕様に応じて 制限し，探索空間を削減する．
演習問題