《M-可解性、M-計算複雜性與計算機科學的模型理論》是依託上海交通大學，由傅育熙擔任項目負責人的重點項目。
基本介紹
- 中文名：M-可解性、M-計算複雜性與計算機科學的模型理論
- 項目類別：重點項目
- 項目負責人：傅育熙
- 依託單位：上海交通大學
項目摘要,結題摘要,
項目摘要
在分析計算模型和互動模型（如進程演算）的共性和特性的基礎上，提出並研究計算機科學的模型理論，該理論有如下特點：一、統一了計算模型與互動模型，其核心內容是不依賴於任何模型的統一理論；二、將計算機科學的一些基本假定以類似公理的形式給出，精確地刻畫出模型世界的特徵；三、支撐獨立於具體模型的M-可解理論、M-複雜性理論和M-程式理論。擬用模型理論的標準，考察已有模型的完備性；對於已知的完備模型（如π-演算、VPC、IM等），研究並建立其模型理論、可解理論、計算理論、程式理論。. 本項研究的意義在於探索計算機科學的一個更為基本的理論框架（即模型理論），該理論框架可以支撐對可解理論、計算理論、程式理論的相對化研究。
結題摘要
在以互動為中心的資訊時代，建立計算與互動的統一模型理論是計算機科學研究的基本任務之一。本項目的目標是建立計算機科學的模型理論的核心框架，並在模型理論的基礎上研究互動的基本理論模型、互動的複雜性、互動的機率方法、互動的程式理論。經過四年探索，完成了以下幾方面的研究工作。 1. 從四條公理出發，建立了適用於所有互動模型的等價理論、表達能力理論、完備理論。主要結果包括：解決了-演算和VPC-演算的關係問題；形式化證明了CCS和高階進程演算的非完備性；指出了通用進程的存在性和如何利用通用進程深入研究互動理論的方法和證明否定結果的方法。 2. 研究了描述複雜性和參數複雜性中的一系列問題，建立了證明複雜性中最優證明系統存在性與多項式時間邏輯存在性之間的關聯；揭示了可證算法與邏輯完備性之間的聯繫，給出了不完備性定理的基於複雜性理論的證明。 3. 對概論並發計算模型的語義進行了深入研究。證明了馬爾可夫自動機上弱互模擬語義與一種外延等價關係的一致性；比較了一般回報測試語義與允許實數值的回報測試語義對收斂進程的影響。 4. 對並發計算模型可判定的界進行了研究，提出了良結構下推系統，研究了其表達能力，證明了其中的一些問題的可判定性，給出了可覆蓋性算法。 基於上述研究結果在國際學術界有影響的會議和期刊上發表了一系列論文，其中有兩篇LICS論文，五篇ICALP論文，十餘篇Theoretical Computer Science和Information and Computation刊物論文。項目執行期間，年均舉辦國際交流活動一項以上。項目組成員在國際學術界發揮了影響，陳翌佳在Journal of ACM上以第一作者發表了論文，鄧玉欣出版了機率模型的專著，傅育熙成為了Mathematical Structures in Computer Science的編委。項目組有三人多次在LICS和ICALP會議任程式委員會成員。一人獲上海市優秀學科帶頭人，一人獲中創軟體人才獎。 本項目的研究過程中所使用的一些方法和技術可用於大規模並發系統的模型驗證和等價測試的可判定性和算法研究中。項目組成員已在這些領域解決了一些公開問題，未來幾年還將持續在這些領域進行研究。
