《Pi演算的可程式性研究》是依託上海交通大學，由蔡小娟擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：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）均是良序下推自動機的特例。
