2003 Fiscal Year Final Research Report Summary
Research Project for A Theory of Mobile Concurrent Computations
| 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
|
| 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.
|
Research Products
(4 results)
