社団法人 電子情報通信学会
THE INSTITUTE OF ELECTRONICS,INFORMATION AND COMMUNICATION ENGINEERS

信学技報
TECHNICAL REPORT OF IEICE.

実時間システムを対象とした CEGAR による抽象洗練の並列化手法
田中俊彰†

長岡武志†

岡野浩三†

楠本真二†

† 大阪大学大学院情報科学研究科 〒 565–0871 大阪府吹田市山田丘 1–5
E-mail: †{tstanaka,t-nagaok,okano,kusumoto}@ist.osaka-u.ac.jp
あらまし

時間オートマトンの CEGAR を用いた到達可能性解析を行う手法について，高速化に関する技法を提案する．本稿では、初期抽象を行ったモデルに対して複数の反例を生じさせ、反例による洗練結果を統合することにより，より高速な解析手法を提案する．また，提案した手法に対して並列計算機を用いた評価実験を行い，その台数効果による速度向上が行われているかを調べた．その結果，例では台数効果があることを確認した．
キーワード時間オートマトン，モデル検査，CEGAR，並列処理

Reachability Analysis for Timed Systems using Parallel Processing
Toshiaki TANAKA† , Takeshi NAGAOKA† , Kozo OKANO† , and Shinji KUSUMOTO†† Graduate School of Infomation Science and Texhnology, Osaka University
Yamada-oka 1–5, Suita City, Osaka, 565–0871 Japan
E-mail: †{tstanaka,t-nagaok,okano,kusumoto}@ist.osaka-u.ac.jp
Abstract This report proposes efficient parallel processing of reachability analysis for timed automaton. Our research group
has already proposed CEGAR loop for timed automaton. The report proposes parallel processing version of the CEGAR loop.
The new version performs in parallel model checking with different parameters and the master node synthesizes multiple
counter examples generated by workers and refines the model. We have prototyped a tool and performed experiments. We
found that some of the results show the effeciency of the proposed parallel processing.
Key words Timed Automaton, Model Checking, CEGAR, Parallel Processing

1. ま え が き

そこで，本研究では文献 [14] の手法を見直し，初期の段階で反例抽出処理を並列に行い，一度に複数の反例から洗練を行う

本稿では，時間オートマトンに対してクロック変数を除去する手法を用いて，処理の高速化を目指す．また，実際に提案手法

時間抽象化を行う抽象洗練手法 [14] に対する，高速化を目的とに対して速度向上の効果があるかについて実験を行い，その結した手法の改良を提案する．[14] は Clarke らの Counter-example

果を評価する．

Guided Abstraction Refinement [1] の枠組みを利用しており，時以下 2. では，まずモデルとして利用される時間オートマトン間オートマトンのモデル検査に対して状態爆発を回避する効果について述べる．また，本稿で利用する CEGAR ループついて的な手法ではあるが，処理速度が通常のモデル検査に対して劣簡潔に述べる．3. では，本研究で提案する CEGAR ループの反る．これは，状態数を削減する処理に起因する．

例抽出並列化手法の概要とアルゴリズムおよび，正当性の略証

そこで，本研究では [14] の手法を見直し，初期の段階で反例抽出処理を並列に行い，一度に複数の反例から洗練を行う手法を用いて，処理の高速化を目指す．また，実際に提案手法に対して速度向上の効果があるかについて実験を行い，その結果を評価する．
文献 [14] は Clarke らの Counter-example Guided AbstractionRefinement [1] の枠組みを利用しており，時間オートマトンのを与える．4. では，提案する手法に対する評価実験を行い，5.
でまとめる．

2. 準備

本節では, 時間オートマトンの定義とその意味，そして一般的な CEGAR のアルゴリズムについて述べる．

2. 1 時間オートマトン

モデル検査に対して状態爆発を回避する効果的な手法ではある

定義 2.1 (C 上の差分不等式). クロックの有限集合 C 上の差分が，処理速度が通常のモデル検査に対して劣る．これは，状態不等式 E の構文と意味を以下のように与える. E ::= x − y ∼ a

数を削減する処理に起因する．

| x ∼ a, ここで x, y ∈ C, a は実数定数リテラル, ∼∈ {<=, >=, <—1—

, >}. 差分不等式の意味は通常の不等式と同じである.
定義 2.2 (C のクロック制約式). クロックの有限集合 C 上のクロック制約式 c(C) を以下のように与える．クロックの有限集合

C 上の差分方程式全てからなる集合を c(C) とする．ある要素
in1 と in2 が c(C) の要素である時，in1 ∧ in2 も同様に c(C)の要素である．
定 義 2.3 (時 間 オ ー ト マ ト ン). 時 間 オ ー ト マ ト ン A は(A, L, l0 , C, I, T ) という以下の 6 個の要素から成る
図1

A: アクションの有限集合

一般的な CEGAR アルゴリズム

Fig. 1 General CEGAR Algorithm

L: ロケーションの有限集合
l0 ∈ L: 初期ロケーション

象モデルに対してモデル検査を行う．この段階で，抽象モデル

C: クロックの有限集合
I ⊂ (L → c(C)): クロック制約式をロケーションに写像したもので，ロケーションインバリアントと呼ばれるが与えられた性質を満たすのであれば，実際のモデルでも性質を満たすと結論付けることができる．これは，抽象モデルが実T ⊂ L × A × c(C) × R × L, ここで c(C) はクロック制約式で際のモデルの over-approximation であるためである．もしモデあり, ガードと呼ぶ．R = 2C : リセットクロック集合.

ル検査器がモデルは性質を満たさないという結果を返してきた
場合，検出された反例が本来実行可能でない反例（偽反例と呼a,g,rある遷移 t = (l1 , a, g, r, l2 ) ∈ T は l1 −→ l2 と表記する.

ぶ）であるか否かを検証する段階に入る．(これをシミュレー

ν : C → R>となる ν をクロックの評価関数と呼ぶ.
=0ションと呼ぶ) シミュレーションで，もし反例が実際のモデル

d ∈ R>に対して (ν + d)(x) = ν(x) + d と定義する.
=0でも存在するものであるのならば，ループを終了する．そうでr ∈ 2C に対して、r(ν) = ν[x 7→ 0], x ∈ r と定義する．このないのならば，間違った反例をなくすような抽象モデルの洗練

時， ν[x 7→ 0] は各クロック x に対する値を 0 とするクロック評価関数を表すとする．

を行う．これらの段階を繰り返し，正しい出力を得る．

3. 提 案 手 法

ν の全てからなる集合を N とする．
定 義 2.4 (時 間 オ ー ト マ ト ン の 意 味). 時 間 オ ー ト マ ト ン

A = (A, L, l0 , C, I, T ) に対して A の状態集合を S = L × Nとする．A の初期状態は (l0 , 0C ) ∈ S で与えられる．状態遷移a,g,rl1 −→ l2 (∈ T ), に対して、次の二つの遷移が定義される. 前者をイベント遷移，後者を時間遷移と呼ぶ．

本章では，本稿で提案する確率時間オートマトンの抽象化洗練手法について示す．提案する抽象化洗練手法では，著者らが文献 [14] で提案した時間オートマトンの抽象洗練手法を利用し、さらに高速化のために反例抽出を並列に行っている（図 2）．
（ 1 ） 入力として与えられたモデルと満たすべき性質に対して，時間抽象による初期抽象化を行う．

a,g,r

l1 −→ l2 , g(ν), I(l2 )(r(ν))
a(l1 , ν) ⇒ (l2 , r(ν))

,′
∀d′ <
= d I(l1 )(ν + d )d(l1 , ν) ⇒ (l1 , ν + d)

定義 2.5 (時間オートマトンの意味モデル). 時間オートマトン

A = (A, L, l0 , C, I, T ) について，初期状態から開始するモデルである A の意味に従って，無限の遷移を持ったシステムであると定義される．T (A ) = (S, s0 , ⇒) は A の意味上のモデルであることを示す．
本論文では，あるロケーション l 上の状態とは， l のインバリアントを満たす ν の任意の意味上の状態 (l, ν) を意味する．

（2）

初期抽象化したモデルをそれぞれのワーカ計算機に配布する．このとき，配布されるモデルは同一のものである．
（3）

抽象モデルを受け取ったワーカ計算機は，モデル検査を行う．この時，性質を満たすのであれば True を，満たさないのであれば反例を出力する．
（4）

反例が出力された場合，反例を基にシミュレーションが行われる．シミュレーションによって，抽象化していないもとモデルでも成立する反例であるのならば False を，元のモデルでは存在しない反例ならばシミュレーション結果を返す．
（ 5 ） 各ワーカ計算機で求められたシミュレーション結果を，マスタ計算機で統合する．

2. 2 CEGAR アルゴリズム（6）

モデル抽象化は時に実際のモデルの過度な抽象化を行うこと元に，抽象モデルを洗練する．

がある．これにより，実際のモデルでは存在しない，誤った反例マスタ計算機で統合されたシミュレーション結果を

以下，提案手法の各操作について詳細に述べる．

を生成する可能性がある．文献 [1] は CEGAR(Counterexample-Guided Abstraction Refinement) と呼ばれるアルゴリズムを提案

3. 1 初期抽象化している (図 1).

初期抽象化では，文献 [14] と同様に，クロック変数に関するアルゴリズムにおいて，第一段階として実際のモデルを過度に抽象化する (これを初期抽象化と呼ぶ)．次に，生成された抽制約を全て除去することで，over approximation を満たすように抽象化を行う．

—2—

Refinement
Inputs Ai , π, succ list
{π = ⟨l0

a1 ,g1 ,r1−→

l1

a2 ,g2 ,r2−→···

an ,gn ,rn−→ln (ln = e)⟩ }{succ list = ⟨(l0 , D0 ), (l1 , D1 ), · · · , (lk , Dk )⟩,where (lj , Dj ) represents the j-th reachable state set along with π, andlk is the last location reachable from the initial state. }Ai+1 := Aifor j := succ list.length downto 1 doej := (lj−1 , aj−1 , gj−1 , rj−1 , lj )Ai+1 := Duplication(Ai+1 , succ listj, ej){Duplication of the Location and Transitions}
if IsRemovable(Ai+1 , succ listj , ej ) thenAi+1 := RemoveTransition(Ai+1 , ej ){Removal of Transitions}
図2

break

並列実行環境を利用した CEGAR アルゴリズム

else if j = 1 thenFig. 2 Our CEGAR Algorithm

Ai+1 := DuplicateInitialLocation(Ai+1 , (l0 , D0 )){Duplicate the initial location and transitions

定義 3.1 (抽象化関数 h). 時間オートマトン A とその意味上

from the initial location}のモデル T (A ) = (S, s0 , ⇒) について，抽象化を行う関数

h : S → Ŝ を以下のように定義する．
h((l, ν)) = l.

end ifend forreturn Ai+1
図 3 アルゴリズム 1 ： 洗練アルゴリズム

その逆関数 h−1 : Ŝ → 2S は h を用いて以下のように定義する．

Fig. 3 algorithm 1: Refinement Algorithmŝ = l である抽象モデルに対して h−1 (ŝ) = (l, DI(l) )定義 3.2 (抽象モデル). 時間オートマトン A = (A, L, l0 , C, I, T )から求められる抽象モデル M̂ = (Ŝ, ŝ0 , ⇒)ˆ とその意味上のモデル T (A ) = (S, s0 , ⇒) は以下のように定義される．

•Ŝ = L,•sˆ0 = h(s0 )•⇒ˆ = {(h(s1 ), a, h(s2 )) | s1 ⇒ s2 )}.

3. 5 シミュレーション結果の統合
各ワーカ計算機上で計算されたシミュレーション結果を，マスター計算機送り，統合する．このとき，モデル検査やシミュレーションでの終了判定も行う．

a3. 6 抽象モデルの洗練
抽象モデルの洗練は，文献 [14] で述べられている手法を基に

3. 2 抽象モデルの配布
初期抽象化した抽象モデルを，各ワーカ計算機に配布する．
この時，配布される抽象モデルは同一のものである．

している．

3. 6. 1 洗練時に行われる処理
抽象モデルを洗練するとき，以下の 3 つの処理が行われている．

3. 3 モデル検査
モデル検査は、文献 [14] と同様に行う．
定義 3.3 (抽象モデル上の反例). 抽象モデル M̂ = (Ŝ, ŝ0 , ⇒)ˆ 上•

状態を複製する•

状態間の遷移を追加する•

状態間の遷移を除去するの反例は Ŝ の連続する状態と遷移の系列である．ある長さ n の

このとき，状態の複製，遷移の複製，除去に関しての条件は文抽象モデルの反例 ρ̂ は以下のように表わされる．

献 [14] において定義されている (アルゴリズム 1:図 3)．

a1a2

a3

an−1anρ̂ = ⟨ŝ0 → ŝ1 → ŝ2 → · · · → ŝn−1 → ŝn ⟩
このとき，到達度解析を行うアルゴリズムの探索戦略を各計算機において変化させることで，抽象モデル上で性質を満たさないと判定された場合に出力される反例が異なることが期待できる．

ここで示されているアルゴリズム 1 を，提案手法に対応させるために以下のように変更したアルゴリズム 1 (図 4) を与える．
ある反例の集合 P̂ に対して，順にアルゴリズム 1 を実行する．その結果は時間オートマトン A に反映される．もし仮に，反例の badstate を解消できない場合は，アルゴリズム 1 を適用

3. 4 シミュレーション
シミュレーションでは，[14] で提案されているシミュレーションアルゴリズムに従って，各ワーカ計算機上で DBM の演算によって到達可能か判定する．

せず，P̂ の次の反例に対して処理を繰り返す.

3. 6. 2 反例の重複抽象モデルを洗練するときに問題となるのは，複数の反例を抽象モデルの洗練に適用した際，反例の選択順序により誤った洗練を行わないことを保証することである.

—3—

A

RefinementOfCEs
Inputs Ai , P{P = ⟨ρ0 , ρ1 , · · · , ρk )⟩}Bx>3

CEy >= 5y := 0x<5Ai+1 := Aix<8Dfor j := P.length downto 1 doy >= 8

Ai+1 := Ref inement(Ai+1 , ρj )x < 10end for
return Ai+1

図5

元モデルの時間オートマトン

Fig. 5 A Timed Automaton

図 4 アルゴリズム 1’： 洗練アルゴリズム (複数パス)

Fig. 4 algorithm 1’ : Refinment Algorithm of CEs

ABCEy >= 5

まず，反例の重複について, 定義 3.4 で与える．

x<5x<8x>3

定義 3.4 (反例の重複). ある反例 ρ̂1 と ρ̂2 が重複しているといB1D

3<x<8&x–y>3x < 10y := 0y >= 8うことは，反例 ρ̂1 と ρ̂2 が共通する 1 つ以上の初期状態以外の状態 ŝ を保持していることである．反例の集合が重複していな
いとは，その集合のどの 2 つをとっても重複していないことを

図 6 図 3 において B-C から洗練して得られた時間オートマトン

Fig. 6 A Timed Automaton Refinement of B-C Trantision

意味する．

A定義 3.5 (badstate). ある反例 ρ̂ に含まれる遷移において，時間B制約を満たさない最初の抽象モデル上の状態のことを badstate

CEy >= 5とする．

x<5x<8x>3

定義 3.6. ある抽象モデル M̂ と，与えられた反例の集合 P̂ に対して，大域的に正しい洗練 M̂ ′ とは，P̂ が Pˆ1 (=| ∅), Pˆ2 に分割

B1

D

3<x<8&x–y>3x < 10y := 0

でき，Pˆ1 に含まれる反例に対しては badstate が解消され，Pˆ2y >= 8

D1の中の反例は M̂ ′ で実行不能な洗練のことである．
定理 3.1. 到達可能性解析においては反例集合の反例をどのよ

3 < x < 10 & x – y > 3

うな順番でアルゴリズム 1’ を適用しても大域的に正しい洗練

図7である．

図 3 において D-E から洗練して得られた時間オートマトン

Fig. 7 A Timed Automaton Refinement of D-E Trantision

証明 3.1. 以下の定理 3.2，3.3 より明らかである．

2なくともアルゴリズム 1 が適用されるため，ρ1 は空ではない．

定理 3.2. 重複のない反例の集合に対して，到達可能性解析においては反例集合の反例をどのような順番でアルゴリズム 3 を2
なお，反例の適用順序により一般に得られる抽象モデルは異適応しても大域的に正しい洗練になる．

なり得る可能性がある．また,定理 3.3. 重複のある反例集合に対して，到達可能性解析にお結果を生み出すこともある．その例を 3. 6. 3 で示す．

逆に適用順に関わらず同一のいては反例集合の反例をどのような順番でアルゴリズム 1’ を適応しても大域的に正しい洗練になる．

3. 6. 3 反例解消の例
実際の例を用いて，提案手法の処理について説明する．例え定理 3.2 は自明であるため，ここでは定理 3.3 の略証を与える．
略証ば，図 5 のようなモデルがあるとする．このモデルは，状態 Bから状態 C への遷移と，状態 D から状態 E への遷移に対して反例集合内の反例をすでに n 個についてアルゴリズム1 を適用した状況を考える．そのときの抽象モデルを M̂ ′ n で表す．n + 1 番目の反例を任意に選んだとき以下の場合が考えられる．

時間制約を満たさない．このようなモデルに対して，提案手法を適応した場合についての例を示す．
まず、このモデルを提案手法に適応した場合，得られる反例は以下の二つが考えられる．

（ 1 ） M̂ ′ n 上でその反例は実行不能である．

•（ 2 ） M̂ ′ n 上でその反例は実行可能である．

A→B→C→E•

A→B→D→E

前者の場合はアルゴリズム 1を適用したのちの M̂ ′ n+1 はM̂ ′ n と同形であり，M̂ ′ 0 に対して正しい洗練である．
後者の場合は，その反例の badstate がアルゴリズム 1 で新たに実行不可能にある．よって，M̂ ′ n+1 は M̂ ′ 0 に対して大域的この二つの反例が得られたと仮定して，洗練手法を適応する．
まず，反例 A → B → C → E から洗練を行った場合の例を示す．
状態 B から状態 C への遷移は時間制約を満たさないため，に正しい洗練である．なお，反例集合中最初に選んだ反例は少—4—

450

成された状態 B1 をから状態 D に遷移を生成し，さらに状態 A400から状態 B1 への遷移を生成する．最後に，状態 A から状態 B350への遷移を削除することで洗練が終了する（図 6）．

300

number of loop

まずは時間制約を満たす状態 B1 を新たに生成する．次に，生

反例 A → B → D → E に対する洗練を行う．前回と同じように時間制約を満たす状態 D1 を新たに生成する．次に，状態D1 の時間制約を満たす状態 B1 の生成を行うが，前回生成しShortest Trace
Fastest Trace

250200150100た状態 B1 が状態 D1 の時間制約を満たすため生成しない．最50後に，状態 B1 から状態 D への遷移を削除する (図 7)．

0

次に，反例 A → B → D → E から洗練を行った場合の例を12345678910 11 12 13 14

computer node示す．
まず，状態 D から状態 E への遷移は時間制約を満たさない

図 8 ループ回数ため，時間制約を満たす状態 D1 を新たに生成する．このとき，Fig. 8 Number of iterations

状態 B は状態 D1 の時間制約を満たさないため，同時に状態B1 も生成する．最後に，状態 A から状態 B への遷移を削除し250000て，洗練を終了する (図 7)．
200000

次に，反例 A → B → C → E に対する洗練を行うが，状態 A から状態 C に到達するパスは存在しないため，何もせずに終了となる．この場合，反例 A → B → C → E と反例

Fastest Tracetime(ms)態 D から状態 E への遷移に対する洗練を行った段階で，状Shortest Trace

A → B → D → E の洗練の順序を入れ替えたとしても，最終15000010000050000

的には同じ洗練結果が得られることがわかる．
0123454. 評 価 実 験678910 11 12 13 14

computer node

本章では提案手法について評価実験を行う．

図9 処理時間4. 1 実 験 環 境

Fig. 9 Excute time

4. 1. 1 計算機環境
提案手法を実行する並列計算環境を以下に示す．

使用を管理するプロトコルである．また，モデルの生成についマスター計算機

CPU : Intel(R) Core

TM2 Duo

CPU L7700 1.80GHz
メモリ : 2.00GB

このプロトコルでは，n 個のプロセス間で一つしかない資源のOS : Ubuntu 10.0.4ても，UPPAAL が行う．

4. 1. 4 探索戦略について
今回の実験では，出力される反例の性質の違いに対してもその違いが現れるかについて実験を行った．反例の選択としワーカ計算機（14 台）

CPU : Dual Core AMD OpteronT Mては，探索された反例の中で最も早く発見された反例を返す

Processor 2210 HE 1.80GHz

Fastest Trace と，発見された反例の中で最短の長さの反例を返メモリ : 6.00GB

OS : CentOS 5.4

す Shortest Trace の二つについて 実験を行った．

また，マスター・ワーカ間の通信には Java の RMI フレームワー

4. 2 実 験 結 果

クを利用した．

4. 2. 1 ループ回数

4. 1. 2 モデル検査ツール

まず，ワーカ計算機を増やした時のループ回数に対する台数

今回の実験においてモデル検査は，モデル検査ツール UP-効果について傾向を調べる．ここで、ループ回数とは提案手法

PAAL [7] のモデル検査モジュールを利用する．探索戦略は深さの処理が行われた回数のことを示している．図 8 は，ループ回優先の最適化探索とし，出力するパスはランダムに設定する．

数に対する台数効果を表している．利用しているワーカ計算機

このことで今回目的とする複数種類の反例を出力させる．の台数が増えるほど，図 8 ではループ回数が減少していること

反例抽出処理がランダムであるため，今回は出力の均一化のたが解る.

めに 1 つの事象につき 5 回の実験を行い，その平均を取って実験結果とする．

4. 1. 3 対象とした例題

4. 2. 2 実 行 時 間
次に，実行時間に対数台数効果について傾向を調べる．

この実験では，Fischer の相互排除プロトコルを利用する．こ図 9 は，処理時間に対する台数効果を表している．図 8 とは違

れは実時間モデル検査のアルゴリズムの比較によく用いられる．

い，7 台目辺りから処理時間が横ばいであることが図 9 から解—5—

いて解決していきたい．

600

また，提案手法では，洗練を逐次的に行っていたが，シュミ
500

number of state

レーション結果から，重複するような洗練，またはある洗練の400部分集合となるような洗練をを排除することで，洗練を行う時間を削減し，更なる高速化手法を提案していきたい．

300

200

Shortest Trace
Fastest Trace100

謝辞

本研究の一部は科学研究費補助金基盤 C(21500036) と文部科学省「次世代 IT 基盤構築のための研究開発」(研究開発
領域名：ソフトウェア構築状況の可視化技術の普及) の助成による．

012345678910 11 12 13 14computer node

図 10状 態数

Fig. 10 Number of states

る．ループ回数は順調に減少しているため，1 回のループ辺りの探索時間が増大していることが考えられる．

4. 2. 3 生成状態数
最後に，生成状態数の増加量について傾向を調べる．
図 10 は，台数に対する生成状態数の数を表している．新たに状態が生成される場合は主に洗練時であるため，生成状態数が増えることは抽象モデルに対して不必要な洗練が行われている可能性がある，ということを示している．反例パスの探索手法により生成状態数に差があるが，これは出力される反例が短いほうが生成される状態数が少なくなることを示していると考えられる．

4. 3 実験結果の考察
実験結果に対する考察を行う．
実験の結果，ループ回数はワーカ計算機を増やすことによる台数効果が出ていることが分かる．しかしながら，図 9,10 が示すように，ワーカ計算機の台数を増やすことにより本来不要な洗練が行われ，そのためにモデルが不必要に肥大化し，結果 1ループ辺りの処理時間が増大することで台数効果を打ち消している可能性も示している．
また，出力される反例が短い場合，新たに生成される状態数を抑えることが可能であるため探索速度の向上するという結果が得られた．
今回は反例を抽出するモデル検査の処理がランダム出力であったため，詳しい解析はできなかった．この事象をさらに調査するために，今後はランダム性のないモデル検査手法が必要となる．

5. お わ り に
本稿では，時間オートマトンに対する時間抽象化を用いた洗練手法を拡張し，抽象モデルに対して複数の異なった反例抽出，洗練を行うことで手法の高速化を提案，実験を行った．

文

献[1] E M. Clarke, O. Grumberg, S. Jha, Y. Lu, and V. Helmut: “Counterexample-guided abstraction refinement for symbolic modelchecking,” Journal of the ACM, vol.50(5), pp752-794, 2003.
[2] E M. Clarke, A. Gupta, J. Kukula, and O. Strichman: “SAT based
Abstraction-Refinement using ILP and Machine Learning Techniques,” In Proc. of the 14th Int. Conf. on Computer Aided Verification, Lecture Notes in Computer Science, vol.2404, pp.695-709,2002.
[3] E M. Clarke, A. Fehnker, Z. Han, J Ouaknine, O. Stursberg, and M.
Theobald: “Abstraction and Counterexample-guided Refinement inModel Checking of Hybrid Systems,” In Int. Journal of Foundationsof Computer Science, vol.14(4), 2003.
[4] R. Alur: “Techniques for Automatic Verification of Real-Time Systems,” PhD thesis, Stanford University, 1991.
[5] R. Alur, C. Courcoubetis, and D. L. Dill: “Model-checking for realtime systems,” In Proc. of the 5th Annual Symposium on Logic in
Computer Science, IEEE, pp.414-425, 1990.
[6] S. Das, D. L. Dill, and S.Park : “Experience with predicate abstraction,” In Proc. of the 11th Int. Conf. on Computer Aided Verification,
Lecture Notes in Computer Science, vol.1633, pp.160-171, 1999.
[7] J. Bengtsson, and W .Yi: “Timed Automata: Semantics, Algorithms
and Tools,” In Lectures on Concurrency and Petri Nets, Lecture
Notes in Computer Science, vol.3098, pp.87-124, 2004.
[8] F. Wang, K. Schmidt, G D. Huang, F. Yu, B Y. Wang: “Formal Verification of Timed Systems: A Survey and Perspective,” In Proc. ofthe IEEE, vol.92, No.8, pp.1283-1307, 2004.
[9] G. Behrmann, A. David, and K G. Larsen: “A Tutorial on UPPAAL,”In Proc. of the 4th Int. School on Formal Methods for the Design ofComputer, Communication, and Software Systems, Lecture Notes in
Computer Science, vol.3185, pp.200-236, 2004[10] A. David, J. Hakansson, K G. Larsen, and P. pettersson: “ModelChecking Timed Automata with Priorities using DBM Subtraction,”
In Proc. of the 4th Int. Conf. on Formal Modelling and Analysisof Timed Systems, Lecture Notes in Computer Science, vol.4202,pp.128-142, 2006[11] H. Nakajima and Y. Kameyama: “Improvement on Real-Time Model
Checking using Abstraction-Refinement (In Japanese),” In Transactions of Information Processing Society of Japan, vol.45, No.SIG12(PRO23), pp.11-24.
[12] S. Kemper, and A. Platzer: “SAT-based Abstraction Refinement forReal-time Systems,” In Proc. of the Third Int. Workshop on Formal
Aspects of Component Software, vol.182, pp.107-122, 2006.
[13] H. Dierks, S. Kupferschmid, and K G. Larsen: “Automatic Abstraction Refinement for Timed Automata,” In Proc. of the 5th Int. Conf.
on Formal Modelling and Analysis of Timed Systems, Lecture Notes
in Computer Science, vol.4763, pp.114-129, 2007.
[14] T. Nagaoka, K. Okano, and S. Kusumoto: “An Abstraction refinement technique for timed automata based on CounterexampleGuided Abstraction Refinement Loop,” IEICE Transactions on Information and Systems, vol.E93-D, No.5, pp.994-1005, 2010.

今後の課題としては，今回の評価実験で見られた，実行時間に対する台数効果の阻害要因を調べるために，k− 最短路による到達度解析を行うモデル検査ツールを実装し，その挙動につ—6—