数理解析研究所講究録
第 1744 巻 2011 年 25-34

25

2010 年度冬の LA シンポジウム [4]確率時間 WiGAR による PTCTL サブクラスのモデル検査
高橋

1

導入

1.1

研究背景

正樹 *

清水

近年，情報化社会が進むにつれてシステムの重要性が高くなってきており，誤作動を起こした場合に多大な影響を及ぼすシステムが存在する．その中には通信プロトコルのように確率的リアルタイム動作をする組込みシステムも存在する．そのため確率リ
アルタイムシステムに対しても網羅的な検証が可能である形式的手法による検証手法の確立が求められている．確率リアルタイムシステムのモデル化には
確率時間オートマトン [8] を用いるのが一般的である．しかし実際のシステムを単純に適用しただけでは状態数が膨大になり計算不可能となる状態爆発という問題が生じる．そのため状態爆発を解決した形
式的検証手法の確立が求められている

12

隆也 \dag er

山根

智 \d ag er

証項目全てに対して検証が可能である．しかし，この手法においても検証に必要なモデルの状態数が大きくなってしまう場合が存在する．一方，確率時間
CEGAR の手法は反例を用いて抽象モデルに対して精錬を繰り返すことで検証に必要なモデルの状態数を削減することができる CEGAR の枠組みを確率リ

アルタイムシステムに対しも利用できるように拡張した研究である．そのため少ない状態数で確率リア
ルタイムシステムを検証できる．しかし，確率時間
CEGAR の手法では PTCTL 式で表現できる検証項
目の一部である単純な確率到達可能性問題しか検証を行えないという欠点が存在する．

13

提案手法

本研究では上記で述べた関連研究の特徴から CEGAR の枠組みを拡張することで PTCTL 式で表現できる検証項目の全てではないが確率到達性問題

関連研究

以上の検証項目を検証することができる確率時間

確率リアルタイムシステムに対する形式的検証手法 WiGAR(Witness Guided Abstraction Refinement)の手法を提案する．具体的には 4 章において述べるの研究としては Symbolic model checking[8] が存在の枠組みを PTCTL の検証に適する．また CEGAR(Counter Example Guided Ab- が，単純に CEGAR
用した場合，「抽象モデルが PTCTL 式を満たすな
straction Refinement) の枠組みを用いたリアルタイ
らば必ず具体モデルも PTCTL 式を満たす」というムシステムに対する CTL のモデル検査 [11] の流れによる検証に必要となる抽象モデルを構築
CEGAR
を受け継いだ研究として確率 CEGAR による確率
できないという問題が発生する．そこで本研究では，システムの確率到達性問題の検証 [5], 確率時間 CE「抽象モデルが PTCTL 式を満たさないならば必ず
GAR による確率リアルタイムシステムに対する確体モデルも PTCTL 式を満たさない」 という性質
率到達性問題の検証 [12] が挙げられる．Symbolic:を持つ抽象モデルを構築し，さらに反例ではなく実model checking では PTCTL(Probabilistic Timedを用いることでことでその問題を解決している．
Computation Tkee Logic) 式 [8] であらわされる検以下では，2 章において確率リアルタイムシステム$=\Xi$$lF|\rfloor$

金沢大学大学院自然科学研究科
第 1 著者に同じ\ddagger 金沢大学$*$$\dagger$を表現するモデルである確率時間オートマトン，その意味である確率時間システム，そして検証項目を

26
表現する PTCTL の定義を行う．3 章では確率時間
オートマトンの意味である確率時間システムの抽象モデルを定義し，その構築方法について述べる．4 章
では，確率時間 WiGAR の流れについて説明する．5
章では実際に確率時間 WiGAR を用いて実験を行い

既存手法と比較することで，その有効性を示す．最後に 6 章ではまとめと今後の課題について述べる．

具体モデルと PTCTL

2

確率リアルタイムシステムのモデルとして確率時
間オートマトン [6] を定義する．

図 1: 確率時間オートマトン

定義 2.1(確率時間オートマトン) 確率時間オート$C,$ $Inv$ , probで定義さマトンは以下の組 $(L,$
$G$

.
.

$l_{0},$

確率分布 $p\in$ Dist $(2^{C}\cross L)$ の組である．確率分布

$)$

れる．

.
.
.

: $2^{C}\cross Larrow(0,1]$ は，リセットするクロック変数の集合 $X\in 2^{C}$ と，遷移先ロケーション $l’\in L$ から$p$

ロケーションの有限集合$L$

遷移確率 $p(X, l’)\in(O, 1]$ を与える写像である．
初期ロケーション $l_{0}\in L$

状態 $(l, \nu)$ からの離散遷移を考える．遷移関係が, リセットするクロックの集合が $X$ , 遷移先$(l, \zeta_{g},p)$

クロック変数の有限集合 $C$

ロケーションがロケーションに不変条件を割り付ける関数 $Inv$ :であったとき，離散遷移先の状態.

以下の二つを満たすとき離散遷移可能である．

確率遷移関係の有限集合 $prob\subseteq L\cross Zones(C)\cross$

Dist

$l’$

は $(l’, \nu[X:=0])$ となる．

$Larrow Zones(C)$.

$(2^{C}\cross L)$

口$G$$G_{1}$の状態 はロケーションとクロック評価の対 $(l, \nu)$$s$で表現される． の動作は，初期ロケーション$G$$l_{0}$と全てのクロック変数の値が であるクロック評価の対である初期状態
から開始する．
から状態間を時間遷移か離散遷移を行うことによって動作する．
状態 $(l, \nu)$
時間遷移は同一ロケーション内で行から時間遷移する場合は，確率 1 で状態$0$

遷移元状態のクロック評価が遷移条件を満たしている．

遷移先状態のクロック評価が遷移先ロケーショ

ンの不変条件を満たしている．

つまり．

$\nu\triangleright\zeta_{g}$かつ $\nu[X:=0]\triangleright Inv(l’)$ でなければならない．

$\nu_{0}$$(l_{0}, \nu_{0})$$(l_{0}, \nu_{0})$$A\searrow$

確率時間オートマトンの動作例を，図 1 のモデルを例にとり説明する．

$ffl\rfloor 2.1$$|$

$x,$ $y$

$C$

$\in$

はクロック 変数であはロケーション
り，start, sent, nsent, error
で sentである．図 1 における start から確率$(l, \nu+t)$ になる．ただしロケーションの不変条件にを満たさなければならない． に，確率 0.2 で unsent に離散遷移する確率分布
より，は,unsent から確率 0.9 で sent に，確率 0.1 で離散遷移は確率遷移関係 $(l, \zeta_{g},p)\in prob$ を用いて をとする．
ロケーション間で行う遷移である．確率遷移関係は， unsent 離散遷移する確率分布を$t\in \mathbb{R}^{>0}$

$u$

$\in$

$L$

$\theta.8$$t$$\nu+t\triangleright Inv(l)$$\mu 0$.

遷移元ロケーション $l\in L$ 遷移条件$\zeta_{g}\in$Zones $(C)$ ,.

$\}_{\llcorner}^{-}$$\mu_{1}$初期状態 start, $x=0\wedge y=0)$
$($

27

.

.

2 単位時間の時間経過 start, $x=2\wedge y=2)$ こ
こでは不変条件 $x<3$ より 3 単位時間以上時間

時間遷移における経過時間を単位時$G$ における確率遷移関係を $(l, \zeta_{g)}p)\in prob$ と間，経過できない．

$(l, \nu)\in S$ から $(l’, \nu’)\in S$ への遷移関係
して，

$($

.

$((l, \nu), t, \mu)\in Steps$

離散遷移関係 (start, $x>1,$ ) により確率 0.2の離散遷移 unsent, $x=0\wedge y=2)$ (リセット$\mu_{0}$$($$[\{x\}:=0]$ によりクロック $x$ のみ $0$ にリセット.
$\circ$$\in \mathbb{R}^{>0}$

$t$

$t$

を以下のように定義する．

単位時間の時間遷移$(l, \nu)arrow(l’, \nu’)t,\mu\perp(\emptyset,(l’,\nu’))$

される)

ただし，

1 単位時間の時間経過 unsent, $x=1\wedge y=3)$$($

離散遷移関係 (unsent, true, ) により確率 $0.9$の離散遷移 sent, $x=1\wedge y=3)$$\mu\perp(\emptyset, (l’, \nu’))=\{\begin{array}{l}1if l’=l\wedge\nu’=\nu+t\wedge\nu’\triangleright Inv(l)\wedge t>00 otherwise\end{array}$$\mu_{1}$$($以上のように時間遷移，離散遷移を繰り返すことに.

よりシステムは動作する．

2.1$(l, \zeta_{g}, p)$による離散遷移$(l, \nu)arrow(l’, \nu’)0,\mu(X,(l’,\nu’))$

意味論

ただし，

確率時間オートマトン $G$ の意味を時間確率システム$\mathcal{M}[6]$とし，抽象化における具体モデルとして利用

する．時間確率システムはマルコフ決定過程の形をとる．さらに与えられたパスの充足条件を満たすパスの合計確率である充足確率を定義するため，時間
確率システムの非決定を解決するアドバサリを導入
し，離散時間マルコフ連鎖の形に変換する．

$\mu(X, (l’, \nu’))=\{\begin{array}{ll}p(X, l’) if \nu\triangleright\zeta_{g}\wedge\nu’=\nu[X:=0]0 otherwise\end{array}$

口上の状態遷移関係の確率 $\mu(X, (l’, \nu’))$ による遷
移は，クロック変数 $X$ をリセットして状態 $(l’, \nu’)$ へ$G$ 上の確率到達する遷移である．離散遷移ついて，$\mu(X,(l’, \nu’))$ が
$p(X,
l’)$
には
分布
上の確率分布$\mathcal{M}$

定義 22(時間確率システム) 確率時間オートマト
ン $G=$ $(L,$ $C,$ $Inv$ , prob,の意味となる時間確率シ
応しているため，これらの確率は等しい．
ステムを組 ( , Steps, ) とする．
$\mathcal{M}$$\mathcal{L})$

.
.

$S$

$\mathcal{M}c$$7?\backslash$$\mathcal{L}’$$\cdot$$\mathcal{M}$

状態集合$\omega$は以下のような$\mathcal{M}$の状態 $s\in S$

から始まる以下のような非空の有限または無限列で$S\subseteq L\cross \mathcal{V}_{C}$

状態遷移関係上のパス$Steps\subseteq S\cross \mathbb{R}^{>0}\cross$Dist$(2^{C}\cross S)$

ある．
$\omega=sarrow s’arrow s’’arrow t,\mu(X,s’)t’,\mu’(X’,s’’)t’’,\mu’’(X’’,s’’’)\ldots$$\circ$

ラベリング関数任意の $(l, \nu)\in S$ に対して
4$\mathcal{L}’(l, \nu)=\mathcal{L}(l)$パスが有限長である場合，$\omega fin$

状態集合 $S$ に含まれる状態 $(l, \nu)\in S$ は$\nu\triangleright Inv(l)$を満たしていなければならない．

る．状態遷移関係における確率分布を$S)$$\mu\in$Dist$(\omega fin)$る．無限長である場合，と表記しする．また状態とし，特に時間遷移における確率分布を

1$s$$\mu\perp$と(Pathfin $(s)$ ) とする．また，$\Sigma_{s\in S}Path_{fu\downarrow}(s)$.であるすべての無限長のパスの集合を
$1$

する．

を最後の状態とすから始まる全ての無限長 (有限長) のパスの集合を$Path_{ful}(s)$$(2^{C}\cross$$|\omega fin|$

を長さ (遷移の回数) , last$\omega_{ful}$

状態遷移関係 Steps は時間遷移と離散遷移からなと表記し，その-ロ様に$\Sigma_{s\in S}Path_{\int ul}(s)$$Path_{ful}$とし，であるすべての有限長のパスの集合を $Pathfin$ と記述する．

28
次に，時間確率システムの非決定的選択を解決さ$s\models^{\text{ョ}}p_{>\lambda}[\phi_{1}\mathcal{U}\phi_{2}]$$P_{S}^{A}(\phi_{1}\mathcal{U}\phi_{2})>\lambda$$\Leftrightarrow$である$A\in Adv$ が存在する．
せるものとして，アドバサリを導入する．

定義 2.3 (時間確率システムのアドバサリ)
アドバサリ

は，有限長のパス$A$$\mathcal{M}$

ここで

の

から，パ

Path $fut(s)|\omega$
$A$

$A$

$P^{A}$ $(\phi_{1}\mathcal{U}\phi_{2})=Prob_{s}\{\omega$

$\in$

$s$

$\models$}
スの最後の状態を遷移元とする状態遷移関係$\omega\in Path_{ful}$ がパスの充足条件
また，任意のパス) Steps の時間遷移量と確率分布を(last$\omega fin$ある$\phi_{1}\mathcal{U}\phi_{2}$$\backslash Q$$(\omega fin),$ $t,$

$\mu$

$\in$

関係

と表している，を充足することをは以下のように定義される．
$\omega\models\phi_{1}\mathcal{U}\phi_{2}$$\phi_{1}\mathcal{U}\phi_{2}$

害リリ当てる関数 $A:Pathfinarrow \mathbb{R}^{\geq 0}\cross Dist(2^{C}\cross S)$
である．全てのアドバサリからなる集合を $A\in Adv$とする．

$\models$$\omega\models\phi_{1}\mathcal{U}\phi_{2}$$\Leftrightarrow$ョ$i\in \mathcal{N}.(\omega(i)\models\phi_{2}$ かつ $\forall j<$$i.\omega(j)\models\phi_{1}\mathcal{U}\phi_{2})$

2.2

PTCTL

口

ここでは確率時間オートマトンの検証に用いられる Probabilistic Timed Computation Three

ここである状態がパス論理式と呼ばれる$\text{ョ_{}p_{>\lambda}[\phi_{1}\mathcal{U}\phi_{2}]}$である形の PTCTL 式を満たし

Logic (PTCTL) [8] のサブクラスを紹介する．PTCTL た場合，必ず実例と呼ばれる
は時間論理 (TCTL) と確率論理 (PCTL) を結合させ を満たす状態 $s\in S$ , アドバサリ $A\in Adv,\Omega\in$であるパスの有限集合たものであり，時間的，確率的なシステムの特性をのサブクラスの構$(s,A,\Omega)$
表現することができる．PTCTLが存在する．
の組み$\sum_{uJ\in\Omega}Prob_{fin}^{A}(\omega)>\lambda$$\{Path_{ful}^{A}(s)|\omega\models\phi_{1}\mathcal{U}\phi_{2}\}$$\Omega$

上記のように PTCTL 式の意味論は状態に対して定義されている．ここでシステムが PTCTL 式 で

文は以下のように定義される．

$\theta$

定義 2.4(制限された PTCTL の構文)$\phi::=a|\zeta|\phi\vee\phi|\phi$A表現された特性を満たすとはシステムの具体モデル$\phi|^{\text{ョ}}\mathcal{P}_{>\lambda}[\phi \mathcal{U}\phi]$の初期状態

ここで $a\in AP,$ $\zeta\in Zones(C),$ $\lambda\in[0,1]$ である．

$s_{0}$

が$s_{0}\models\theta$となる時であり，その時に口限る．つまり，PTCTL のモデル検査とは具体モデ

本論文では以後，明示しない限り PTCTL は制限

ルの初期状態が PTCTL 式を充足するかどうかの検証であると言える．

された PTCTL であるとする．

次に制限された PTCTL の意味論を定義する．
定義 2.5 (制限された PTCTL の意味論) $TPS=$( $S$ , TStep, ) を確率時間オートマトン $PTA$ に対しての時間確率システムとする．任意の状態 $s\in$$S$ ,PTCTL のフオーミュラ, に対して が を充$\mathcal{L}’$$\theta$

足することを$s\models\theta$と表す．関係$s$$\models$$\theta$

抽象モデルと PTCTL

3

本研究では具体モデルである時間確率システムに対して時間の述語抽象化を行うことで抽象モデルを構築する．以下では述語抽象化について述べる．

は以下のように定義 31(抽象化述語) クロック変数の集合 $C$ において，述語 は以下のように定義される．

再帰的に定義される．

$\psi$$s\models a$$\Leftrightarrow$$a\in \mathcal{L}’(s)$$s\models\zeta$$\Leftrightarrow$$s\triangleright\zeta$$s\models\phi_{1}\vee\phi_{2}$$\Leftrightarrow$$S\models\phi_{1}$$s\models\phi_{1}\wedge\phi_{2}$$\Leftrightarrow$$s\models\phi_{1}$or$\psi$$::=x_{1}\leq c|x_{1}<c|x_{1}-x_{2}<d|true$

ここで，

and

$s\models\phi_{2}$

ク評価

$\nu$

$x_{2}\in C,$$c\in N,$$d\in \mathbb{Z}$である．クロッ. 抽象化述語 において， に関する述語$x_{1},$$s\models\phi_{2}$$\psi$

$\nu$

の真偽値を
{true, false} とすると， 中のクロック変数 $x\in C$ に対応する値 $\nu(x)$ を代入した$\psi$$\psi\nu\in$$\psi$

29
結果得られる式が真となるとき，かつそのときに限はり$\psi\nu=true$ であるという．
ノをみたし，ンの定義にある $x>c,$ $x\geq c,$ $x_{1}-x_{2}<d$ は，そ口$\grave$$\grave$$\psi$

$\nu$

–

また，

をその述語とビットベクトルが示すンとして以下のように定義して用いる．
$b^{l}\Psi^{l}$

れぞれ $x\leq c,$ $x<c,$ $x_{2}-x_{1}\geq-d$ の述語で真偽値が $\psi\nu=false$ の場合としてとらえることができる．また，すべてのクロック評価$\psi=$ true は，$\psi\nu=true$ とする．

$\nu\in \mathcal{V}_{C}$$b^{l}\Psi^{l}=\zeta s.t$

において
口

3.1

本研究ではロケーションごとに抽象化述語の集合$\Psi^{l}=\{\psi_{0}^{l}, \cdots, \psi_{n-1}^{l}\}$

ケーション

$l$

$\psi_{i}^{l}$$\Psi^{l}$$b^{l}$$b^{l}$

を用いて，組$\Psi$$\mathcal{B}$

$(l,$

$b$

りを抽象状態$s\#$

体モデルがもつ遷移を抽象モデルに全て持たせることで，抽象化に健全性を持たせる近似である．

とする．ま, 抽象状態の集合を $s\#$ とする．

により$\mathcal{M}$の状態 $(l, \nu)$ から抽象状態マッピングである抽象化関数$\alpha$:$Sarrow s\#$$(l, b^{l})$定義 33(抽象モデルの形成) 確率時間オートマト$C,$ $Inv$ , Steps
ン $G=$ $(L,$から変換された時間確率システム( , Steps, ) における，述語集合への$l_{0},$

が決定さ$\mathcal{M}=$れる．

$\Psi$

この関数によって得られる抽象状態におけるについて，その 番目の要素を$(l, b^{l})$$\alpha((l, \nu))$$b^{l}(i)$$b^{l}$$)$$S$

による抽象モデル$\mathcal{L}’$$\mathcal{M}_{\Psi}^{\#}=(S\#, Steps^{\#}, \mathcal{L}’)$を以下のように構築する．

$=$

$i$

とすると，

$\psi_{i}^{\iota_{\nu=}}b^{l}(i)$.

である．例えば，$o$$\Psi^{l}=$$\{x\leq 1, x-y<-1\}$ において状態 $s=(l,$ $x=1\wedge y=$.

1 を抽象化した抽象状態は $\alpha(s)=$ ( , (true, false))となる． の逆像を，具体化関数 : $s\#arrow 2^{S}$ とす
$)$

$l$

$\alpha$$\gamma$る．
ともに，全射でも単射でもない．このを以下のように定義する．
$\alpha,$における時間確率システムの抽象モデルに含まれる述語の数と等しい長さの，近似になるように定義する．オーバー近似とは，具を考える．そのようなビットベク

た，全てのロケーションにおけるビットベクトルの集合を$\Psi$を構築する．抽象モデルは時間確率システムと同様にマルコフ決定過程の形をとる．抽象モデルは文献[11] に従い確率分布の導入により拡張し，オーバーとする．

ビットベクトル
トル

抽象モデル

述語集合

てのロケーションにおける抽象化述語の族を $\Psi=$
述語集合$\nu\triangleright\zeta\wedge\psi_{i}^{l}\nu\equiv b(i)$抽象化述語と抽象化・具体化関数を用いて，あるを与える．ここで， は，ロにおける抽象化述語である．また，全$\{\Psi^{l_{O}}, \cdots, \Psi^{l_{k}}\}$.

$\backslash \grave{\text{ノ}}^{\backslash }-$$\gamma$$\alpha$と$\gamma$

抽象状態集合$s\#_{=L}\cross \mathcal{B}$

抽象状態遷移関係 Steps
ラベリング関数$\#\subseteq s\#\cross$Dist$(2^{C}\cross S\#)$$\mathcal{L}’(l, b)=\mathcal{L}(l)$ョ. $(l, \nu)\in\gamma((l, b)).((l, \nu), \mu)\in Steps$ であるとき，遷@ $((l, b), \mu\#)\in Steps^{\#}$ が存在する．
:$J$

定義 32(抽象化・具体化)$C$$((l, \nu), t, \mu)$

はクロックの集合とし， は対応するクロック評価の集合とする．
述語の有限集合が与えられたとき，抽象化関数 : $Sarrow s\#$ は以下のように定$\mathcal{V}_{C}$$\Psi=\{\Psi^{l_{O}}, \cdots , \Psi^{l_{k}}\}$に対応する $((l, b), \mu\#)$ における$\mu\#$

は以下 で定義される確率分布である．ただし $\alpha((l, \nu))=$$(l, b),$ $\alpha((l’, \nu’))=(l’, b’)$
$|$

である．

$\alpha$$\mu^{\#}(X, (l’, b’))=\mu(X, (l’, \nu’))$

義される．
$\alpha((l, \nu))=(l, b^{l})s.t$.

口$\forall i.b^{l}(i)=\psi_{i}^{l}\nu$$\mathcal{M}\#$

また具体化関数$\gamma$: $s\#arrow 2^{S}$ は以下のように定義される．

上のアドバサリ $A\#$ は，時間遷移量のき，$A\#:Path^{\#}finarrow Dist(2^{C}\cross S\#)$である．

$\mathcal{M}\#$を省は$\mathcal{M}$と同じくマルコフ決定過程であるため， で用いてた表現に を付けることで， でも同様に表現$\mathcal{M}$$\#$$\iota\backslash$$|$$\gamma((l, b^{l}))=\{(l, \nu)\in L\cross \mathcal{V}_{C}|Inv(l)\wedge\bigwedge_{i=0}^{n-1}b^{l}(i)=\psi_{i}^{l}\nu\}$

$t$

する．

$\mathcal{M}\#$

30
と表してい
を充足することをる，関係 は以下のように定義される．
$\omega\#\models\phi_{1}\mathcal{U}\phi_{2}$$\phi_{1}\mathcal{U}\phi_{2}$$\models$$\omega^{\#}\models\phi_{1}\mathcal{U}\phi_{2}\Leftrightarrow$ョ

$i\in \mathcal{N}.(\omega^{\#}(i)\models\phi_{2}$かつ$\forall j<i.\omega^{\#}(j)\models\phi_{1}\vee\phi_{2})$口

以上のように抽象モデルに対する PTCTL の意味論を定義することで次の定理がいえる．

の初期状態 と，そ定理 3.1 時間確率システムの初期抽象状態のオーバ近似である抽象モデル
に対して以式あった時，任意の形の PTCTL$\mathcal{M}$$s_{0}$$\mathcal{M}^{\#}$$\theta$$s_{0}^{\#}h^{\backslash ^{\backslash }}$下のことがいえる．

$so\models\thetaarrow s_{0}^{\#}\models\theta$

口

図 2:

$G_{1}$の抽象構造$\mathcal{M}b$

ここである状態がパス論理式と呼ばれ
例 31 図 1 の$G_{1}$

を抽象化した場合の抽象構造を図 2 に示す．抽象化に伴う述語集合は$\mathcal{M}_{\Psi}^{\#}$$\psi_{0}^{un}=x\leq$る$\text{ョ_{}p_{>\lambda}[\phi_{1}\mathcal{U}\phi_{2}]}$

$\in$

集合

抽象モデル上での PTCTL の定義$>$$\sum_{\omega\#\in\Omega\#}Prob^{A^{\mathfrak{p}}}fin(\omega\#)$

$s\#$

3.2

PTCTL 式を満たした場合，必ず実例の候補と呼ばれる

1, $\psi_{1}^{un}=x\leq 5$ である．

である形の

$s\#$

,

アドバサリ

$A$

$\lambda$$\in Adv\#$を満たす状態とパスの有限$\Omega\#\in\{\omega^{\#}fin|\omega_{ful}^{\#}\in Path^{A^{\#}}fin(s\#)\wedge\omega\#\models\phi_{1}\mathcal{U}\phi_{2}\}$の組み $(s, A, \Omega)$ が存在する．

本論文では PTCTL の充足性問題の解析を状態爆発を防ぐために抽象モデル上で行う．そのため抽象モデル上で PTCTL の意味論，PTCTL を充足する
抽象状態の集合及び充足性問題を以下のように定義する．ただし状態$s\#=(l, b^{l})$

この章では確率時間 WiGAR の枠組みによる検証とする．の流れについて解説する．ここで具体モデルと抽象
モデルは定理 31 により PTCTL で表現される特性

定義 3.4(抽象モデル上での PTCTL の意味論)に対して健全性を保っている．つまり図 3 の関係になっている．

$a\in \mathcal{L}’(s\#)$$s\#\models a$$\Leftrightarrow$$s^{\#}\models\zeta$$\Leftrightarrow$$s\#\models\phi\vee\psi$$\Leftrightarrow$$s^{\#}\models\phi$or$s^{\#}\models\phi\wedge\psi$$\Leftrightarrow$$s^{\#}\models\phi$and$s^{\#}\models^{\text{ョ}}\mathcal{P}_{>\lambda}[\phi_{1}\mathcal{U}\phi_{2}]$確率時間 WiGAR

4$b^{l}\Psi^{l}\wedge\zeta\neq\emptyset$$s^{\#}\models\psi$$s\#\models\psi$$P_{s}v^{A^{\#}}(\phi_{1}\mathcal{U}\phi_{2})>\lambda$$\Leftrightarrow$となる$A\in Adv$ が存在する．

ここで$P_{s\not\in}^{A^{\#}}(\phi_{1}\mathcal{U}\phi_{2})$$=$$Path_{ful}^{A^{\#}}(s\#)|\omega\#\models\phi_{1}\mathcal{U}\phi_{2}\}$

また，任意のパス

Prob$\theta A\{\omega\#$

$\in$

ある．

$\omega\#\in Path_{ful}^{\#}$

がパスの充足条件

図 3: 具体モデルと抽象モ

デルの関係

31
つまり検証したい特性を抽象モデルが満たさなかったならば具体モデルでも満たさないことがわかる．本
研究では具体モデルが抽象モデルに対して健全性をもつことを利用して図 4 の流れで検証を行う．

する．具体的には古典的なモデル検査の手法により
PTCTL 式を満たす状態集合を厳密に求めていくことになる．しかし，パス論理式と呼ばれるを満たす状態集合を正確に導出することは難しい．そこで本研究では，抽象モデル上でパス論理式を満たしたときに得られる実例 (Witness) の候補を解析することで，パス論理式を満たす状態集合の部分集合を求める方法を提案する．ここで，実例の候補は抽象状態 , アドバサリの組である, パス集合時間確率システム
PTCTL

入力

$A\#$

$s\#$

$(s, A, \Omega)$

具体モデルも満たさな

$A\#$

とパス集合

$\Omega\#$の取り方として無限の組み合わせが存在する場合があるため，全ての実例の候補を解析した場合，解析が有限時間で終わらない．そこで本論文では解析する実例の候補のアドバサリとしては最大確率を与えるアドバサリを$——–\Downarrow_{------\Downarrow_{--------}}^{\frac{\yen\pi 1IO)8l*\alpha \text{く}g\#\text{し}t_{\overline{\delta}}\iota\backslash }{-------------}\leq mh^{S}ff\not\in}-$$\underline{\cap lii}$$\Omega\#$の形をとる．しかし，実例の候補の要素であるアドバサリ$|$$\exists_{\mathcal{P}_{>\lambda}[\phi_{1}u\phi_{2}]}$$l\backslash |$図 4: 確率時間 WiGAR による検証の流れ

選択し，パス集合の選択方法として最小反例 [3] の
以下では「抽象モデルの構築」，「抽象モデル検査」， 手法を採用する．この最小反例の採用により，有限「実例解析」，「精錬」の 4 つのそれぞれのフェーズについて簡単に述べる．

4.1

ことができる．そして，この実例の候補のみを解析することで実例解析は有限時間で終えることができる．ただし，この手法により得られる状態集合は実際にパス論理式を満たす状態集合の部分集合である．
なお，この手法により求まった PTCTL 式を満たす

抽象モデルの構築

ここでは確率時間オートマトンの意味にあたる確
率時間システムに対して文献手法 [11] により提案されている述語抽象化抽象により抽象化を行う．この抽象化により無限状態遷移系であった確率時間シス
テムを有限状態遷移系に変換することができる．

4.2のパス集合から成る実例の候補をただ一つ構成する

抽象モデル検査

状態集合に具体モデルの初期状態が含まれていれば，$|$

時間確率システムは PTCTL 式を満たすということがわかり，確率時間 WiGAR による検証を終えるこ

次に，述語抽象化により得られた抽象モデル上で とができる．逆に，初期状態を含んでいなかった場
検証したい PTCTL 式のモデル検査を行う．検証方 合は精錬のフェーズに移行する．
法としては文献 [13] で提案されているラベル付け手 4.4 精錬法による PCTL の検証を PTCTL に拡張した手法を精錬では，抽象モデルは PTCTL 式を満たしたが，用いて行う．ここで抽象モデルは有限遷移系である その満たした実例の候補を解析したところ具体モデ
ため有限時間内でラベル付け手法による検証を終えの初期状態は PTCTL 式を満たさなかった場合にることができる．なお，この検証により抽象モデル -d う．そのため，再び同じ誤った実例の候補によりが PTCTL 式を満たさなければ，具体モデルである ?fi 象モデルが PTCTL 式を満たしてしまうことがな
確率時間システムもまた PTCTL 式を満たさないこい ように抽象モデルを再構築する必要がある．つま}$)\triangleright$$t’\overline{7}$$-$$4^{\backslash }$とがわかり確率時間 WiGAR による検証を終えるこり，精錬ではそのような抽象モデルの再構築に必要とができる．逆にもし満たした場合は，実例解析の,な述語の導出を行う．

フェーズに移行する．

4.3

実例解析

実例解析では抽象モデルでは PTCTL 式を満たしたが，具体モデルでも満たすのかということを解析

以上が確率時間 WiGAR を構成する 4 つのフェーズである．以上のように確率時間 WiGAR では 4 つ(のフェイズを検証結果が得られるまで繰り返すことなる．ここで必要に応じて抽象モデルを具体化し$’$$\iota_{\llcorner}^{\vee}$32ているため，できるだけ少ない状態数で検証を終えることができ，効率的な検証が可能になっている．

5

実験

この章では，これまで述べてきた確率時間 WiGAR
文献 [8] によるの枠組みを用いて実際に検証を行
Symbolic model checking と状態数を比較することで確率時間 WiGAR の有効性を示す．なお，確率時間
WiGAR の実装においてゾーン演算は QE(Quantifier
Elimination) [17] を利用して行う．
$A\searrow$

実験は IEEE1394 FireWire root contention プロ

トコルの確率時間オートマトンのモデル上において実験を行った．
ここで IEEE1394 FireWire root contention プロ

効率的に抽象モデルを再構築できたためであると考えられる．また，状態数の減少は Symbolic model
checking では検証に多くの状態数を持つモデルを構築する必要があったデッドラインを大きく設定場合により顕著に表れた．この場合確率時間 WiGAR においても検証には多くの WIGAR のループ回数が必要とされたが，そのそれぞれのループにおいて最小実例の採用により効率的に抽象モデルの構築が行われている．そのため 1 ループ毎の効率的な抽象モデルの構築が積み重なり，結果的に確率時間 WiGAR
では Symbolic model checking と比べより良好な結果が得られたためであると考えられる．またこのことは状態数の増加によりメモリ制約が厳しい検証に対してより有効であるといえ，既存の検証手法では状態爆発の原因により検証できなかったものを検証できる可能性があるという点で有効性があると考えられる．

トコルとは 2 つのノードが接続されたネットワーク
上でリーダを選出するためのプロトコルである．
このプロトコル動作を確率時間オートマトンによ6 まとめり表現したものが図 5 である．
本研究では確率的，リアルタイム的動作をするシス
今回の実験ではデットライン (表 5 での DLine)を設定した上で，1 以上の確率でそのデッドライン テムのモデル検査において CEGAR の枠組みを改良に到達できるか) した WiGAR の枠組みを導入することで空間計算量以内にリーダを選出できるか (どうかを検証項目とする．この検証項目を PTCTL を大幅に減らす枠組みの提案を行った．また WiGAR
DLine)] と表現す の枠組みにおいて必要となる実例解析の手法，及び式では ョ(elect[true
ることができる．この実験において Symbolic model 実例が存在しなかった場合における精錬の手法の提checking と確率時間 WiGAR とで結果を返すことが 案を行った．
できたモデルの状態数を比較したものが表 5 であり， 今後の課題としては，制限されていない PTCTL でそれをグラフかしたものが図 6 である．なお，計算 表現される特性に対しても CEGAR の枠組みを用い
時間やメモリ使用量は実行環境が異なるため比較対 て検証できるように理論を拡張することを目的とし$el\omega t$$\mathcal{P}_{>0}$$\mathcal{U}$$\wedge t>$

象から除外した．

ている．

また，充足性問題の解ははデッドライン，検証手法にかかわらず’no’ となった．
表 5 に示されるように確率時間 WiGAR ではどのようなデッドラインの値に対しても Symolic model
checking よりも少ない状態数でのモデル上で検証を終えることができることを確認できた．これは，確率時間 WiGAR では最小実例を採用することにより，
PTCTL 式を満たす上で最も大きな貢献をした (確率が最も大きくなる) パスから解析することにより

参考文献[1] Alfro, ,D,Model Checking of probabilistic
systems,Springernondeterministic
and$(1995)499-513$.
Verlaf,LNCS 1026,$L$[2] Clarke. E. $M$ , Grumberg. , Peled. D.
Model Checking,The MIT Press,(2000)
$O$

$A$

,

33

図 5: FireWire のプロトコルの確率時間オートマトン

F$reWire root contention protocol$8400_{\ovalbox{\tt\small REJECT}}$;$-ff$ 禍 GAR$*$ Symbo $fc\mathfrak{W}de1$ Cbec $kng$

$0$

5000

$20006$$S000$$I\}\Leftrightarrow ad$

26000

25000

$3\ddagger 000$

沖家$e$

図 6: 状態数の比較のグラフ

35900

34
表 1: 実験結果 3[3] Han, T. and Katoen, J. P.: Counterexamples in probabilistic model checking, LNCS
4424, (2007) 72-86.

[10] S. Graf, H. Saidi, Construction of Abstract
State Graphs with PVS,LNCS 1254, (1997)72-[4] Henzinger. T. , Nicollin. X, Sifakis. , Yovine.
, Symbolic Model Checking for Real-Time
Systems, Information and Computation 111$(1994)394-406$ .

[11] Sorea. $M$ , Oller. M. O. $M$ , Rue. , Predicate
abstraction for dense real-time systems, Electronic Notes in Theoretical Computer Science[5] Hermanns. , Wachter. , Zhang. , Probabilistic CEGAR, LNCS 5123, $(2008)162-175$ .

[12] 森下篤，駒形龍太，山根智，確率時間 CEGAR,
電子情報通信学会技術研究報告．CST, コンカレ

, Segala. $R$ ,[6] Kwiatkowska. $M$ , Norman.
Sproston. , Automatic Verification ofRealTime Systems with Discrete Probability Distributions, LNCS, 1601 (1999) 75-95.

[13] Hansson. , Jonsson. B,A Framework for Reasoning about Time and Reliability(2002)102-

$A$

$J$

$S$

$H$

$L$

$B$

83.
$H$

65(6)(2002).

ント工学 $109(73)(2009)25-30$ .

$G$

$J$

, Segala. $R$ ,[7] Kwiatkowska. $M$ , Norman.
Sproston. , Automatic verification of realtime systems with discrete probability distributions, Theor. Comput. Sci 282(1)(2002)101$G$

$J$

150.
[8] M. Kwiatkowska, G. Norman, J. Sproston andF. Wang, Symbolic ModelChecking for Probabilistic Timed Automata, Information andComputation $205(7)(2007)1027-1077$ .
[9] Puterman. $M$ , Markov Decision Processes:
Discrete Stochastic Dynamic Programming,
Wiley- Interscience, (1994).

$H$

111.
, Yi. $W$ , Timed[14] Bengtsson.
tomata:Semantics,Algorithms
Tools,LNCS 3098, $(2004)87-124$ .
$J$

Auand

[15] T. Henzinger, X. Nicollin, J. Sifakis, S. Yovine,
Symbolic model checking for real-time systems, Information and Computation 111(2)$(1994)193-244$ .

analyse formelle des systemes[16] S. Tkipakis,
temporises en pratique, Ph.D. thesis, Universite Joseph Fourier(1998).
$L$‘[17] A. Tarski, A decision method for elementary
algebra and geometry, University of California
Press (Berkeley) (1951).