《機率並發理論》是依託上海交通大學，由鄧玉欣擔任項目負責人的面上項目。
基本介紹
- 中文名：機率並發理論
- 項目類別：面上項目
- 項目負責人：鄧玉欣
- 依託單位：上海交通大學
項目摘要,結題摘要,
項目摘要
與經典並發理論相比，機率並發進程的語義理論還不成熟，在形式化語義方面還有許多公開問題未被解決。其中一個基本問題是如何在特定機率模型上比較各種常見的語義如互模擬語義、測試語義和trace 語義。在本項目中我們將對這一問題進行全面探索，力圖澄清一般無限狀態無限分支、無限狀態有限分支、有限狀態無限分支、有限狀態有限分支模型、以及一般完全機率模型上互模擬語義、模擬語義、測試語義、trace 語義等之間的相互關係，建立關於機率並發進程比較完整的語義理論。另外，目前在有限狀態有限分支模型上對機率行為等價和前序關係的判定僅限於劃分求精算法，這要求預先生成被考慮系統的整個狀態空間，且只適用於等價關係的判定，在實際套用中往往表現不佳。因此，在本項目中我們考慮設計局部算法以判定行為等價和前序關係。這類算法可動態生成所需的狀態空間，對等價關係和前序關係的判定均適用，且在驗證否定結論時通等常效率較高而具套用前景。
結題摘要
隨著計算機網路和通信技術的發展，對並發分散式系統的研究變得越來越重要。機率並發理論探討如何用形式化的方法嚴格描述並發計算系統以期指導實際系統的規範、設計和定量的分析與驗證。經過多年的努力，我們對機率並發進程語義的認識逐漸加深,已經取得階段性的成果，具體反映在如下幾個方面：（1）釐清了有限狀態機率標號遷移系統上測試語義與模擬語義的聯繫與區別；並把有關結論擴展到其它高級的模型如機率Pi演算、加權的馬爾可夫決策進程、馬爾可夫自動機等；（2）引入其它形式的語義如實數值回報測試和利益測試語義，並與經典的測試語義綜合比較；（3）出版英文專著《Semantics of Probabilistic Processes：An Operational Approach》,對互模擬語義從度量、邏輯、以及算法等角度進行刻畫,對測試語義從模態邏輯和余歸納的角度來刻畫。後者很重要因為我們得到一種語義對正面和負面結論都容易證明：為說明兩個進程是行為關聯的，我們用余歸納的方法；為說明兩個進程不是關聯的，我們只需給出一個測試進程見證這兩個進程的差別；（4）我們發現利用機率互模擬的思想可以幫助理解量子進程的行為，定義量子並發程式行為等價關係，並開發算法驗證程式等價；（5）對於量子高階函式式語言，可以為線性上下文等價關係找到合適的余歸納證明方法。因此，我們從程式等價的角度初步建立了機率並發理論的基本思想、原理和證明方法，而且指出其對於研究量子程式語義的作用，這為我們將來深入研究量子程式的語義理論奠定了堅實的基礎。
