修士学位論文

題目

時間抽象を行う洗練手法を用いた
確率時間システムの到達可能性解析手法

指導教員
楠本 真二 教授

報告者
伊藤 明彦

平成 22 年 2 月 8 日

大阪大学 大学院情報科学研究科
コンピュータサイエンス専攻

平成 21 年度 修士学位論文

時間抽象を行う洗練手法を用いた確率時間システムの到達可能性解析手法
伊藤 明彦

内容梗概
モデル検査は，システムの設計段階での不具合の発見に有用である．そのため，システムの高信頼設計において適用されるようになってきている．ネットワークシステムのような，振る舞いに確率的な要素を含むシステムの場合，そのシステムが不具合を示す確率を計測することが非常に重要であり，そのシステムの信頼性を計測するために必要不可欠な性質であると考えられる．さらにそれが実時間のシステムであれば，時間的な制約を持ち，状態数が時間制約に応じて指数的に増加するため，検査に対するスケーラビリティに大きな制約が加わる．一方，Clarke らが古典的な Kripke 構造を持つオートマトンに対して反例に基づく抽象化洗練 CEGAR を提案し，状態爆発を回避しながらモデル検査を自動で行う枠組みを提案した．この枠組みは時間オートマトンをはじめとして，多くのオートマトンモデルに対しての有用性を示した．
既存研究として，時間オートマトンに対する抽象化洗練手法が提案されている．その手法に基づいて，本研究では確率時間オートマトンの CEGAR を用いた到達可能性解析を行う手法を提案する．ただし，確率時間システムでは，反例となるパスの組み合わせが各ロケー
ションにおける時間経過によって変動するため，単純に複数個のパスの探索では正しい反例を提示できない．本研究では，そのパスの組み合わせを決定するために，元モデルの等価変換を行うことで解決している．
本論文では，実際の確率時間オートマトンに対して適用し，提案手法の概要を示したの
ち，また提案手法の具体的なアルゴリズムを形式的に記述し，提案手法の正当性を示す．さらに，提案手法の部分的な実装を行い，状態数や実行時間などで，手法について比較考察を行う．最後に，今後の課題とまとめについて述べる．

主な用語
確率時間オートマトン, 時間オートマトン, マルコフ決定過程, 離散時間マルコフ連鎖, CEGAR
ループ, モデル検査，到達可能性解析

目次
1 まえがき

1

2 準備

3

2.1

確率分布 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

3

2.2

確率オートマトン . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

3

2.2.1

離散時間マルコフ連鎖 (DTMC:Discrete Timed Markov Chain) . . . . .

3

2.2.2

マルコフ決定過程 (MDP:Markov Desicion Process) . . . . . . . . . . .

4

2.2.3

連続時間マルコフ連鎖 . . . . . . . . . . . . . . . . . . . . . . . . . .

4

確率オートマトンの性質 . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

4

2.3.1

PCTL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

5

2.3.2

CSL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

6

2.4

確率的モデル検査 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

7

2.5

マルコフ決定過程のモデル検査手法 . . . . . . . . . . . . . . . . . . . . . . .

7

2.6

クロック変数とゾーン . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

8

2.7

時間オートマトン . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

8

2.3

2.8

2.9

2.7.1

時間オートマトンの意味 . . . . . . . . . . . . . . . . . . . . . . . . . 10

2.7.2

確率時間オートマトンの状態空間の表現 . . . . . . . . . . . . . . . . 10

2.7.3

Clock Zone と DBM . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

確率時間オートマトン . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12

2.8.1

確率時間システム . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12

2.8.2

確率時間オートマトン . . . . . . . . . . . . . . . . . . . . . . . . . . 12

2.8.3

well-f ormed な確率時間オートマトン . . . . . . . . . . . . . . . . . 14

確率時間オートマトンの同時実行可能性 . . . . . . . . . . . . . . . . . . . . 14

2.10 CEGAR loop . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.11 時間オートマトンの抽象化洗練手法 . . . . . . . . . . . . . . . . . . . . . . . 16
3 関連研究17

3.1

forward Reachability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

3.2

backward Reachability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

3.3

Digital clocks[19] . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

3.4

Stochastic game based . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19

3.5

その他の手法 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19i

4 提案手法

20

4.1

初期抽象化

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21

4.2

モデル検査

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21

4.3

シミュレーション . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21

4.4

抽象モデルの洗練 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21

4.5

同時実行可能性の検査 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

4.5.1

後方シミュレーション . . . . . . . . . . . . . . . . . . . . . . . . . . 22

4.5.2

同時実行可能性の判定 . . . . . . . . . . . . . . . . . . . . . . . . . . 25

4.6

同時実行可能性を考慮したモデル変換 . . . . . . . . . . . . . . . . . . . . . . 25

4.7

確率時間オートマトンの変換例 . . . . . . . . . . . . . . . . . . . . . . . . . 27

4.8

モデルの等価性に関する証明 . . . . . . . . . . . . . . . . . . . . . . . . . . . 31

5 実験

33

5.1

実験の目的

5.2

実験環境 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33

5.3

実験対象となる確率時間オートマトン . . . . . . . . . . . . . . . . . . . . . . 33

5.4

実験方法 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34

5.5

実験結果 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35

5.6

考察 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33

5.6.1

メモリ消費量・状態数 . . . . . . . . . . . . . . . . . . . . . . . . . . 36

5.6.2

実行時間 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36

5.6.3

パス数 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37

6 評価

38

7 あとがき

39

謝辞

40

参考文献

41

ii

図目次
1

時間オートマトン . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

2

確率時間オートマトンの例 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13

3

CEGAR ループ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

4

Digital clocks で表した確率時間オートマトン . . . . . . . . . . . . . . . . . . 18

5

Stochastic games for Verification 概要 . . . . . . . . . . . . . . . . . . . . . . . 19

6

提案手法 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20

7

出発条件に対する遷移関係 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30

8

変換後の確率時間オートマトン . . . . . . . . . . . . . . . . . . . . . . . . . 30

9FireWire Root Contention Protocol (Abstract) Deadline100 . . . . . . . . . . . . 34

iii

9

表目次
1

FireWire Abst モデルの実験結果 . . . . . . . . . . . . . . . . . . . . . . . . . 35

2

FireWire Abst モデルの実験結果（k 個の探索まで実行した場合） . . . . . . . 36

iv

1 まえがき
近年, 情報システムの高信頼設計にモデル検査 [4][8] を利用することが望まれている．モ
デル検査によって，設計されたシステムのシステムの振る舞いに関する不具合を早期に発見できることが期待されるためである．モデル検査は，システムを有限の状態遷移系として形式的に記述し，また検査を実行する性質を論理式で入力することで，状態遷移系の全状態を網羅的に探索する．それにより，設計されたシステムが仕様（性質）を満たしているかど
うかを保証する手法である. しかし, 大規模なシステムに対しては状態数爆発を起こすなど,
スケーラビリティの低さが課題となっている．モデル検査のスケーラビリティの低さを改善する手法として, 検査する性質ごとにモデルの状態数を適切に削減し，さらにはその抽象化の度合いを自動的にコントロールするモデル抽象化手法が注目されている [17][29]．とりわけ，モデル検査時における反例を用いて抽象度を自動コントロールする CEGAR(Counter

Example Guided Abstraction Refinement) ループが大きな注目を浴びている [7]．
実際に検査対象となるモデルとしては，ネットワークプロトコルなどのランダム性を持つモデルを検証する場合，確率モデルが用いられる．確率モデルとは，有限の状態遷移系に，
状態遷移確率を付加したモデルである．確率モデルの最も代表的なものに，マルコフ決定過程 [28] が挙げられる．確率モデルを検査するための代表的なツールとして，確率的モデル
検査ツール PRISM[16] があり，これを用いて実際のネットワークシステムの検証が広く行われている [12][21][24]．
さらに，この確率モデルに実時間の性質が加わった確率時間システムの動作検証には，確率時間オートマトンと呼ばれるモデルが用いられる．確率時間オートマトンでは, 有限のロケーションと呼ばれる状態に，実数値をとるクロック変数を用いた制約が付加されるため，
確率時間オートマトンは無限の状態空間を持つことになる．モデル抽象化を行わない従来のモデル検査では時間領域が実質有限個に抑えられることを利用し有限状態のモデルに対し検査を行う．しかし，この状態数はロケーションやクロックの個数に対して指数的に増加する
ため，状態数を適切に縮小するモデル抽象化手法が必要となる．本研究では，文献 [22] で定義されている一般的な確率時間オートマトンを対象としており，時間オートマトンにおけるクロック変数を除去する時間抽象を行う抽象化洗練手法 [23][25][26] を，確率時間オート
マトンの抽象化洗練手法として拡張した手法を提案する．確率時間オートマトンの時間抽象化を行うことで，確率モデルに変換し，確率モデルの反例を探索する手法 [1][13] に基づいて反例を探索することができる．
ただし，確率時間オートマトンの一般的な性質に対する反例というのは，時間オートマト
ンにおける CEGAR とは異なり，確率的な性質を検査したい場合，性質を満たさないパス 1
つだけでなく，反例が複数個のパスを含む場合が存在する．このため，パスが複数個にわた1

る場合，反例となるパス群の同時実行可能性について考慮しなければならない．確率時間
オートマトンでは非決定的に時間経過が行われるため，それらのパスが同時に実行されることは無いからである．
この問題があるため，単純に従来の CEGAR の手法を適用できない．よって，提案手法の中で，元の確率時間オートマトンの変換を繰り返し，同時実行不可能なパスを明確化することで，抽象モデル上で同時に発見されないようにする変換手法を考案した．
よって，本手法を利用することで，CEGAR の枠組みを用いた確率時間オートマトンのモデ
ル検査を実行することができる．本研究では，手法のために必要なアルゴリズムの定義を行い，手法の理論的な正しさに関する議論を述べている．さらに，提案手法を実現するツールのプロトタイプを作成し，評価を行った．実験として，既存手法の一つである Digital cloks[19]との比較を行った．実験対象として用いたモデルは，FireWire Root Contention Protocol[15]，である．実験結果として，状態数を大幅に削減し，実行時間も削減することができた．
以下 2．では，まずモデルとして利用されるオートマトン（確率オートマトン，時間オート
マトン，確率時間オートマトン）について述べる．また，本研究でも利用する CEGAR ルー
プについて，さらにモデル検査によって調べられる性質について述べる．次の 4．では，確率時間オートマトンに対する一般的なモデル検査についてと，その検査を行う既存手法，さらに本研究で提案する手法について説明する．5．では，提案手法を実装し，実際のモデルへの適用実験を行った結果を紹介する．6．では，5．で行った結果を元に，本研究での提案手法の有用性について考察する．

2

2 準備
2.1 確率分布
有限集合 Q 上の（離散的な）確率分布は関数 µ : Q → [0, 1] によって割り当てられ，∑q∈Q µ(q) = 1 である．support(µ) を q ∈ support(µ) である Q の部分集合とし，かつその時に限り µ(q) > 0 である．無限集合 Q∞ において，Dist(Q∞ ) を Q∞ の有限部分集合上の確率分布の集合とする．

2.2 確率オートマトン
確率オートマトン [27] は，有限状態数のオートマトンに対し，状態遷移を行う条件に，確率の値を付加しているものである．確率オートマトンは，以下 3 つのオートマトンに大別される．

• 離散時間マルコフ連鎖 (DTMC:Discrete Timed Markov Chain)• 連続時間マルコフ連鎖 (CTMC:Continuous Timed Markov Chain)• マルコフ決定過程 (MDP:Markov Desicion Process)2.2.1 離散時間マルコフ連鎖 (DTMC:Discrete Timed Markov Chain)
定義 2.1 (離散時間マルコフ連鎖の構文). マルコフ連鎖 DTMC は 4 項組 DTMC = (S, s̄, P, L)によって定義される．

• S ：状態の有限集合• s̄ ∈ S ：初期状態• P : S × S → [0, 1]：確率遷移行列• L : S → 2AP ：ラベル付け関数
要素 P は，状態 s から ′s への遷移確率を与える行列である．s ∈ S であるすべての状態∑に対し， s∈S P = 1 である必要がある．終端となる状態は，自身へのループ（確率が 1 で同じ状態への遷移）を付加することでモデル化される．ラベル付け関数 L は，AP 中の原子
命題式を状態から状態への写像を与える．

3

2.2.2 マルコフ決定過程 (MDP:Markov Desicion Process)定義 2.2 (マルコフ決定過程の構文). マルコフ決定過程 MDP は以下の 4 項組 MDP = (S, s̄, Steps, L)
によって定義される．

• S ：状態の有限集合• s̄ ∈ S ：初期状態• Steps : S × S → [0, 1]：遷移関数• L : S → 2AP ：ラベル付け関数
集合 S ，初期状態 s̄ とラベル付け関数 L は，DTMC と同様である．確率遷移行列 P は，

Steps によって代替される．これは，各 s ∈ S を Dist(S) の空でない部分集合にマッピングする関数である．すなわち，すべての確率分布の集合である．直観的に，状態 s ∈ S に対し，Steps(S) の要素は，「非決定的な選択」を表している．各々の非決定的な選択は，他の状態への遷移の可能性を与える確率分布である．

2.2.3 連続時間マルコフ連鎖
定義 2.3 (連続時間マルコフ連鎖の構文). 連続時間マルコフ連鎖 CTMC は以下の 4 項組

CTMC = (S, s̄, R, L) によって定義される．
• S ：状態の有限集合• s̄ ∈ S ：初期状態• R : S × S →：遷移割合行列• L : S → 2AP ：ラベル付け関数
S ，̄
s と L に関しては DTMC と同様である．しかし，遷移割合行列 R に関しては，確率，でなく状態間の遷移を決める割合を与える．

2.3 確率オートマトンの性質
本節では，確率オートマトンの性質を明確化するための一般的な形式を示す．PCTL は

DTMCs，MDPs によって解釈され，CSL は CTMCs によって解釈される．

4

2.3.1 PCTL
PCTL(Probabilistic Computational Tree Logic)[14] は，時相論理 CTL の確率的な拡張である．本来は，pCTL[3] と同様なものである．PCTL の文法は以下のように与えられる．

ϕ := true | a | ϕ ∧ ϕ | ¬ϕ | P◃▹p [ψ](1)ψ := Xϕ | ϕ U ≤k ϕ | ϕ U ϕ(2)

ここで，a は原子命題式，◃▹∈ {≤, <, >, ≥}, p ∈ [0, 1] であり，k ∈ N である．PCTL 式は，

DTMC，MDP 上で解釈される．原子命題式 a はこの DTMC，MDP の各状態にラベル付けす
るために使用される集合から用いられる．
これらの文法では，状態式 ϕ とパス式 ψ を区別しており，それぞれ状態，パス上において評価される．モデルに性質は，常に状態式において表現される．パス式は確率的なパスオ
ペレータ P◃▹p [ψ] のパラメータとしてのみ表記される．直観的に，もし状態 s までのパスが

ψ を満たしているならば，状態 s は P◃▹p [ψ] を満たす．
パス式として，X(next)，U ≤k (until)，U(bounded until) オペレータを用いている．これ
らは時相論理において基準となるものである．直観的に，ϕ が次の状態で満たされる場合にXϕ が真となり，ϕ1 U ≤k ϕ2 では，ϕ2 が k ステップまでに満たされ，ϕ1 がその状態まで真であり続ける場合に，真となる．ϕ1 U ≤k ϕ2 は，ϕ2 が任意の点で真となり，ϕ1 がその状態まで真であり続ける場合に，真となる．

PCTL over DTMC
DTMC(S, s̄, P, L)，状態 s ∈ S と PCTL 式 ϕ に対し，ϕ が s において満たされることを，s |= ϕ と表記する．また，Sat(ϕ) によって，ϕ を満たすすべての状態の集合 {s ∈ S | s |= ϕ}を示す．同様に，パス式 ψ を満たすパス ω に対し，ω |= ψ とする．ここで，DTMC に対す
る PCTL の意味定義を以下で与える．パス ω に対して，

ω |= Xϕ⇔ ω(1) |= ϕ

ω |= ϕ1 U ≤k ϕ2 ⇔ ∃i ≤ k . (ω(i) |= ϕ2 ∧ ω(j) |= ϕ1 ∀j < i)
ω |= ϕ1 U ϕ2

⇔ ∃k ≥ 0 . ω |= ϕ1 U ≤k ϕ2

5

そして，状態 s ∈ S に対し，

s |= true

for all s ∈ S

s |= a⇔ a ∈ L(s)s |= ϕ1 ∧ ϕ2 ⇔ s |= ϕ1 ∧ s |= ϕ2s |= ¬ϕ⇔ s ̸|= ϕs |= P◃▹p [ψ]⇔ ps (ψ) ◃▹ p

ここで，ps (ψ) = P rob({ω ∈ P aths | ω |= ψ}) である．確率 P robs は，パスの集合に確率を割り当てる．

PCTL over MDP
パスの集合の確率は，特定のアドバーサリに対し計算される．pA
s (ψ) によって，アドバーサA
リ A の元でパス式 ψ を満たす s からのパスの確率を示す．すなわち，pAs (ψ) = P robs ({ω ∈P athAs | ω |= ψ})．セマンティクスを与えるために，アドバーサリ Adv のクラスを選択す
る．もしすべてのアドバーサリ A ∈ Adv において pAs (ψ) ◃▹ p ならば，状態 s は P◃▹p [ψ] を満たす．それ故に，この充足関係はアドバーサリ Adv のクラスによってパラメータ化される．

s |=Adv trues |=Adv a

for all s ∈ S⇔ a ∈ L(s)s |=Adv ϕ1 ∧ ϕ2 ⇔ s |= ϕ1 ∧ s |= ϕ2
s |=Adv ¬ϕ⇔ s ̸|= ϕs |=Adv P⇔ pA
s (ψ) ◃▹ p f or all A ∈ Adv

2.3.2 CSL
CSL(Countinuous Sthochastic Logic) の論理は，PCTL と似ているが，CTMC モデルにおける性質を明確化するためのものである．

ϕ ::= true | a | ϕ ∧ ϕ | ¬ϕ | P◃▹p [ψ] | S◃▹p [ϕ](3)ψ ::= Xϕ | ϕ U ≤t ϕ | ϕ U ϕ(4)

ここで，a は原子命題式，◃▹∈ {≤, <, >, ≥}, p ∈ [0, 1] であり，t ∈ N≤0 である．PCTL 式に対し，P◃▹p [ψ] は，制限 ◃▹ p を満たす状態から，パス式 ψ が満たされる確率を示す．パス式
は，CSL に関しても PCTL と同様であるが，bounded until オペレータ ϕ1 U ≤t ϕ2 のパラメー
タ t においては，PCTL のように非負の整数ではなく，非負の実数である．この式は，ϕ2 が6

[0, t] 内の任意の時間で満たされ，ϕ1 が先行しているすべての瞬間において満たされることを意味する．混乱を避けるため，time-boundeduntil としてこれを言及する．この S オペレー
タは，CTMC の定常状態の振る舞いを示す．式 S◃▹p [ϕ] は，制限 ◃▹ p で，ϕ を満たす状態に到達する定常状態の確率を表明する．

2.4 確率的モデル検査
確率的モデル検査アルゴリズムは，PCTL over DTMCs，PCTL over MDPs，CSL over CTMCsの 3 つのタイプの検査が存在する．モデル検査アルゴリズムは，PCTL もしくは CSL の論理
式 ϕ とその論理式に適合するモデルを用い，ϕ を満たす状態を含む集合 SAT (ϕ) を返す．
モデル検査アルゴリズムの大まかな構造は，3 つのケース共に同じであり，[6] によって示されている従来の CTL モデル検査アルゴリズムに由来する．最初に，式 ϕ の解析木の構成を行う．解析木における各ノードは，ϕ のサブ式によってラベル付けされる．そのルートノードは ϕ 自身によってラベル付けされ，木の葉っぱとなるノードは，true もしくは原子
命題 a によってラベル付けされる．木のルートに向かって，サブ式をそれぞれ満たす状態の集合を，再帰的に計算し，最終的に，各状態は ϕ を満たすかどうかを決定する．

2.5 マルコフ決定過程のモデル検査手法
マルコフ決定過程 MDP に対するのモデル検査手法のうち，代表的な手法として ValueIteration[5]が挙げられる．ValueIteration（Algorithm1 に示す）では，パラメータ g,f に設定された値に従って，到達可能性，安全性における最大確率値，最小確率値を計算する．例えば，f = max
であり，g = min の場合に到達可能性の最大確率を計算する．さらに，各状態において，パラメータに適合するアクションが選択されるため，ValueIteration によって求められた確率を示すアドバーサリを求めることができる．

Algorithm 1 ValIter(T, f, g, ϵf loat )v := [T ]repeatv̂ := v
for all s ∈ S do∑v(s) := f ([T ](s), g{ s′ ∈S p(s, a, s′ ) · v̂(s′ ) | a ∈ Γ(s)})

end foruntil ||v − v̂|| ≤ ϵf loat
return v

7

2.6 クロック変数とゾーン
確率時間オートマトンモデルでは，非負数の実数の集合 R 上の値である，クロック変数を使用する．クロック変数の有限集合 X を 1 つ定めるする．関数 v : X → R は，クロック評価として参照される．すべてのクロック評価の集合は，RX を意味する．また，すべてのクロック変数の値が 0 であるようなクロック評価を ν0 とする．
任意の v ∈ RX ，t ∈ R と X ⊆ X に対し，t と，0 にリセットする X 中のクロックを評価するための v[X := 0] および，すべてのクロック変数をインクリメントする v においてクロック評価を意味する，v + t の 2 つを使用する．

X のゾーンの集合を Zones(X ) と記述し，文法的に以下のように定義する．
ζ ::= x ∼ c | x − y ∼ c | ζ ∧ ζ | true
ここで，x, y ∈ X であり，∼ ∈ {<, 6, >} である．ゾーン ζ は，ζ を満たす（v ◃ ζ を意味する）クロック評価 v の集合を示す．すなわち，v(x) で true となる各クロック x の代替として，ζ を用いる．

2.7 時間オートマトン
時間オートマトンは，有限状態数のオートマトンに，時間経過を表すクロック変数を付加したオートマトンである．本節では，時間オートマトンに関する定義を与えている
定義 2.4 (時間オートマトンの構文). 時間オートマトン TA は，次のタプル TA = (A, L, l0 , C, I, T )によって定義される．各項目は以下のように定義される．

• A：アクションの有限集合• L：ロケーションの有限集合• l0 ∈ L：初期ロケーション• C ：クロック変数• I : L → c(C)：ロケーションからインバリアントへの写像• T ：遷移集合
遷移集合 T は T ⊂ L × A × c(C) × 2C × L を満たす．
a,g,r

遷移 t = (l1 , a, g, r, l2 ) ∈ T を l1 −→ l2 と表記する．g をガード，r をリセットクロックと
呼ぶ．

8

hi
x>=2
x:=0, y:=0

x<=3
x>=2
x:=0

wr

wi
x>=2
x:=0,y:=0y<=1

x<=3 && y<=7

x:=0
x>=2
y==7
x:=0, y:=0
aa

ri

x:=0, y:=0
図 1: 時間オートマトン9定義 2.5 (クロックの評価関数). ν : C → R≥0 なる ν をクロックの評価関数と呼ぶ.

d ∈ R≥0 に対して (ν + d)(x) = ν(x) + d と定義する.
r ∈ 2C に対して r(ν) = ν[x 7→ 0], x ∈ r と定義する.
g ∈ c(C) に対して g(ν) を ν の各クロックの評価のもとでの, g の評価と定義する.
また, 0C で x ∈ C なる各クロック x に対する値を 0 とするクロック評価関数を表すとする.

ν の全てからなる集合を N ⊆ RC
≥0 とする．
2.7.1 時間オートマトンの意味
定義 2.6 (時間オートマトンの意味). 時間オートマトン A = (A, L, l0 , C, I, T ) に対して

A の状態集合を S = L × N とする．
A の初期状態は (l0 , 0C ) ∈ S で与えられる．
a,g,r

状態遷移 l1 −→ l2 (∈ T ) に対し，次の 2 つの遷移が定義される．
a,g,r

l1 −→ l2 , g(ν), I(l2 )(r(ν))
a(l1 , ν) ⇒ (l2 , r(ν))∀d′ ≤ d I(l1 )(ν + d′ )d(l1 , ν) ⇒ (l1 , ν + d)
前者を離散遷移, 後者を時間遷移と呼ぶ.
定義 2.7 (時間オートマトンの意味モデル). 時間オートマトン A = (A, L, l0 , C, I, T ) に対して上記の意味づけのもとで，初期状態から始まる，(状態数無限の) 状態遷移系を定義できる．
これを T (A ) で表記する.
一般に確率時間オートマトンを考えるときは, ゼノンのパラドックスを回避するため以下の性質 (Non-Zeno) を仮定する．
定義 2.8 (Non-Zeno). 有限の時間内に発生する離散遷移は有限個である．

2.7.2 確率時間オートマトンの状態空間の表現
確率時間オートマトンの無限の状態空間の表現方法として，ゾーンと呼ばれる表現を用いている．ゾーンはクロックに関する制約の集合であり，ゾーンが持つ制約を満たす全ての状態を表現する．確率時間オートマトンが持つ状態空間は有限個のゾーンから構成されるゾーングラフで表現することができる．また，ゾーンが持つ制約の集合は，DBM(Difference

Bound Matrix) とよばれる行列として表現することができる [2][9]．DBM では，時間制約が一般に 2 クロック変数の差分不等式の集合で表されることを利用し，確率時間オートマ

10

トンが持つ n 個のクロックに対して (n + 1) × (n + 1) の行列として全ての制約を表現す
る．DBM のクロック制約を満たす全ての解の空間を D とすると，時間オートマトンの状態集合として (l, D) = ∪u∈D (l, u) として表現することとする．また，全ての l ∈ L に対して

Dlinv = ∪u∈I(l) u と表現する．
2.7.3 Clock Zone と DBM
本質的にクロックの値が非負であることに注意するとクロック制約式は以下の形で表すことができる．
∧x0 = 0 0≤i̸=j≤n xi − xj ∼ ci,j
ここで ∼ は ≤ または <, ci,j は非負実数である. また x0 は一クロックの制約式も 2 クロッ
クの差分不等式として表せるよう 0 定数を表すために便宜上導入されている.
この形の表現式を Clock Zone と呼ぶ.
さらに, Clock Zone のかわりに，クロック数が n のときに n + 1 × n + 1 の行列を考え，この行列の要素として ci,j , ∼ の 2 項組を与えると DBM となる.
クロックゾーンに関して以下の操作を定義することができる.

Intersection ϕ, ψ がクロックゾーンのとき ϕ ∧ ψ(意味はこれらの論理積) もクロックゾーン
である (クロックゾーンの式の定義より自明).

Projection ϕ がクロックゾーンでクロック変数 x が ϕ において自由のとき ∃xϕ もクロックゾーンである.

Clock Reset

R をクロックの集合とする. ϕ がクロックゾーンのとき ϕ[R := 0](意味 ϕ 中のクロックのうち R に現れるクロックの値を 0 にする) もクロックゾーンである.
∧
ϕ[R := 0] は ∃xi (ϕ ∧ xi ∈R x = 0) と等価である.

Elapsing Time ϕ がクロックゾーンで t を新しいクロック変数とするとき ϕ + t もクロックゾーンである.

ϕ がクロックゾーンのとき ϕ⇑ もクロックゾーンである.
ϕ⇑ は ∃t ≤ 0(ϕ + t), ただし t は新しいクロック変数と等価である．

11

2.8 確率時間オートマトン
2.8.1 確率時間システム
定義 2.9 (確率時間システムの構文). 確率時間オートマトン PTA の意味論を示す確率時間シ
ステム TPSPTA は，ラベル付けされたマルコフ決定過程であり，以下の 4 項組 TPSP T A =(S, s0 , T Steps, L) によって定義される．
• S ：状態の有限集合• s0 ：初期状態• T Steps ⊆ S × R0 × Dist(S)：確率時間遷移関係 (s, t, µ) ∈ T Steps かつ t > 0 である
場合，µ は点分布である．

• L : S → 2AP ：状態に原子命題式を割り当てるラベル付け関数
タプル (s, t, µ) の t は，duration と呼ばれる．確率的なシステムと同様に，確率時間シス
テムに対するアドバーサリとパスを導入する．

2.8.2 確率時間オートマトン
定義 2.10 (確率時間オートマトンの構文). 確率時間オートマトン PTA は，7 項目 PTA =(L, l0 , Act, X , inv, prob, L) によって定義される．
• L：ロケーションの有限集合• l0 ：初期ロケーション• Act：アクションの有限集合• X ：クロック変数の有限集合• inv : L → Zones(X )：インバリアントを割り当てる関数• prob ⊆ L × Zones(X ) × Dist(2X × L)：確率エッジ関係をを割り当てる有限集合• L : L → 2AP ：ロケーションへ原子命題式を割り当てるラベル付け関数
確率時間オートマトンの具体例を，図 2 に示す．

12

clock x,y;

b

0.5

a

0.5
x:=0

c

1

1

x==0

d
x==0∧y==1

図 2: 確率時間オートマトンの例

定義 2.11 (確率時間オートマトンの遷移). (l, p, g) ∈ prob によって生成される確率時間オー
トマトンの遷移は，p(X, l′ ) > 0 である 5 項目 (l, g, p, X, l′ ) である．edges(l, g, p) を (l, g, p)
によって生成される遷移の集合とする．また，edges = {edges(l, p, g) | (l, g, p) ∈ prob} とする．
定義 2.12 (確率時間オートマトンの意味). 確率時間オートマトン PTA = (L, l0 , Act, X , inv, prob, L)の意味は，時間確率システム TPSPTA = (S, s0 , T Steps, L′ ) によって以下のように定義される．

• S ⊆ L × RX ，(l, ν) ∈ S かつその時に限り，ν ◃ inv(l) である．
• s0 = (l0 , ν0 )• ((l, ν), t, µ) ∈ T Steps の場合，かつその時に限り，以下に従う．
time transitions t 6 0 の時，µ = µ(l,ν+t) である．また，すべての 0 > t′ > t に対し，ν + t′ ◃ inv(l) である．

discrete transitions t = 0 であり，ν ◃ g ，すべての (X, l′ ) ∈ support(p) に対し，
ν[X := 0] ◃ inv(l′ ) である (l, g, p) ∈ prob が存在する場合，すべての (l′ , ν) ∈ S に対し，µ=∑X⊆X &ν ′ =ν[X:=0]• L′ ((l, ν)) = L(l) for all (l, ν) ∈ S

13p(X, l′ )2.8.3 well-f ormed な確率時間オートマトン
確率時間オートマトンにおける確率的な遷移が常に有効である場合に限り，その確率時間オートマトンを well-f ormed であるとする [22]．形式的には，確率時間オートマトン

PTA = (L, l0 , Act, X , inv, prob, L) が，常に以下の条件を満たせば well-formed である．

′ ′′∀(l, g, p) ∈ prob. ∀ν ∈ RX
>0 . (ν ◃ g) → (∀(X , l ) ∈ support(p). ν[X := 0] ◃ inv(l )).

確率時間オートマトンは，確率的な各遷移 (l, g, p) ∈ prob におけるガード式を置き換える
ことで，単純に well-f ormed な確率時間オートマトンに変換可能である．

(∧(X,l′ )∈support(p) [X := 0]inv(l′ )) ∧ g
この変換において，オートマトンの意味への影響は全く無い．本研究で扱う確率時間オー
トマトンは，すべて well-f ormed な確率時間オートマトンであるとする．

2.9 確率時間オートマトンの同時実行可能性
確率時間オートマトンでは，ある性質を満たす確率で構成されるパスが複数個ある場合が存在する．この時，同じロケーションを出発するパスは，同じゾーンによって遷移している必要がある．確率時間オートマトンにおける時間遷移は，非決定的な遷移であり，異なる
ゾーンで各パスが出発している場合，それらのパスは異なるアドバーサリで動作しているためである．
ここで，同時実行可能性に関する次の補題を与える．
補題 2.1 (2 つのパスの同時実行可能性). 確率時間オートマトン PTA 上の 2 つの任意のパス
pα ,tαpα ,tααpαn−1 ,tn−1

pβ ,tβpβ ,tβ

0 0
1 1
1 1
0 0
ω α = ⟨l0α , ν0β ⟩ −−−→ ⟨l1α , ν1α ⟩ −−−→ . . . −−−−−−→ ⟨lnα , νnα ⟩ と ω β = ⟨l0β , ν0β ⟩ −−−→ ⟨l1β , ν1β ⟩ −−−→βpβ
m−1 ,tm−1ββ. . . −−−−−−−→ ⟨lm, νm⟩ が以下の性質を満たすとき，ω α と ω β は同時実行可能である．

isCompatible(ω α , ω β ) = trueif( ∃i ∈ N such that ω α (i + 1) ̸= ω β (i + 1)∧∀j 6 i ∈ N. ω α (j) = ω β (j)). tαi = tβif alse otherwisetrue になる条件としては，パスにおける i 番目の状態で同じ状態のものの中で，そのロケー
ションにおける時間経過が同じものである．さらに，i + 1 番目の状態が異なるようなパスである．単純には，i 番目まで全く同一の遷移が行われ，i + 1 番目の遷移によって異なる遷

14

移が行われるものである．さらに，この補題を元に，3 つ以上のパス集合に関する同時実行
可能性についての補題を与える．
補題 2.2 (2 つ以上のパスの同時実行可能性). 確率時間オートマトン PTA 上のパス集合 Ω が以下の性質を満たすとき，Ω は同時実行可能である．

isCompatible(Ω) = true




















∧

if( ∃i ∈ N such thatω α (i+1)̸=ω β (i+1)ω α ,ω β ∈Ωαβ∧ ∧ω ̸=ωω α (j) = ω β (j)).

∧(∀j 6 i ∈ N.

ω α ,ω β ∈Ω∧∧ω α ̸=ω β
αβti = ti



β
α
ω
,ω
∈Ω



∧ω α ̸=ω β





∧(∀Ω′ ∈ 2Ω such that Ω′ ̸= Ω ∧ |Ω′ | ≥ 2).





isCompatible(Ω′ ) f alse otherwise
補題 2.1 では 2 つの場合を与えたが，補題 2.2 ではパスの集合 Ω に関するものである．

isCompatible(Ω) が true になる条件は，集合に含まれる任意の 2 つのパスが同時実行可能であり，かつその部分集合も同様である，というものである．
続いて，同時実行可能性を満たさないようなパスに関する例を与える．図 2 におけるロケーション a から d へ遷移するパスを求めた場合，ロケーション b を経由して d に遷移する
0.5,0

1.0,0

パスは，ω α = ⟨a, x = 0 ∧ y = 0⟩ −−−→ ⟨b, x = 0 ∧ y = 0⟩ −−−→ ⟨d, x = 0 ∧ y = 0⟩，とな
0.5,1り，ロケーション c を経由して d に遷移するパスは，ω β = ⟨a, x = 0 ∧ y = 0⟩ −−−→ ⟨c, x =1.0,00 ∧ y = 1⟩ −−−→ ⟨d, x = 0 ∧ y = 1⟩，となる．ω α で d へ遷移するためには，b → d の遷移に対するガード式 x == 0 が存在するため，a において時間遷移無しで動作する必要がある．
一方，ω β で d へ遷移するためには，b → d の遷移に対するガード式 x == 0 ∧ y == 1 が存在するため，a において 1 単位時間の遷移を行い，クロック変数 y を a の時点でインクリメ
ントしておかなければ d へ到達できない．
図 2 の確率時間オートマトンのようにロケーションにおける離散遷移の分岐において出発条件が異なる場合，各パスの時間的な振る舞いを考慮して反例となるパス群を考慮する必要がある．

2.10 CEGAR loop
CEGAR ループ [7] とは，CounterExample-Guided Abstraction Refinement の略であり，直訳すると反例に基づいた抽象化洗練ループである．図 3 に，一般的な CEGAR フレームワー

15クを示す．
Concrete
model

Initial Abstraction
Counter-example

property

true
property is

Model Checking

Simulation

satisfied

false
property is notsatisfiedrefined model+property
Refinement

図 3: CEGAR ループ

モデルの抽象化によって，本来の抽象化前のモデル（具体モデル）上で発見され得ない，
偽反例が発見されてしまうことがある．一般的な CEGAR ループでは，抽象化済みモデル（抽象モデル）上で発見された偽反例を具体モデル上でのシミュレーションによって確認する．この時，具体モデル上で起こり得ない反例であった場合は，抽象モデル上でその反例が二度と発見されないようにモデルの改善（洗練）を行う．この繰り返しによって，最終的に具体モデル上で発生するであろう反例を見つけ，検査を終了する．
ただし，最初のモデル検査の段階で反例が出力されなければ，over approximation を満たす抽象化に限定されているため，具体モデル上でも反例が必ず存在しない．よって，この場
合は検査結果を true として終了する．

2.11

時間オートマトンの抽象化洗練手法

著者らは [25][26] で，Clarke らの Counter-example Guided Abstraction Refinement[7] の枠組みを利用した，時間オートマトンに関する抽象化洗練手法を提案している．この手法では，時間に関する制約をすべて除去する抽象化行い，抽象モデル上で偽反例が出力された場合，抽象状態の複製によって抽象モデルの洗練を行う．

16

3 関連研究
本研究では，確率時間オートマトンに対するモデル検査手法を提案している．
ここでは，既存の確率時間オートマトンに対するモデル検査アプローチを簡潔に紹介する．

3.1 forward Reachability
forward Reachability アルゴリズム [20] は，確率時間オートマトンを前方に探索してゾー
ングラフ化することで，初期状態から到達可能なゾーングラフ（Reachability graph）を生成する．
そのグラフに対し，マルコフ決定過程と同様の到達可能性解析を実行することで，確率時間オートマトンに対する到達可能性解析を行う．
このアプローチは，DBM のようなデータ構造と共に実行することで，極めて効率的な方法であるため，有効な手法である．しかしながら，確率時間オートマトンの同時実行可能性
問題を解決できないため，この技術は最大到達確率の上限値を求めるに留まっている．

3.2 backward Reachability
backward Reachability アルゴリズム [22] もその名の通り，forward Reachability アルゴリズ
ムとは全く逆の手法で，性質を満たす集合から初期状態まで，後ろ向きに探索を行っていく手法である．
性質を満たす状態集合を生成し，その集合とモデルを元に，バックワードに状態を拡大していく．拡大された状態が初期状態まで到達した場合，そのグラフをマルコフ決定過程と同様の到達可能性解析を実行し，モデル検査を行う．この手法は，最大，最小到達確率を正確な値で計算できるが，計算コストが非常に高いために，適用範囲に限界がある．

3.3 Digital clocks[19]確率オートマトン上に，Integer の制約としてクロック変数を記述したものである（図 4）．

Integer の制約なので，本来は実数であるべきクロック変数を，自然数として記述することになる．この手法では，確率オートマトンを記述する形になるので計算は容易だが，状態数は爆発的に増加し，さらに，自然数として記述することで，元の確率時間オートマトン上で存在する状態が一部削られてしまう．よって，検査を実行する性質によっては，誤った結果を得ることになる．結局，限られたクラスの確率時間オートマトンに対してしか適用することができない．

17

a

a

x=0
y=0

a

x=1
y=1

b

x=0
y=0

c

x=0
y=0

x=2

a

x=2
y=2

b y=2

b

x=1
y=1

d

x=1
y=1

c

x=0
y=1

c

x=1
y=2

d

x=0
y=0

d

x=0
y=1

d

c

x=1
y=1

x=0
y=1

c

x=1
y=1

図 4: Digital clocks で表した確率時間オートマトン

18

x=3
y=3

3.4 Stochastic game based
上記 3 つの手法を踏まえて考案された技術がこれから示す Stochastic game verification[18]である．この手法では，forward Reachability アルゴリズムによって得られたグラフから，確率ゲームの形式に変換・修正を実行することによってグラフの洗練を繰り返していく手法である．
具体的な手法の流れは，図 5 によって示される．
input：
・PTA
・Reachability property

BuildReachGraph

BuildGame
RefineAnalyseGame

BuildGame
AnalyseGame

図 5: Stochastic games for Verification 概要

3.5 その他の手法
その他の手法として，時間オートマトンモデル検査ツール KRONOS[11] と，PRISM を組
み合わせて解析を行う手法が提案されている [10]．

19Concrete
Initial Abstraction

modelCounter-example

property

true

property issatisfiedModel Checking

Simulation

false

property is notsatisfiedrefined model+property

refined Concrete model

Refinement+property
Compatibility

Model Transformation

Checking

図 6: 提案手法

4 提案手法
本章では，本稿で提案する確率時間オートマトンの抽象化洗練手法を示す．提案する抽象化洗練手法では，著者らが [25][26] で提案した時間オートマトンの抽象化洗練手法を利用している．さらに，前節で述べた，同時実行可能性を考慮した反例を生成するために，後方シミュレーションに加えて，時間遷移を明確化したロケーションを生成することで，同時実行可能性を明確化した確率時間オートマトンを生成する．
図 6 は本稿で提案する抽象化洗練の枠組みである．図で示すように，同時実行可能性を明確化するため，一般的な CEGAR の枠組みにモデル変換のフローを追加している．入力として，確率時間オートマトン PTA，性質を与える．検査対象とする性質は，P<p [ true U err]という PCTL 式に限定する．
これは，err（エラー状態を示す）に到達する確率は p 以下である，という到達可能性解析に関するモデル検査を実行する式である．err には，PCTL の状態式に関する任意の記述
を与える．

20

4.1 初期抽象化
初期抽象化では，[25][26] と同様に，クロック変数に関する制約をすべて除去することで，over approximation を満たすように抽象化を行う．
確率時間オートマトンのクロック変数に関する制約をすべて除去するため，この初期抽象化では，確率時間オートマトンをマルコフ決定過程に変換することになる．よって，後述のモデル検査では，マルコフ決定過程の既存の検査手法を採用し，マルコフ決定過程における到達可能性解析を実行する．

4.2 モデル検査
モデル検査では，抽象モデルとして生成されたマルコフ決定過程に対して ValueIterationを適用する．
本手法では，到達可能性の最大確率を計算する手法を提案しているため，ValueIteration に入力するパラメータを，f = max，g = max に設定してモデル検査を実行する．このアルゴリズムによって計算された結果が入力された性質の p を満たしている場合，確率時間オー
トマトンのモデル検査結果を true として計算を終える．

ValueIteration では，到達可能性の最大確率を計算することが可能であるが，入力された性質の p を上回る確率を持つ場合の具体的なパス（群）を示さない．よって，抽象モデル上で反例となるパス（群）を探索するために，文献 [1] で提案されている，PCTL 式に対する反例を探索する手法を採用する．

4.3 シミュレーション
シミュレーションでは，k-最短路探索によって得られたパス（群）に対して，元の確率時間オートマトン上で実行可能かどうかを調べる．本手法では，[26] で提案されているシュミ
レーションアルゴリズムに従って，DBM の演算によって到達可能か判定する．

4.4 抽象モデルの洗練
抽象モデル上で発生した偽反例を，元の確率時間オートマトン上で発生しないように，抽象モデルの洗練を行う．本手法では，[26] で提案されている抽象状態の複製による手法を用いる．

21

4.5 同時実行可能性の検査
k-最短路探索によって得られたパス（群）が全て元の確率時間オートマトン上で実行可能
であり，かつ確率の和が与えられた確率 p を超える場合，さらにそれらのパスの同時実行可能性（補題 2.2）を調べる必要がある．確率時間オートマトンのある性質に対する反例中に同時実行可能性が存在する場合，その反例は正しくない．
そのために，反例として出力されたパス群に対し，同時実行可能性が偽となる分岐が存在しているかどうかを判定する．まず後方シミュレーションを行って，各パスを通過する各ロケーションにおいて目的ロケーションへ到達するために必要となる出発条件を求める．その後，補題 2.2 に従って，各分岐に対して同時実行可能かどうかを検査する．

4.5.1 後方シミュレーション
後方シミュレーション（Algorithm2）では 1 つのパスに対し，そのパスが通過するすべてのロケーションに対する出発条件を求める．
離散遷移 e = (lprev , ge , pe , Xe , l) に対してロケーション l から lprev への後方シミュレーショ
ンを考える．
まず，後方シミュレーションを行った際に，リセット式によって除去される制約式を求める関数を以下のように定義する．入力となる ζ は，inv(l) である．



free(ζ α , e) ∧ free(ζ β , e), if ζ = ζ α ∧ ζ β true,if ζ = x ∼ c where x ∈ Xe
free(ζ, e) =or ζ = x − y ∼ c where x ∈ Xe or y ∈ Xe




 ζ,
otherwise(5)

free(ζ, e) では，入力されたゾーン中に，遷移 e 上のリセット式 Xe に含まれるクロック変数に関する制約が含まれていた場合，その制約を除去する，という計算を行っている．

free を用いてロケーション lprev から l を示すエッジ e 上で後方シミュレーションを実行し，lprev から l に出発条件となる遷移可能なゾーンを求めると，以下のように示される．
ζ lprev = free(inv(l), e) ∧ ge ∧ inv(lprev )ここで，ζ lprev を lprev における出発条件として決定する．つづいて，lprev = l0 でなければ，
続けて後方シミュレーションを行う．この時，ζ lprev に対し，時間経過の逆算である down
演算を行い，先ほどの式を用いてシミュレーションを継続していく．down 演算を行う関数
を以下のように定義する．

22


α
β
α
β

 down(ζ ) ∧ down(ζ ), if ζ = ζ ∧ ζdown(ζ) =





true,

if ζ = x > cζ,otherwise(6)

down(ζ) では，入力されたゾーン中の下限値に関する制約についてすべて除去する，という計算を行っている．この演算によって，「時間経過後のゾーン」から，「時間経過前から時間経過後のゾーン」に拡大することができる．
以上の流れを用いて，パス ω に対する後方シミュレーションのアルゴリズムを Algorithm2
p1

p2

pn

に示す．入力には，元の確率時間オートマトン PTA と，反例候補 ω = l0 −→ l1 −→ · · · −→ lnを用いる．

Algorithm 2 BackwardSimulation(PTA, ω)
1: ζ := true
2: for i := n down to 2 do
3:{n はパス ω の長さ }4:lcurr := ω[i], lprev := ω[i − 1]5:

ζ := ζ ∧ inv(lcurr )6:

e := (lprev , g, p, X, lcurr ) {∈ edges}7:ζ := free(ζ, e) ∧ ge ∧ inv(lprev )8:Zω [i] := ζ {Zω [i] に出発条件を追加 }9:

ER := ER ∪ (l, lcurr , e, ζ){ 出発条件と遷移の関係を保持 }10:down(ζ)11: end for
12: return (Z, ER)

このアルゴリズムでは，得られたパスを後方にシミュレーションを行い，ζ lprev に対しゾーンを求めていく．
後方シミュレーションが適用されるとき，与えられるパスは既に (前方) シミュレーション
によって実行可能であると判定されているため，後方シミュレーションにおけるゾーンの計
算の中で空になることはない．
パス中の各ロケーションにおいて求められた出発条件 ζ を，Zlpath [lprev ] に追加しておく．
上記の条件を満たし，lprev = l0 であれば，シミュレーションを終える．そうでなければζ lprev に対し，時間経過の逆算を行い，ゾーンを拡大する．その後，残りの経路に基づいて上述のゾーン演算を実行していく．

23

Algorithm 3 IsCompatible(Ω, Z, index)
1: ζ := true, NSIM := ∅, N LS := ∅2: for all ω ′ ∈ Ω such that |ω ′ | > index do3:

lnext := ω ′ [index + 1]

4:

if lnext ̸∈ N LS then5:

N LS := N LS ∪ lnext

6:Ωlnext := ∅7:

end if8:Ωlnext := Ωlnext ∪ {ω ′ }9: end for
10: if |N LS| > 2 then11:

for all ω ′ ∈ Ω do12:

ζ := ζ ∧ Zω′ [index]

13:

if ζ = f alse then
NSIM := NSIM ∪ {ω ′ [index]} { 同時実行できないロケーション集合 NSIM を作成

14:

}
break

15:
16:

end if17:

end for18:

for all lnext ∈ N LS do

19:
20:

NSIM := NSIM ∪ IsCompatible(index + 1, Ωlnext )end for

21: end if
22: return NSIM

24

4.5.2 同時実行可能性の判定
後方シミュレーションによって各パス，各ロケーションの出発条件が求められたが，同時実行可能性の補題における isCompatible を満たしているかを調べる必要がある．そのために，IsCompatible（Algorithm3）を実行する．
このアルゴリズムでは，後方シミュレーションによって求められた出発条件その条件を持
つパスの集合を元に，同時実行性を検査する．最終的に，NSIM に同時実行できないロケー
ションの集合が求められる．
具体的には，抽象モデル上のパスであるロケーションの系列 ω の集合 Ω が与えられ，Ωに含まれるパスの分岐が存在するかどうかを調べる．その分岐上で出発条件を比較し，同時に実行できないと判断された場合，同時実行できないロケーションの集合 NSIM に追加される．分岐において同じ遷移を示すパスは，その集合を用いて再帰的に IsCompatible を実行
し，パス中のすべてのロケーションに対する同時実行可能性を検査する．

4.6 同時実行可能性を考慮したモデル変換
同時実行可能性の検査によって，同時実行可能性が偽であると判断された場合，偽であると判定された分岐において，時間遷移による振る舞いの違いを明確にするために，新たなロケーションを生成し，遷移関係を操作する．この複製されるロケーションを，本稿では複製ゾーンロケーションと呼ぶ．
直観的には，あるロケーション l 上の時間遷移が取り得るすべてのパターンを，離散遷移上で明示的に行うようにする．この時間遷移が取れるパターンに応じたロケーションの複製を行って，元モデル PTA に対し変換を施す．同時実行可能性となる反例パスが出力されてしまうのは，PTA 上の時間制約に関するラベルをすべて除去してしまうため，非決定的な時
間遷移について同じパス群に含まれてしまうためである．このようなケースに対し，時間遷
移を離散遷移のように扱うことで抽象モデル上で異なる非決定的な遷移として扱うようになり，抽象モデル上でも同時に実行可能でない，と判断できる．
変換の手順として，具体的には次のように処理が実行される．

Algorithm3 によって得られた集合 NSIM の要素であるロケーション l に対し，l において出発条件が異なるパスが存在する，つまり同時に実行不可能な分岐であると判断した場
合，TransformPTA(Algorithm4) によって複製ゾーンロケーションの生成を実行する．ただし，TransformPTA に入力される確率時間オートマトン PTA は，時間に関する制約のラベルを除去した抽象モデル MDP において，各状態において取りうるアクションが（ValueIteration によって）決定されている PTA とする．
まず，複製されるロケーションのインバリアントを示す．元モデル M のロケーション l25に対応する，複製ゾーンロケーション ˜
l における inv(˜l) を示す．
以下のように複製ゾーンロケーションのインバリアント inv(˜l) を求める関数 dupinv を定義する．

dupinv(l, lprev , e, ζ)= ↗ ((¬ζ ∧ inv(lprev ) ∧ ge )[X := 0]) ∧ inv(l)入力となる l は複製元のロケーション，lprev は複製元のロケーションへ 1 ステップで遷移できるロケーションである．また，e はその遷移を示すエッジである．ζ は，l を経由して目的の状態へ到達するために必要となる出発条件である．この処理を行うために，後方シミュレーションで得られた出発条件と，その出発条件がどのロケーションに対する出発条件
なのかについての関係の情報を保持しておく必要がある．そのために，後方シミュレーショ
ンアルゴリズムの 19 行目において，出発上限と遷移の関係を示す集合 ER を定義しておき，

dupinv に対する入力を与える（アルゴリズム 6，4 行目）．
Algorithm 4 TransformPTA(PTA, Z, a)
1: DLS := ∅, POWZ := ∅2: for all l ∈ NSIM do
3:

POWZ := PowZ(l, Z)

4:

E :=getTransitionSet(l) {E は l における遷移の集合 }5:

DLS := MakeDuplicateZoneLocation(l, DLS)

6:MakeTransition(l, a, POWZ, DLS)

7:

RemoveTransition(E) { 元の遷移 E の除去 }8: end for
9: return PTA

続いて，複製ゾーンロケーション ˜
l の遷移関係について述べる．まず，˜l からの遷移は，複製元ロケーションからの遷移をそのまま保持する．ただし，inv(˜l) を満たすガードの遷移のみとする．この処理はアルゴリズム 6 の 6 行目に相当する．
複製ゾーンロケーションを追加した場合，そのロケーションへの遷移だけでなく，出発条
件の組み合わせに応じた遷移を追加する．例えば，出発条件が ζ1 , ζ2 の 2 つのパターンが発見された場合，ζ1 ∧ ζ2 ，¬ζ1 ∧ ζ2 ，ζ1 ∧ ¬ζ2 ，¬ζ1 ∧ ¬ζ2 の 4 つのパターンが存在すると考えられる．今回の提案手法では，そのパターンを明確に区別し，そのパターンに応じた遷移を追加することによって，出発条件の異なる，つまり同時実行不可能な遷移を厳密に分解する．ただし，空となるパターンは区別せず，遷移の追加を行わない．
提案するアルゴリズム 7 では，出発条件のパターンを用いて，複製ゾーンロケーションへ

26

Algorithm 5 PowZ(l, ER)
1: ζpow := true, Zoc := ∅, POWZ[l] := ∅2: for all (lcurr , l′ , e, ζ) ∈ ER such that lcurr = l do
3:

Zoc := Zoc ∪ {ζ} {l における出発条件の集合を取得 }4: end for
5: for all Z ∈ POWERSET(Zoc ) do
6:

{POWERSET によってべき集合を作成し，要素 Z を取りだす }7:for all ζ l ∈ Zoc do

8:if ζ l ∈ Z then

9:
10:
11:

ζpow := ζpow ∧ ζ lelse
ζpow := ζpow ∧ ¬ζ l

12:

end if13:

end for14:

if ζpow ̸= ∅ then

15:

POWZ[l] := POWZ[l] ∪ {ζpow }16:

end if17:

ζpow := true

18: end for
19: return POWZ[l]の遷移，元の PTA からそのまま保持するロケーションへの遷移，の 2 つの遷移生成アルゴ
リズムを示している．それぞれ，6，13 行目によって遷移の追加処理が行われる．
例えば，powZ によって生成された l における出発条件のパターンのうち ζ1 ∧ ¬ζ2 についての遷移関係を構築する場合，l からの遷移は，ζ1 の出発条件で遷移できる次のロケーショ
ン (この場合 l1 とする) は，そのまま追加し，ζ2 は否定が付いているため，l2 の複製ゾーン
ロケーションへ遷移することになる．この処理を繰り返すことで，出発条件のパターン毎の遷移関係を構築することができる．

4.7 確率時間オートマトンの変換例
図 2 の確率時間オートマトン上での複製ゾーンロケーションの生成例を以下に示す．
まず，前提として，すでに反例候補のパスが探索されているものとする．この PTA の抽象モデル上で探索されるパスは以下の 2 つ（ω1 ，ω2 ）である．

27

Algorithm 6 MakeDuplicateZoneLocation(l, DLS)
1: for all ltmp ∈ N EXT (l) do
2:

ldup := newLocation() { ロケーションを生成 }3:

for all (lprev , l′ , e, ζtmp ) ∈ ER such that lprev = l and ltmp = l′ do4:

inv(ldup ) := dupinv(l, ltmp , e, ζtmp )5:

end for6:

L := L ∪ {ldup }7:

DLS := DLS ∪ {ldup } { 複製ゾーンロケーションの集合を生成 }8:

for all (lprev , g, p, X, l′ ) ∈ edges such that lprev = ltmp and g ∈ inv(ldup ) do

9:10:edges := edges ∪ {(ldup , g, p, X, l′ )}end for

11: end for
12: return DLS• ω1 = a → b → d• ω2 = a → c → d
これらのパスは，シミュレーション行った結果，元の PTA 上でも到達可能である．これらのパスを元に，後方シミュレーションを行う．ω1 では，a における出発条件が x == 1 ∧ y == 0
（ζ1 とする）となる．ω1 では，a における出発条件が y == 1（ζ2 とする）となる．また，算出された出発条件は 2 つであり，2 つの条件を組み合わせを考える（powZ の計算を行う）と，• ζ1 ∧ ζ2• ζ1 ∧ ¬ζ2• ¬ζ1 ∧ ζ2
• ¬ζ1 ∧ ¬ζ2となる．これらの条件より実際の出発条件を計算すると，• ζ1 ∧ ζ2 = ∅• ζ1 ∧ ¬ζ2 = x == 0 ∧ 1 > y ≤ 0 ∧ y > 1• ¬ζ1 ∧ ζ2 = x > 0 ∧ y > 0• ¬ζ1 ∧ ¬ζ2 = x > 0 ∨ 1 > y > 0 ∧ y > 1
28

Algorithm 7 MakeTransition(l, POWZ[l], DLS)
1: for all ζ ∈ POWZ[l] do2:

for all lnext ∈ N EXT (l) do

3:{N EXT は l の次状態の集合を表す }4:

if lnext ∈ DLS then5:ldup := DupZoneM ap(lnext )6:

for all (lprev , g, p, X, l′ ) ∈ edges such that lprev = l doedges := edges ∪ {(lprev , g, p, X, ldup )}

7:
8:
9:
10:

end forelse
for all (lprev , g, p, X, l′ ) ∈ edges such that lprev = l and l′ = lnext doedges := edges ∪ {(l, g, p, X, l′ )}

11:
12:

end for13:

end if14:

end for

15: end for

Algorithm 8 RemoveTransition(E)1: edges := edges \ Eとなり，実際に生成される遷移関係は図 7 のようになる．
次に，複製ゾーンロケーションの生成を行う．複製ゾーンロケーションは，ロケーション

a から同じアクションによって遷移できる遷移先に対し生成される．この場合，ロケーショ
ン b，c に対して複製を行う．複製ゾーンロケーション b′ では，b を通るパス ω1 の，a での出発条件を用いて inv(b′ ) の計算を行う．よって，

inv(b′ ) = x > 0 ∨ y > 0となる．c′ では，c を通るパス ω2 の，a での出発条件を用いて inv(c′ ) の計算を行う．

inv(b′ ) = (y < 1 ∨ y > 0) ∧ x == 0
x==0となる．さらに，遷移関係を構築すると，inv(b′ ) では b −−−→ d を満たさないため，b′ に対
x==0∧y==1

する遷移の追加は行われない．また，inv(c′ ) では b −−−−−−−−→ d を満たさないため，c′ に対する遷移の追加も行われない．よって，以下の図 8 のような確率時間オートマトンになる．

29

∧￢
￢∧
￢ ∧￢
ζ1

a

ζ1

ζ1

ζ2

ζ2

ζ2

図 7: 出発条件に対する遷移関係

b
a

x==0

b´
c

x==0∧y==1c´
図 8: 変換後の確率時間オートマトン

30d4.8 モデルの等価性に関する証明
本稿で提案する抽象化洗練手法では，確率時間オートマトンのパス群に対する同時実行可能性を考慮し，各パスが各ロケーションにおいて，どのくらいの時間遷移を実行する必要があるか，を明確化するために複製ゾーンロケーションの生成を行う．
ここでは，前章において述べてきた変換後の確率時間オートマトンに対する定義を用いて，モデルの変換前後の等価性について証明を行う．

L̃ から複製元である L にマップする関数 DupZoneM ap：L̃ → L を DupZoneM ap(˜l) = lとする．このマップでは，入力として変換後のモデル M のロケーション ˜
l を与えると，元モデル M の複製元に対応するロケーション l を返すものとする．
元モデル M の任意の状態を ⟨l, ν⟩ とし，さらに変換後のモデル M̃ から得られた任意の状
態を ⟨˜l, ν̃⟩ とする．また，M のロケーションの集合を L とし，M̃ の複製ゾーンロケーショ
ンの集合を L̃ とする．

L̃ から複製元である L にマップする関数 DupZoneM ap を定義する．
DupZoneM ap : L̃ → L
以下では，この複製ゾーンロケーションの生成前後において，モデルの等価性に関する証明を行う．
定理 4.1. 元の確率時間システム M と，変換後の確率時間システム M̃ は等価である．
証明 4.1. 変換前後のモデルにおける各状態 (⟨l, ν⟩, ⟨˜l, ν⟩) の対応関係は，以下の R によって定義する．

R = {(⟨l, ν⟩, ⟨˜l, ν̃⟩) | (l = ˜l ∧ ν = ν̃ ∧ l ∈ L ∧ ˜l ∈ L) ∨ (l = DupZoneM ap(˜l) ∧ ν = ν̃ ∧ ν̃ ∈inv(˜l) ∧ l ∈ L ∧ ˜l ∈ L̃)}
M 上の任意の l に対し，1 回の離散遷移で l に遷移可能な任意のロケーションを lprev とする．また，任意のロケーション l において，分布中の遷移確率 p の遷移に対するガード式
を gl (p) とする．⟨l, ν⟩ に対応する ⟨˜l, ν⟩ は，R より，(i) (l = ˜l ∧ ν = ν̃ ∧ l ∈ L ∧ ˜l ∈ L)(ii) (l = DupZoneM ap(˜l) ∧ ν = ν̃ ∧ ν̃ ∈ inv(˜l) ∧ l ∈ L ∧ ˜l ∈ L̃)の 2 つのロケーションが存在する．以下では，⟨l, ν⟩ に対応する ⟨˜l, ν̃⟩ を上記の番号によって表記する．
先ず，M 上の任意の遷移が，M̃ に存在することを示す．

31

Case:⟨lprev , ν⟩ における振る舞い
時間遷移に関しては自明．離散遷移は，⟨l, ν⟩ からの遷移は，アルゴリズムより M̃ 上に必ず保持され，ガードや遷移する確率も同じ．よって，すべての振る舞いが M 上に存在する．

Case:⟨l, ν⟩ における振る舞い(i) の場合．時間遷移に関しては自明．離散遷移は，⟨l, ν⟩ と同様に，すべての振る舞いがM 上に存在する．(ii) の場合．時間遷移について考える．⟨l, ν⟩ の時間遷移は ν + t ∈ inv(l)である t において可能である．これに対し，inv(˜l) の定義より，ν ∈ inv(˜l) が存在する場合，
˜l への任意の遷移は元モデル M に存在する．
Case:⟨˜l, ν⟩ における振る舞い
時間遷移について．
˜⟨l, ν⟩ で時間遷移可能なゾーンは，上述の inv(˜l) によって示される．複製元のロケーション l
に対し，明らかに inv(˜l) ∈ inv(l) という関係が成り立つ．よって，˜l 上の任意の時間遷移が，M 上の l で成立する．ν + t ∈ inv(˜l) となる同様の時間遷移が存在する．離散遷移は，アルゴリズムより，M̃ では inv(˜l) を満たす l 上の遷移を ˜l に保存するため，inv(˜l) を満たす l 上の遷移は，M̃ 上に必ず存在する．
続いて，M̃ 上の任意の遷移が，M に存在することを示す．
Case:⟨˜lprev , ν⟩ における振る舞い
時間遷移について．
アルゴリズムより，˜lprev と対応するロケーション lprev が元モデル上に存在する．

(i) の ˜l に関しては自明なため，以下では ˜l は (ii) であるとする．
離散遷移について．
˜lprev から ˜l への離散遷移が実行可能なゾーン ζ l̃˜

enab は，well-f ormed より，(inv(lprev ) ∧gl̃prev (p))[X := 0] ∧ inv(˜l) を満たすものに限られる．lprev から l へ離散遷移可能なゾーll̃l
ン ζenabは，(inv(lprev ) ∧ glprev )[X := 0] ∧ inv(l) であり，定義より，明らかに ζenab∈ ζenabである．
離散遷移について．
アルゴリズムより，l 上で inv(˜l) を満たす gl (p) を持つ離散遷移が ˜l で再現されるため，同様の離散遷移が l で存在する．

32

5 実験
5.1 実験の目的
本研究において提案する手法がどの程度スケーラビリティの低さを改善できているかを評価することが，この実験の目的となる．メモリ消費量の節約ができていれば，提案手法が有用であるということができる．以下では，実験環境と実験方法について述べた後，実験の対象となるモデル 2 つを紹介し，最後に実験結果として得られたデータを掲載する．
ただし，本研究における「複製ゾーンロケーションの生成」部に関しては未実装であるため，同時実行可能性が偽であるようなモデルには適用できない．以降に示す実験結果は，同時実行可能性はすべて真であったものである．

5.2 実験環境
今回の実験において利用した環境，ツールを以下に示す．

OS: CentOS 5.3

CPU: Pentium4 3.20GHz

Memory : 2GB
PRISM: version 3.3

Eclipse: version 3.5.1

JDK: version 1.6.0 b09

5.3 実験対象となる確率時間オートマトン
本研究で実験の対象としたモデルは，FireWire Root Contention Protocol[15] である．以下
では，そのモデルの振る舞いや検査対象とする性質について簡潔に述べる．

IEEE1394 ハイパフォーマンスシリアルバスは，マルチメディアシステムやデバイスのネッ
トワークとして，テレビやパソコンのようなデジタル機器で多く用いられている．このシステムは，多くの異なるプロトコルを，各用途に利用しているが，FireWire Root Contention

Protocol（図 9）とは，含まれるプロトコルの一種である．
このプロトコルは，バスのリセットが行われた後で使用される．例えば，ネットワーク内のノード（デバイス）に追加や削除が行われるような場合である．バスをリセットし，その後にすべてのノードを同じ状態にする．このプロトコルの目的は，ネットワークトポロジが木構造になっているかどうかを検査することである．スパニング木を構成するために，リーダーがプロトコルによって選出される．

33

リーダーを選出するために，ノードは，「親になって下さい」という要求を隣同士で交換する．しかしながら，2 つのノードが同時に「親になって下さい」と送信した場合，「争い」が起きるかもしれない．この争いを打開する方法は，root contention と呼ばれる，確率的，時間的な要素を用いた次のような方法で解決する．各ノードがコインを振ることで，要求のために長い時間待機するか，もしくは短い時間待機するか，を選択する．このプロトコルの興
味深い性質は，リーダーが deadline までに選出されるかどうか，である．
図 9 において示した確率時間オートマトンは，文献 [30] のモデルの確率的な拡張であり，簡単化されたモデルである．タイミングの制約は IEEE1394a の規格に従う．例えば，もしノードがロングワイヤーを使用しているならば，360ns の通信遅延が発生し，他のタイプのワイヤーをが異なる通信遅延を持つ場合，このパラメータを変化させることで検証を行うことができる．本研究において検証を行う性質は，「deadline までにリーダーが選出されない確率が p 未満である」とい内容で検証を行う．
x:=0
x>=760faststart

fastfastx:=0

x<=360x:=0z>10000 && x>=1230
x:=0
fastslow
beforez<=10000 && x>=1230
x:=0x<=1670 z>10000&& x>=1230
x:=0z<=10000 && x>=1230
slowfast
after
x:=0z>10000 && x>=1230
x:=0x<=1670z<=10000 && x>=1230
x:=0
slowslowz>10000 && x>=1230
x:=0x<=1670x:=0x<=850slowstart
x:=0
startstartx<=360x<=360x:=0x:=0

startfastx:=0x<=360x:=0startslow
x:=0
x<=360z<=10000 && x>=1230

x>1590x:=0

図 9: FireWire Root Contention Protocol (Abstract) Deadline100

5.4 実験方法
各モデルに対し，性質中の Deadline によってモデルサイズに大きく影響するため，Deadlineを増やしていった場合に，モデル検査の状態数，モデルをビルドする時間，検査を実行する時間の観点で Digital clocks[19] との比較を行う．入力となる性質に含まれる閾値 p は，Digitalclocks によってあらかじめ求められた最大確率の半分に設定し，入力とする．提案手法によ34

表 1: FireWire Abst モデルの実験結果

Digital clocks[19]DStatesTime(s)Build

MCproposal approach
Mem
(MB)

Loop

StatesTime(s)
Build

MC

Mem
(MB)

Max
reachability
probability

50298165

7.5

8.43

9.1

27

44

0.86

0.79

4.93

0.21875

100

686165

26.5

56.3

24.4

142

165

0.91

12.74

7.01

0.02526855

200

1462165

97.4

376.3

54.9

563

602

1.86

2233

10.03

0.00037044

D：DeadLine，States：モデルの状態数，Build：モデルのエンコード時間，
MC：モデル検査にかかった時間，Loop：CEGAR ループ回数，
Max reachability probability：最大到達確率をそれぞれ表す．

る実験では，k-最短路探索における k の値を k = 10，k = 100，k = 1000 の 3 通りとして行った．
提案手法における実行時間の計測は，java.lang.System クラスの currentTimeMills() を利用
し，モデルのビルド時間，検査時間の両方を計測する．一方，メモリ消費量は，jconsole によるプロセスの監視によってデータを取得した．PRISM では，ログの出力にメモリ消費量
や実行時間が出力されるため，その値を結果としてそのまま用いる．実験は 5 回ずつ行い，その平均値を結果として掲載する．

5.5 実験結果
実験結果を表 1，2 に示す．表 1 では，状態数，実行時間，メモリ消費における Digital clocksとの比較を示している．なお，表 1 の提案手法の結果はパスの最大探索数 k を 1000 としている．D=50，100 のときは，状態数，実行時間，メモリ消費において提案手法が優れているという結果になった．一方で，D=200 のときは，パス数が 1000 の場合でも指定した確率
値に達しなかったため，正しい結果が得られずに終了した．表 2 では，k の値を変えたときの提案手法の結果を示している．D=50，100 の場合は 1000 程度で十分であると考えられるが，D=200 の場合は最大値の半分も達していないため，反例を構成するパス数が非常に多くなると予想できる．

35

表 2: FireWire Abst モデルの実験結果（k 個の探索まで実行した場合）

proposal approach
D

k

Loop

States

10

36

100

Time(s)Mem(MB)probability

1.14

4.94

0.1445312

0.85

3.87

4.94

0.2187318

95

1.00

39.30

6.40

0.2187499

123

144

0.87

8.12

6.29

0.0046386

100

157

185

1.13

18.57

7.00

0.0170898

1000

216

283

1.20

340.237.79

0.0252670

10

473

504

1.84

500.709.43

0.0000045

100

519

552

1.33

661.609.67

0.0000259

1000

563

602

1.87

2233.1110.04

0.0000917

Build

MC

53

0.95

62

95

1000

62

10

50

100

200

Max
reachability
probability

0.21875

0.02526855

0.00037044

k ：k-最短路アルゴリズムによって探索するパスの数，
probability：k 個のパスによって計算された確率を表す

5.6 考察5.6.1 メモリ消費量・状態数
表 1 を見ると，Digital clocks に比べて，最大で 5 分の 1 程度と大きくメモリ消費量が削減されていることがわかる．提案手法では，確率時間オートマトン中のクロック変数に関する制約をすべて除去したモデルであり，クロック変数制約をそのまま自然数として表したモデ
ルよりも状態数が非常小さくなっているためであると考えられる．しかし，メモリ消費量は状態数程の差は見られない．これは，k-最短路によって複数個のパスを探すためのメモリがある程度必要であることが根拠として挙げられる．

5.6.2 実行時間
モデル検査時間に関しても，Digital clocks に比べ早くなっている．これは，状態数の大きな差によるものであると考えられる．一方で，D=200 でパスの数が 10 の場合でも計算時間が多く掛っているが，Loop 回数や状態数も初期抽象化の段階より 10 倍以上に増加しており，これは最短パス近辺で洗練が実行され続けている，ということが言える．本実験において入力した性質は，リーダーを選出するまでに deadline を超えてしまう，という内容である
ため，反例として探索するパスは，deadline を超えるパスである．D=200 では，dealine を超36

えるパスは，目的ロケーションに到達するまでにモデルのある地点を何度かループする必要があり，最短路はループを行うような長いパスではないため，その点で洗練が多く行われていると考えられる．

5.6.3 パス数
deadline が 50，100 の場合は 1000 程度で十分であると考えられるが，200 の場合は最大値の半分も達していない．ただし，deadline が 200 の場合，探索パス数の上限値まで正しい反例を求めても，入力された p 値に届かず，検査をきちんと実行できなかった．これは，deadlineの値を増加させることで，実行時間において述べたように，各パスは deadline を超えてしまうような経路を選択する必要がある．よって，それぞれのパスの重みは小さくなり，有効な反例とするに必要なパス数が増えているためと考えられる．

37

6 評価
評価では，実験結果を踏まえた今後の課題について言及する．
実験結果では，全体的に状態数の削減が目立ち，状態数削減では有効な手法であると考えられる．ただし，反例に必要なパス数が増加すると，計算量が増大し，実行時間が増えてしまった．これは，パス数によって k-最短路のコストが指数的に増えているためであると考えられる．
実験結果の D=200 の場合のように，入力された性質の反例において必要なパス数が多い
場合が存在する．提案手法では k 個のパスが必要な反例を探索するため，この場合は反例となるパスを探索しない従来手法に比べて，どのようにしても効率化を図ることが難しい．
また，実際には f alse であるにも関わらず，k 個のパスで反例が入力の p（p 値とする）を超えなかった場合に true と出力してしまう，信頼性の問題が浮上する．本手法では，抽象モデル上の確率的モデル検査を ValueIteration を用いて行っている．この ValueIteration ではア
ドバーサリを求めるだけでなく，抽象モデル上の到達確率（v 値とする）を出力する．よって，v 値が p 値よりも小さい場合，当然 true として終了だが，v 値が p 値よりも超えている
場合，「正しい答えが得られなかった」と警告を出力して終了することで，検査結果の信頼性を保持することができる．
さらに，反例を構成するパスが多くなる場合を判定し，ハイブリッドに検査を実行する手法が有用ではないかと考えられる．パス数が増大する場合，反例を出力はできないが，従来の ValueIteration のような数値解析の手法によって検査結果を判定し，そうでない場合に提案手法を用いて反例解析を行う，という手法である．
ここで，反例を構成するパスが多くなる場合をどのように判定するかであるが，単純には，以下の 2 つの方法が考えられる．

• k の値に上限を定める• 最短パスの重みによって判断
最短パスの重みによって判断する方法とは，具体的には，性質として入力された p 値に対し，最初に探索されたパスの確率の値が非常に小さい場合などで判断する．現在は k の上限を定めることによってアルゴリズムが終了する．今後は，最短パスの重みの評価することでハイブリッド手法を展開していくことを考えたい．

38

7 あとがき本研究では，時間オートマトンの時間抽象化とその洗練手法を拡張し，確率時間オートマ
トンの CEGAR ループに基づくフレームワークを提案した．また，反例となるパス群の同時実行可能性について言及し，同時に起こり得ないパスが抽象モデル上で発生しないようにするために，具体モデルの等価変換を行うことで解決した．加えて，完全な実装ではないが，同時実行可能性以外の面を実装したツールを用いて，確率時間オートマトンの CEGAR ルー
プに対する評価実験を行った．
評価実験では，実用的な例題 FireWire Root Contention Protocol を用いて，Digital clocks との比較を行った．パスの数が多くない場合だと，実行時間・メモリ消費量の点で優れている
ことがわかった．不具合の箇所を特定するのに有用な反例を導出することができる．よって，

6 で述べたようなハイブリッドな検査手法が有効であると考えられる．
今後の課題としては，提案手法の完全な実装が挙げられる．提案手法では，出発条件のパターンを区別するためにゾーンに対する not 演算が必要である．一般的な DBM では not
演算に対応していないため，現段階では完全な実装を行うことができない．not 演算に関する既存研究を用いるなどして，解決していきたい．

39

謝辞
本研究を行うにあたり，理解あるご指導を賜り，常に励まして頂きました楠本真二教授に心から感謝申し上げます．
本研究の全過程を通じ，適切かつ丁寧なご指導を頂きました岡野浩三准教授に深く感謝申し上げます．
本研究において，常に適切なご助言およびご指導を頂きました肥後芳樹助教に深く感謝致
します.
本研究に多大なるご助言およびご指導を頂きました柿元健特任助教に深く感謝致します.
本研究の全過程を通じ，多大な協力，助言を頂きました大阪大学大学院情報科学研究科コンピュータサイエンス専攻博士後期課程 2 年長岡武志氏に深く感謝申し上げます．
本研究について熱心に協力を頂いた大阪大学大学院情報科学研究科コンピュータサイエン
ス専攻博士前期課程 1 年田中俊彰氏に感謝します．
その他楠本研究室の皆様のご協力に，心より感謝致します．
最後に，コンピュータサイエンス専攻にてお世話頂きました諸先生方にお礼申し上げます．

40

参考文献
[1] H. Aljazzar and S. Leue. Counterexamples for model checking of markov decision processes. Technical Report soft-08-01, Chair for Software Engineering, 2007.
[2] R. Alur and D.L. Dill. A theory of timed automata. In Theoretical Computer Science, Vol.
125, pp. 183–235, 1994.
[3] A. Aziz, K. Sanwal, V. Singhal, and R. Brayton. Verifying continuous time markov chains.
In R. Alur and T. Henzinger, editers, Proc. 8th International Conference on Computer Aided
Verification (CAV’95), Vol. 1102 of LNCS, pp. 269–276, 1996.
[4] C. Baier and J.P. Katoen. Principles of model checking (representation and mind series).
The MIT Press, 2008.
[5] D.P. Bertsekas. Dynamic programming and optimal control. Athena Scientific, 1995.
[6] E.M. Clarke, E. Emerson, and A. Sistla. Automatic verification of finite-state concurrent
systems using temporal logics. ACM Transactions on Programming Languages and Systems,
Vol. 8(2), pp. 244–263, 1986.
[7] E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction
refinement. International Conference on Computer Aided Verification (CAV’00), pp. 154–
169, 2000.
[8] E.M. Clarke, O. Grumberg, and D.A. Peled. Model checking. The MIT Press, 1999.
[9] A. David, J. Hakansson, K. G. Larsen, and P. Petterson. Model checking timed automata
with priorities using dbm subtraction. Lecture Notes in Computer Science, Vol. 2402, pp.
128–142, 2006.
[10] C. Daws, M. Kwiatkowska, and G. Norman. Automatic verification of the ieee 1394 root
contention protocol with kronos and prism. International Journal on Software Tools forTechnology Transfer (STTT), Vol. 5(2), pp. 221–236, 2004.
[11] C. Dawsm, A. Olivero, S. Tripakis, and S. Yovine. The tool kronos. In R. Alur, T. A.
Henzinger and E. D. Sontag, editers, Hybrid Systems III, Lecture Notes in Computer Science,Vol. 1066, pp. 208–219, 1336.

41

[12] M. Fruth. Probabilistic model checking of contention resolution in the ieee 802.15.4 low-rate
wireless personal area network protocol. In Proc. 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISOLA’06), November
2006.
[13] T. Han and J. Katoen. Counterexamples in probabilistic model checking. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 72–86, 2007.
[14] H. Hansson and B. Jonsson. A logic for reasoning about time and probability. Formal
Aspects of Computing, Vol. 6, pp. 512–535, 1994.
[15] M. Kwiatkowska, G. Norman, and J.Sproston. Probabilistic model checking of deadline
properties in the ieee1394 firewire root contention protocol. Formal Aspects of Computing,Vol. 14(3), pp. 295–318, 2003.
[16] M. Kwiatkowska, G. Norman, and D. Parker. Prism 2.0: A tool for probabilistic model
checking. In Proc. 1st International Conference on Quantitative Evaluation of Systems(QEST’04), pp. 322–323, 2004.
[17] M. Kwiatkowska, G. Norman, and D. Parker. Game-based abstraction for markov decision
processes. In Proc. 3rd International Conference on Quantitative Evaluation of Systems(QEST’06), pages 157-166, IEEE CS Press. Winner of the QEST’06 Best Paper Award.,
2006.
[18] M. Kwiatkowska, G. Norman, and D. Parker. Stochastic games for verification of probabilistic timed automata. In Proc. 7th International Conference on Formal Modeling and Analysis
of Timed Systems (FORMATS’09), LNCS, Vol. 5813, pp. 212–227, Springer, 2009.
[19] M. Kwiatkowska, G. Norman, D. Parker, and J. Sproston. Performance analysis of probabilistic timed automata using digital clocks. Formal Methods in System Design, Vol. 29, pp.
33–78, 2006.
[20] M. Kwiatkowska, G. Norman, R. Segala, and J. Sproston. Automatic verification of realtime systems with discrete probability distributions. Theoretial Computer Science, Vol. 282,
pp. 101–150, 2002.
[21] M. Kwiatkowska, G. Norman, and J. Sproston. Probabilistic model checking of the ieee802.11 wireless local area network protocol. In H. Hermanns and R. Segala (editors) Proc.

42

PAPM/PROBMIV’02, volume 2399 of Lecture Notes in Computer Science, Vol. 2399, pp.
169–187, 2002.
[22] M. Kwiatkowska, G. Norman, J. Sproston, and F. Wang. Symbolic model checking forprobabilistic timed automata. Inf. and Comp., Vol. 205(7), pp. 1027–1077, 2007.
[23] T. Nagaoka. Model abstraction of timed automata based on counterexample-guided abstraction refinement loop. Department of Computer Science, Graduate School of Information
Scinece and Technology, 2008.
[24] T. Nagaoka, A. Ito, K. Okano, and S. Kusumoto. Qos evaluation for real-time distributed
systems using the probabilistic model checker prism. In Proceedings of International Workshop on Informatics, pp. 60–66, 2009.
[25] T. Nagaoka, K. Okano, and S. Kusumoto.

Abstraction of timed automata based on

counterexample-guided abstraction refinement loop. IEICE Technical Report, Vol. 107, No.
505, pp. 103–108, 2008.
[26] T. Nagaoka, K. Okano, and S. Kusumoto. An abstraction refinement technique for timed
automata based on counterexample-guided abstraction refinement loop. IEICE Transactions
on Information and Systems, Vol. E93-D, No. 5, p. to appear, 2010.
[27] D. Parker. Implementation of Symbolic Model Checking for Probabilistic Systems. PhD
thesis, University of Birmingham, 2002.
[28] M Puter. Markov decision processes: Discrete stochastic dynamic programming. Wiley
Interscience, 1994.
[29] P. Roy, D. Parker, G. Norman, and L. de Alfaro. Symbolic magnifying lens abstraction inmarkov decision processes. In Proc. 5th International Conference on Quantitative Evaluation of Systems (QEST’08), pages 103-112, IEEE CS Press, 2008.
[30] D. Simons and M. Stoelinga. Mechanical verification of the ieee 1394a root contention
protocol using uppaal2k. Springer International Journal of Software Tools for Technology
Transger, 2001.

43