進程理論中的否定結果研究

《進程理論中的否定結果研究》是依託上海交通大學，由傅育熙擔任項目負責人的面上項目。

基本介紹

• 中文名：進程理論中的否定結果研究
• 項目類別：面上項目
• 項目負責人：傅育熙
• 依託單位：上海交通大學

項目摘要

否定結果在數學、數理邏輯、計算機科學中扮演著重要角色。在進程理論中，否定結果能推進進程理論向深度發展。本申請項目擬探索進程理論中有重要意義的否定結果，主要考察兩個方面：一、研究進程表達能力的否定結果，即證明一個模型的表達能力不比另一個強，或兩個模型的表達能力不一致等結果。表達能力的否定結果是建立現有模型之間關係圖的關鍵步驟。二、研究不可有限公理化問題，主要研究有限狀態進程上等價關係的不可有限公理化問題，這裡有限公理化是指不使用規不動點歸納的完備系統。不可有限公理化方面的結論不僅對設計驗證系統有實際套用，而且對模型設計和運算元選擇具有指導意義。本申請項目的意義在於通過探索具有重要意義的否定結果，推進進程理論證明技術和低層理論的研究，加快進程理論的深度研究以及對模型無關的核心理論的探討。

結題摘要

本項研究取得四項進展。一、否定了此前有關高階進程演算和一階pi-演算之間關係的偽命題。我們證明了：一般地，高階演算無法在一階pi-演算中得到解釋，故高階進程模型的表達能力不超過一階pi-演算的結論是錯誤的。我們還研究了高階模型的若干變種之間的表達能力關係。二、我們提出了extensional Petri網模型，在該模型中，Petri網是可複合的，這解決了傳統Petri網不可複合的問題。三、我們加強了Senizergues獲得哥德爾獎的結果，證明了epsilon-pushing nPDA和epsilon-popping PDA均為可判定的。這方面的兩篇文章尚在審稿中。最後，我們研究了C-圖的計數問題，證明了不確定計算的結構是非常複雜的。這方面的一篇文章也在審稿中。