| 研究課題/領域番号 |
02F02748
|
|---|
| 研究種目 |
特別研究員奨励費
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 外国 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 東京大学 |
|---|
研究代表者 |
米澤 明憲 東京大学, 大学院・情報理工学系研究科, 教授
|
|---|
| 研究分担者 |
PESCHANSKI Frederic 東京大学, 大学院・情報理工学系研究科, 外国人特別研究員
|
|---|
| 研究期間 (年度) |
2002 – 2004
|
| 研究課題ステータス |
完了 (2004年度)
|
| 配分額 *注記 |
300千円 (直接経費: 300千円)
2004年度: 300千円 (直接経費: 300千円)
|
|---|
| キーワード | モバイルエージェントシステム / チャネルパッシング計算 / プロセス代数 / トレースモデル |
|---|
| 研究概要 |
本研究活動における本期間では、主にモバイルエージェントシステムの領域における形式的側面についてさらに調査を行った。本研究の中心モデルであるinteraction spaceは、モバイルエージェントシステムを設計およびreasonするために、幾何学的な特徴化を用いる。Interaction spaceはまだ完全に形式化されていない非常に若い理論である。最近はその理論におけるchannel-passingの新しい特徴化について研究してきた。Channel-passingはモバイル計算の動的構造を非常に簡潔に表現することを可能にするため、非常に重要である。なお、channel-passingは、Cambridge大学のRobin Milnerによって開発されたπ計算の理論によって、計算機科学の世界でよく知られるようになった。本研究で提案するvariant (Cube計算と呼ばれる)は、セマンティクスがトレースモデルを使って定義されるという独自性を持つ。それと比較して、他のπ計算のvariantはラベルつき遷移システムを用いて定義される。両アプローチは利点と不便な点を持つが、本研究はそれらを比較することを可能にする。本研究では、位置の概念を導入することにより、トレースベースとラベルつき遷移システムベースのモデルの両方に対して同じ区別能力を得られる可能性があることを示す。本研究でこれまでに得た重要な結果は、本研究で提案するセマンティクスが、強力な仕様ツールであるrefinement計算をサポートすることである。加えて、本研究で開発した言語は、π計算の大半のvariantとは異なり、fully compositionalである。これらの二つの結果はInternational Conference on Communicating Process Architectures 2004 (CPA2004)に採択された論文の中で詳細に議論されている。
|
