数理解析研究所講究録
第 1799 巻 2012 年 29-36

292011 年度冬の LA シンポジウム [6]

抽象化洗練を用いた時間確率システムに対する形式的検証手法
清水 隆也

*

森下 篤 \dag er

1.3

1

導入

1.1

背景

山根 智 \d ag er
関連研究

これまで CEGAR を適用した検証手法として，リアルタ

イムシステムを対象とした時間 CEGAR[11] や，ハイブリッ
ドシステムを対象とした研究 [5], 確率システムを対象とし

EMClarke らによって，リァクティブシステムの反例に た確率 CEGAR[9], などが研究されてきた．
よる抽象化精錬の枠組み (CEGAR)[6] のモデル検査 [4] が本研究では確率システム及びリアルタイムシステムの両提案された．モデル検査ではシステムの状態数が大きくな 方を併せ持つ性質を対象とするため，検証を行う上での課る状態爆発の解決が課題になるが，述語抽象化 [7] を導入

題として，同時実行可能性の解析手法が必要である．この手
し，状態数を抑えながら検証可能な手法が CEGAR である． 法はこれまで提案されておらず，本稿ではその手法を示す．

本研究は，確率時間オートマトンに対して CEGAR を適用
一方，確率リアルタイムシステムに対する検証の既存手し，モデル検査の特性の 1 つである到逢可能性解析による法として，記号モデル検査 [10] がある，CEGAR は，状態

安全性の検証を行う．

1.2

数を抑えながら検証可能な手法であり，導入することで効確率時間 CEGAR

率的な検証を期待できる．本研究では確率時間 CEGAR を

一般に，抽象化を行うとシステムは本来の性質を損なう． 計算機上に実装して，上記手法との性能比較を行う．
CEGAR[6] では，抽象モデル上での反例の候補の導出と，2反例を用いた抽象モデルの精錬を，結論が得られるまで繰

確率時間オートマトン

21

り返すことで正当性を保証するとともに，偽「x 例から得た

ここでは，クロック変数とゾーン [1]. 確率時間オートマ

情報により，検証に必要な部分のみを詳細化することで状態数を抑えることができる．CEGAR による枠組みを用い

.
.
.

準備

て検証を行うには以下の手法を確立しなければならない．

トン $G[10]$ , 時間確率システム$\mathcal{M}[10],$

時間確率システムのアドバサリ$A[10],$$\mathcal{M}$

$A$

上のパス

$\omega[10]$,で洞を解決した離散時閤マルコフ連鎖を準備する．これらの定義については，それぞれの文献に従うものとする．
$\mathcal{M}C^{A}[10]$

検証したい性質を抽象モデルが持っていれば，具体モデルも持っている健全性を保つ抽象化手法

22 確率到達可能性問題と反例
抽象モデルから反例の候補を導出でき，その反例の候
到達可能性問題はソフトウェアの検証におけるもっとも補が実動作可能な反例であるか解析する反例解析手法． 本的な問題であり，羨々な検証問題は到達可能 性問題に$\ovalbox{\tt\small REJECT}$$|${ 着させることができる．本研究は，時間確率システムの安全性を到達可能性問題によって検証する．

反例解析の結果，反例の候補に対応する反例が存在しないとき，同じ反例の候補を生じさせないように抽象モデルを精錬する手法$\gamma$$\pi\Xi$に
義 21(到逢可能性問題). ロケーション集合$le\in Le$ をもつ状態の集合をついて，ロケーション
本論文ではこれらを確立し，確率時間オートマトンを対象$\{(l_{e}, \nu)\in S|l_{e}\in L_{e}\}$$\lambda\in[0,1]$ を $s0$ から状とする．また，として CEGAR を導入することで，検証対象に応じて抑え.g-.e集合 への到達確率とする．
られた状態空間の構築が可能であることを示す．上記手法$Le\subseteq L$$\not\in$1$S_{e}$$!$$=$$S_{e}$$\grave$と目的ロケーの到達可能性問題を，到達確率の開発において，確率分岐による複数バスの同時の実行可ションの集合の組 ( , Le) とする．
能性を同時実行反例解析によって判定し，その偽反例によ”の答えが到達可能性問題
であるとは，る抽象モデルの精錬手法を実現する．また，本手法の実装$G$$\lambda\in[0,1]$$L_{e}\subseteq L$$\lambda$$(\lambda, L_{e})$実験を行い，既存手法 [lO] と比較することで，より小さい状態空間での検証が可能であることを示す．
$*$$\dagger$$i$

金沢大学大学院自然科学研究科
第 1 著者に同じ
金沢大学理工研究域電子惰報学系$\}_{\llcorner}^{-}$
$1$

おいて，

$\forall A.Prob^{A}(S_{e})\leq\lambda$$\Lambda t$${}^{t}yes$の場合に限る．それ以外の

f 合は ttno” である．口$J$$\varpi$$S_{e}$$\iota($

L。を到達することが望ましくないロケーションの集合，をそのような状態の集合，Pro (Se) を初期状態 か$b$$s_{0}$

30
ら，アドバサリ でのへの到達確率とする．次に，反例を以下のように定義する．
$A$

定義 22(到達可能性問題の反例). あるアドパサリ で非上で得られる有決定を解決した離散時間マルコフ連鎖
限長のパスの集合をとする．PathflnA のうち，目的状態集合に到達するパスからなる有限集合を$A$$\mathcal{M}C^{A}$

PathfinA$\Omega\subseteq\{\omega\in$$S_{\epsilon}$

Path

last

とし，
確率とする．このとき．
$finA|$$Prob^{A}fin(\omega)$$(\omega)\in S_{e}\}$を$\omega\in$$\sum_{\omega\in\Omega}Prob^{A}fln(\omega)>\lambda$$\Omega$が存在するならば，それらを組$(A, \Omega)$

PathflnA$\iota\grave$$\mathcal{M}^{\#}$

で用いていた表現に$\mathcal{M}$とし，その組を反33定理が成り立つ．

でも同様にを時間遷移を表す確率分布として，$\mathcal{M}\#$のパスは$\mathcal{M}$のパスと同様に以下の様に示す．
$\omega^{\#\#^{\mu_{O}^{1}(X_{O\prime}\epsilon_{1}^{1})\mu_{1}^{1}(X_{1},s_{2}^{\})\mu_{2}^{1}(X_{2},\epsilon_{S}^{1})}}=s_{0}arrow s_{1}^{\#}arrow s_{2}^{\#}arrow\cdots$

上の 2 つの状態間の時間遷移は， では
内でであるとき 1 つの抽象状態からを導く際，行われてしまう．よって反例解析にて$\mathcal{M}^{\phi}$$\mathcal{M}$$s_{1},$ $s_{2}$$s\#$$\alpha(s_{1})=\alpha(s_{2})=s\#$$\omega$の状態とする．Pro$b^{A}(S_{e})>\lambda$に到達する有限パスの有限集合
で $\sum_{\omega\in\Omega}Prob^{A}fin(\omega)>\lambda$$(\omega)$を$\omega$の最後

ならば，そのときに限り$S_{e}$$\Omega\subseteq\{\omega\in Path^{A}fin|last(\omega)\in$となる反例が存在する．口内の離散遷移$\omega\#$$s\#arrow^{\mu^{1}}$はその抽象状態で何らかの時間 遷となる． に対応する
移後に離散遷移したにはこの 1 つの抽象状態内の時間遷移を含めないことに$s_{1}|,A^{\mu}s_{2}arrow 0,\mu$

する．

述語抽象化 [7] は無限状態$\not\in$に従い，時間確率システムについて述語抽象化を拡張する．

$\omega$$\Psi$

によって構成されたのパスとは，において， のパス に対応したの全ての遷移に対して，以下の手順によって構成される．

$\mathcal{M}\#$

移系の有限の近似を計算し，状態爆発を抑制するために用いられる．本章は文献 [11] の$\omega$$\omega\#$

定義 32(バスの対応関係). 廻と

述語抽象化

1.

抽象化述語と述語抽象化$\omega$$\omega\#$$\mathcal{M}\#$$\mathcal{M}$$\omega$の遷移が離散遷移$s0,\mu\underline{(x}_{\}^{S’}}$

)

$S’$

ならば， # の遷移は$\omega$$\alpha(s)arrow\alpha(s’)$

抽象化の手法は文献 [7] と同様であるが，その述語には以下のものを用いる．
$\psi$$\mathcal{M}\#$$\omega\#$

定理 21(到達確率と到達パスの集合). last

3.1

を付けることで，抽象モデルと時間確率システムの関係

ロ

る．本研究で対象とする到達可能性問題について，以下の

$\#$

表現する．

$\mu_{\perp}^{\#}$

反例とは，到達可能性問題の解が “no” となる証拠であ

3が時間の制約を伴うマルコフ決定過程であったのに Al
し， は時間のない一般的なマルコフ決定過程であるが，$\mathcal{M}$のとなる $A$ と例とする．

$S_{e}\}$

口$S_{e}$$::=x_{1}\leq c|x_{1}<c|x_{1}-x_{2}<d|$2.

の遷移が時間遷移$S\rangle S’\ell,\mu\underline{\perp(\emptyset}’ s’)$

かつ $\alpha(s)=\alpha(s’)$ な

らば， # の遷移は存在しない．
$\omega$3.

true$\omega$$\omega$の遷移が時間遷移

らば， の遷移は$s^{t,\mu\perp(\emptyset,\epsilon’)}-arrow s’$

かつ $\alpha(s)\neq\alpha(s’)$ な$\alpha(s)arrow\alpha(s’)\mu_{\perp}^{l}(\emptyset,\epsilon’)$$\omega^{\phi}$

確率時間 CEGAR では，導入する述話を basis[11] に含まれる述語に限定することで，停止性を保証する．述語を追加する手法およびその定理については 6 章で示す

3.2

また，このような
Pathfln と抽象化開数と同じ記号を用いて，$\omega\in$$\omega\#\in Pathfln\#\text{の_{}X}^{x}J$

応を，$\alpha_{Path}:Pathflnarrow Path^{\#}fln$と定義する．口抽象モデル

抽象モデルは，文献 [11] を確率分布の導入により拡張し，オーバー近似になるように定義する．

定義 3.3 (アドバサリの対応関係).
$Path^{\#}flnarrow Dist(2^{C}\cross S\#)$$\mathbb{R}^{\geq 0}\cross Dist(2^{C}\cross S)$にが$\mathcal{M}$$\mathcal{M}\#$のアドバサリ$A\#$:のアドバサリ $A:Pathfinarrow$

Xt 応しているとは，以下を満たす場$\Delta$

をビットベクトルの集合， 合である．
定義 31(抽象モデルの形成).
$(t, \mu)\wedge$
を抽象化関数， を具体化関数として，確率時間オートC.
$C,$ $Inv$ ,prob
マトン $G=$ $(L,$から変換された時間確率シ $A\#(\alpha_{Path}(\omega))=\mu\#$ に対して，$\mu(X, s)=\mu\#(X, \alpha(s))$
ステム( , so, Steps) における，述語集合 による抽また，このような $A\in Adv$ と $A\#\in Adv^{\#}$ の対応を抽象化$B$$\alpha$$\gamma$$\forall\omega$$l_{0},$$S$$\mathcal{M}=$

..
.

象モデル

$\in$

$Path^{A}fln.\forall s$$\in$$S.\forall X$$\subseteq$$A(\omega)$

$=$

$)$

$\Psi$$\mathcal{M}^{\#}=(S^{\#}, s_{0}^{\#}, Steps^{\#})$

抽象状態集合初期抽象状態
抽象状態遷移関 {系 Stepsを以下のように構築する．

$\alpha_{Adv}:Advarrow Adv^{\#}$ と定義する．
関数と同じ記号を用いて，

口$s\#_{=L\cross \mathcal{B}}$定義 32 および，定義 33 より，次の定理が成り立つ．
xDist$Path^{A}fln$ に
El $(l, \nu)\in\gamma((l, b)).((l, \nu),\mu)\in$ Steps であるとき，遷移 定理 3.1 (パスの対応定理). あらゆる$((l, b),\mu^{\#})\in Steps^{\#}$ が存在する．
による
おいて，いかなるであっても， 応するパ
$s_{0}^{\#}=\alpha(s_{0})$$\#\subseteq s\#$$(2^{C}\cross S\#)$$\omega$$\Psi$$((l, \nu), t, \mu)$に対応する$((l, b), \mu\#)$における下で定義される確率分布である．ただし$(\downarrow, b),$$\alpha((\nu’$である．

$\mu^{\#}(X.(l’,b’))=\mu(X.(l’, \nu’))$$\mu\#$は以$\alpha((l, \nu))$$=$$\mathcal{M}\#$$\in$$l^{\backslash }A1$

ス $\alpha_{Path}(\omega)=\omega\#\in Path^{A^{1}}fln$ および対応するアドバサリ$\alpha_{Adv}(A)=A\#\in Adv^{\#}$

である．

が存在し，

$Prob^{A}fin(\omega)=Prob^{A^{1}}fin(\omega\#)$31
定理 32(パスの抽象化). $M$ において，アドバサリ によって導出されるパス集合のうち，異なる 2 つの$A$

$Path^{A}fin$

パス $\omega_{1},\omega_{2}\in Path^{A}fin$について，次の関係が成り立っ．

$\alpha_{Path}(\omega_{1})\neq\alpha_{Path}(\omega_{2})$

3.3.1

反例の候補

定義 34 (反例の候補). $G$ と到逢可能性問題て， の意妹$G$$L_{e}$をもつの抽象モデル$\mathcal{M}$$\mathcal{M}\#$におい$l_{e}\in$

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

として，上の集合を $;\subseteq s\#$$\mathcal{M}\#$$(\lambda, L_{e})$の「X 例の候補とは，$G_{1}$$Prob^{A^{\#}}fin(S_{e}\#)>\lambda$とパス集合となる， のアドバサリの組である．
反例 $(A, \Omega)$ が反例の候補 $(A, \Omega)$ に対応しているとは，以$\Lambda 4\#$$A\#$$\Omega^{\phi}$

下の関係を満たしているときである．
$\alpha_{Adv}(A)=A\wedge\forall\omega\in\Omega.\exists\omega\in\Omega\#.\alpha_{Path}(\omega)=\omega\#$は$Prob^{A^{\#}}fln(S_{e}\#)$$\square$へ到達可能なパス集合の合計到達確率$S_{e}\#$

である．次に，反例と反例の候補に関する 2 つの定理を示す．
定理 3.3 (合刮到達確率の関孫).
$\mathcal{M}\#$

上のアドバサリ$A\#$$\mathcal{M}$$\backslash$$S_{e}$

は，アドバサリ

確率時間 CEGAR

述語抽象化及び反例による精錬を自動的に検証に適用し例による抽象化と精 1)[6]の枠組みである．確率時間 CEGAR の検証の流れを図 3 にていくアプローチが CEGAR($Prob^{A}fin(S_{e})\leq Prob^{A}fln(s_{e}^{v})\#$$Prob^{A}fln(S_{e})$$A$$\mathcal{M}_{0}^{\#}$

上のアドバサリ $A$ とが対「，し してぃる場合，それぞれの到 4

達確率について以下が成り立つ．

集合

図 2: 抽象モデル

における$\lambda 4$での目的状態$\ulcorner$示す．

への到達確率である．

定理 3.3 は， において到達確率が最大となるアドバサ
リを考えた時， の最大到達確率が抽象モデル上の最大到達確率以下になることを示す．
$\Lambda\Lambda$$\mathcal{M}$定理 3.4 (反例の存在).

ば，必ず$\Lambda\tau\#$$\mathcal{M}$で反例の候補この定理から$\mathcal{M}\#$

Probab $i|i$ st ic Timed Automaton $G$
Probab $i|i$ st ic Reachab $i|i$ ty Problem$(\lambda,$$L_{e})$

で反例 $(A, \Omega)$ が存在するなら$(A\#_{:}\Omega\#)$が存在する．

で反例の候補が存在しなければ反例が存在しないため，確率到達可能性問題の解は “yes” となる．
34 同時実行
ここで，確率時間オートマトンの同時実行性の問題について，図 1 の確率時間オートマトン({true},{true},$\Psi^{l_{0}}=$$\Psi^{l_{1}}=$による抽象モデル$\mathcal{M}_{1}^{\#}$$G_{1}$と，図 2 の抽象化述語{true},{true})$\Psi$$\Psi^{l_{2}}=$$\Psi^{l_{e}}=$を用いて例を示す．
から反例の候補のパス集合
として，2 つのパス$\Lambda 4_{0}^{\#}$$\Omega\#$$\omega_{1}^{\#}=s_{0}^{\#}arrow s_{1}^{\#}arrow s_{e}\#$する． の$G_{1}$$\Lambda\Lambda$と$\omega_{2}^{\#}=s_{0}^{\#}arrow s_{2}^{\#}arrow s_{e}\#$が挙げられたと上において，この 2 つのパスに対応するパスはそれぞれ存在するが$\omega_{1}^{\#}$に 寸応するパス$x\perp$$\omega_{1}$

おいて 1 単位時間以上の時間遷移をしなければきないのに対し， に対応するパス$\omega_{2}^{\#}$

時間遷移すると態$(l_{0}, \nu_{0})$にて$l_{e}$$\omega_{2}$では， } こ図 3: 確率時間 CEGAR による検証$l_{0}$$l_{e}$に到達ででは， において$l_{0}$に到達する事はできない．つまり初期状

1. 抽象化 : 述語集合
述語集合$\Psi$$\Psi$

から抽象モデルは，$\forall l\in L.\Psi^{l}=$でそれぞれ異なるアドバサリで動作して

から
だけでなく
いる．よって，の対応も調べる必要がある．本研究では，後の反例解析にて，同時実行
反例解析を提案することでこの問題を解決する．
$(A\#, \Omega\#)$$\Omega$$A$を計算する．

{true} として開始する．

2. 反例の候補の導出 :上で反例の候補を求める．反例の候補が存在しない場合，“yes“ を出力し$\mathcal{M}_{\Psi}^{\#}$$\omega_{1}$$\mathcal{M}\#$

検証を終了する．

$(A\#, \Omega\#)$32
3.「 例解析 : 反例の候補 $(A, \Omega)$ に対応する反例$x$$(A, \Omega)$が存在するかどうかを求める．存在すれば “no” を出

5.2

反例解析

力し，検証を終える．存在しなければ，$(A, \Omega)$ は具

5.2.1 反例解析の概要
反例解析はパス反例解析と同時実行反例解析の 2 つの手体モデルで実現できないと判断する．このような反例順からなる．

の候補を偽反例とする．
4. 精錬 :「 例解析の結果，偽反例であればその偽反例$X$$(A\Omega)$

をから取り除くための新しい述語を導出$\lambda 4\#$し，新しい5. (1) に戻る．

$\Psi$

を得る．

まずバス反例解析では， のそれぞれのパス$\Omega\#$て，対応する$\mathcal{M}$上のパス$\omega\#$についが存在するかどうかを求める．

$\omega$

もし，対応するパスがなければ，$\{\omega\in Pathfln|\alpha_{Path}(\omega)=$となる．このようにして得られた各パス集合から，$\omega\#\}=\emptyset$

任意のパスをそれぞれ 1 つ選んで集合

これらのサイクルを繰り返していくことにより，最終的”か “no” かをにシステムが確率到達可能性問題に対しとし，これを反例のパスの集合とする．この の全ての組み合わせからなる集合をとする．ここでは最小反例であるため，反例の候補判定する．

のパスのうち，1 つでも5であれば，この反例の候補 $(A, \Omega)$ は偽反例となることに注$y\infty$

反例解析
本章では，確率時間 CEGAR における反例解析の手法を提案する．これは反例の候補 $(A\Omega)$ の導出と反例解析によって行われる．

$\Omega$$\Omega\#$$\Omega$$\{\omega\in Pathfin|\alpha_{Path}(\omega)=\omega\#\}=\int|$

意する．

次の同時実行解析では，求めたパスの集合

反例の候補の導出$\Omega$

反例の候補を導出する手順を以下に示す．

1. アドバサリを導出: 検証確率なるアドバサリ$A\#$より大きい到迂確率にが存在しなけれを求める．この$\lambda$

$A\#$

$A\#$

$\lambda$$\Omega\#$

$A\#$

が1つ

を確かめる．このようなおよび $A$ が存在しない場合，この反例の候補は偽反例であることがわかる．

ば反例の候補は存在しないにおけるパスのうち，パスの合引確率が，検証確率 より大きくなるような，有限長のを求めるパスからなる有限集合
手順 1. によって検証確率を超える到達確率になるアドバ
サリは存が求まれば，定理 21 より必ずパスの集合

2. パス集合を導出:$\Omega\in\Omega$のアドバサリ $A$ で構成可能かどうかを確かめる．つまり，$\exists\Omega\in\Omega.\exists A\in Adv.\Omega\subseteq Path_{J^{1n}}^{A}$

5.1$\Omega$$\Omega\#$

それぞれの反例解析によって，導出した$(A\#, \Omega\#)$が偽「x例であると判断された場合，同じ反例の候補を導出しない
ように，新しい述語を追加して抽象モデルの精錬を行う．
各手順で求められたパス集合 とアドバサリ $A$ を反例とし，反例が求まれば確率到達可能性問題に対して，no と$\Omega$

いう解を示すことができる．

5.2.2

準備 (ゾーンによる解析)

この) 文例解析の手法では，$\omega\#$に対応するパス集合

在し，手順 2. によりそのパス集合を求めることができる．

$\{\omega|\alpha_{Path}(\omega)=\omega\#\}\text{を_{}\omega}\#$この 2 つの手順により，反例の候補 $(A,\Omega)$ を導出する．まとするこた，ここではとして，最大到達確率になるシンプルな
アドバサリを用い， として，パスの数の少ない最小反例[8] を用いる．
はマルコフ決定過程であるため，最大到達確率とアドバサリは線形計画法によって計算可能であり [2]. シンプ
ルなアドパサリ [2] となる．

ついて，そのゾーンに着目し．以下のように取り扱う．

$A\#$

$\xi$

の各抽象状態に対応するゾーンで取り扱う．つまり，ある$\omega\#$

中の抽象状態$s\#$に$\Omega\#$$\mathcal{M}\#$$\{\nu|\alpha_{Path}(\omega)=\omega^{\#} A 1i.(\alpha(\omega(i))=s^{\#}\wedge\omega(i)=(l, \nu))\}$

定義 32 の (2) より， に現れない時間遷移を考慮する$\omega\#$

必要があることに注意する．そのため，集める各抽象状態のゾーンを，時間遷移前のゾーンである到達条件と，時間遷
ここで求めた最大到達確率が検証確率以下であれば反例 移後のゾーンである出発条件の 2 つとする． の & 目の$\omega\#$の候補は存在しないと言うことができる．さらに定理 34 より，具体モデルにおいて反例が存在しないといえる．従って，最大到達確率が検証確率以下であれば確率到達可能 性問題に対して yeS” と答えることができる．

, 到達条件を$i$の出発条件を聯とする．ここで，「例解析で用いるゾーン演算を定義する．

状態$(l, b)$$\zeta_{\omega}^{d\epsilon p},$$\zeta$$|$定義 51(ゾーン演算). 時間確率システムのゾーンを
prob, リセットク
によっての非決定が解決されると，その動作 $Zones(C)$ , 確率遷移関係を
は離散時間マルコフ連鎖として記述される．そこで，確 ロック変数の集合を $X\subseteq C$ として，ゾーンを変形する以率 CEGAR[9] でも利用されている，最小反例 (smallest
counterexample[8] を用いる．このような $(A, \Omega)$ を収例$A\#$$\mathcal{M}\#$$)$の候補として利用する．

$\zeta\in$$(l_{\}}\zeta_{9}, p)\in$33
下の演算を定義する．

ここで，の到達条件が false になれば (line: 17),意する．もし，$\omega\#(0)$$time_{-}succ[\zeta]$$=$$\{\nu|\exists t\in \mathbb{R}^{\geq 0}.\nu-t\triangleright\zeta\}$

によって初期状態 $s_{0}=(l_{0}, \nu_{0})$ から目的状態に到達でき$\omega^{\#}$

time$-pre[\zeta]$$=$$\{\nu|$ョ$t\in \mathbb{R}^{\geq 0}.\nu+t\triangleright\zeta\}$reset$[\zeta, X]$$=$$\{\nu[X :=0]|\nu\triangleright\zeta\}$free$[\zeta, X]$$=$$\{\nu|\nu[X:=0]\triangleright\zeta\}$iscrete-succ$[\zeta, \zeta^{g}, X]$

$=$

reset

$discrete_{-}pre[\zeta, \zeta^{9}, X]$

$=$

free

$d$

ないことがわかるため，この反例の候補を偽反例とすることができる．精錬では，$l_{0}s.t$$[\zeta\wedge\zeta^{g}, X]$

$d$

ロ

$d$

散遷移の演算であり，discretesuccが$\zeta^{g}$$[\zeta,$$[\zeta, \zeta^{g}, X]$$\zeta$$(^{g},$

は，ガード条件

からガード条件およびリセットクロックを考慮して遷移可能なゾーンを返す．discrete$-pre[(_{:}\zeta^{9},$ $X]$

様の離散遷移によって，あるゾーン$\zeta$は同へ遷移可能なゾーンを返す$\omega\#\in\Omega\#$$xl:for\omega\#\in\Omega d$2:$\zeta_{|\omega\#|,\omega\#}^{rw}arrow\zeta_{|\omega^{\gamma}|,\omega\#}$for $(i=|\omega\#|-1, \ldots.0)$ do

3:

if

4:

$\omega\#(i)^{\mu^{\#}}-4$

is atime transition then5:$\zeta_{i,\omega\#}^{dep}arrow time_{-}pre[\zeta_{i+1,\omega\#}^{r\infty}]\wedge\zeta_{i,\omega\#}$

6:

if

7:

retum
time
end if$\zeta_{i,\omega}^{dep}\#=$

false thenspurious$-succ[\zeta_{i,\omega\#}]$

5.2.3

パス反例解析

8.

$x$ 例の候補のパス反例解析では，「めに，各抽象パス$\omega\#\in\Omega\#$

から

を求めるた

9:

上の，各抽象状態の到逢条件と10:$\Omega\#$$\Omega$$\zeta_{0}$$||$, リセットクロック集合が $X$ である離散遷移によって，

あるゾーン

.

$Algorithm1$ パス「 例解析手 F 1

はそれぞれ時問遷移の演算であ$X]$ は離iscrete-preおよび$[\zeta, \zeta^{g}, X]$$\zeta_{0,\omega\#}^{m}$について，具体モデル上に対応するパスが存在することが分かった場合，exist を出力し，パス反例解析の手順 2. を行う．
すべての$[\zeta, X]\wedge\zeta^{g}$

ここで $(\nu-t)$ は，全てのクロック $x\in C$ について $(\nu-$$[\zeta],time_{-}pre[\zeta]$. $\omega\#(0)=(l_{0}, b),$の情報が必要になる．

$t)(x)=\nu(x)-t$ となるクロック評価である．

time succ
る．iscretesucc

でなければならないことに注$\zeta_{0}=\{l\ovalbox{\tt\small REJECT}_{0}\}\subseteq\zeta_{0,\omega}^{oea_{\#}}$$\omega\#$,,$\zeta_{i+1,\omega\#}^{na}$$\zeta_{i,\omega\#}^{dep}arrow$

$d$

$d$

$l_{i+1,\omega\#}$$\zeta_{i+1,\omega\#}$else

出発条件を以下の手順で求める．
1. 目的状態に到達可能な到達条件と出発条件を， の目的状態から time-pre または iscrete-pre 演算を用いて後方から求める

A

if

11:

iscrete-pre$\zeta_{i,\omega\#}^{dep}=$$[\zeta_{i+1,\omega\#}^{na}, \zeta_{i,\omega\#}^{g}, X_{i,\omega\#}]$

return12:

A$\zeta_{i,\omega\#}$false thenspurious$l_{i+1,\omega\#}$,$\zeta_{i+1,\omega\#}^{m}$,$discrete_{-}succ[\zeta_{i,\omega}\not\in, \zeta_{i,\omega\#}^{g}, X_{i,\omega\#}]\wedge$$\zeta_{i+1,w\#}$

2. 求めた到達条件と出発条件上で，初期状態から到達司能 13:
な到達条件と出発条件を， の初期状態から timesucc 14:
または discrete-succ 演算を用いて前方から求める
15:

end ifend iftime.preA
end for
if 陥
false then$\omega\#$$\omega\#(i)$を$\omega^{\phi}$

ケーション

の

$i$

$l_{i,\omega\#}$番目の抽象状態,とし，このロ$(l_{\omega\#,i}, b^{\omega i})\#$

での $G$ での不変条件を $Inv(l_{i,\omega\#})$ とする．

また，香目の遷移のクロック変数のリセットを$\zeta_{i,\omega\#}^{r\omega}arrow$

16:
17:

$[\zeta_{i,\omega\#}^{dep}]$$\wedge\zeta_{0}=$$\zeta$retum spurious

lS:$\zeta_{i,\omega}v$$l_{0},$$\zeta_{0,\omega\#}^{rea},$$\zeta_{0}$とし，19:
end if
この遷移に対応する $G$ でのガード条件をと表現する．
20: end for
以降 血を単にと表記する．
$i$$X_{i,\omega\#}$$\zeta_{i,\#}^{g_{\omega}}$$v(l_{i,\omega\#})\wedge b^{i,\omega}\Psi^{\iota_{:,\omega}}\#\#$$\zeta_{i,\omega}v$

パス反例解析の手順 1. のアルゴリズムを Algorithml に示す．入力は反例の候補のもし$\omega\#(i)$$(line:6,11)$ ,$\omega\#$

上の

exist

「例解析の手順 2. では， (こ対応するパス集合$\omega\#$$\Omega\#$の出 発 条件

この21: returnである．

$\zeta_{i,\omega}^{dep}\#$$\omega\#(i)$にfalse になった場合心する状態集合からはが$x\perp 1\backslash$

$|$

合である

$\Omega$$\Omega$の集を導出する．
「 例解析の手順 2. を Algorithm 2
$x$

に示す

の各状
Algorithm 1, Algorithm 2 によって，抽象パス
目的状態に到達できないことを示しており，偽反例であるに態における到達条件および出発条件を求めることで，としてを精錬する．具体的には，,L
村
する具体モデル上でのバス集合を導出できた．この到$ls.t$ . $\omega\#(i+1)=(l, b),$or
埋条件と出 条件を用いて，次の同時英行「x 例解析を行う．
iscrete-succ
5.2.4 同時実行反例解析の情報が必要になる．
$\omega\#$$\omega\#$$\mathcal{M}\#$$\check\grave$$|$$\zeta_{i+1,\omega}^{na}\#,$$time_{-}succ(b^{i,\omega}\Psi y\#\iota_{:.\#})$$\mathfrak{X}$$d$$(b^{i,\omega^{\gamma}}\Psi^{l_{i,\omega}}\#, \zeta^{g}, X)$

このように，パスの最初の抽象状態
条件$\zeta_{0,.\omega\#}^{na}$$\omega\#(0)$における到達を求めるまで，この手順を繰り返す．

同時実行反例解析では，各つずつ選び出して新たな集合$\Omega$

から任意のパス$\Omega’$$\omega\in\Omega$を1とし， に含まれる全て$\Omega’$34$Algorithm2$ パス「 例解析手 ffi 2$\overline{\frac{A1gorithm3\prod\overline{o}\text{時実行}\ulcorner x\text{例解析}}{1:for\omega\#\in Pato}}$$xl:for\omega\#\in\Omega d$2:$\zeta_{0,\omega\#}^{m}arrow(0$

for

3:

$(i=0, \ldots , |\omega\#|-1)$

4:$\zeta_{1\omega}^{dep}arrow$

5:

if

,
A
time succ
is time transition thentime$\omega\#(i)^{\mu}3$6:do$\zeta_{i+1,\omega^{l}}^{m}arrow$A

9:$\zeta_{+1,\omega 1}^{\dot{r}}$end ifend for10:
11: end for

時間遷移量と確率分布を返すため，に含まれる任意の 2 つのバス

それぞれのプレフィックス$\omega_{1}’,\omega_{2}’$

14:

15:

if

が存在するかを確かめる．13:$A$$\omega_{1}’,\omega_{2}’$で導出可能なパス集$\omega_{1},$が$\omega_{2}\in\Omega$$\omega_{1}’=\omega_{2}’$$\Omega$$|\omega\#|>i$

について，16:A$\zeta_{|+1,\omega^{l}}$

do
then

$\zeta_{\omega_{\vee th}}^{dep}!\wedge\zeta_{\dot{*},\omega^{l}}^{d\epsilon p}=$false then$l_{\dot{*},\omega}\iota,$$\zeta_{i,\omega^{1}}^{d\epsilon p}$$\zeta_{\omega_{i}^{t_{-\iota h}}}^{dep},$$\zeta_{\omega_{\vee th}}^{dep}!arrow\zeta_{\omega_{*-\ell h}}^{d\epsilon p}!\wedge\zeta_{i,w^{1}}^{d\epsilon p}$

if

19:

について，等しいプレフィックス があるならば，
20:
その次の遷移は，同じ時間経過量による時間遷移，または
21:
同じ確率分布による離散遷移であることを確かめれば良い．
ス $\omega\in\Omega$$succ[\zeta_{\omega_{\wedge th}}^{m_{!}}]$

return spurious
end ifであるとき，17.

に含まれる各パ

time$\omega\#\in\Omega\#$

からの時間遷移量と確率分布が等しいと言える．す 18:

なわち同時実行反例解析で 1 は バス集合

do
then

$|\omega\#|>i$

end ifend for
for
if

12:

アドバサリはパスを入力することで，次の遷移におけるdo$C_{\Omega_{\infty R}}$$\cdots,$$\omega\#\in\Omega\#$$\zeta_{t}^{dep}arrow$

11:

$A$

0

$\zeta_{\omega_{-\ell h}}^{m_{!}}arrow\zeta_{\omega^{1_{-\ell h}}}^{m}\wedge\zeta_{\omega^{1}}^{\dot{M}}$10:のパスを導出司能なアドバサリ

true$arrow\zeta$

for
if

8:

$\zeta_{i+1.\omega’}^{m}arrow$$\Omega$

髭 8o$\zeta$7:$discrete_{-}succ[\zeta_{i,\omega^{1}}^{d\epsilon p}, \zeta_{\dot{\iota},\omega^{\downarrow}}^{g}, X_{i,\omega^{l}}]$true

6: for $i=0,$$succ[\zeta_{1,\omega^{1}}^{dep}]\wedge(_{i+1,\omega^{1}}^{r}$

9.

合

3:

$\zeta_{\omega^{1}}^{dep}arrow$

5:

$a$

else

7:
8.

$\zeta_{\omega^{1}}^{m}arrow$

4: end for$\zeta_{i,\omega}^{dep}$$[\zeta_{\omega}^{m},]$2:

is a time transition then$\omega\#(i)^{\mu^{\#}}-*$$\omega’$$m$て積を取ることで，そのプレフィックスの出発条件$\omega:$$\omega_{(*+1)}$$e$

同時実行反例解析では，共通のブレフィックスを持つパ 22:
スについて，各状態の出発条件，到達条件それぞれについ$\zeta_{\omega_{*-th}}^{d\epsilon p}!$$arrow time_{-}succ[\zeta^{dep}]$$\zeta t$A$\zeta_{i+1,\omega^{l}}$-th化e$\zeta_{\omega_{(:+1)-th}^{l}}^{m}arrow$discrete-succと$[(_{\omega_{i\ell h}^{1_{\wedge}}}^{d\epsilon p},$$\zeta_{\dot{\iota},\omega^{\mathfrak{j}}}^{g},$$X_{i,\omega’}]$A$(:+1,\omega^{)}$

end ifend if
同時実行反例解析では，いずれかのプレフィックスの出 24:
for
end
25:
$fal\Re$となったとき，複数のパスで発条件または到達条件が
for
end
26:
共通の時間経過量によって具体モデル上で実行できないとして，反例の候補を偽反例とし，精錬を行う．27: return exist
到達条件

をゾーンとして求める．

$\zeta^{m_{1}}$$\omega:$

23:

-th

同時実行反例解析のアルゴリズムを Algorithm3 に示す．次章では，これら反例解析および同時実行解析の情報をアルゴリズムに対する入力は，パス反例解析の結果得られ用いて精錬を行う手法を示す．
た$\omega\#\in\Omega\#$

る．出力はの各抽象状態における到達条件と出発条件であ$(A, \Omega)$が存在していれば exist, 偽反例であると分かれば spurious を返す．このアルゴリズムは，Algorithm

6精錬
反例解析において，反例の候補が偽反例であることが分2 で求めた，各バスの各抽象状態における到達条件およびかった場合，精錬を行う．精錬では，その偽反例を導出す
を構築
出発条件を利用し，前方からブレフィックスに対する出発 る原因となった抽象パスを持たない抽象モデル$\lambda 4^{\phi}$

条件と到達条件を timesucc または iscrete-succ 演算によっ$d$

できる新しい述語$\Psi$

を導出する．

て計算する．具体的には，ある 1 つのロケーションと，そのロケーショ
もし実行中にゾーンが false になれば (line:15-17) 偽反 ンに追加するための 1 つ以上の述語を導出する．述語は，あの情報を用いて精錬を行う る 2 つのゾーンを分割可能な述語とする．
例と判断し，$l_{i,\omega},$$\zeta_{\omega_{-5h}}^{dep}!’\zeta_{1,\omega^{1}}^{dep}$(line:16)
全てのブレフィックスの出発条件および到達条件が false
でなければ，exists と出力され (line:27). 「例が存在する

事が分かり，確率到達可能性問題に対して yae と答える

6.1
6.1.1

パス反例解析による精錬$\#$$\omega(i)$の 出発条件$\omega^{t}$が falae になった場合

から $\omega(i+1)$ への遷 移が抽象モデル構築において$\omega\#(i+1)$ に含まに含まれる状態から構築されるのは，$\#$$\omega(i)$$\omega^{\phi}(i)$ことができる．

$\zeta^{d\epsilon p}$

$\#$

35
め，図 4 では$\zeta_{i,\omega^{\#}}^{dep}\ovalbox{\tt\small REJECT}$を導出するためにはこ含まれる状態から$\omega_{1}^{\#}$に AX 応するパス$\iota$に含まれる状態へ遷移する確率$\zeta_{i+1,\omega_{1}^{\#}}^{r\omega}$

分布を選択しなければならず， に対応するパスを導出す$\omega_{2}^{\#}$

るためには，$\zeta_{i,\omega_{2}^{\#}}^{dep}$に含まれる状態へ時間$\mathscr{E}\grave$

移し，そこからに含まれる状態へ遷移する確率分布を選択しなければならない．つまり，両方のパスを導出可能な確率分布は存在しないことになる．従って，これらのパスを導出可能
なアドバサリが存在しないことが分かる．
$\zeta_{i+1,\omega_{1}^{\#}}^{r\infty}$A

このように， 応するパス集合を同一のアドバサリによっ$\iota$$\lambda$て実行できない事が分かった場合，

図 4: 同時実行反例解析における精錬と$\zeta_{\#}^{dep}$$\zeta_{i,\omega\#}^{dep}$

を分割す$\omega_{l}$ることで精錬を行う．なぜなら，これらを分割する述語を加のゾーン内に隠れていたれる状態への遷移が存在するためであるが，このパスを実 えることで，これまで行するための状態間には遷移が存在しない事が原因である． と間の時間遷移が抽象モデル上に確率分布として現わ$\omega^{\phi}(i)$$\zeta_{\omega_{-\cdot h}^{\#}}^{dep}$$\zeta_{i,\omega\#}^{dep}$

よって，この抽象状態のゾーン

をを含むゾーンと $discrete_{-}succ(\zeta_{i,\omega\#}, \zeta^{g}, X)$ または $time_{-}succ(\zeta_{i,w^{l}})$遷移が時間を含むゾーンに分割することで，このパスを取り除くこと

解析の

ができる．

612

$\zeta_{0_{\omega}\#}^{oea}$と$\zeta_{0}$象パス$\omega\#$$\zeta_{i+1,\omega t}^{oea}$$A\#$$\mathscr{E}\grave$(図 4 では，$\zeta_{i,\omega_{1}^{\#}}^{dep}$から$\zeta_{i,\omega_{2}^{\#}}^{dep}$

への

$x$ 例
移としてモデル上に現われた). よって，「
またはを含む抽象状の導出において，$\zeta_{\omega_{sim th}}^{dep}\#$$\zeta_{i,\omega}^{dep}\#$態は，これまで存在した抽象確率分布に加え，この新たに現われた時間遷移の抽象確率分布を選択できるようになり，から始まる．よって，全 これらの確率分布からいずれか 1 つが選ばれるため，同様$\zeta_{0}=\{\nu_{0}\}$$\nu_{0}$を含む抽象状態から始まるが，抽の最初の抽象状態$\omega\#(0)$の到達条件

まれていないため，具体モデルでは初期状態$\zeta_{0,\omega\#}^{rea}$$\nu_{0}$}こ$\zeta_{0}$

含

からこのパ

スを実行できないことがわかる．
をを含むゾーン
よって，この抽象状態のゾーンを含むゾーンに分割することで，このパスを取り除$\zeta_{0,\omega\#}$とれるようになるためであるの積が false になった場合

具体モデル上の全てのパスはての抽象パスは$\zeta_{i+1,\omega\#}$$(0$の同時実行の問題は発生しない．

6.3

新たな述語の導出と検証の停止性

定理 6.1(サイクル毎に新たな述語を導出可能). 確率時間
CEGAR は，到達可能性問題の解が得られるまで，サイクル毎に新たな述語を導出可能である．

$\zeta_{0,\omega\#}^{na}$くことができる．

6.2

同時実行反例解析による精錬
同時実行反例解析では， が false になることと，反$\zeta_{\#}^{dep}$$\omega_{\ovalbox{\tt\small REJECT}\ovalbox{\tt\small REJECT}\ovalbox{\tt\small REJECT}}$

例の候補である全てのパスを同じアドバサリで実行できな
いことは同値である．図 4 を用いてこれを説明する．抽象パス$\omega_{1}^{\#}$

および$\omega_{2}^{\#}$

はそれぞれの共通のブレフィヅクス$\omega_{i}^{\#}$

番目までの遷移においてを持つとし，$i+1$ 番目の遷移$i$において，初めて異なる抽象状態へ遷移するものとする．
パス反例解析の Algorithml および Algorithm2 によって，$\zeta_{i+1,\omega_{1}^{\#}}^{rw}$に遷移可能な状態集合として，$\zeta_{i,\omega_{1}^{\#}}^{dep}$

つまりく id,epl# こ含まれる状態からのみ$\ovalbox{\tt\small REJECT}$$\omega$$\zeta_{i+1,\omega_{1}^{\#}}^{oea}$を定理 62(検証の停止性). 確率時間 CEGAR による検証は有限回数のサイクルで解を得ることができる．

7

実験
本章では，確率時間 CEGAR のプロトタイプを Scala によって実装し，実験を行って既存手法とその状態数について比較する．

7.1

述語の選択

確率時間 CEGAR を実装するにあたり，精錬における述

p- 算した． 語選択のアルゴリズムを決定する必要がある．ゾーンの実$\equiv$$+$に含まれる状装として DBM を用いることで，ゾーンによって表される

領城の辺を容易に取り扱うことができる．これを利用し，$\grave{L}_{-}^{J\backslash }t^{\sim}$態へ遷移できる． についても同様である．よ って，に含まれるが， こは含まれない状態からは遷移できない．
$\omega_{2}^{\#}$$(_{i,w_{1}^{\#}}^{dep}$$\zeta_{i,\omega_{2}^{\#}}^{dep}\ovalbox{\tt\small REJECT}$$\zeta_{i+1,\omega_{2}^{\#}}^{m}$

語の選択は以下のアルゴリズムにより行う．
へ

1. 分割したい 2 つのゾーンを構成する辺を元とする集合

から案集合を得る
アドバサリは，あるパスを入力することで次の遷移における時間遷移量と確率分布を返すものであった．すなわち， 2. その案集合の元のうち，要素が少ないものから順に，2つのゾーンが分割できるものを探す
あるアドバサリが存在するとは，全ての状態においてその
CEGAR における述語抽象化では，分割に用いる述語の増時間遷移量と確率分布が一意に決まる事を意味する．
と
ところが，
の両方へ

$\zeta_{l}^{dep}$$\zeta_{i,\omega_{1}^{\#}}^{dep}$とに共通部分が無い場合，加に応じて抽象モデルの状態数が増える．そのため，この$\zeta_{i+1,\omega_{1}}^{na}\#$l,

ロ能な状態は存在しない．そのた$\omega\tau$$\mathscr{E}\mathscr{C}$$\zeta_{i+1,\omega_{2}^{f}}^{rea}$

アルゴリズムは，2 つのゾーンを分割可能な述語の組み合36MC$\frac{D}{2000}$
PT

4000
6000
8000
10000
20000
30000
40000
50000
60000

$CEGAR10$$Symbolicl5$

14
18
22
26
46
63
78
93

1206
2168
3426

108

4964

状態 比

25
47

81
126
528

$\bigoplus_{66}$0.56000.38300.27160.20630.0871
0.05220.03600.0271
0.0218

表 1: 状態数の比$x: FireWire root contention protocol

わせのうち，より少ない数の述語で分割しようとするものである．

さらに，述語として $x_{1}-x_{2}\leq d$ や $x_{1}-x_{2}<d$ のような diagonal 制痢を優先して用いる．これは，diagonal 制約を用いないと，分割した状態間に時間遷移が生じる場合があり，これに起因して必要のない状態が生成され，状態数が増加することが考えられるためである．

72

実験モデルの制限

DBM のように，モデルに表れる最大定数を用いてゾーンを表現する場合，前方解析が正しく行えない事が知られているため [3], 本実験では，クロック変数が 3 以下のモデノレのみを対象とする．

7.3

FireWire root contention protocol

本実験では Symbolic model cheddng[10] で対象とされている IEEE 1394 FireWire root contention protocol に対し，

デッドラインが 2000 から 60000 まで同様の性質，すなわち等価な到逢可能性問題を( , {elect}) について検$(\lambda, L_{\epsilon})=$$O$

証することで，その状態数の比較を行う．

74

実験結果

表 1 に実験結果を示す．全ての Dead Line について，既存手法よりも少ない状態数で検証を終えている．また，状態数比の推移から，Dead Line の増加に伴い，状態数がより削減されていることがわかる．

8

まとめ
本論文では，確率時間オートマトンの到達可能性解析において，CEGAR による枠組みを適用した検証手法を確立した．本論文の主な貢献は以下の 3 点である．

.

.
.

確率時間オートマトンにおいて，確率分 による複数パスの同時の実行可能性を同時実行反例解析として判$\mathbb{R}$定し，偽反例による抽象モデルの精錬手法を実現した
本手法を実装して実験を行い，既存手法と比較し，より少ない状態数での検証が可能であることを示した

参考文献[1] Bengtsson, J. and Yi, W.: Timed Automata: Semantics, Algorithms and Tools, LNCS, Vol. 3098, pp. 87-

124 (2004).
[2] Bianco, A. and de Alfaro, L.: Model checking ofprobabilistic and nondeterministic systems, LNCS,
Vol. 1026, pp. 499-513 (1995).
[3] Bouyer, P.: Untameable Timed Automata!, LNCS,
Vol. 2607, pp. $62t\vdash 631$ (2003).
[4] Clarke, E. M., Grumberg, O. and Peled, D.: Model
Checking, MIT (2000).
[5] Clarke, E. M., Fehnker, A., Han, Z., Krogh, B. H.,
Ouaknine, J., Stursberg, O. and Theobald, M.: Abstraction and CounterexampleGuided Refinement inModel Checking of Hybrid Systems, IJFCS, Vol. 14,
No. 4, pp. 583-604 (2003).

[6] Clarke, E. M., Grumberg, O., Jha, S., Lu, Y. andVeith, H.: Counterexample-Guided Abstraction Refinement, LNCS, Vol. 1855, pp. 154-169 (2000).
[7] Graf, S. and Sa’idi, H.: Construction of Abstract
State Graphs with PVS, LNCS, Vol. 1254, pp. 7283 (1997).

[8] Han, T. and Katoen, J. P.: Counterexamples in probabilistic model checking, LNCS, Vol. 4424, pp. 72-86(2007).
[9] Hemanns, H., Wachter, B. and Zhang, L.: Probabilistic CEGAR, LNCS, Vol. 5123, pp. 162-175(2008).
[10] Kwiatkowska, M., Norman, G., Sproston, J. andWang, F.: Symbolic model checking for probabilistic timed automata, Information And Computation,
Vol. 205, No. 7, pp. 1027-1077 (2007).

[11] Moller, M. O., Rues, H. and Sorea, M.: Predicate
Abstraction for Dense Real-Time Systems, Electronic
確率時間オートマトンの到達可能性解析において，CB
Notes in Theoretical Computer Science, Vol. 65,
GAR を導入することにより，検証対象に応じた状態空No. 6, pp. 218-237 (2002).
間の構築を可能にした