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会议任程序委员会成员。一人获上海市优秀学科带头人，一人获中创软件人才奖。.本项目的研究过程中所使用的一些方法和技术可用于大规模并发系统的模型验证和等价测试的可判定性和算法研究中。项目组成员已在这些领域解决了一些公开问题，未来几年还将持续在这些领域进行研究。