Basic Research on the logical semantics of agent calculi based on concurrent process calculi

本文的主要研究内容如下：（1）提出了一个高阶并发进程的计算模型，建立了高阶并发进程的理论操作语义。(2)在此基础上，我们实现了一个程序设计环境，并应用于几个实际的例子，得到了以下结果：（1）高阶进程演算的压缩我们提出了一个高阶进程演算来严格描述并发系统。该演算给出了以下研究项目（2）和（3）的数学基础。(2)高阶过程操作语义的数学基础的建立对于（1）中提出的计算演算，我们进行了下列工作并取得了一些结果：（a）过程的等价性：我们给出了高阶过程基于操作语义的等价性理论。(b)高阶模态系统和模型检测：我们提出了高阶过程演算的证明系统，并给出了可靠性和完备性定理。给出了该系统的力学模型检验方法。(c)类型系统：我们已经给出了微积分的类型系统，并讨论了它的性质。(3)编程环境的开发我们已经实现了微积分的编程环境，并将其应用于几个实际的例子。

The main objectives of this research are as follows:(1) We propose a computational model of higher order concurrent processes and establish their theoretical operational semantics.(2) Based on the foundations we implement a programming environment and apply it to several practical examples.We have obtained the following results:(1) Contraction of a Higher Order Process CalculusWe have proposed a higher order process calculus to describe concurrent systems rigorously. This calculus gives mathematical foundations of the following research items (2) and (3).(2) Establishment of Mathematical Foundations on Operational Semantics of Higher Order ProcessesFor the computational calculus proposed in (1), we have carried out the following items with their results:(a) Equivalence of Processes:We have given a theory on equivalence of higher order processes based on their operational semantics.(b) Higher Order Modal System and Model Checking:We have proposed a proof system for the higher order process calculus and given the theorems on soundness and completeness. A mechanical model checking method for the system have been given as well.(c) A Type System:We have given a type system for the calculus and discussed its properties.(3) Development of Programming EnvironmentWe have implemented the programming environment for the calculus and applied it to several practical examples.