| Project/Area Number |
02F02748
|
|---|
| Research Category |
Grant-in-Aid for JSPS Fellows
|
| Allocation Type | Single-year Grants |
|---|
| Section | 外国 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
米澤 明憲 東京大学, 大学院・情報理工学系研究科, 教授
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
PESCHANSKI Frederic 東京大学, 大学院・情報理工学系研究科, 外国人特別研究員
|
|---|
| Project Period (FY) |
2002 – 2004
|
| Project Status |
Completed (Fiscal Year 2004)
|
| Budget Amount *help |
¥300,000 (Direct Cost: ¥300,000)
Fiscal Year 2004: ¥300,000 (Direct Cost: ¥300,000)
|
|---|
| Keywords | モバイルエージェントシステム / チャネルパッシング計算 / プロセス代数 / トレースモデル |
|---|
| Research Abstract |
本研究活動における本期間では、主にモバイルエージェントシステムの領域における形式的側面についてさらに調査を行った。本研究の中心モデルである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)に採択された論文の中で詳細に議論されている。
|
