Development and Evaluation of Symolic Model-Checker Based on Approximation for Real-Time Systems

(1)

実時間システムのための近似手法に基づいた記号モデル検査器の開発と評価

山根智

^†

中村一博

^††

Development and Evaluation of Symolic Model-Checker Based on Approximation for Real-Time Systems

Satoshi YAMANE

^†

and Kazuhiro NAKAMURA

^††

あらまし本論文では，近似手法に基づく実時間システムの記号モデル検査について述べる．実時間システムの記号モデル検査では，時間付き状態の処理に起因する検証コストの増大をいかに削減するかが重要な課題である．一方，実時間システムの到達可能性解析では，正確な時間付き状態の代わりに近似状態集合を用いる検証手法が提案され，検証コストの削減に効果を上げている．そこで我々は，近似状態集合を用いた実時間システムの記号モデル検査手法を提案する．検証アルゴリズムは，時相論理式に応じて近似手法に基づく不動点計算を行い，

近似状態集合を算出する．我々は提案アルゴリズムを実装し，既存の実時間記号モデル検査器との比較を行った．

そして，提案手法がクロック変数を多く含む大規模システムの検証に有効であることを示す結果が得られた．

キーワード記号モデル検査，実時間システム，2分決定グラフ，近似手法，時相論理

1.

まえがき

通信プロトコルやオペレーティングシステム，論理回路などの実時間システムの多様化に伴って，形式的手法を用いた自動検証が重要になっている．

実時間システムの動作は，論理的な正当性だけでなく，タイミングの正当性が要求される．そのため，検証性質の記述性に優れ，有限状態システムが時相論理式を充足するかどうかを自動判定するモデル検査手法の研究がなされ検証に効果を上げている

[1], [2]

．一般に，実時間システムのモデル検査では，時間に依存したシステムの動作を解析するために，リージョングラフと呼ばれる状態グラフが生成される

[1]

．しかし，

リージョングラフのサイズは非常に大きくなるため，

検証コストを削減するヒューリスティックな手法が提案されている．

Henzinger

らは，完全なリージョングラフではなく，時相論理式の充足性により区別されな

†金沢大学工学部情報システム工学科，金沢市

Faculty of Engineering, Kanazawa University, 2–40–20 Ko- datsuno, Kanazawa-shi, 920–8667 Japan

†名古屋大学情報メディア教育センター，名古屋市

Center for Information Media Studies, Nagoya University, Furo-cho, Chikusa-ku, Nagoya-shi, 464–8603 Japan

い状態の和集合を論理式によって記号表現して記号検証する手法を提案している

[3]

．

Larsen

らは，並列プロセスに関してプロセスごとに検証可能とする構成的な検証手法を提案している

[4]

．

一方，実時間システムの

safety

検証を行う近似的手法が

Dill

らにより提案され，大規模システムの検証が可能であることが示された

[5], [6]

．この手法は，最小不動点計算による

safety

検証で，近似手法により実時間システムの状態とタイムゾーンを，

BDDs (Binary De- cision Diagrams) [9]

と

DBMs (Diﬀerence Bounded Matrices) [10], [11]

により記号表現し検証を行う．

本論文では，

liveness

検証のための近似手法に基づいた記号モデル検査手法を提案する．一般に，記号モデル検査は，部分論理式を充足する状態集合の再帰処理により，論理式を充足する状態集合を求めることで実現される．我々は，この処理を近似手法に基づいて行うアルゴリズムと，最大不動点計算の近似アルゴリズムを導入し記号モデル検査を実現する．また，

この記号モデル検査手法を実装し，イーサネットの

CSMA/CD

プロトコルの検証への適用と既存の実時

間記号モデル検査器

[3], [4]

との比較を行った．その結果から，クロック変数を多く含む大規模システムのモ

(2)

デル検査に有効であることを示す．

以下

2.

^{では準備，}

3.

では実時間近似モデル検査手法，

4.

では記号モデル検査器の実装と評価を示す．

2.

準備

本章では，実時間システムを記述する時間

Kripke

構造と，検証性質の記述に用いる時相論理

(Computation Tree Logic, CTL)

の定義を示す．

2. 1

時間

Kripke

構造

本節では，時間オートマトン

[7]

に基づいた時間

Kripke

構造の定義を示す．

［定義

1

］（時間

Kripke

構造の構文）

時間

Kripke

構造は

M = ( Q, P, T, Q

⁰

)

により定義される．ここで，

• Q

^{は有限状態集合，}

• P

は

Q → 2

^AP で，各状態に成立する原子命題の集合を割り付けるラベリング関数，

• T

^は

T ⊆ Q × Q × 2

^C

× Φ( C )

で，時間付き状態遷移関係，

• Q

0

⊆ Q

^{は初期状態集合．}

である．ただし，

AP

は原子命題の集合，

C

はクロック変数の集合，

Φ( C )

はタイミング制約式

δ

^の集合である．そして，

y

^{をクロック変数，}

d ∈

^N を時間定数とすると，

δ

は次のように再帰的に定義される：

δ ::= y ≤ d | y ≥ d | ¬δ | δ

1

∧ δ

2

.

q, q

, λ, δ ∈ T

は状態

s

から

s

への状態遷移，

λ

はリセットアクションによりリセットされるクロック

変数集合を表す．

✷

以下の遷移システムにより時間

kripke

構造の操作的意味を定義する．

［定義

2

］（遷移システム）

遷移システムの状態は，状態

q

^{とクロック変数値の}

n

^{次元ベクトル}^x

∈

^Rⁿの組

q,

^x

とする．

時間

Kripke

構造

M = ( Q, P, T, Q

0

)

に対する，状態遷移システムは

M

= ( S, S

0

, N )

により定義される．

ここで，

• S ⊆ Q ×

^Rⁿ^{は時間付き状態集合，}

• S

0

= {q

0

,

^x0

| q

0

∈ Q

0

,

^x0

= 0}

^{は初期状態} 集合，

• N

は状態遷移と時間の経過を表す遷移関係で，

リセットアクション

a (

^x

, λ )

と，タイミング制約式に成立するタイムゾーンを割り当てる関数

I : Φ( C ) → 2

^Rⁿ を含む状態遷移

N

state

= { ( q,

^x

, q

,

^x

) | ( q, q

, λ, δ )

∈ T,

^x

∈ I ( δ ) ,

^x

= a (

^x

, λ )}

と，時間の経過を表す

N

time

= { ( q,

^x

, q,

^x

+

^t

) | q ∈ Q,

x

,

^t

∈

^Rⁿ

}

の和

N = N

state

∪ N

time である．

✷

2. 2

時相論理

(CTL)

本節では，検証性質の記述言語として用いるとき相

論理

(CTL)

のサブセットの定義を示す．近似手法によ

る部分論理式ごとの再帰処理において，近似の一貫性を保つために，論理否定を除いたサブセットを用いる．

［定義

3

］（

CTL

の構文）

CTL

式

φ

は次のように再帰的に定義される．

φ ::= p | EXφ | EGφ | Eφ

1

Uφ

2

| EF φ

| φ

1

∨ φ

2

| φ

1

∧ φ

2

ここで，

• p ∈ AP

（原子命題），

• ∨, ∧

は論理和，論理積，

• EXφ

^{はある次状態で}

φ

^{が成り立つ，}

• EGφ

はある状態列で過去の性質

φ

^{が常に成り} 立つ，

• Eφ

¹

Uφ

² ^は

φ

² ^{が成り立つまで常に}

φ

¹ ^が成り立つ，

• EF φ

1 は将来いつか

φ

1 が成り立つで，

E true Uφ

1に等しい．

である．

✷

CTL

の意味は，時間

Kripke

構造の遷移システムに対して定義される．

［定義

4

］（

CTL

の意味）

時間

Kripke

構造

M

^{と時間付き状態}

q

0

,

^x0

^，時相論理式

φ

に対して，

CTL

式

φ

が成立することを

( M, q

0

,

^x⁰

) | = φ

^{と表す．これを}

q

0

,

^x⁰

| = φ

^と記述すると，

CTL

の意味は次のように定義される．

• q

0

,

^x0

| = p iﬀ p ∈ P ( q

0

),

• q

0

,

^x0

| = φ

1

∧ φ

2

iﬀ q

0

,

^x0

| = φ

1

∧ q

0

,

^x⁰

| = φ

²

,

• q

⁰

,

^x⁰

| = φ

¹

∨ φ

²

iﬀ q

⁰

,

^x⁰

| = φ

¹

∨ q

0

,

^x0

| = φ

2

,

• q

0

,

^x0

| = EG φ iﬀ

ある状態列

q

0

,

^x0

, q

1

,

^x1

, . . .

に対して，次の

(a)

，

(b)

が成り立つ，

(a) q

i

,

^xi

| = φ ( i ≥ 0)

(b) ( q

i

,

^xⁱ

, q

i+1

,

^xⁱ+1

) ∈ N ( i ≥ 0)

• q

0

,

^x0

| = E[ φ

1

U φ

2

] iﬀ

ある状態列

q

0

,

^x0

,

(3)

q

1

,

^x1

, . . .

^{に対して，次の}

(a)

，

(b)

が成り立つ，

(a) ∃n ≥ 0 , q

n

,

^xn

| = φ

²

,

q

i

,

^xi

| = φ

¹

(0 ≤ i < n ) (b) ( q

i

,

^xi

, q

i+1

,

^xi+1

) ∈ N ( i ≥ 0)

• q

0

,

^x0

| = EX φ iﬀ

ある状態

q

,

^x

^に対して，

q

,

^x

| = φ, ( q

0

,

^x0

, q

,

^x

) ∈ N .

• q

0

,

^x⁰

| = EF φ iﬀ

ある状態列

q

0

,

^x⁰

, q

1

,

^x1

, . . .

に対して，

∃n ≥ 0 , q

n

,

^xn

| = φ , ( q

i

,

^xi

, q

i+1

,

^xi+1

) ∈ N (0 ≤ i < n ) ✷ 3.

実時間記号モデル検査手法

本章では，我々が提案する記号モデル検査手法を述べる．

3. 1

実時間システムの記号表現方法

一般に，実時間システムの状態は，

q

0

,

^z0

のように状態とクロック値のベクトルの対で表現される．以下では，その近似状態集合に着目する．時間

Kripke

構造の状態集合を

Q

，そのタイムゾーン（クロックの値のベクトルの集合）を

Z

とすると，実時間システムの近似状態集合は

Q, Z

のように記号表現される．

Q

^は

2

分決定グラフ

(Binary Decision Diagrams, BDDs)

により記号表現され

[2]

，

Z

^は

time predeces- sors

や

intersection

などのタイムゾーン上の演算が可能な

DBMs (Diﬀerence Bounds Matrices)

により記号表現される

[10], [11]

．なお，正確な和演算

∪

は，本来の時間付き状態集合にのみ適用可能で，

Q, Z

のような表現には適用できない．このため，以下に示す近似演算が用いられる．

BDDs

は広く知られているので，本論文ではその詳細は省略する．しかし，

DBMs

はあまり知られていないので，以下に定義する．

［定義

5

］（

DBMs

の定義）

R

n の

DBMs

はクロック変数

x

1

, . . . , x

n をもち，

( n + 1) × ( n + 1)

の行列

D

^{である．任意の}

i

^に対して，要素

D

i0 はクロック変数

x

i の上限を表して，

要素

D

0i はクロック変数

x

i の下限を表す．任意の

i , j

^{に対して，要素}

D

ij はクロック変数

x

iと

x

jの差の上限を表す．厳密な境界と厳密でない境界を区別

（例えば，

x < 2

と

x ≤ 2

の区別）して，境界が存在しないことを表すために，上限と下限の値の領域は

Z

× {<,≤} ∪ {∞}

とする．具体的には以下のとおりである：

∞

は境界が存在しないことを表して，境界

( c, ≤ )

は

≤ c

^{を表して，境界}

( c, < )

は

< c

^を表す．

例えば，

(0 ≤ x

1

< 2) ∧ (0 < x

2

< 1) ∧ ( x

1

−x

2

≥ 0)

は，以下のように，

DBMs

で表される：

0

B

@

∞ (0 , ≤ )(0 , < ) (2 , < ) ∞ ∞ (1 , < )(0 , ≤) ∞

1

C

A

. ✷

また，

DBMs

は最短パスを求める

Floyd-Warshall

のアルゴリズムにより，標準形が計算できることが知られている．

［定義

6

］（

DBMs

の定義）

DBMs

には，以下の演算が定義できる：

（

1

）積演算：

DBMs D

^と

D

に対して，

DBMs

の積

D = D ∩ D

は，以下のように計算できる

DBMs

D

^の標準形

D

^である：

D

ij

= min{D

ij

, D

ij

}

min{D

ij

, D

ij

}

は，

D

の

ij -

要素と

D

の

ij -

要素の最小値から構成する

DBMs

である．

（

2

）逆像演算：時間経過して

DBMs D

^に到達できる

DBMs D

は以下のように計算できる：

すべての下限の要素

∀i.D

0i を

(0 , ≤ )

で置換．

（

3

）和演算：

DBMs D

と

D

に対して，

DBMs

の和

D

ij

= prejoin ( D, D)

は以下のように計算できる：

D

ij

= max{D

ij

, D

ij

}

（

4

）差演算：

DBMs D

^と

D

^{に対して，}

DBMs

の差

D − D

を定義する．差演算

D − D

は，

D

の

x

i

−x

j

≤ D

ij

ごとに，

D

^から

x

i

−x

j

≥ D

ij

を削り取った部分を集めることによって，計算する．

DBMs

の差

D − D

^{の計算では，}

D ∩ D = ∅

^{のときは差が}

D

^であり，

D ∩ D = D

^{のときは差が}

∅

^{であり，その} 他のときは，以下のように各要素

x

i

− x

jごとに

D

から

D

を削除する．

D

^から

x

i

− x

j

≥ D

ij

を削り取る必要があるかどうかの判定は，まず，

closure ( D)

により，

D

^{の不等式の形式を}

x

i

− x

j

≤ D

ij

^にして，

次に，

res ()

により，それを

x

i

− x

j

= D

ij

^で制約したものと

D

との交わりを判定する．それらに交わりがあれば，

x

i

− x

j

≤ D

ij

に関して，

D

^は

D

と交わりがあるので，

D

^から

x

i

− x

j

≥ D

ij

^{を削り取った} 部分は差演算

D − D

の部分となり得るので，それを差演算

D − D

の結果に格納する．また，

D − D

^に

x

i

− x

j

< D

ij を満たす部分を追加したので，

D

に制約

x

i

− x

j

< D

ijをかけて，以降の処理を効率化する．

DBMs

の差

D − D

は，以下のように計算できる：

procedure diﬀerence

(4)

begin

input DBMs D ; input DBMs D;

output a set of DBMs D;

done:=FALSE;

D := ∅ ;

C := closure ( D );

for (i,j

について（ただし，

i = j

^）

) do if (¬ done) then

A := D ∩ D ; if ( A = ∅ ) then

D := D + D ; done:=TRUE;

else

if ( A = D ) then done:=TRUE;

else

B := res ( C, x

i

− x

j

= D

ij

);

if ( B ∩ D = ∅) then if ( D

ij

が

<

^の形式

) then

D := D

+ res ( D, x

i

− x

j

≥ D

ij

);

D := res ( D, x

i

− x

j

< D

ij

);

else

D := D

+ res ( D, x

i

− x

j

> D

ij

);

D := res ( D, x

i

− x

j

≤ D

ij

);

endif endif endif endif endif endfor end procedure

ただし，

closure ( D )

は

D

^{のすべての要素}

( c, < )

を

( c, ≤ )

で置換することを意味する．

closure ( D )

により，

D

をすべて

x

i

− x

j

≤ D

ij

形式にして，

res ( C, x

i

− x

j

= D

ij

)

の演算を可能とする．これにより，

res ( C, x

i

− x

j

= D

ij

)

と

D

^{との積演算によ} り，

x

i

− x

j

≤ D

ij

^{に関する，}

D

^と

D

^{との交わりを} 計算する．

また，

res ( C, x

i

− x

j

= D

ij

), res ( D, x

i

− x

j

<

D

ij

)

は，それぞれ

x

i

− x

j

= D

ij

，

x

i

− x

j

< D

ij

を満たす点へ

C, D

を制限することを意味する．その計算方法は，それぞれ

C, D

^の

DBMs

に

x

i

−x

j

= D

ij

^，

x

i

− x

j

< D

ij

を追加して，その標準形を計算する．

（

5

）リセットの逆像演算：クロック変数集合

λ

^と

DBMs D

^{に対して，}

x

i

∈ λ

のリセットアクションと，

時間経過により

D

^{に到達できる}

D

^{は，以下のよう} に計算できる：

（

a

）

D

^の，

x

i

∈ λ

^{リセット直後の}

DBMs D

を計算する：

DBMs D

^の

x

i

∈ λ

^を

0

にして，標準形を求める．

（

b

）

D

^の，

x

i

∈ λ

^{のみ時間経過させ，}

x

iリセット前の

DBMs D

を計算する：

x

i

∈ λ

の上限の要素

D

i0

と，

x

i に関係する要素

∀j.D

ij

，

D

ji

( j = i )

を

∞

で置換して，標準形を求める．

リセットの逆像演算は，ある時間経過したタイムゾーンから，リセットアクションにより，特定のクロックのみ

0

になったタイムゾーンに対して，リセットアクションを戻す演算である．そして，リセットアクションと時間経過により，現在のタイムゾーンに遷移可能なタイムゾーンを求めることを意図している．

（

6

）遷移の逆像演算：タイミング制約式

δ

及び，

クロック変数集合

λ

のリセットアクションをもつ遷移と，

DBMs D

に対して，この遷移により

D

^に到達できる

DBMs D

は，以下のように計算できる：

（

a

）クロック変数集合

λ

^と

DBMs D

^{に対して，}

上記

(5)

のリセットの逆像演算を行い，結果を

D

とする．

（

b

）

D ∩ δ

が成り立つタイムゾーンの

DBMs

という処理行い，結果を

D

^とする．

（

c

）

D

^{に対して，上記}

(2)

の逆像演算を行い，

D

^を得る．

遷移の逆像演算は，時間経過によりあるタイミング制約式を満たし，遷移したタイムゾーンを，遷移前に戻す演算である．そして，時間経過によりタイミング制約を満たし，現在のタイムゾーンに遷移可能なタイムゾーンを求めることを意図している．

✷

3. 2

近似手法による実時間記号モデル検査一般に，記号モデル検査では，

CTL

式（検証性質）

を充足する状態集合を部分論理式の再帰処理により求め，その状態集合が初期状態を包含するかどうかにより検証性質の充足性を判定する．我々は，

CTL

式を充足する状態集合を実時間システムのための近似手法

[5], [6]

の応用により求め，その近似の状態集合が初

(5)

期状態を包含するかどうかにより検証性質の充足性判定を行う．

3. 2. 1

実時間システムのための近似手法

大規模な実時間システムの検証では，正確な時間付き状態集合の算出が困難である．そこで，

[5], [6]

の近似手法では，正確な状態集合を算出する代わりに，正確な状態集合を包含する状態集合と，正確な状態集合に包含される状態集合を求める．前者の状態集合を求めることをオーバ近似，後者の状態集合を求めることをアンダ近似という．ここでは，この

2

種類の近似を行う近似演算，オーバ近似演算

^{とアンダ近似演} 算

✄

⁺ の定義を示す．これらの演算が，

∪

の代わりに

Q, Z

のような表現に適用される．

［定義

7

］（オーバ近似演算

^）

Q

1

, Z

1

, Q

2

, Z

2

^を時間

Kripke

構造の近似状態集合とすると，オーバ近似演算は次のように定義される．

Q

1

, Z

¹

Q

2

, Z

²

^def

= Q

1

∪Q

2

, prejoin ( Z

¹

, Z

²

)

✷ DBMs

は和演算

∪

に関して閉じていないため，

Z

1

∪ Z

2 の結果を

DBMs

で表現しようとすると二つの

DBMs

のリストになる．これらを近似により一つのタイムゾーンにするために，二つのタイムゾーンから，それらを包含する最小のタイムゾーンを求める

prejoin ()

が用いられる．定義

7

のオーバ近似演算を二つの近似状態集合に適用すると，状態集合については通常の和集合，タイムゾーンについては二つのタイムゾーンをカバーするように丸められた近似状態集合が得られる．

S

¹

, S

² を近似状態集合とすると，

は必ず

( S

1

∪

A

S

2

) ⊆ ( S

1

S

2

)

のように

∪

A で求まる状態集合を包含する状態集合を与える．ただし，

∪

A は近似状態集合の正確な和集合を意味する．したがって，

オーバ近似によって得られた状態集合について，検証性質が充足されない場合，検証結果は

FALSE

であると判定できる．検証性質が充足される場合は，検証結果の判定は行えない．

［定義

8

］（アンダ近似演算

✄

⁺^）

Q

1

, Z

¹

, Q

2

, Z

²

を時間

Kripke

構造の近似状態集合とすると，アンダ近似演算は次のように定義される．

Q

1

, Z

1

✄

⁺

Q

2

, Z

2

def

=

8

>

<

>

:

Q

2

, Z

²

Q

¹

⊆ Q

²

∧ Z

¹

⊆ Z

²

Q

1

∪ Q

2

, Z

1

Q

1

⊆ Q

2

∧ Z

1

⊆ Z

2

Q

1

, Z

1

^その他

✷

定義

8

のアンダ近似演算では，一方の近似状態集合がもう一方を完全に包含していれば，大きい方の近似状態集合が得られ，そうでなければ，どちらか一方の状態

/

タイムゾーンを用いた近似状態集合になる．

S

1

, S

2 を近似状態集合とすると，

✄

⁺ ^は必ず

( S

1

✄

⁺

S

2

) ⊆ ( S

1

∪

A

S

2

)

のように

∪

Aで求まる状態集合に包含される状態集合を与える．したがって，アンダ近似によって得られた状態集合について，検証性質が充足される場合，検証結果は

TRUE

であると判定できる．検証性質が充足されない場合は，検証結果の判定は行えない．オーバ近似とアンダ近似の結果から検証結果の判定が行えない場合は，近似精度を上げて再びオーバ近似とアンダ近似を行い，検証結果の判定ができるまでこれを繰り返す．

次項に，近似の精度に関係する分割クラス，分割構造，近似構造の定義を示す．

3. 2. 2

状態空間と状態集合の分割

状態空間をいくつかのブロックに分割する分割構造の定義を示す．

［定義

9

］（分割構造と分割クラス）

D

を状態空間，

C

1

, C

2

, . . . , C

n を

n

個の状態集合とするとき，

D = C

¹

∪

C

²

∪

C

. . . ∪

C

nを満たす

C

iを分割クラス，

C = {C

1

, C

²

, . . . , C

n

}

を分割構造と呼ぶ．ただし，

∪

C は分割クラスの和集合を意

味する．

✷

状態空間は，分割構造によりいくつかのブロック

（近似クラス）に分けられ，各ブロック内で独立にオーバ

/

アンダ近似が行われる．したがって，近似の精度はこの分割構造の決め方に依存する．すなわち，状態空間を粗く分割すると近似精度が下がり，細かく分割すると精度が上がる．しかし，分割が細かくなると状態集合の処理コストは大きくなる．

次に，分割構造に基づいた状態集合の表現である近似構造の定義を示す．

［定義

10

］（近似構造）

C = {C

1

, C

2

, . . . , C

n

}

を分割構造，

A

をある近似状態集合，

A

i

= A ∩ C

i

( i = 1 , 2 , . . . , n )

とするとき，

A = {A

¹

, A

²

, . . . , A

n

}

^を

A

^の

C

^に関する

近似構造と呼ぶ．

✷

オーバ近似やアンダ近似は，この近似構造に含まれる状態集合に対して行われる．すなわち，

A

1

=

{A

11

, A

¹²

, . . . , A

1n

}

，

A

2

= {A

21

, A

²²

, . . . , A

2n

}

，とすると，オーバ近似演算は

A

¹

A

²

= {A

¹¹

A

21

, A

12

A

22

, . . . , A

1n

A

2n

}

^{，アンダ近似演算は}

(6)

A

1

✄

⁺

A

2

= {A

11

✄

⁺

A

21

, A

12

✄

⁺

A

22

, . . . , A

1n

✄

⁺

A

2n

}

となる．

3. 2. 3

^{状態空間の自動分割}

前項で述べたように，近似精度は分割構造の決め方により変化する．本節では，粗い分割構造（つまり，

分割クラスの数が少ない）から細かい分割構造（つまり，分割クラスの数が多い）を自動的に生成し，近似精度を上げて行く機構

[5], [6]

について述べる．本論文で開発した検査器では，検証の最初は初期状態集合とその他の状態集合の二つの分割クラスから分割構造を構成して，検証が進むに従って分割構造の中の分割クラスの数を自動的に増加させる．そして，正しい検証の結果が得られるまで分割構造の精錬化（つまり，分割クラスの増加）を継続する．最悪の場合は，すべての分割クラスが一つの状態から構成される．つまり，

最悪の場合は近似手法の利点が全く生かせないことになる．しかし，現実的な多数の問題において，近似手法の有効性が示されており

[5], [6]

，本論文においても実験的に，その有効性を示す．

まず，近似の不正確さが増すオーバ近似演算を避けて分割構造を精錬化するために，オーバ近似演算と分割構造との関係を整理する．本論文では，本来の状態集合のサブセットであるアンダ近似の近似構造に着目して，近似の不正確さが増す原因を分析する．

A

under

= {A

under1

, A

under2

, . . . , A

under n

}

^をアンダ近似の近似構造，

A

1

, A

2を近似状態集合として，

オーバ近似演算

A

¹

A

² をするかどうかを判定する場合を考える．

オーバ近似演算を避けて分割構造を精錬化する場合は，図

1

の場合のどれかに分類できて，分割クラスを細分割して，近似の精度を向上させることができる．

（

i

）次の（

a

），（

b

）が成り立つ

（

a

）

∀A

under i

(1 ≤ i ≤ n )

について，

A

1

∩ A

under i

= ∅, A

2

∩ A

under i

= ∅

（

b

）

∃A

under i

, ( A

1

A

2

) ∩ A

under i

= ∅

（

ii

）次の（

a

），（

b

）が成り立つ

（

a

）

∀A

under i

(1 ≤ i ≤ n )

について，

A

¹

∩ A

under i

= ∅

（

b

）

∃A

under i

, A

2

∩ A

under i

= ∅

（

iii

）次の（

a

），（

b

）が成り立つ

（

a

）

∀A

under i

(1 ≤ i ≤ n )

について，

A

²

∩ A

under i

= ∅

（

b

）

∃A

under i

, A

¹

∩ A

under i

= ∅

（

iv

）次の（

a

），（

b

）が成り立つ

図1 オーバ近似演算と分割クラスの精錬化 Fig. 1 Overapproximation and reﬁning separating

classes.

（

a

）

∀A

under i

(1 ≤ i ≤ n )

について，

A

1

∩ A

under i

= ∅, A

2

∩ A

under i

= ∅

（

b

）

∀A

under i

, ( A

1

A

2

) ∩ A

under i

= ∅

（

v

）次が成り立つ

∀A

under i

(1 ≤ i ≤ n )

について，

A

under i

⊂ A

¹

,

または，

A

under i

⊂ A

² なお，近似状態集合の交わり演算は以下のとおりである：

A

1

∩ A

under i は，

A

1 を

< Q

1

, Z

1

>

^として

A

under i を

< Q

under i

, Z

under i

>

とするならば，

< Q

¹

∧ Q

under i

, Z

¹

∩ Z

under i

>

^{である．ただ}

し，

Q

¹

∧ Q

under i の

∧

は

BDDs

の論理積であり，

Z

1

∩ Z

under i の

∩

^は

DBMs

の積演算である．

また，近似状態集合の差演算は以下のとおりである：

A

1

− A

under iは，

< Q

1

∧ Q

under i

, Z

1

− Z

under i

>

である．ただし，

Q

under iは

Q

under i の否定であり，

Z

¹

− Z

under iは

DBMs

の差の計算である．

（

i

）は，

A

1

, A

2 ともに

A

under と交わりをもたないが，

^{演算を行うと}

A

under と交わりが生じる場合で，本来の状態集合を全く含まない近似状態集合が，

演算により本来の状態を新たに含んでしまうことを検出している．

（

ii

）と（

iii

）は，

A

1，

A

2 のどちらか一方のみが

(7)

図2 オーバ近似とアンダ近似の差分による近似の精度の低下

Fig. 2 Less accurate approximation by diﬀerence be- tween overapproximation and underapproxi- mation.

A

under と交わりをもっている場合で，本来の状態を

含まないことがわかっている近似状態集合と，そうでない近似状態集合が近似により混ざり合ってしまうことを検出している．

これらの（

i

），（

ii

），（

iii

）の三つのどれかが検出された場合には，近似演算

A

1

A

2 を行わず

A

1

, A

2

を独立した近似状態集合のまま残しておく．この近似状態集合

A

¹

, A

²を異なる分割クラスにする．

（

iv

）は，

A

¹

, A

² ^ともに

A

under と交わりをもたず，

^{演算を行っても}

A

under と交わりをもたない場合である．この場合は，近似演算

A

1

A

2 を行うが，

A

1

A

2 と

A

under を別の分割クラスとする．

（

v

）は，

A

¹ ^と

A

² ^が

A

under を完全に包含する

場合であり，オーバ近似とアンダ近似の差分に近似の精度を低下させる原因が存在する．図

2

に示すよう

に，

A

1

A

2により，

A

under iでない領域が増加して，

近似の精度が低下する可能性がある．このために，近似演算

A

¹

A

² ^{を行わず，}

A

¹

−

^S_A_i∈K

A

under iと

S

A i∈K

A

under iを分割して二つの分割クラスとして，

A

2

−

^S_A_i∈L

A

under iと

S

A _i∈L

A

under iを分割して二つの分割クラスとする．ただし，

A

under i

⊂ A

1

となる

i

の集合を

K

として，

A

under i

⊂ A

2 となる

i

^の集合を

L

^とする．

図

3

に，（

i

）（，

ii

）（，

iii

）（，

iv

）（，

v

）の条件に基づいて，

近似の不正確さが増す近似演算を避けながらオーバ近似を行うアルゴリズムを示す．

conditional-join()

は，分割構造

C

で閉じたオーバ近似を行うために，分割クラス

C

^{ごとに近似構造}

A

1，

A

2，

A

underの条件付きオーバ近似を行う．各

C

^{に属する近似状態集合} ごとに条件判定を行い，近似結果

A

3 の近似状態集合

図3 条件付きオーバ近似アルゴリズム Fig. 3 Algorithm for conditional-join.

A

³ を求めていく．最終的に，近似の不正確さが増すことを避けるために，近似されずに分割された近似状態集合を含む近似構造

A

3が得られる．この近似構造を分割構造として利用することにより，より細かい分割構造が自動生成できて，近似精度を自動的に上げていくことが可能になる．

3. 2. 4 CTL

式を充足する状態集合の再帰処理

我々は，近似手法により

CTL

式を充足する状態集合の近似構造を求め，近似手法による実時間記号モデル検査を実現する．

CTL

式を充足する状態集合の近似構造は，

CTL

の部分論理式を充足する状態集合の再帰処理により求められる．我々は，

CTL

の各部分論理式を再帰的に処理し，各部分論理式を充足する状態集合の近似構造を求めていく．長さ

1

の部分論理式から始まり，長さ

2 , 3 , . . .

という具合に近似構造を求めて行き，最終的に

CTL

式を充足する状態集合の近似構造を求める．この処理で，

CTL

式の原子命題に対してはその原子命題が成り立つ状態集合の近似構造が生成され，演算に対しては演算の種類に応じた近似処理が行われる．次節に，アルゴリズムの詳細を示す．

3. 3

実時間記号モデル検査アルゴリズム

本節では，

Dill

と

Wong-Toi

の近似手法

[5], [6]

に基

(8)

づいた記号モデル検査アルゴリズムを示す．

3. 3. 1

^{アルゴリズムの概要}

図

4

に，近似手法を用いた記号モデル検査アルゴリズムの充足可能性判定部を示す．アルゴリズムは，

CTL

式

φ

0 と時間

Kripke

構造の初期状態集合

Init

を入力とし，オーバ近似とアンダ近似を行う．オーバ近似では，

φ

0を充足する状態集合の近似構造

A

overを求める．そして，

Init ⊆ A

overが成り立てば，

FALSE

（充足不能）を返す．条件が成り立たなければ，アンダ近似に進み，

φ

⁰ を充足する状態集合の近似構造

A

under を求める．そして，

Init ⊆ A

underが成り立

てば，

TRUE

（充足可能）を返す．この条件が成り立たなければ，充足不能

/

充足可能性の判定ができるま

で，

3. 2. 3

の手法により近似精度を上げながらオー

バ近似とアンダ近似を繰り返す．なお，近似精度を上げる処理は，

over-approximation()

^{の中で行われる．}

over-approximation()

^と

under-approximation()

は，

CTL

式の各部分論理式を再帰的に処理し，各部分論理式を充足する状態集合の近似構造を求めていく．なお，

Init ⊆ A

under は以下のとおりである：

Init = {< q

0 1

,

^x0

>, < q

02

,

^x0

>, . . . , <

q

0n

,

^x0

>}

及び

A

under

= < Q

under

, Z

under

>

とする．

{q

0 1

, . . . , q

⁰n

} ⊆ Q

underかつ^x0

∩ Z

under

=

^x0

であるとき，

Init ⊆ A

underである．

3. 3. 2

部分論理式ごとのアルゴリズム

本項では，オーバ近似により部分論理式の再帰処理を行う

over-approximation()

と，アンダ近似を行う

under-approximation()

のアルゴリズムを示す．

図

5

に，オーバ近似により

CTL

式を充足する状態集合を算出するアルゴリズムを示す．分割構造の初期値は，時間

Kripke

構造の初期状態集合

Init = Q

0

, 0

^{に基づいて状態空間を}

2

分割する

図4 近似手法を用いた記号モデル検査アルゴリズム Fig. 4 Symbolic model-checking algorithm using

approximation method.

C

i

= {Q

0

, ∞, ¬Q

0

, ∞}

とする．ここで，タイムゾーン

∞

は最も大きな無限大のタイムゾーンを表す．

また，アンダ近似の結果

A

under_i の初期値は空集合とした．各部分論理式

φ

iに対しては，演算の種類に応じた処理が行われ，原子命題に対しては，その原子命題が成り立つ状態集合の近似構造が分割構造

C

i

に基づいて生成される．正確な

∪

演算は近似状態集合には適用できないため，演算

∨

に対しては，アンダ近似の結果

A

under_i を考慮した条件付きオーバ近似演算を行う．一方，

∧

演算は近似状態集合にも適用可能なので，演算

∧

に対しては近似構造に含まれる状態集合ごとの

∧

を行う．時相演算

EU

に対しては，

[5], [6]

で提案された最小不動点のオーバ近似手法が，時相演算

EG

に対しては，我々の提案する最大不動点オーバ近似手法が適用される．そして，

∧

^以外の場合には，近似の精度を上げるために，図

3

の関数

conditional−join

で作成された近似構造により，図

5

図5 部分論理式のためのオーバ近似アルゴリズム Fig. 5 Over-approximation algorithm for sub-formulae.

(9)

の

/*

更新

*/

行で，既存の分割構造

C

iが更新されて，

新しい分割構造

C

i が作られる．ここで，

m, h, l

^は，

それぞれ

OverGreatestFixp() , OverLeastFixp() , conditional-join()

^{から得られる近似構造}

A

over

に含まれる近似状態集合の数である．入れ子構造の論理式にも近似手法を適用するために，分割構造は部分論理式ごとに独立である．

図

6

に，アンダ近似により

CTL

式を充足する状態集合を算出するアルゴリズムを示す．

over-approximation()

と異なる点は，各演算に対する処理でアンダ近似が行われる点，分割構造の更新処理がない点，オーバ近似中にアンダ近似の結果を参照できるように，アンダ近似の結果を部分論理式ごとに格納しておく点である．

図

7

に，分割構造

C

に関する近似構造のアンダ近似アルゴリズム

plus()

^を示す．

plus()

^{は，分割構造}

C

の分割クラス

C

ごとに

✄

⁺ 演算を行い，アンダ近似の結果，

A

3 を求めていく．

3. 3. 3

最大不動点計算

本項では，時相演算子

EG

のための最大不動点計算

図6 部分論理式のためのアンダ近似アルゴリズム Fig. 6 Under-approximation algorithm for sub-formulae.

を行う

OverGreatestFixp()

を示す．我々は，これを時相演算子

EG

の処理に用いる．

図

8

に，

EG φ

が成り立つ状態集合のオーバ近似を求めるアルゴリズムを示す．

CTL

式

φ

^{が成り立つ状態集} 合の近似構造

A

φから始まり，

A

f ixpが変わらなくな

図7 アンダ近似アルゴリズム Fig. 7 Algorithm for plus.

図8 最大不動点のオーバ近似アルゴリズム Fig. 8 Over-approximation algorithm for greatest

ﬁxpoint.

(10)

るまで，状態空間の後向き探索が繰り返される．

A

f ixp

== A

new f ixp の判定は，

A

f ixp

⊆ A

new f ixp かつ

A

new f ixp

⊆ A

f ixpの判定により行う．また，

A

f ixp

⊆

A

new f ixp の判定は以下のとおりである：

A

f ixp

=

{A

f ixp1

, . . . , A

_{f ixpi}

, . . . , A

_{f ixpn}

}

^と

A

new f ixp

= {A

new f ixp1

, . . . , A

_{new f ixpi}

, . . . , A

_{new f ixpn}

}

^{とす} ると，各

A

_{f ixpi} と

A

_{new f ixpi}は近似状態集合であり，

A

_{f ixpi}

= < Q

_{f ixpi}

, Z

_{f ixpi}

>

^及び

A

_{new f ixpi}

= <

Q

_{new f ixpi}

, Z

_{new f ixpi}

>

と表現できる．任意の

i

に対して，

Q

_{new f ixpi} ^が

Q

_{f ixpi} を包含して，かつ，

Z

_{f ixpi} ^{を包含すれば，}

A

f ixp

⊆ A

new f ixp と判定する．

Q

_{new f ixpi} が

Q

_{f ixpi} を包含することは，

BDDs

の包含関係の処理であり，一般の記号モデル検査で広く知られている

[2]

．一方，

Z

_{f ixpi} ^{を包含することは，}

Z

_{new f ixpi}

− Z

_{f ixpi}

,

つまり

DBMs

の差が作れるかどうかで判

定する．

A

new f ixp

⊆ A

f ixpの判定も同様に行う．外側の

foreach

^{では，（近似構造}

A

f ixp からの逆像）

∩A

φの近似構造を求めるために，

A

f ixp

(∈ A

f ixp

)

ごとの処理が行われる．内側の

foreach

^{では，（状態}

集合

A

f ixp からの逆像）

∩A

φの近似構造を求めるた

めに，状態遷移関係

N

δ

( ∈ N

Φ(C)

)

ごとの逆像計算が行われる．ただし，

Prev()

の結果をオーバ近似演算により，近似状態集合としてコンパクトに記号表現する．そのため，通常

∪

演算を使わない最大不動点計算でも

conditional-join()

^{を使ってオーバ近似} を行う．二つの

foreach

^を用いて

A

f ixp

(∈ A

f ixp

)

，

N

δ

( ∈ N

Φ(C)

)

ごとに，

A

= Prev(A

f ixp

, N

δ

)

^を求め，

A

f ixpと

A

^の

∩

^{の結果を，}

conditional-join()

を用いて

A

new f ixp に加えていく．この処理により，

オーバ近似が実現される．

一般的に，最大不動点計算でオーバ近似を行うと，

A

f ixp が最大不動点へ収束しなくなり，大きくなって

いくだけであったり，振動したりする可能性がある．

本アルゴリズムでは，最大不動点への収束性を保証するために，

conditional-join()

^{の四つ目の引き数に}

C

を与える．これにより，

conditional-join()

^は，

常に，分割構造

C

の中の分割クラスを細分割して，近似の精度を向上させる．オーバ近似は，分割クラス単位の近似であり，分割クラスの数が多くなればなるほど，近似の精度が向上する．したがって，不動点計算は単調減少し，

A

new f ixp

⊆ A

f ixpなので，大きくな

図9 逆像計算のアルゴリズム

Fig. 9 Algorithm for inverse image computation.

らないで必ず収束する．

図

9

に，

Prev()

のアルゴリズムを示す．

Prev()

^は，

BDD-basedPrev()

^と

DBM-basedPrev()

^{からなり，こ} れらを用いて逆像計算を行う．

BDD-basedPrev()

^は，

BDDs

により記号表現された状態集合

S

から，

N

δに基づく逆像計算を行い，その結果の

BDDs

表現を返す．また，

DBM-basedPrev()

^は，

DBMs

により記号表現されたタイムゾーン

Z

^から，

δ

^{に基づくタイム} ゾーン上での逆像計算を行い，その結果の

DBMs

を返す．

DBM-basedPrev(Z, δ)

は［定義

6

］の逆像演算と基本的には同じであり，タイムゾーン

Z ∩ δ

^から逆像演算する．つまり，

δ

を引き数にとっているのは，

タイミング制約

δ

の状態遷移からタイムゾーン

Z

^に状態遷移する場合の逆像演算をするためである．一般に，タイムゾーン

Z

に状態遷移するタイミング制約は複数ありえるので，タイミング制約

δ

^{ごとに逆像演算} して，それらの和集合を計算することで

Z

^{の逆像が得} られる．図

9

の

Prev(A, N

δ

)

^{の定義より，}

S, Z

は

S, Z

^から

S

^{の一つ前の}

untimed state

とその取り得るタイムゾーンを計算しており，

S, Z

は取り得る逆像であり，アンダ近似の場合も全く問題とならない．

また，図

10

に

UnderGreatestFixp()

^{を示す．最大} 不動点計算のアンダ近似を行う

UnderGreatestFixp()

では，図

8

の

conditional - join ( A

new f ixp

, A

tmp

, A

under

, C)

をアンダ近似演算

plus (A

new f ixp

, A

tmp

, C)

に変える．

3. 3. 4

最小不動点計算

本項では，

[5], [6]

で提案された最小不動点計算の近似アルゴリズム

OverLeastFixp()

^{を示す．我々は，こ} れを時相演算子

EU

の処理に用いる．

図

11

に，

E[ φ 1U φ 2]

が成り立つ状態集合のオーバ近似を求めるアルゴリズムを示す．

CTL

式

φ 2

が成り立つ状態集合の近似構造から始まり，

A

f ixp が変わ

Development and Evaluation of Symolic Model-Checker Based on Approximation for Real-Time Systems

実時間システムのための近似手法に基づいた記号モデル検査器の 開発と評価

山根 智

中村 一博