アンビエント計算におけるプロセス発見問題 名古屋大学大学院工学研究科 木崎真一郎 酒井正彦 坂部俊樹 背景 ネットワーク上を移動しながら計算を進めるソフトウェア モバイルエージェント etc. 信頼性・安全性? 検証 アンビエント計算 モバイル計算を表現可能なプロセス計算モデル アンビエント計算(1/3) • プロセスの移動に焦点を当てた計算モデル. – プロセスの構造等価関係・遷移関係からなる. • プロセス n 0 in n. P out n. P open n. P P P|Q !P (n) P 例 m 0 | (n) n c 0 | 0 アンビエント計算(2/3) • 構造等価関係 – 次の条件を満たす合同関係. 0|P≡P !P ≡ P | !P P ≡ Q ⇒ !P ≡ !Q P ≡ Q ⇒ n[P] ≡ n[Q] ・ ・ ・ ・ ・ ・ 例 m 0 | n 0 |P ≡ m n P| 0 アンビエント計算(3/3) • 遷移関係. m n m n in n. P | Q n m P m out n. P Q Q n P | Q n open n. P | Q P|Q 動機 • 動機 – 注目するプロセスが,あるアンビエント内に到達可能 かどうかを調べる. • ファイアーウォールの例 (w) w k c X 0 Y * (w) w c Y 0 h open h. 0 out w. in k. in w. 0 open k. 0 目的 • 指定したプロセス状況に遷移可能なプロセスを 探す. 形式化 プロセス発見問題 与えられたプロセス P, Q に対して, P Q * である代入 :V P を発見せよ. アプローチ • アンビエント計算を書き換え規則で表す. プロセス P 項 Q P R Q • ナローイングを用いて代入θを求める. – ナローイング • 項書き換え系で,方程式の解を求めるために使われる手法 の一つ. アンビエント計算の 書き換えによる表現(1/2) • 遷移関係は文脈に依存する関係. ⇒文脈依存書き換え[Lucas’95] m[ in n.P|Q ] | n[R] → n[ m[P|Q] | R ] m[ in n.P|Q ] | n[R] →RS n[ m[P|Q] | R ] 遷移関係 RS:文脈依存書換え規則の集合 アンビエント計算の 書き換えによる表現(2/2) • 構造等価関係は文脈には縛られない関係. ⇒(条件付)文脈自由書き換え 0|P≡P (νn)(P | Q) ≡ P | (νn)Q if n ∈ fn(P) 0 | P →RF P, P →RF 0 | P (νn)(P | Q) →RF P | (νn)Q fn(P) → false 構造等価関係 RF:文脈自由条件付書換え規則の集合 •構造等価関係も文脈依存書き換えにすると・・・ ! の引数以下が書き換えられないとすると, !(P | Q) ≡ !(Q | P) であるが, !(P | Q) →R !(Q | P) とならない. 拡張文脈依存書換え系 • 拡張文脈依存書換え系(RS,RF) def ( Rs , RF ) RS RF • 定理 – P → Q ならば, P →(RS,RF) Q . – P →(RS,RF) Q ならば, P → Q または P ≡ Q . プロセス発見問題の解法 • 条件付ナローイング[Kaplan’87]と文脈依存ナ ローイング[Lucas’98]を組み合わせたナローイン グを使用. – 条件付ナローイングする位置が,文脈依存書き換え で書き換え可能な位置であるときのみナローイングす る. 例題(問題と解) k P k[ X | n[0]] | w[Y ] Q w[n[0] | 0] 方程式 : 解 : X w n Y 0 w n 0 0 { k[ X | n[0]] | w[Y ] ? w[0 | n[0]] } { X in w.0, Y open k .0} in w. 0 open k. 0 例題(流れ図) { k[ X | n[0]] | w[Y ] w[0 | n[0]] } ? ① { X in w.P } { w[k[ P | n[0]] | Y ] ? w[0 | n[0]] } 規則を適用するために 必要になる代入 ② ⑤ { true } ① ② ⑤ 適用した書き換え規則 n[in m.P | Q] | m[ R] m[n[ P | Q] | R] P|Q Q| P Z ? Z true まとめ • アンビエント計算におけるプロセス発見問題を形 式化し,ナローイングを利用して解く方法を提案 した. – アンビエント計算を表現する書換え系. • 2種類の書き換え規則の和にすることで問題点を解決. – 条件付ナローイングと文脈依存ナローイングを組み合 わせて問題の解法. 今後の課題 • 拡張文脈依存書換え系の解析法. • 拡張文脈依存ナローイングにより解が求まるプ ロセス発見問題のクラスの解析.
© Copyright 2024 ExpyDoc