モデル検査（５） CTLモデル検査アルゴリズム

Presentation on theme: "モデル検査（５） CTLモデル検査アルゴリズム"— Presentation transcript:

1 モデル検査（５） CTLモデル検査アルゴリズム
表現系工学特論 モデル検査（５） CTLモデル検査アルゴリズム １．CTL の復習 ２．CTL モデル検査 ３．その他のモデル検査アルゴリズム 参考文献 Model Checking, E.M. Clarke, Jr. et al, MIT Press (1999)

2 モデル検査の概要(復習) モデル検査器 検査結果 モデル （状態遷移系） ＯＫ 反例 性質 モデル記述言語 （安全性，活性） C言語風のもの
モデル検査の概要(復習)　　 モデル検査器 モデル （状態遷移系） 検査結果 ＯＫ 反例 性質 （安全性，活性） モデル記述言語 C言語風のもの プロセス代数 性質の記述 時相論理(CTL, LTL) ω-オートマトン

3 1. CTLの復習 状態遷移系　⇒　クリプキ構造でモデル化 仕様（性質）　⇒　時相論理で記述 時相論理には，CTLやLTLがある

4 クリプキ構造 初期状態 start oven open door cook open door close door done
reset start oven start cooking warmup

5 時相演算子と経路限量子

6 CTL式

7 CTL式の例 ready start ready start

8 モデル検査の問題定義 アルゴリズムの基本設計 アルゴリズムの概要 例題
２．ＣＴＬモデル検査 モデル検査の問題定義 アルゴリズムの基本設計 アルゴリズムの概要 例題

9 モデル検査の問題定義

10 アルゴリズムの基本設計(1/3) 仕様 すべての部分式の集合

11 仕様

12 アルゴリズムの基本設計(3/3)

13 アルゴリズムの概要(1/13)

14 アルゴリズムの概要(2/13) For all paths: Never exists:

15 アルゴリズムの概要(3/13) 以下の６通りのみを扱えば十分．

16 アルゴリズムの概要(4/13)

17 アルゴリズムの概要(5/13)

18 アルゴリズムの概要(6/13)

19 アルゴリズムの概要(7/13)

20 t s t s

21 アルゴリズムの概要(9/13) M’

22 Strongly Connected Component
アルゴリズムの概要(10/13) Strongly Connected Component M’ SCC SCC Trivial SCC SCC

23 アルゴリズムの概要(11/13) M’ SCC

24 SCC t s

25 アルゴリズムの概要(13/13)計算量 CheckEUとCheckEGは，O(|S|+|R|).
全体で， O(|f|・(|S|+|R|)).

26 例題

27 ３．その他のモデル検査アルゴリズム(1/2) グラフ理論に基づくLTLモデル検査アルゴリズム 複雑かつNP-困難 記号モデル検査
　　状態遷移関係をグラフではなく命題論理式で表現し， 　　BDD（二分決定木）で実装して状態数を削減する．

28 ３．その他のモデル検査アルゴリズム(2/2) ω-オートマトンで仕様を記述
　　ω-オートマトンはモデルが想定された動作をするか 　　どうか監視する． 　　LTL式の仕様の否定をω-オートマトンに自動変換 　　することができる． 半順序簡約(partial order reduction) 　　２つ以上のプロセスのインタリーブを，仕様に応じて 　　制限し，探索空間を削減する．

29 演習問題