モデル検査（1）概要 - 知能ソフトウェア研究室

表現系工学特論
モデル検査（５）
CTLモデル検査アルゴリズム
１．CTL の復習
２．CTL モデル検査
３．その他のモデル検査アルゴリズム
参考文献
Model Checking, E.M. Clarke, Jr. et al, MIT Press (1999)
モデル検査の概要(復習)
モデル
（状態遷移系）
モデル記述言語
•C言語風のもの
•プロセス代数
モデル検査器
性質
（安全性，活性）
性質の記述
•時相論理(CTL, LTL)
•ω-オートマトン
検査結果
ＯＫ
反例
1. CTLの復習
状態遷移系 ⇒ クリプキ構造でモデル化
仕様（性質） ⇒ 時相論理で記述
時相論理には，CTLやLTLがある
クリプキ構造
M  (S , S0 , R, L)
AP  {start , close,
初期状態
heat , error}
start oven
open door
start
open door
error
close door
start close
error
close door
close
reset
start
open door
done
start oven
close
warmup
cook
close heat
start cooking
start close
heat
時相演算子と経路限量子
Xf
neXt time
パス上の次の状態で f が成り立つ．
Ff
Finally
パス上のある状態で f が成り立つ．
Gf
Globally
パス上のすべての状態 f が成り立つ．
f Ug
Until
パス上のある状態 g が成り立ち，かつ，
その直前までの全状態で f が成り立つ．
Ef
there Exists a path
この状態から始まるあるパスにおい
て f が成り立つ．
Af
for All paths
この状態から始まるすべてのパス
において f が成り立つ．
CTL式
 p  AP が原始命題ならば， p は CTL 式である．
 f , g が CTL 式ならば，
f , f  g , f  g , f  g
もそれぞれ CTL 式である．
 f , g が CTL 式ならば，
EXf , EFf , EGf , E( f Ug ), AXf , AFf , AGf , A( f Ug )
もそれぞれ CTL 式である．
CTL式の例
EF( start  ready )
start は真だが ready が偽である状態に至る経路が存在する．
ready
ready
start
start
２．ＣＴＬモデル検査
モデル検査の問題定義
アルゴリズムの基本設計
アルゴリズムの概要
例題
モデル検査の問題定義
有限状態並行システムを表現するクリプキ構造 M  (S , S0 , R, L)
およびその仕様（性質）を表現する時相論理式 f が与えられたとき，
f を満たすすべての状態の集合 s  S | s | f  を求めよ．
初期状態の集合 S0 がその集合に包含されるなら，システムはそ
の仕様を満たす．
アルゴリズムの基本設計(1/3)
CTL 式 f を構成するすべての部分式の集合を考え，各状態 s
に， s において真である部分式の集合 label ( s) をラベル付ける．
仕様
f  E(true U (q  EX(q)))
すべての部分式
の集合
q
q
EX(q)
q  EX(q)
E(true U (q  EX(q)))
p, q
s1
仕様
p, q
s2
label ( s2 )
q
q
EX(q)
q  EX(q)
U (q  EX(q)))
q
s4
E(true U (q  EX(q)))
label ( s1 )
E(true
p
s3
E(true
U (q  EX(q)))
label ( s3 )
label ( s4 )
q
q
EX(q)
アルゴリズムの基本設計(3/3)
手順は，論理式のネスト（入れ子）が少ない順に進む．すなわち，
ある論理式 g を処理する段階では， g のすべての部分式はすでに
処理済みであるものとする．
第 0 段階では， label ( s) はクリプキ構造で与えられた原始
命題のラベル L( s ) である．
第 i 段階では，第 i  1 重にネストされた部分式を処理して，
それを真とする各状態のラベルに追加する．
f 自体の処理が終わるとアルゴリズムが停止し，その時点で
s | f  f  label (s)
が成り立つ．
アルゴリズムの概要(1/13)
CTL 式は，  ，  ， EX, EG, EU だけを用いて表現できる．
f  g  (f  g )
f  g  f  g
AX f  EX(f )
AF f  EG(f )
EF f  E(true U f )
AG f  EF(f )
A( f U g )  E(g U (f  g ))  EG(g )
アルゴリズムの概要(2/13)
A( f U g )  E(g U (f  g ))  EG(g )
For all paths:
f , g
f , g
f , g
Never exists:
g
g
g
g
g
f , g
f , g
g
g
g
アルゴリズムの概要(3/13)
以下の６通りのみを扱えば十分．
 g  AP が原始命題のとき：
g  L( s) である全状態 s に対して， g を label ( s) に追加．
g
g
p, q
g
g
アルゴリズムの概要(4/13)
 g  f1 の形のとき：
f1  label (s) である全状態 s に対して，
g を label ( s) に追加．
p, q
f1
f1
f1
アルゴリズムの概要(5/13)
 g  f1  f 2 のとき：
f1  label (s) または f2  label (s) である全状態 s に対して，
g を label ( s) に追加．
p, q
f1
f1  f 2
f2
f1  f 2
アルゴリズムの概要(6/13)
 g  EX f1 のとき：
f1  label (t ) を満たす直後の状態 t が存在するような
全状態 s に対して， g を label ( s) に追加．
p, q
EX f1
f1
アルゴリズムの概要(7/13)
 g  E( f1 U f 2 ) のとき：
f 2 でラベル付けられた全状態を求め，その各状態から状態遷
移を逆にさかのぼりながら， f1 でラベル付けられた状態からなる
パスによって到達可能な状態 s を見つける．そのようなすべての
状態 s に対して， g を label ( s) に追加．
p, q
f1
f1
f2
E( f1 U f 2 )
E( f1 U f 2 )
E( f1 U f 2 )
procedure CheckEU( f1 , f 2 )
T : s | f 2  label ( s )  ;
for all s  T do label ( s ) : label ( s )  E( f1 U f 2 ) ;
while T   do
choose s  T ; T : T \ s ;
for all t such that R (t , s ) do
if E( f1 U f 2 )  label (t ) and f1  label (t ) then
label (t ) : label (t )  E( f1 U f 2 ) ;
T : T  t ;
end if;
end for all;
end while;
end procedure
t
t
s
s
p, q
f1
f1
f2
E( f1 U f 2 )
E( f1 U f 2 )
E( f1 U f 2 )
アルゴリズムの概要(9/13)
 g  EG f1 のとき：
(1) f1 を満たさない全状態（およびそれに付随する状態遷移）
を M から削除したクリプキ構造を M   ( S , S0 , R, L) とする．
M’
p, q
f1
f1
f2
アルゴリズムの概要(10/13)
Strongly
Connected
Component
 g  EG f1 のとき：
(2) 有向グラフ ( S , R) を強連結成分(SCC)に分解する．
M’
SCC
Trivial
SCC
SCC
アルゴリズムの概要(11/13)
 g  EG f1 のとき：
(3) 自明でない(nontrivial)ＳＣＣ内の状態から， R  の状態遷
移を逆にさかのぼりながら， f1 でラベル付けられた状態か
らなるパスによって到達可能な状態 s を見つける．
そのようなすべての状態 s に対して， g を label ( s) に追加．
M’
SCC
p, q
f1
f1
f1
f1
EG f1
EG f1
EG f1
EG f1
procedure CheckEG( f1 )
S  : s | f1  label ( s)  ;
SCC : C | C is a nontrivial SCC of S  ;
T :
CSCC
s | s  C;
for all s  T do label ( s ) : label ( s)  EG f1 ;
while T   do
choose s  T ; T : T \ s ;
for all t such that t  S  and R(t , s ) do
if EG f1  label (t ) then
label (t ) : label (t )  EG f1 ;
SCC
t
T : T  t ;
p, q
end if;
end for all;
end while;
end procedure
s
f1
f1
f1
EG f1
EG f1
EG f1
アルゴリズムの概要(13/13)計算量
 CheckEUとCheckEGは，O(|S|+|R|).
 全体で， O(|f|・(|S|+|R|)).
例題 E(true U (q  EX(q)))
p, q
s1
p, q
label ( s1 )
label ( s2 )
q
s2
U (q  EX(q)))
q
s4
label ( s3 )
label ( s4 )
q
q
q
EX(q)
EX(q)
q  EX(q)
E(true
p
s3
E(true
U (q  EX(q)))
３．その他のモデル検査アルゴリズム(1/2)
グラフ理論に基づくLTLモデル検査アルゴリズム
複雑かつNP-困難
記号モデル検査
状態遷移関係をグラフではなく命題論理式で表現し，
BDD（二分決定木）で実装して状態数を削減する．
３．その他のモデル検査アルゴリズム(2/2)
ω-オートマトンで仕様を記述
ω-オートマトンはモデルが想定された動作をするか
どうか監視する．
LTL式の仕様の否定をω-オートマトンに自動変換
することができる．
半順序簡約(partial order reduction)
２つ以上のプロセスのインタリーブを，仕様に応じて
制限し，探索空間を削減する．
演習問題
例題で用いた状態遷移系において，仕様
E (q U (p))
を満たす状態の集合を，CTL モデル検査アルゴリズムによって
求めよ．

Download Report