Research Project for A Theory of Mobile Concurrent Computations

本研究计画致力于分散式并发系统之形式化模型之研究。其中，移动的并发系统的形式化模型是本课题的主要研究内容。首先，我们提出了一个具有发送和接收高阶项能力的并发系统的形式化模型。这是异步高阶π演算的一个修改。引入了一种新的操作：输入流。一个输入进程由一个输入流和一个进程P组成，它可以在P的执行过程中接收一个高阶项t.输入前缀和输出进程也被修改为表示非原子通信.演算模型的计算传输移动的代码和广域网上的异步方式的链接。提出了一种用于操作语义的带标签变迁系统（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.