Research Project for A Theory of Mobile Concurrent Computations

本研究项目致力于研究分布式并发系统的形式化模型。其中，移动并发系统的形式化模型是本课题的主要研究内容。首先，我们提出了一个具有发送和接收高阶项能力的并发系统的形式化模型。这是对异步高阶微积分的一种修改。引入了一个新的操作：输入流。一个输入过程由一个输入流和进程p组成，它可以在p的执行过程中接收一个高阶项t。输入前缀和输出过程也被修改为表示非原子通信。在广域网中以异步方式传输移动代码和链路的计算模型。为操作语义提供了标记转换系统（lts）。介绍了基于lts的等价关系。该项目还提出了一个分布式系统的正式模型，该模型具有名称范围的新表示。我们使用多组线性逻辑公式来表示在分布式环境中工作的网络站点的开放式系统。本文提出的方法是对多组线性逻辑公式进行推理的计算模型。为了表示分布式系统中的名称范围，我们考虑模型中每个自由名称的显式作用域。也就是说，我们允许一个名称的作用域分布到两个以上的站点。我们定义了一个标记的转换系统作为我们模型的操作语义，并定义了基于lts的双仿真等价。给出了等价的一个同余结果。

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.