時間オートマトンを対象としたコンポーネント部分合成による抽象化洗練手法の改良
長 岡 武 志†

岡 野 浩

三†

楠 本

真

二†

著者らの提案している時間オートマトンの抽象化精錬手法では，時間オートマトンが持つクロック
変数をすべて除去するという抽象化を行うため，生成する抽象モデルは有限状態オートマトンとなる．
これまでの手法では，複数のプロセスが並列に動作するようなモデルを検査する場合，事前に複数のプロセスを並列合成する必要があった．しかし，事前に合成を行ったモデルに対して検査を行う場合，
モデル検査実行時に合成を行う場合に比べ，消費するメモリ量が増加し，抽象化の効率が低下してしまう．そこで本稿ではそのようなプロセス合成をインクリメンタルに行うことにより，部分的にとどめるような手法を提案する．また簡単な例題に対する予備実験の結果を報告する．

Improvement of Abstraction Refinement
for Timed Automata based on Partial Parallel Composition
TAKESHI NAGAOKA ,† KOZO O KANO † and S HINJI K USUMOTO†
We have proposed an abstraction refinement technique for timed automata. In our former abstraction technique, we perform abstraction by removing all clock variables from timed automata. Therefore, generated
abstract models are finite automata. In the method, a network of parallel timed automata should be composed
into a single timed automaton, as preliminary of model checking. Such an approach, however, often yeilds
to memory consumption; which decreases the efficiency. This paper improves our abstraction technique not
to need full parallel composition, by incremental construction technique. The result of a small experiment isalso described.

1. ま え が きを行わない従来の時間モデル検査では時間領域が実質，有限個に押さえられることを利用し有限状態のモモデル検査手法はシステムを有限の状態遷移系としデルに対し検査を行う．しかし，この状態数はロケーて記述し，状態遷移系の全状態を探索することで，シションやクロックの個数に対して指数的に増加する．

ステムが仕様を満たすかどうかを証明する手法であしたがって時間オートマトンに対しても，状態数を削る．しかし，大規模なシステムに対しては状態数爆発減するための適切な抽象化の方法が必要となる．著者を起こすなど，スケーラビリティの弱さが課題となっらは文献 9)，10) で，時間オートマトンを対象としたている．モデル検査のスケーラビリティの弱さを改善

モデル抽象化手法を提案している．9)，10) で提案しする手法として，検査する性質ごとに，モデルの状態ている手法では，抽象化を適用したモデル（抽象モデ数を適切に削減するモデル抽象化手法が注目されていル）上で発生した反例を利用して抽象モデルの洗練をる1),2) ．

行う，CounterExample-Guided Abstraction Refinement

一方，実時間システムの動作検証には，有限の状態

Loop(CEGAR Loop)1) の枠組みを利用しており，抽象遷移系に実時間制約を付加した時間オートマトン5) が化の全工程を自動で行うことができる．また，提案し用いられる．時間オートマトンでは，有限のロケーている手法では，時間オートマトンが持つクロック変ションと呼ばれる状態に，実数値をとるクロック変数

数をすべて削除し，時間による振る舞いの違いをモデを用いた制約が付加されるため，時間オートマトン

ルの遷移関係を操作することで抽象モデルを洗練しては無限の状態空間を持つことになる．モデル抽象化

いく．具体的には，状態，遷移の複製，遷移の除去など† 大阪大学大学院情報科学研究科
Graduate School of Information Science and Technology, Osaka
Universityの操作を行うことで実現している．しかしこれまでの手法では, 複数のプロセスが並列に動作するようなモデルを検査する場合，事前に複数のプロセスを並列合成する必要があった．このように事前に合成を行った

定義 2.2 (時間オートマトンの意味). 時間オートマト

モデルに対して検査を行った場合，モデル検査実行時

ン A = (L, l0 , T, I, C, A) に対してに合成を行う場合に比べ，消費するメモリ量が増加し，A の状態集合を S = L × N とする．

抽象化の効率が低下してしまうという問題が生じる．

A の初期状態は (l0 , 0C ) ∈ S で与えられる．

本稿では，このような問題を解決するため，これまでの手法を，モデルが持つ並列プロセスの合成が必要とならないよう改善する．具体的には，抽象モデル洗

a,g,r

状態遷移 l1 −→ l2 (∈ T ) に対し，次の２つの遷移が定義される．
a,g,r
l1 −→ l2 , g(ν), I(l2 )(r(ν))
a(l1 , ν) ⇒ (l2 , r(ν))∀d′ ≤ d I(l1 )(ν + d′ )練の際に，状態，遷移の複製，遷移の削除などの操作が必要な部分について部分的に並列合成を行うことで，モデル全体を合成することを回避している．このとき，部分的に合成したプロセスの動作とその他のプロセスの動作を同期させることで，もとの時間オートマト
ンと等価な動きをすることを保証する．その際，モデ
ル検査器 UPPAAL6),7) で用いられる拡張時間オートマトンの構成要素である整数変数や Broadcast Channel，Committed Location などを利用している．

定義 2.3 (DBM(Difference Bound Matrix)). 時間オー
トマトン A = (L, l0 , T, I, C, A) に対して DBM は|C| -次元ユークリッド空間上の凸空間を表現し，Nの要素の集合として表現される．DBM D に対して，(l , D) = {(l , ν)|ν ∈ D} と表記する．
2.2 ネットワーク時間オートマトン

以降，2 では準備として時間オートマトンの定義を与え，一般的な CEGAR ループ，著者らが提案している抽象化アルゴリズムを説明する．3 では，2 で説明した既存のアルゴリズムを並列合成が必要とならない
ように改善する手法を述べる．さらに 4 で実験結果を示し，最後に，5 でまとめる．

2. 準

d

(l1 , ν) ⇒ (l1 , ν + d)
前者をイベント遷移, 後者を時間遷移と呼ぶ.

時間オートマトン間の並列実行，同期化を実現する
ため，オートマトン間の同期を行う半アクション (チャネル) が用いられる5) ．なお，半アクションに対して，
単一プロセス内のみで行われるアクションを全アクションとする．時間オートマトン A1 , . . . , An に対して並列合成モデル A := A1 ||A2 || · · · ||An はネットワーク
時間オートマトンである．

備

定義 2.4 (ネットワーク時間オートマトンの意味). ネッ
本章では準備として一般的な時間オートマトン，ネッ
トワーク時間オートマトンの定義を与え，UPPAAL 拡
張時間オートマトン，著者らがこれまでに提案してきた抽象化手法について説明する．
時間オートマトンは有限状態のオートマトンに時間経過を表現するクロック変数を付加したオートマトン
である．
定義 2.1 (時間オートマトン). 時間オートマトン A =(L, l0 , T, I, C, A)，C : クロックの有限集合;，A : アクションの有限集合;，L : ロケーションの有限集合;，l0 ∈L :初期ロケーション;，T ⊂ L × A × 2

c(C)× R × L;，

ここで, 2c(C) : ガード群;，R = 2C : リセットクロッ
ク群;，I ⊂ (L → 2c(C) ) : インバリアント付加関数.
a,g,r

遷移 t = (l1 , a, g, r, l2 ) ∈ T は l1 −→ l2 と表記する．ν : C → R≥0 はクロックに値を割り当てる関数である．さらに，ν のドメインを ν ∈ RC
≥0 と拡張することができる．d ∈ R≥0 に対して，(ν +d)(x) = ν(x)+dとし，r ∈ 2C に対して，r(ν) = ν[x 7→ 0], x ∈ r とする．また ν 全体の集合を N と表記する．
さらに，時間オートマトンの意味は次のように与え∪C としたとき，ν ∈ RC≥01≤i≤n iCとする．また s0 = (⃗l0 , 0 ) (⃗l0 = (l1,0 , . . . , ln,0 )) である．⃗l [li′ /li ] は ⃗l の li を li′ に置き換えたベクトルを表ン) とする．C =2.1 一般的な時間オートマトン

ることができる．

トワーク時間オートマトン A := A1 ||A2 || · · · ||An に対して遷移システム (S, s0 , →) が定義される．(⃗l , ν) ∈S に対して，⃗l = (l1 , . . . , ln ) (li は Ai 上のロケーショ

す．ネットワーク時間オートマトンの遷移 → は次のように定義される．

• Ai の全アクション a に対して，
a(⃗l , ν) ⇒ (⃗l [li′ /li ], r(ν))
a,g,r

if li −→ li′ (∈ Ti ) and g(ν)• Ai ，Aj (i ̸= j) の半アクション x!，x? に対して，
x(⃗l , ν) ⇒ (⃗l [li′ /li , lj′ /lj ], ri ∪ rj (ν))
if li

x!,gi ,ri−→li′ (∈ Ti ) and lj

x?,gj ,rj−→lj′ (∈Tj ) and gi (ν) and gj (ν)• d ∈ R≥0 に対して
d(⃗l , ν) ⇒ (⃗l , ν + d), if ∀i, ∀d′ ≤ d, I(li )(ν + d′ )DBM D を 用 い て S の 部 分 集 合 を (⃗l , D)⃗{(l , ν)|ν ∈ D} と表記する．

∈

2.3 UPPAAL 拡張時間オートマトン
時間モデル検査器である UPPAAL では，標準的な時

間オートマトンに対して拡張を行った拡張時間オート
マトンを検証モデルとしている7) ．本節では，UPPAAL
拡張時間オートマトンの構成要素の中で，本稿で利用する整数変数，Broadcast Cannel，ロケーションについて説明する．

2.3.1 整 数 変 数
整数変数は，インバリアントやガード制約，変数の代入文に含めることが可能であり，ロケーションの遷移時に値を更新することが可能である．

図 1 CEGAR ループ

2.3.2 Broadcast Channel
本稿では，2 プロセス間の同期を行う Binary Channel

るシミュレーションを行う．さらに，反例が具体モデに加え，現状態で同期可能なプロセスすべてと同期をル上で実行不可能である (そのような反例を偽反例と行う Broadcast Channel を用いる．

呼ぶ) 場合は，偽反例が生じないよう抽象モデルの洗Broadcast Channel として宣言されたチャネル c は，練を行い，再びモデル検査を適用する．CEGAR ルー

c! とラベル付けされた送信側の遷移に対して，現状態

プでは以上の流れを正しい検査結果が得られるまで繰

から実行可能なすべての受信側の遷移 (c? とラベル付り返す．

けされた遷移) と同期する．ただし，c! とラベル付け

2.5 これまでに提案してきた抽象化手法

された遷移に対して，現状態から実行可能な c? とラ

本節では，文献9),10) でこれまでに提案してきた抽象

ベル付けされた遷移が存在しなければ、c! とラベル付

化アルゴリズムを示す．提案してきた抽象化はシステけされた遷移が他の遷移と同期することなく単独で実ムの異常状態への到達可能性に関する検証を目的とし

行される．

ている．

2.3.3 Committed Location

まず初期抽象化によって，抽象化関数 h によって時Committed Location はそのロケーション上での時間

間オートマトン A から抽象モデル M̂ を生成し，M̂

経過が不可能であり，あるプロセスが Committed Lo-に対してモデル検査を行う．モデル検査の結果，反例

cation に遷移した場合は，次に起こるアクション遷移T̂ が発生した場合は，T̂ の系列を h の逆関数 h−1 をは必ず Committed Location から抜け出す遷移でなけれ用いて具体化する．この T̂ を具体化した A 上の実行ばならない．また，同様に時間経過を許さないロケー

系列の集合を T とする．シミュレーションでは T のションとして Urgent Location がある．しかしあるプ

各要素について DBM の操作関数を用いて A 上で実ロセスが Urgent Location へ遷移した場合，そのプロ

行可能かどうかを調べる．T のすべての要素が実行不セスが Urgent Location から抜け出す遷移の前に他の可能であれば，反例 T̂ が実行不可能となるように改プロセスのアクション遷移が割り込むことが許されて良を行わなければならない．提案してきた抽象化アルいる．

ゴリズムでは，改良の際に直接 M̂ の変形を行うので

2.4 一般的な CEGAR ループ

はなく，A に対して等価変形を行い，変形後の時間

モデル抽象化では，過剰な抽象化や誤った抽象化に

オートマトンに対して再び抽象化関数 h を適用し，新よって本来のモデルでは発生するはずのない見せかけしい抽象モデルを生成する．以上の提案アルゴリズムの反例が発生してしまう場合がある．文献 1) では，最による CEGAR ループの流れを図 2 に示す．

初に十分な抽象化を行い，抽象モデル上で見せかけの2.5.1 抽象モデル

反例が発生すればその反例が発生しないように抽象

時間オートマトン A によって生成される抽象モデ化されたモデルを洗練する，CEGAR(Counterexample-

ル M̂ = (Ŝ, ŝ0 , →)
ˆ は A からクロック変数をすべてGuided Abstraction Refinement) アルゴリズムを提案し削除した状態遷移モデルであり，同時に，遷移のラベている．一般的な CEGAR アルゴリズムを図 1 に示す．

ルやロケーションのインバリアントからクロック変数

一般的な CEGAR ループでは，まず最初に十分な抽に関する部分が除去されている．したがって，抽象化象化を行う初期抽象化を行う．次に抽象化を適用した

関数 h : L → Ŝ は定義 2.5 のように与えられる．

モデル (抽象モデル) に対してモデル検査を適用する．

定義 2.5 (抽象化関数 h). 時間オートマトン A =このとき，反例が検出された場合は，その反例が本来(L, l0 , T, I, C, A) に対し，抽象化関数 h : L → Ŝ を以のモデル (具体モデル) 上で実行可能かどうかを調べ

下のように定義する.

図 3 反例
図 2 これまでに提案している抽象化• ∀li , lj ∈ L. h(li ) = h(lj ) ⇐⇒ li = lj
同様に抽象化関数 h の逆関数として h−1 : Ŝ → L も定義される．
定義 2.5 の抽象化関数 h を用いて生成される，時間
オートマトン A に対する抽象モデル M̂ を定義 2.6 で与える．
定義 2.6 (抽象モデル). 時間オートマトン A=(L, l0 , T, I, C, A) を定義 2.5 の抽象化関数 h によって抽象化したモデル M̂ = (Ŝ, ŝ0 , →)
ˆ を以下のように与

図4

洗練後のモデルえる．

• Ŝ = {h(l )|l ∈ L)}

2.5.4 抽象モデル洗練• sˆ0 = h(l0 )• →ˆ = {(lˆ1 , a, lˆ2 )|(l1 , a, g, r, l2 ) ∈ T ∧ ˆ
l1 = h(l1 ) ∧ˆ
l2 = h(l2 )}抽象モデル上の反例が偽反例である場合，図 3 のように，初期状態 (l0 , 0C ) からは到達可能であるが次のロケーション lnext への遷移が不可能であるような状

定義 2.7 (反例). M̂ 上の反例は抽象状態 Ŝ の系列であ態の集合 B1 = (lb , D1 ) と，(l0 , 0C ) からは到達不可

り，長さ n の反例 T̂ は T̂ = ⟨ŝ0 , · · · , ŝn ⟩ と表記する．

能であるが lnext への遷移が可能であるような状態の

反例 T̂ = ⟨ŝ0 , · · · , ŝn ⟩ に対し，A 上で T̂ に対応す
る遷移の系列の集合 T は抽象化関数の逆関数 h−1 を集合 B2 = (lb , D2 ) の両方が縮約されている抽象状態l̂b が存在する．このとき ˆ
lb を Bad State と呼ぶことと用いて以下のように求められる．

する．このような場合，本来 (l0 , 0C ) からは到達不可

T = {(l0a1 ,g1 ,r1−→ l1

a2 ,g2 ,r2−→ · · ·an ,gn ,rn

−→

ln )|

( li = h−1 (si ) for 0 ≤ i ≤ n ) ∧( (li−1 , ai , gi , ri , li ) ∈ T for 1 ≤ i ≤ n )}

能な状態集合 B2 からの遷移によって，偽反例が生じてしまう．したがって，B2 に対応する抽象状態へ偽反例のパスでは到達不可能となるように洗練をおこなう必要がある．提案アルゴリズムでは，具体モデル上

2.5.2 初期抽象化

で B1 に対応するロケーション lb′ を複製し，lprev か

初期抽象化では時間オートマトン A = (L, l0 , T, I,ら lb への遷移を削除することによって，抽象モデル

C, A) に対して抽象化関数 h を適用し，抽象モデル M̂

においても B2 が縮約されている抽象状態へ到達不能を生成する．

となるように洗練を行う．図 4 は洗練後のモデルを示

2.5.3 シミュレーションしている．図 4 の点線で描かれた遷移は洗練によってシミュレーションでは，反例 T̂ に対応する A 上の削除された遷移を表している．なお B1 はシミュレー

遷移の系列の集合 T に対し，T の各の系列 t についション時に同時に求めることができる．

てシミュレーションを行う．シミュレーションでは時

2.5.5 提案してきた手法の問題点

間オートマトンのクロックに関する状態空間を操作す

これまでに提案してきた抽象化アルゴリズムをネッ

5)

ケーションから最後のロケーションまで到達可能であトワーク時間オートマトンに対して適用する場合，抽象モデルの洗練の際に，状態集合 (⃗l , D) の複製や遷るかどうかを調べる．

移 (⃗l , ν) ⇒ (⃗l [li′ /li ], r(ν)) の削除などの操作が必要とるためのデータ構造 DBM を利用し，t の先頭のロaなる．このとき，洗練操作の対象はネットワーク時間
li

オートマトンの意味モデルとなっている．したがって，’

l ia’com?

ネットワーク時間オートマトンに対して既存の抽象化
l comを適用するためには，事前にネットワーク時間オート

a’com!

’l com

マトンのすべてのプロセスを並列合成したモデルを記
図 5 独立な遷移の同期

述する必要がある．このように事前にプロセスを並列合成したモデルをモデル検査器に入力すると，モデル検査の際のメモリ消費量が大幅に増加してしまい，抽

ルでは，2n 個の大域変数を新たに追加する．Ai の象化の効率を低下させてしまうことが問題となってい現状態を管理する整数を stati ，直前に実行した遷移

る．これは，事前に並列合成を行うことにより，Partialを管理する変数を tri と表記する．各プロセスの各ロ

Order Reduction8) など，モデル検査時に並列プロセス

ケーション，遷移には固有の ID を割り当て (l の IDの状態探索を効率的に行うテクニックが活用できないを Idloc (l )，遷移 t の ID を Idtr (t) とする)，Ai の各

ことが原因の一つとして挙げられる．したがって，並遷移 ti = (l1 , a, g, r, l2 ) について，stati := Idloc (l2 )，列プロセスを合成せずに，別々のプロセスとして表現

tri := Idtr (ti ) という代入文を付加する．このようにす

したまま洗練操作が適用可能となるように洗練操作をることで，Ai の現在のロケーションは Idloc (l ) = stati

改良する必要がある．

であるようなロケーションであり，直前に実行した遷3. 提案する洗練手法

移は Idtr (t) = tri であるような遷移であることが他プロセスからも把握することができる．
また，同様に Acom の管理変数 statcom ，trcom も本章では，2.5 節で述べた既存の抽象化手法の改善
手法を述べる，これまでの手法では，ネットワーク時

追加する．

間オートマトンを入力とした場合，予め並列プロセス

3.2 他のプロセスの遷移との同期の合成を行い一つのプロセスとして表現した後，抽象

本節では Acom と他のプロセスとの同期方法を述べ化を適用していた．改善手法では，事前の並列合成を′る．ここでは，Acom の遷移 tcom = lcom −→ lcom

行わず，別々のプロセスとして表現したまま抽象化をを他のプロセスの遷移と同期させることを考える．こ

適用する．

のとき，同期させる遷移が，全アクションによる遷移

a,g,r

提案手法の基本的なアイデアとしては，モデル検査，(単一プロセス内で行われる遷移) である場合と，半アシミュレーションによって検出した偽反例を取り除く

クションによる遷移 (他のプロセスの遷移と同期するために必要となる部分に関して，部分的な合成モデル

遷移) である場合のそれぞれについて説明する．

を生成し，部分的に合成したプロセスの動作とその他

i) 全アクションによる遷移
a ,g ,rのプロセスの動作を同期させることで，本来は実行不i i ′Ai の独立な遷移 ti = li i−→li と同期させる場可能であるような動作を制限する．このとき部分的に合，新たな 2 プロセス間のチャネル a′com を生成し，合成したモデルを Acom と表記する．

a′com を通じて tcom と ti を同期させる (図 5)．

提案手法では，ネットワーク時間オートマトン A =ii) 半アクションによる遷移

A1 || · · · ||An に対して，部分的な合成モデル Acom を′

tcom と同期させる遷移を ti = lia?,gj ,rj

lj′a!,gi ,ri−→li′ tj =追加した A = A1 || · · · ||An ||Acom に対して初期抽象

lj

化，モデル検査，シミュレーション，モデルの洗練操アクションを実行できないため，Ai ，Aj にそれぞ作を適用する．

れ新たなロケーション li′′ ，lj′′ を生成し，新たに遷移提案手法では，Acom が他のプロセスの動作を制御するために，新たに大域整数変数を追加している．また，チャネルや Committed Location を利用して Acom
が他のプロセスの遷移と同期して動作するようにしている．

−→(i ̸= j) とする．同一の遷移で複数のa′com ,gj ,rj ′′a′com ,gi ,ri ′′−→ li ，t′j = lj−→ li を追加する．
このとき a′com は Broadcast Channel であり，遷移 tcom′′ a!,gi ,ri ′との同期を行う．さらにそれぞれ t′′−→ li ，
i = lia?,gj ,rjt′′j = lj′′ −→ lj′ を生成し Ai と Aj の遷移を同期さ

t′i = liせる．また，これらの遷移が連続して実行されるよう

3.1 管 理 変 数に，生成するロケーション li′′ ，lj′′ は Committed Loca-

各プロセスの現状態と，直前に実行した遷移を管理

tion とする．図 6 は Acom と同期させる遷移が互いにするために，各プロセスごとに 2 つの大域整数変数

同期する遷移である場合の図である．c と書かれたロを追加する．したがって n 個のプロセスを持つモデ’lia’com?

’’i
c

l

a!
l com

’

lj

l i

l j

a’com?
a’com!

’’j
c

l

a?

’

l com

3.4.1 前 処 理
提案手法による CEGAR ループを実行する前処理として，Acom を生成する．Acom のロケーション集合
Lcom は A の初期状態の集合 (⃗l0 , D0 ) を表す lcom,0とそれ以外の状態を表現する lother のみから構成される．また，(⃗l0 , D0 ) から実行可能なアクション遷移は
すべて Acom の lcom,0 から lother への遷移と同期さ

図6

互いに同期する遷移との同期せる必要がある．

3.4.2 初期抽象化
ケーションは Committed Location を表している．

A の個々の時間オートマトンから，クロック変数，

3.3 部分的な合成モデル Acom

クロック変数に関する制約式やリセット式などを削除提案手法では，抽象モデル上の偽反例を除去するたする．このとき，整数変数やチャネルは保持する．まめ，部分的な並列合成モデル Acom を生成し，モデル

た，Acom はクロック変数を持たず，他のクロック変全体の動作を制限する．モデルの動作を制限する必要数を参照することもないため，Acom には処理は行わがあるのは偽反例に関する部分であり，Bad State である ⃗lb への遷移と ⃗lb からの遷移を制限する必要があない．

る．したがって，提案手法では抽象モデルの洗練の際に，(⃗lb , D1 ) を表現する合成ロケーション lcom,b を追ない有限オートマトンのネットワークとして表現する

加していく．

トマトンの状態の積として表現可能である．以降ではAcom はクロック変数を持たないプロセスであり，Acom のロケーション集合 Lcom は以下の要素から構成される．

• 初期状態の集合 (⃗l0 , D0 ) ((⃗l0 , 0C ) から時間遷移のみによって到達可能な状態集合) が合成されたロケーション lcom,0• 状態の複製が適用される状態集合 B1 = (⃗lb , D1 )を表現する合成ロケーション

また，生成される抽象モデルはクロック変数を持たことができる．従って抽象モデルの状態は各有限オー
ネットワーク時間オートマトンのロケーションベクトˆル ⃗l に対応する抽象状態を⃗l のように表現する．

3.4.3 モデル検査
A ′ に対して初期抽象化を行ったモデルに対してモ
デル検査器を用いて検証を行う．

3.4.4 シミュレーション
モデル検査によって検出された反例 T̂ について対応する A ′ 上の遷移の系列 T を求め，T に含まれる• 上記以外の状態集合を表すロケーション lother

すべての系列についてシミュレーションを行う．各系

Acom では，偽反例を除去するために状態の複製を適用する状態 B1 = (⃗lb , D1 ) に対する合成ロケーショ

列のシミュレーションはネットワーク時間オートマト

ンが追加されていく．しかし，それ以外の状態をすべとで，実現することができる．

て lother として表すことで，A のすべての状態を合成することを回避している．つまり，Acom は偽反例を取り除くために必要な部分のみが合成されているよ
うな合成モデルであると言える．

ンの意味モデルに従い DBM の操作関数を適用するこ

3.4.5 抽象モデル洗練
抽象モデルの洗練では，シミュレーションによって得′られる B1 = (⃗lb′ , D1 )，⃗lb′ の前後のロケーション ⃗lprev
，
′
′
′
′
⃗lnext を用いる．⃗lb ，⃗lprev ，⃗lnext において A のロケー

3.4 提案手法による CEGAR ループ

ションベクトルをそれぞれ ⃗lb ，⃗lprev ，⃗lnext ，Acom の提案手法による抽象化方法について各ステップごとロケーションをそれぞれ lcom,b ，lcom,prev ，lcom,nextに説明する．前述のとおり，提案手法では，ネットワーと表すこととする．

ク時間オートマトン A = A1 || · · · ||An に対して，部

抽象モデルの洗練手法は，状態の複製，遷移の複分的な合成モデル Acom を追加した A ′ = A ||Acom

製，遷移の除去の操作から構成されている．状態のに対して初期抽象化，モデル検査，シミュレーション，

複製，遷移の複製，遷移の除去のアルゴリズムはそ

モデルの洗練操作を適用する．以降では，記号の右肩

れぞれ図 7，8，9 に示している．なお，アルゴリズに ‘ ′ ’(プライム) を添えた場合，A に Acom を追加

ム中では記述を簡単化するため，ネットワーク時間′

した A の要素を表し，右下に ‘com’ を添えた記号は

オートマトン A = A1 || . . . ||An を仮想的に合成した

Acom の要素を表している．

A = (L, l0 , T, I, C, A) という表現を用いている．またネットワーク時間オートマトン上の非同期の遷移まDuplicateState
Input Acom , B1 = (⃗lb′ , D1 ){Acom = (Lcom , lcom,0 , Tcom , Icom , Ccom , Acom )}lcom,new := newLoc() {Generate a new location lb′ }Lcom := Lcom ∪ {lcom,new }I( lcom,new ) := Invariant(D1 ){A set of inequalities representing
V D1 }I(lcom,new ) := I(lcom,new ) ∧ 1≤i≤n (stati ==Idloc (lb,i )){lb,i is the i-th element of ⃗lb }図7

Duplication of States

RemoveTransition
Inputs A ′ , B1 = (⃗lb′ , D1 ), ⃗tb = (⃗lprev , a, g, r,⃗lb ), lcom,new{⃗tb : a transition to ⃗lb }if lcom,prev ̸= lother thenforeach tb,i = (lprev,i , ai , gi , ri , lb,i ) such that tb,i isan element of ⃗tb and also a transition of Ai do
gi := gi ∪ {statcom ̸= Idloc (lcom,new )}end forelse
I( lcom,b
V ) := I( lcom,b )∧tb,i is the element of ⃗tb tri ̸= Idtr (tb,i )end if
図9

DuplicateTransition
Inputs A ′ , B1 = (l⃗b′ , D1 ), ⃗tb , lcom,new{⃗tb = (⃗lprev , a, g, r,⃗lb )}acom := newChannel() {generate a new channel}
tcom,new := (lprev,com , acom , ∅, ∅, lcom,new ){generate a transition to the duplicated locationlcom,new }Tcom := Tcom ∪ {tcom,new }⃗tnew := (⃗lprev , acom , g, r,⃗lb ) {duplicate the transition ⃗tb }T := T ∪ {⃗tnew }Synchronize(tcom,new , ⃗tnew )foreach ⃗tsucc = (⃗l1 , a, g, r,⃗l2 ) ∈ T such that ⃗l1 = ⃗lb do
Succ := Reach(A , (⃗lb , D1 ), ⃗tsucc ){Reach returns the reachable state set from (⃗lb , D1 )}if Succ ̸= ∅ thenacom := newChannel() {generate a new channel}⃗tnew := (⃗lb , acom , g, r,⃗l2 ){duplicate the transition ⃗tsucc }T := T ∪ {⃗tnew }if A location corresponding to the state set Succ is already generated thentcom,new := (lcom,new , acom , ∅, ∅, lcom,succ ){lcom,succ is the location corresponding to Succ}
else
tcom,new := (lcom,new , acom , ∅, ∅, lcom,other )end ifTcom := Tcom ∪ {tcom,new }Synchronize(tcom,new , ⃗tnew )gnew := g ∪ {statcom ̸= Idloc (lcom,new )}setGuard(⃗tsucc , gnew ){set the guard condition gnew into ⃗tsucc }end ifend for
図 8 Duplication of Transitions

たは同期する複数の遷移を仮想的に ⃗t′ というように表記する．
状態の複製では 2.5 節の図 3 の状態集合 B1 を複製する．提案手法は (⃗lb , D1 ) を表現する合成ロケー
ション lcom,new を生成し，Acom へ追加する．Acomに複製されたロケーション lcom,new は複製の元となる∧⃗l = (l1 , . . . , ln ) について，
stati == Idloc (li )1≤i≤nというインバリアントを付加し，他のプロセスの状態

Removal of Transitionsが ⃗l のときのみ lcom へ到達するようにしている．これは，Broadcast Channel で同期させる際に，意図しないプロセスとの同期を防ぐためである．状態の複製は
図 7 のアルゴリズムによって行われる．
遷移の複製 (図 8) では複製した状態への遷移と複製した状態からの遷移をそれぞれ複製する．提案手法では
まず lcom,prev から lcom,new への遷移の複製 tcom,newを生成し，⃗lprev から ⃗lb への各遷移と同期させる (図8 : 2–9 行目)．アルゴリズム中の関数 Synchronize
は Acom 上の遷移と A 上の遷移を同期させる関数である．遷移の同期については 3.2 節で示した方法で行う．さらに A において (⃗lb , D1 ) からアクション遷
移，時間遷移を一回ずつ行うことによって到達可能な状態を求める．そして (⃗lb , D1 ) から到達可能な各状態(⃗lsucc , D) について Acom 上で対応する状態 lcom,succが存在するならば lcom,new から lcom,succ への遷移を複製する．対応する状態 lcom,succ が存在しないならば

lcom,new から lother への遷移として複製する．なお，これらの遷移は ⃗lb から ⃗lsucc への各遷移と同期させる(図 8 : 10–32 行目)．また，28–29 行目では，Acom がlcom,new である状態で複製の素となる遷移が実行されないように，遷移のガード制約を操作している．
′
遷移の削除 (図 9) では，⃗lprev
から ⃗lb′ への遷移を削除する．提案手法では，⃗lprev から ⃗lb への各遷移にstatcom ̸= Idloc (lcom,prev ) とおいうガード制約を追′加し，Acom が lcom,prev に滞在する間は ⃗lprev
から ⃗lb′への遷移を実行不可能にする．このとき，lcom,prev が′lother である場合は，このような制約を加えると ⃗lprev
から ⃗lb′ への遷移以外の遷移も削除されてしまう．このような場合は lcom,b のインバリアントで，直前に実行する遷移を制限する制約を記述することで遷移の削除を実現している．⃗lprev から ⃗lb への遷移を ⃗tb とす
ると，具体的には lcom,b のインバリアントに対して，

p

P1

stat2 == 0

t

other

acom!
statcom := 1
tr com := 0

p

u

r

stat1 == 0 &&a?

a!

q x > 10

図 10

p_s

s

v

y == 10

P2

ネットワーク時間オートマトンの例

acom?

s
a!

stat1 := 1
tr1 := 0

stat1 := 1
tr 1 := 1qc tra!:=21
q_cr

stat1 := 2
tr 1 :=3

acom?

stat2 := 1
tr2 := 0a?
ct_c tr2 := 2a?

stat2 := 1
tr 2 := 1t

stat2 := 3
tr2 := 4

stat2 := 2
tr 2 := 3vu⃗tprev の各要素 tb,i について，tri ̸= Idtr (tb,i ) という制約を追加する．

P1

このように偽反例を検出するたびにインクリメンタ

P2

図 11 部分合成モデルを追加したモデル

ルに Acom が構成される．また，検出された偽反例がこれまでに検出した偽反例と独立であれば，偽反例をアクションによる遷移であることから，Acom と同期さ除去するためのパスがそれまでの Acom とは独立に生せる際に Committed Location を介している．また，図11 では Acom が p s である状態のまま遷移 (p → q)，

成されていく．

3.4.6 考察(s → t) を実行することは， Acom のロケーション p s

提案手法では，ネットワーク時間オートマトン A にのインバリアント (stat1 == 0)&&(stat2 == 0) に対して部分的な並列合成モデル Acom を用いて A のよって制限されている (Idloc (p) = 0，Idloc (s) = 0)．

動作を制御している．Acom で制御するのは，クロッ

図 11 のモデルに対してモデル検査を適用すると，

ク変数を持つ本来のモデルでは実行不可能となるよう⇒ (other, (q c, t c)) ⇒ (other, (q, t)) ⇒(p s, (p, s)) comaa

な動作であり，本来制限すべきでない動作を制限する(other, (q, v))

ことはない．したがって A に Acom を加えたモデルという反例が検出されるが，これは偽反例である．このは A と等価であると言える．

偽反例に対するモデルの洗練では，状態集合 ((q, t), D1

また，抽象化洗練の各ループにおいて，状態の複製の複製を行う．なお D1 は x == y ∧ x > 10 を満たす

によって複製された状態 lcom,new が Acom に追加されような状態の集合である．提案手法では ((q, t), D1 ) をていくが，このとき，遷移の複製によって lcom,new か意味する状態 q t を Acom へ生成し，遷移 (p → q c)，

ら到達可能な遷移はすべて複製しており，前回のルー(s → t c) と遷移 (p s → q t) 同期させ，P2 の遷移

プにおける Acom との整合性が保たれるようにして(t → v) に (statcom ! = 2) というガード制約を与える

いる．

ことで，偽反例をモデルから除去している．提案手法

3.5 洗練手法適用例
提案手法を用いて偽反例を取り除く例を示す．
図 10 はネットワーク時間オートマトンの例である．

による洗練を適用したモデルを図 12 に示す．

4. 実

験

図 10 の例では，プロセス P2 のロケーション v を異

本章では，提案手法による抽象化洗練手法を実装し，常状態とし，異常状態への到達可能性を検証する．図

例題に適用した結果を示す．実験では実行時間，メモ

10 の例を初期状態から実行した場合，ロケーション

リ消費量という点について既存手法との比較を行う．

(q, t) へ到達した時点で，x == y ∧ x > 10 が成り立っ

なおモデル検査では UPPAAL のモデル検査モジューている．これより y > 10 も成り立つため，P2 の v へル verifyta を利用している．実験環境は以下の通りでは到達不可能である．

ある．

このモデルに対して，部分合成モデル Acom を追加し，初期抽象化 (すべてのクロック変数を除去) を適用したモデルを図 11 に示す．Acom は初期状態 p s とother から構成されている．各プロセスの初期ロケー

OS
CPUMemoryUPPAAL::::

Fedora 7
AMD Athlon(tm) 64 Processor 3400+ 2.2GHz
930MB
version 4.0.6

ションからの遷移はすべて Acom の遷移 (p s → other)と同期させている．なお，遷移 (p → q)，(s → t) は半提案手法を適用する例題として，Fischer の相互排除

表 1 Fischer の相互排除プロトコルに対する実験結果
既存手法
提案手法

Proc
2
3
4
5
6
7
8

stat1 == 0 &&stat2 == 0

p_sstatcom := 1
tr com := 0

statcom := 2 trcom := 1

stat2 == 1

stat1 := 1
tr1 := 0

q_tacom,2?

stat1 := 2
tr1 :=3

P1

stat2 := 1
tr2 := 0a?
ct_c tr2 := 2

loop
5
13
25
41
61
85
N/A

time
2.06s
15.1s
36.6s
102s
360s
1329s
4723s

mem
19.5MB
36.9MB
37.6MB
39.5MB
45.0MB
61.0MB
129MB

loop
3
15
28
45
66
91
120

ルと並列合成後のモデル) ため，verifyta による状態探索の順序に違いが生じ，発生した反例が異なったためであると考えられる．CEGAR ループによる抽象モデ
ルの洗練は発生する反例に依存するため，このような差が生じたものと考えられる．

acom,1?

stat1 := 1
tr 1 := 1c tra!:=2
1
q_c
racom,2!

s
a!

q

mem
2.82MB
2.82MB
21.6MB
48.1MB
95.0MB
293MB
N/A

statcom := 1
trcom := 1pacom,1?

time
0.74s
2.44s
10.9s
69.4s
662s
12571sN/A

other

acom,0!

acom,1!
stat1 == 1 &&

clock
2
3
4
5
6
7
8

なお，文献 6) では，本例題に対して純粋に UPPAAL
のみを用いて検証を行った結果を示しており，各プロ

a?

t

stat2 := 1
tr 2 := 1

acom,2?

stat com != 2

acom,2?

stat2 := 3 tr2 := 4

stat2 := 2
tr2 := 3uv
P2

図 12 洗練後のモデル

セスの対称性を利用した Symmetry Reduction により，メモリ消費量はプロセス数に対して線形的な増加に抑えられている．よって本例題のようにプロセス間に対称性があるような例題に対しては提案手法による抽象化よりも Symmetry Reduction が有効であると考えられる．今後の課題としては，プロセス間に対称性が存在せず Symmetry Reduction を利用できない例題に対して提案手法を適用し，提案手法による抽象化の有効7)

プロトコル ，を選択し実験を行った．実験結果を表 1

性を評価することが挙げられる．また，このような対に示す．Proc はモデルを構成するプロセス数，Clock称性を利用し，抽象モデルの洗練を効率的に行う方法

はモデル全体のクロック変数の個数である．既存手法の考案も課題として挙げられる．

の列は事前にモデル全体を並列合成し，抽象化を適用した結果を示し，提案手法の列は提案手法による実験

5. お わ り に結果を示している．time は CEGAR ループ全体の実行

本稿では，著者らがこれまでに提案してきた時間

時間，mem はモデル検査で消費した最大のメモリ量，

オートマトンに対する抽象化洗練手法に関する問題点

loop は CEGAR ループの繰り返し回数である．既存手の改善を行った．既存の抽象化手法では, 複数のプロ

法の 8 プロセスに対する実験では，並列合成によりロセスが並列に動作するようなモデルを検査する場合，ケーション数が 48 個となり verifyta の仕様により実事前に複数のプロセスを並列合成する必要があり，抽行不可能であった．

象化効率の低下の原因となっていた．本稿では，この表 1 の結果より，5 プロセス以上では提案手法がメような問題を解決するため，そのような合成を部分的

モリ消費量の点で優れていることがわかる．特に 7 プにとどめるような手法を提案した．また提案手法を簡ロセスではメモリ消費量を約 80 パーセント削減でき，単な例題に対して適用し，メモリ消費量，実行時間の既存手法では適用不可能であった 8 プロセスのモデル

両面において既存手法を改善できていることを示した．

でも適用できるなど，提案手法が有効であることを示

今後の課題としては，アルゴリズムを並列化し，抽している．さらに，実行時間についても 7 プロセスで象化全体の実行時間を縮小することが挙げられる．まは約 90 パーセント削減しており，実行時間の点でもた，より規模の大きい例題に適用し，提案手法の有効提案手法が優れた結果を示すことができた．

性を評価したいと考えている．

提案手法と既存手法で CEGAR ループの回数が異なっているのは，提案手法と既存手法では入力となるモデルの表現方法が異なっている (並列プロセスモデ

参 考

文 献

1) E. Clarke, O. Grumberg, S. Jha, Y. Lu, and V. Helmut: “Counterexample-guided Abstraction Refinement,” Computer Aided Verification:12th International Conference, vol.1855, pp.154-169, 2000.
2) E. Clarke, A, Gupta, J. Kukula, and O. Strichman: “SAT based Abstraction-Refinement using
ILP and Machine Learning Techniques,” Computer
Aided Verification:14th International Conference,
vol.2404, pp.695-709, 2002.
3) R. Alur: “Techniques for Automatic Verification of
Real-Time Systems,” PhD thesis, Stanford University, 1991.
4) R. Alur, C.Courcoubetis, and D. L. Dill: “Modelchecking for real-time systems,” In Proceedings of
the 5th Annual Symposium on Logic in Computer
Science, pp.414-425. IEEE Computer Society Press,
1990.
5) J. Bengtsson, and W.Yi: “Timed Automata: Semantics, Algorithms and Tools,” Lectures on Concurrency and Petri Nets, vol.3098, pp.87-124, 2004.
6) G.Behrmann, A.David, K. G. Larsen, J. Håkansson,
P. Pettersson, W. Yi and M. Hendriks: “UPPAAL
4.0,” In Proc. of the 3rd Int. Conf. on the Quantitative Evaluation of Systems (QEST), pp125-126,
IEEE Computer Society, 2006,
7) 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 of Computer,
Communication, and Software Systems, vol.3185,
pp.200-236, 2004
8) J. Håkansson, and P. Pettersson: “Partial Order Reduction for Verification of Real-Time Components,”
In Proc. of the 5th Int. Conf of Formal Modellingand Analysis of Timed Systems, vol.4763, pp211226, 2007.
9) 長岡 武志，岡野浩三，楠本真二: “UPPAAL 拡張
時間オートマトンの反例に基づく抽象化改良ループによるモデル抽象化手法,” 電子情報通信学会技術研究報告，vol.107，No.176，pp.77-82，2007
10) T. Nagaoka, K. Okano, and S. Kusumoto: “Abstraction of Timed Automata Based on CounterexampleGuided Abstraction Refinement Loop,” IEICE Technical Report, vol.107, No.505, pp.103-108，2008.