Research Project for A Theory of Mobile Concurrent Computations

移动并发计算理论研究项目

基本信息

批准号：
12680352
负责人：
MURAKAMI Masaki
金额：
$ 1.47万
依托单位：
OKAYAMA UNIVERSITY
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
2000
资助国家：
日本
起止时间：
2000 至 2003
项目状态：
已结题

项目摘要

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.

该研究项目专门用于研究分布式并发系统的形式模型。特别是，移动并发系统的正式模型是该项目的主要主题。首先，我们提出了一个正式的并发系统模型，该模型配备了发送和接收高阶条款的功能。这是异步高阶Pi-Calculus的修改。新操作：引入输入流。输入过程由输入流和一个过程P组成。在执行P.输入前缀和输出过程期间，它可以接收更高订单项t，以表示代表非原子通信。微积分模型的计算以异步方式在广域网络上传输移动代码和链接。为操作语义提出了标记的过渡系统（LTS）。引入了基于LTS的等价关系。该项目还提出了一个正式的分布式系统模型，并具有新的名称范围的新表示。我们代表开放式的系统，这些系统使用线性逻辑公式的多组来建模正在分布式环境中工作的网络站点。此处介绍的方法模拟了对线性逻辑公式的多组推断的计算。我们考虑模型中每个免费名称的明确范围，以表示分布式系统中名称的范围。也就是说，我们允许将范围分布到两个以上站点的名称。我们将标记的过渡系统定义为模型的操作语义，并根据LTS定义双拟层等效性。同等性的一致性结果。