• 検索結果がありません。

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

N/A
N/A
Protected

Academic year: 2022

シェア "Development and Evaluation of Symolic Model-Checker Based on Approximation for Real-Time Systems"

Copied!
16
0
0

読み込み中.... (全文を見る)

全文

(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 (Difference 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

0

)

により定 義される.ここで,

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

Rnの組

q,

x

とする.

時間

Kripke

構造

M = ( Q, P, T, Q

0

)

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

M

= ( S, S

0

, N )

により定義さ れる.

ここで,

S Q ×

Rnは時間付き状態集合,

S

0

= {q

0

,

x0

| q

0

Q

0

,

x0

= 0}

は初期状態 集合,

N

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

リセットアクション

a (

x

, λ )

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

I : Φ( C ) 2

Rn を含む状態遷移

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

Rn

}

の和

N = N

state

N

time である.

2. 2

時相論理

(CTL)

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

論理

(CTL)

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

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

[定義

3

](

CTL

の構文)

CTL

φ

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

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

1

2

| EF φ

| φ

1

φ

2

| φ

1

φ

2

ここで,

p AP

(原子命題),

• ∨,

は論理和,論理積,

EXφ

はある次状態で

φ

が成り立つ,

EGφ

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

φ

が常に成り 立つ,

1

2

φ

2 が成り立つまで常に

φ

1 が成り 立つ,

EF φ

1 は 将 来 い つ か

φ

1 が 成 り 立 つ で ,

E true

1に等しい.

である.

CTL

の意味は,時間

Kripke

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

[定義

4

](

CTL

の意味)

時間

Kripke

構造

M

と時間付き状態

q

0

,

x0

,時 相論理式

φ

に対して,

CTL

φ

が成立することを

( M, q

0

,

x0

) | = φ

と表す.これを

q

0

,

x0

| = φ

と記 述すると,

CTL

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

• q

0

,

x0

| = p iff p P ( q

0

),

• q

0

,

x0

| = φ

1

φ

2

iff q

0

,

x0

| = φ

1

∧ q

0

,

x0

| = φ

2

,

• q

0

,

x0

| = φ

1

φ

2

iff q

0

,

x0

| = φ

1

∨ q

0

,

x0

| = φ

2

,

• q

0

,

x0

| = EG φ iff

ある状態列

q

0

,

x0

, q

1

,

x1

, . . .

に対して,次の

(a)

(b)

が成り立つ,

(a) q

i

,

xi

| = φ ( i 0)

(b) ( q

i

,

xi

, q

i+1

,

xi+1

) N ( i 0)

• q

0

,

x0

| = E[ φ

1

U φ

2

] iff

ある状態列

q

0

,

x0

,

(3)

q

1

,

x1

, . . .

に対して,次の

(a)

(b)

が成り立 つ,

(a) ∃n 0 , q

n

,

xn

| = φ

2

,

q

i

,

xi

| = φ

1

(0 i < n ) (b) ( q

i

,

xi

, q

i+1

,

xi+1

) N ( i 0)

• q

0

,

x0

| = EX φ iff

ある状態

q

,

x

に対し て,

q

,

x

| = φ, ( q

0

,

x0

, q

,

x

) N .

• q

0

,

x0

| = EF φ iff

ある状態列

q

0

,

x0

, 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 (Difference 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 difference

(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

1

Q

2

, Z

2

def

= Q

1

∪Q

2

, prejoin ( Z

1

, Z

2

)

DBMs

は 和演 算

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

Z

1

Z

2 の結果を

DBMs

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

DBMs

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

prejoin ()

が用いられる.定義

7

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

S

1

, S

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

は必 ず

( S

1

A

S

2

) ( S

1

S

2

)

のように

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

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

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

FALSE

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

[定義

8

](アンダ近似演算

+

Q

1

, Z

1

, Q

2

, Z

2

を時間

Kripke

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

Q

1

, Z

1

+

Q

2

, Z

2

def

=

8

>

<

>

:

Q

2

, Z

2

Q

1

Q

2

Z

1

Z

2

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

1

C

C

2

C

. . .

C

C

nを満た す

C

iを分割クラス,

C = {C

1

, C

2

, . . . , C

n

}

を分割 構造と呼ぶ.ただし,

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

味する.

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

(近似クラス)に分けられ,各ブロック内で独立にオー バ

/

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

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

[定義

10

](近似構造)

C = {C

1

, C

2

, . . . , C

n

}

を分割構造,

A

をある近 似状態集合,

A

i

= A C

i

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

とする とき,

A = {A

1

, A

2

, . . . , A

n

}

A

C

に関する

近似構造と呼ぶ.

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

A

1

=

{A

11

, A

12

, . . . , A

1n

}

A

2

= {A

21

, A

22

, . . . , A

2n

}

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

A

1

A

2

= {A

11

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

1

A

2 をするかどうかを判定する 場合を考える.

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

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

1

A

under i

=

b

∃A

under i

, A

2

A

under i

=

iii

) 次の(

a

),(

b

)が成り立つ

a

∀A

under i

(1 i n )

に つ い て ,

A

2

A

under i

=

b

∃A

under i

, A

1

A

under i

=

iv

) 次の(

a

),(

b

)が成り立つ

1 オーバ近似演算と分割クラスの精錬化 Fig. 1 Overapproximation and refining 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

1

,

または,

A

under i

A

2 なお,近似状態集合の交わり演算は以下のとおり で ある:

A

1

A

under i は ,

A

1

< Q

1

, Z

1

>

して

A

under i

< Q

under i

, Z

under i

>

とするなら ば,

< Q

1

Q

under i

, Z

1

Z

under i

>

である.ただ

し,

Q

1

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

1

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 difference be- tween overapproximation and underapproxi- mation.

A

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

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

これらの(

i

),(

ii

),(

iii

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

A

1

A

2 を行わず

A

1

, A

2

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

A

1

, A

2を異なる分割クラスにする.

iv

)は,

A

1

, A

2 ともに

A

under と交わりをもた ず,

演算を行っても

A

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

A

1

A

2 を行うが,

A

1

A

2

A

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

v

)は,

A

1

A

2

A

under を完全に包含する

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

2

に示すよう

に,

A

1

A

2により,

A

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

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

A

1

A

2 を行わず,

A

1

SAi∈K

A

under i

S

Ai∈K

A

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

A

2

SAi∈L

A

under i

S

Ai∈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

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

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

(充足不能)を返す.条件が成り立たなければ,アン ダ近似に進み,

φ

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

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

0n

} ⊆ 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

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

φ

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

C

i

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

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

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

A

underi を考慮した条件付きオーバ近 似演算を行う.一方,

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

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

を行う.時相演算

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

fixpoint.

(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

new f ixpi

Z

f ixpi を包含すれば,

A

f ixp

A

new f ixp と判定する.

Q

new f ixpi

Q

f ixpi を包 含することは,

BDDs

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

[2]

.一方,

Z

new f ixpi

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

(状態集合,状態遷移関係)

は,状態空間の後向き探索を行い状態集合を返す.本 アルゴリズムでは,

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 が変わ

参照

関連したドキュメント

• ネット:0個以上のセルのポートをワイヤーを使って結んだも

当社は「世界を変える、新しい流れを。」というミッションの下、インターネットを通じて、法人・個人の垣根 を 壊 し 、 誰 もが 多様 な 専門性 を 生 かすことで 今 まで

調査の結果を反映し、IoT

利用している暖房機器について今冬の使用開始月と使用終了月(見込) 、今冬の使用日 数(見込)

SST を活用し、ひとり ひとりの個 性に合 わせた   

認知症の周辺症状の状況に合わせた臨機応変な活動や個々のご利用者の「でき ること」

捕獲数を使って、動物の個体数を推定 しています。狩猟資源を維持・管理してい くために、捕獲禁止・制限措置の実施又