JAIST Repository: 形式手法の新展開 : 離散と連続の融合

JAIST Repository https://dspace.jaist.ac.jp/ Title 形式手法の新展開 : 離散と連続の融合 Author(s) 平石, 邦彦 Citation Issue Date 2007-09-06 Type Presentation Text version publisher

URL http://hdl.handle.net/10119/8251 Rights

Description

北陸先端科学技術大学院大学 21世紀COEシンポジウム 「検証進化可能電子社会」 = JAIST 21st Century COE Symposium “Verifiable and Evolvable e-Society”, 開催：2007年9月6日∼7日, 開催場所：キャンパス・イ ノベーションセンター東京 国際会議室(1F), 2007年 9月6日（木）, 「JAIST-COE/AIST-CVS シンポジウム ：形式検証技術―現状と安心電子社会への適用」発表 資料

形式手法の新展開

－離散と連続の融合－

平石 邦彦

内容

オートマトンからハイブリッドオートマトンへ

ハイブリッドオートマトンに対するモデル検査

離散状態の流体近似と保証付計算

内容

オートマトンからハイブリッドオートマトンへ

ハイブリッドオートマトンに対するモデル検査

離散状態の流体近似と保証付計算

M

m

オン/オフ

センサ

コントローラ

M

m

t

₀

t

₁

t

₂

t

₃

t

₄

σ

₀

σ

₁

σ

₂

σ

₃

σ

₄

σ

₅

time

離散的状態遷移（モード切替）

室温のオン

/オフ制御

オートマトンからハイブリッドオートマトンへ

b

a

a

c

a

b

x

y

z

オートマトン

x: クロック

a

b

a, x := 0

a, x := 0

b, (x < 2)?

1

2

3

4

0

①

②

①

②

①

③

④

③

④

③

④

< 2

< 2

< 2

状態

イベント

a

b

a

b

a

b

a

b

a

b

オートマトンからハイブリッドオートマトンへ

時間オートマトン

M

x =

1

l

M

x ≤

0

l

m

x ≥

Kx

x

&

=

−

_x

&

=

_K

₍

_h

−

_x

₎

on, x = m

off, x = M

オートマトンからハイブリッドオートマトンへ

インバリアント

アクティビティ（連続ダイナミクス）

ロケーション(離散状態） トランジション（遷移条件）

M

x =

1

l

M

x ≤

0

l

m

x ≥

Kx

x

&

=

−

_x

&

=

_K

₍

_h

−

_x

₎

on, x = m

off, x = M

オートマトンからハイブリッドオートマトンへ

ラベル（イベント）

geneA geneB geneC

RNA Polymerase

Activator

Transcription

mRNA

Protein

Translation

遺伝子発現

遺伝子制御ネットワーク

Transcription Factor

α

(Activator)

TF

β

(Repressor)

Gene A

－

＋

Gene B

TF

γ

(Repressor)

Expression

ATG

TAA

TAA

ATG

＋

ハイブリッドシステムとしての

遺伝子相互作用

TFα TF β Gene A － ＋ Gene B TF γ Expression ＋ TF δ

time

factors

α

β

γ

δ

expression of A expression of B

TF α TF β Gene A － ＋ Gene B TF γ Expression ＋ TF δ

v

_A

v

_B

θ

_α

θ

_β

θ

_γ

v

_α

v

_β

v

_γ

v

_δ

Threshold Firing speed

Hybrid Petri net

α

β

γ

δ

ハイブリッドシステムとしての

遺伝子相互作用

ハイブリッドシステム－２つの流れ

計算機科学：リアルタイムシステムの一般化

システム制御理論：モード切替を有する連続システム

（例：区分的線形システム，非線形システムを線形システ

ムの切り替えで近似など）

[

]

[

]

[

]

⎩

⎨

⎧

<

−

≥

=

=

⎥

⎦

⎤

⎢

⎣

⎡

+

⎥

⎦

⎤

⎢

⎣

⎡

−

=

+

0

)

(

0

1

if

3

/

0

)

(

0

1

if

3

/

)

(

)

(

0

1

)

(

)

(

1

0

)

(

)

(

cos

)

(

sin

)

(

sin

)

(

cos

8

.

0

)

1

(

t

x

t

x

t

t

x

t

y

t

u

t

x

t

t

t

t

t

x

π

π

α

α

α

α

α

区分的線形システム

モード切替

最適制御問題

−0.1 0.1 0.3 0.5 0.7 0.9 1.1 1.5 −1 −0.5 0 0.5 1 1.3

スタート

ゴール

内容

オートマトンからハイブリッドオートマトンへ

ハイブリッドオートマトンに対するモデル検査

離散抽象化

ハイブリッドオートマトンから作られるラベル付遷移シス

テムは一般に非可算無限個の状態をもつ．また，１つの

状態の次状態も一般に非可算無限個存在する．

モデル検査アルゴリズムをハイブリッドオートマトンの検

証に用いるために，状態集合を双模倣関係により分割し，

離散状態のラベル付遷移システムに変換する（ただし，

有限状態とは限らない）．

M

m

σ

₁

time

Next Relation

α

σ

₂

σ

₁

α

σ

₂

R’

Pre(R’)

R

R

₁

R

₂

双模倣分割

R

₁

の任意の状態から R’ に行ける．

R

₂

のどの状態からも R’ に行けない．

α

領域 R を R

₁

と R

₂

に分割：

Pre(R) := { q

∈ Q | ∃p ∈ R: q

α

p }

R’

R

₁

R

₂

双模倣分割

双模倣分割

R

₁

R

₂

R

₃

0

l

1

=

x

&

1

=

y

&

10

≤

y

1

l

1

=

x

&

1

=

y

&

2

≤

x

2

l

1

=

x

&

2

−

=

y

&

5

≥

y

3

l

1

=

x

&

2

−

=

y

&

2

≤

x

1

=

y

10

=

y

0

:=

x

2

=

x

5

=

y

0

:=

x

2

=

x

双模倣分割の例

1 ≤ y ≤ 12?

ψ

₃₀₀ ≡ (l = 3 ∧ 0 ≤ x ≤ 2 ∧ 1 ≤ y ≤ 12 ∧ 5 ≤ y + 2x ≤ 14)

ψ

₃₀₁₀≡ (l = 3 ∧ 0 ≤ x ≤ 2 ∧ 1 ≤ y < 5 ∧ 1 ≤ y + 2x < 5)

ψ

₀₀₀≡ (l = 0 ∧ 1 ≤ y ≤ 10)

ψ

₀₀₁≡ (l = 0 ∧ 10 < y ≤ 12)

ψ

₀₁≡ (l = 0 ∧ (0 ≤ y < 1 ∨ y > 12))

ψ

₁₀₀₀≡ (l = 1 ∧ 0 ≤ x ≤ 2 ∧ 3 ≤ y ≤ 12 ∧ 3 ≤ y – x ≤ 12)

ψ

₁₀₀₁≡ (l = 1 ∧ 0 ≤ x ≤ 2 ∧ 1 ≤ y < 3 ∧ 1 ≤ y – x < 3)

ψ

₁₀₁≡ (l = 1 ∧ x > 2 ∧ 1 < y ≤ 12)

ψ

₂₀₀≡ (l = 2 ∧ 5 ≤ y ≤ 12)

ψ

₂₀₁≡ (l = 2 ∧ 1 ≤ y < 5)

ψ

₂₁≡ (l = 2 ∧ (0 ≤ y < 1 ∨ y > 12))

ψ

₃₀₁₁≡ (l = 3 ∧ x > 2 ∧ 1 ≤ y < 12)

ψ

₃₁≡ (l = 3 ∧ (0 ≤ y < 1 ∨ y > 12))

ψ

₁₁≡ (l = 1 ∧ (0 ≤ y < 1 ∨ y > 12))

双模倣分割の例

問題の困難さ

同値類が有限個であるような双模倣が存在するとは限ら

ない．したがって，双模倣分割の停止性は保証されない．

計算方法：数式処理（

Quantifier Eliminationなど），凸多

面体操作アルゴリズム．

非線形ダイナミクスの取り扱い．

ハイブリッドシステムのモデル検査ツール

HyTech (http://www-cad.eecs.berkeley.edu/~tah/HyTech/)

UPPAAL (

http://www.uppaal.com/

)

KRONOS (

http://www-verimag.imag.fr/TEMPORISE/kronos/

)

CheckMate

d/dt (http://www-verimag.imag.fr/~tdang/ddt.html)

内容

オートマトンからハイブリッドオートマトンへ

ハイブリッドオートマトンに対するモデル検査

多くのインスタンスが同時に走る．

十分な量の資源を配分する必要がある．

定量的に求める手法は？

論文査読プロセスのGSPN(一般化確率ペトリネット)によるモデル化

submit

accept

reject

conditional acc.

accept

reject

PAPER POOL

EDITOR POOL

M

N

時間トランジション

瞬間トランジション

∞

∞

∞

0.248 0.065 0.687 0.96 0.04 1 3.5 2.4 2.4 3.9 4.4

Waiting papers

_∞

∞

確率モデル

0.03

0.08

0.21

0.63

1.99

5.94

10.18

#Waiting papers

0.00010

58

384098

9

0.00020

29

213928

8

0.00049

15

110968

7

0.0021

6.2

53053

6

0.013

2.3

23023

5

0.094

0.7

8866

4

0.30

0.3

2926

3

p(#paper pool = 0)

CPU Time

(sec.)

#states

N

Itanium2 1.6GHz/9MBCache, 16GB Memory

離散状態遷移の流体近似

∞

平均遅延時間

τ

_i

で移動

x

_i

_x

_j

平均流速 1/

τ

_i

で移動

x

_i

_{(fluid-flow approximation)}

_x

_j

離散状態遷移の流体近似

i

i

i

i

x

x

&

=

θ

/

τ

l

_i

h

_i

θ

_i

= [l

_i

, u

_i

]

平均流速 1/

τ

_i

で移動

x

_i

_x

_j

遅延

τ

流速 x

_i

/ τ

∞

∞

指数分布

x

_i

(0)

_x

_i

_(t)

w

_i

(0)

E[w

i

(t)]

τ

/

)

(

t

x

x

&

=

−

期待値の保存（指数分布）

k

ke

−t/τ

k

ke

−t/τ

∞

∞

∞

_∞

k

k

x

_i1

(0)

w

_i1

(0)

x

_i2

(0)

x

i1

(t)

x

i2

(t)

流速 2x_i1/ τ 遅延τ/2 指数分布 遅延τ/2 指数分布 流速 2x_i2/ τ

w

_i2

(0)

, / 2 / 2 ) ( / 2 ) ( ₁ 1

τ

τ

τ

i i x x t x x t x − = − = & &

E[w

_i1

(t)]

_E[w

_i2

_(t)]

期待値の保存（アーラン分布）

0

0

ke

−2t/τ

ke

−2t/τ

(2k/

τ

)te

−2t/τ

(2k/

τ

)te

−2t/τ

2 2 2 2 2 2 1 1 1 1 1 1

)

,

(

x

_{a a}

x

_{a r r}

x

_{r a a}

x

_{a r r}

x

_r

R

θ

=

θ

λ

+

θ

λ

+

θ

λ

+

θ

λ

0

2 2 1 1

≥

−

−

−

−

−

=

i r a r a c p

x

x

x

x

x

x

N

x

2 2 2 2 2 2 2 2 2 2 1 1 1 1 1 1 1 1 1 1

)

,

(

)

,

(

)

,

(

)

,

(

r r r ca ca ca r r a a a ca ca ca a a r r r r r a a a a a ca ca ca ca ca s s

x

x

p

x

x

x

p

x

x

x

R

p

x

x

x

R

p

x

x

x

R

p

x

x

R

r

x

λ

θ

λ

θ

λ

θ

λ

θ

λ

θ

θ

λ

θ

θ

λ

θ

θ

θ

−

=

−

=

−

=

−

=

−

=

−

=

&

&

&

&

&

&

0 = p x xp =0 x_s =0 0 = s x 2 2 2 2 2 2 2 2 2 2 1 1 1 1 1 1 1 1 1 1

0

r r r ca ca ca r r a a a ca ca ca a a r r r s r r a a a s a a ca ca ca s ca ca s

x

x

p

x

x

x

p

x

x

r

p

x

x

r

p

x

x

r

p

x

x

λ

θ

λ

θ

λ

θ

λ

θ

λ

θ

λ

θ

λ

θ

−

=

−

=

−

=

−

=

−

=

=

&

&

&

&

&

&

ハイブリッドオートマトン表現

到達可能性の判定

ふるまいの計算：数値解析法（離散時間表現による逐次

計算）．

パラメータ

θ

_i

の存在⇒各時点における可能な状態は集

合．

保証付き計算：インターバル近似法－真の値の範囲の

upper approximation

)

,

(

)

),

(

(

)

),

(

(

)

(

)

(

t

_k+1

=

x

t

_k

+

hf

(0)

x

t

_k

+

e

x

h

=

t

_k+1

−

t

_k

t

_k

≤

≤

t

_k+1

x

θ

ξ

θ

ξ

インターバル近似法

Taylor展開による状態の逐次計算

0

)

0

(

),

(

x

x

x

f

x

&

=

=

常微分方程式

エラー項

])

[

],

([

!

2

]

[

)

),

(

(

(1) 2

θ

θ

ξ

e

_k

h

f

B

_k

x

e

⊆

=

Bounding Boxによるエラー項の見積り

]

[

)

(

.

:

]

[

B

_k

∀

t

_k

≤

t

≤

t

_k+1

x

t

∈

B

_k

Bounding Boxの計算：Picard operator

インターバル近似法

].

[

)

(

.

]

[

])

[

],

([

]

,

0

[

]

[

:

])

([

1 k k k k k k k

B

t

x

t

t

t

B

B

f

h

x

B

∈

≤

≤

∀

⇒

⊆

⋅

+

=

Φ

+

θ

インターバル近似（１階）

]

[

)

,

(

)]

(

[

)]

(

[

x

t

_k+1

=

x

t

_k

+

hf

(0)

x

θ

+

e

_k

x(t

_k

)

∈ [x(t

_k

)] ⇒ x(t

_k+1

)

∈ [x(t

_k+1

)]

真の値を含むインターバルの計算が可能（

upper approximation)

拡張と実装

インターバル近似法をモード切り替えを含むハイブリッド

システムに拡張．

各時点の状態集合をインターバルではなく，システムイン

バリアントを用いた凸多面体により近似．

近似精度が良い

piecewiseインターバル近似を採用．

計算ツール

KCLP-HS上に実装．

ツール

制約充足に基づいた計算ツール

KCLP-HS

=Prolog Interpreter

+ Linear Constraint Solver

+ Quadratic Programming Solver

+ Manipulation of Convex Polyhedra

+ Interval Arithmetic

XCON (N=70) 0 5 10 15 20 25 0 0. 5 1 1. 5 2 2. 5 3 3. 5 4 4. 5 5 5. 5 6 6. 5 7 7. 5 8 8. 5 9 9. 5 ₁₀ 10 .5 ₁₁ 11 .5 ₁₂ Month Pa p e rs XCON (N=100) 0 5 10 15 20 25 Pa pe rs XCON (N=130) 0 5 10 15 20 25 Pap e rs XCON (N=50) 0 5 10 15 20 25 0 0.5 1 1.5 2 2.5 3 3.5 4 4.5 5 5.5 6 6.5 7 7.5 8 8.5 9 9.5 10 10 .5 ₁₁ 11 .5 ₁₂ Month Pap er s

計算結果

流体＋インターバル近似の利点

線形計算のみ

リソースの量に対するスケーラビリティ

保証付き計算法

まとめ－離散と連続の融合

計算機（離散）と実世界（連続）のインタラクション

自然界におけるハイブリッド動作（例：遺伝子発現）

流体近似：状態空間爆発へのブレークスルー？