消息传送进程的代数理论

本项目研究消息传送进程的理论。这类进程可分布于不同的地点，彼此通过发送和接收消息实现协作，共同完成特定和计算任务。我们发展和完善了“符号互模拟”理论，在国际上首次提出了适用于递归消息传送进程的唯一不动点归纳法，在此基础上给出了正则消息传送进程互模拟的完备公理刻划；我们率先提出了π-演算强弱互模拟的完备证明系统，在这一领域的研究中处于国际领先地位；我们还建立了面向消息传送进程的新的计算模型“带赋值的符号迁移图”，并提出了带不动点的—阶谓词演算，得到了计算带赋值的符号迁移图互模拟的算法，推动了这一方向的研究。这些结果为将进程代数理论应用于解决实际问题提供了基础。我们的工作已为国际同行所引用。