ネットワークソフトウェア技術の発展に伴い，データばかりでなく，プロセス自体も ネットワーク上を移動するいわゆるモバイルソフトウェアの利用が広がっている．ア ンビエント計算はモバイルソフトウェアの抽象計算モデルであり，形式的な解析を通 してモバイルソフトウェアの信頼性と安全性を向上できる． 例えば，ある環境にあるプロセスが他の環境に移動できるか否かという安全性の問題 は，プロセス式の方程式の解が存在するか否かという問題により定式化できる．この ことに着目し，本研究ではアンビエント計算におけるプロセス方程式の解法について 研究する． まず，推論規則により遷移関係と構造等価関係が定義される並行計算モデルを表現で きる枠組として拡張文脈依存書換え系を導入する． 拡張文脈依存書換え系は，文脈によって書き換え可能な場所が限定される項書換え系 （文脈依存書換え系という）の対で与えられる計算モデルである． 次に，項書換え系により定められる代数上の方程式を解くために使われるナローイン グを拡張文脈依存書換え系の場合に拡張することで拡張文脈依存ナローイングを定 め，その健全性を証明する． 最後に，アンビエント計算をシミュレートする拡張文脈依存書換え系を与え，その正 しさを証明する．これらの結果により，アンビエント計算におけるプロセス発見問題 を拡張文脈依存ナローイングにより解くことが可能となる．