| Project/Area Number |
12680352
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | OKAYAMA UNIVERSITY |
|---|
Principal Investigator |
MURAKAMI Masaki OKAYAMA UNIVERSITY, the Graduate School of Natural Science and Technology, Associate Professor, 大学院・自然科学研究科, 助教授 (60239499)
|
|---|
| Project Period (FY) |
2000 – 2003
|
| Project Status |
Completed (Fiscal Year 2003)
|
| Budget Amount *help |
¥2,300,000 (Direct Cost: ¥2,300,000)
Fiscal Year 2003: ¥600,000 (Direct Cost: ¥600,000)
Fiscal Year 2002: ¥500,000 (Direct Cost: ¥500,000)
Fiscal Year 2001: ¥500,000 (Direct Cost: ¥500,000)
Fiscal Year 2000: ¥700,000 (Direct Cost: ¥700,000)
|
|---|
| Keywords | concurrency / distributed system / linear logic / process algebra / higher order communication / code streaming / multiset rewriting system / 動的変更 / 名前の有効範囲 / π計算 / コードストリーミング / 非同期分散系 / 国際研究者交流 / イギリス / モーバイルプロセス / プログラム変換 |
|---|
| Research Abstract |
This research project is dedicated for the study of formal models of distributed concurrent systems. Especially, formal models of mobile concurrent systems are main topic of this project.
First, we presented a formal model of concurrent system that is equipped with capabilities of sending and receiving higher-order terms. That is a modification of the asynchronous higher order pi-calculus. A new operation : input streaming is introduced. An input process consists of an input stream and a process P. It can receive a higher order term t during the execution of P. Input prefix and output process are also modified to represent non-atomic communication. The calculus models computations transferring mobile codes and links on a wide-area network in asynchronous manner. A labeled transition system (lts) is presented for the operational semantics. Equivalence relations based on the lts are introduced. This project also presented a formal model of distributed systems with a new representation of the scopes of names. We represent open-ended systems that model network sites that are working in distributed environments using multisets of formulas of linear logic. The method presented here models a computations with inferences on multisets of formulas of linear logic. We consider an explicit scope for each free names in our model in order to represent scopes of names in distributed systems. Namely, we allow a name whose scope is distributed to more than two sites. We define a labeled transition system as the operational semantics of our model, and define the bisimulaiion equivalence based on the lts. A congruence result on the equivalence is presented.
|
