Pi演算的可编程性研究

Pi演算是由Milner、Parrow和Walker提出的并发计算模型，近二十年来，它无论在理论上还是应用上都取得了重要的成果。过去的工作大都集中在对Pi演算本身的研究，但是模型是为解决问题而提出的，因此本项目旨在研究如何在Pi演算上求解问题。由于Pi的语法元素简单，增加了求解问题的复杂度，从而限制了它在描述复杂并发系统上的应用，并增加了比较它与其他演算表达能力的难度。因此，我们认为应用Pi求解问题的关键是构造Pi演算之上的高级语言，它基于Pi演算却高于Pi演算，它的语法元素是Pi演算的提升，但是却在Pi演算中有完全抽象的解释，可以将它想象成在Pi演算"机器"上运行的高级语言。这一语言能以简单的程序建模复杂的系统，探索Pi演算在安全协议分析领域的新应用；也可以用简短的证明代替原来冗长的证明，来研究Pi演算的表达能力，为Pi演算在进程演算家族中找准位置。

π演算是重要的并发计算模型，它有着与生俱来的编程能力。本项目使用π演算的可编程能力探索π演算的新应用，为π演算在进程演算家族中找准位置，更进一步地认识π演算。经过三年的工作，我们在以下一些方面取得重要成果： .1.我们提出了Full λ演算π演算中的翻译，证明该翻译具有完全抽象性，解决了近20年来的开放问题。.2.我们比较了Ambient演算与π演算之间的关系，证明了Fair Ambient和Safe Ambient无法很好地由π演算来模拟行为，同时考察了Mobile Ambient在π演算中的翻译。.3.我们在用 π演算描述安全协议并分析时发现π演算已有的工具所分析的性质非常有限。因而提出了良序下推自动机(Well-Structured Pushdown Systems)模型，证明了其状态可达性和可覆盖性是可判定的，并给出算法，不仅如此，我们发现几种重要的并发程序分析模型（RVASS, Multi-set PDS）均是良序下推自动机的特例。